diff options
Diffstat (limited to 'src/theory/uf/equality_engine.h')
| -rw-r--r-- | src/theory/uf/equality_engine.h | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 01ae6bfb4..29f932e04 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -268,6 +268,11 @@ public: } }; + /** + * Store the application lookup, with enough information to backtrack + */ + void storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId); + private: /** The context we are using */ @@ -294,6 +299,12 @@ private: */ ApplicationIdsMap d_applicationLookup; + /** Application lookups in order, so that we can backtrack. */ + std::vector<FunctionApplication> d_applicationLookups; + + /** Number of application lookups, for backtracking. */ + context::CDO<size_t> d_applicationLookupsCount; + /** Map from ids to the nodes (these need to be nodes as we pick-up the opreators) */ std::vector<Node> d_nodes; @@ -544,6 +555,7 @@ public: d_context(context), d_performNotify(true), d_notify(notify), + d_applicationLookupsCount(context, 0), d_nodesCount(context, 0), d_assertedEqualitiesCount(context, 0), d_equalityTriggersCount(context, 0), |