diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-02-09 21:25:00 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-02-09 21:25:00 +0000 |
| commit | d31ba827811ac3267366496eb3d893b65962bedc (patch) | |
| tree | 2a92b0381d1e47b8f93815d61744cc3b06fc5466 | |
| parent | 5f686317747384555db15fccc725512b743a8b77 (diff) | |
fixing antoher small bug in backtracking
| -rw-r--r-- | src/theory/uf/equality_engine_impl.h | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h index 10131a805..f30006cb9 100644 --- a/src/theory/uf/equality_engine_impl.h +++ b/src/theory/uf/equality_engine_impl.h @@ -375,6 +375,8 @@ void EqualityEngine<NotifyClass>::undoMerge(EqualityNode& class1, EqualityNode& template <typename NotifyClass> void EqualityEngine<NotifyClass>::backtrack() { + Debug("equality::backtrack") << "backtracking" << std::endl; + // If we need to backtrack then do it if (d_assertedEqualitiesCount < d_assertedEqualities.size()) { @@ -429,6 +431,7 @@ void EqualityEngine<NotifyClass>::backtrack() { for (int i = d_applicationLookups.size() - 1, i_end = (int) d_applicationLookupsCount; i >= i_end; -- i) { d_applicationLookup.erase(d_applicationLookups[i]); } + d_applicationLookups.resize(d_applicationLookupsCount); } if (d_nodes.size() > d_nodesCount) { @@ -449,7 +452,6 @@ void EqualityEngine<NotifyClass>::backtrack() { // Now get rid of the nodes and the rest d_nodes.resize(d_nodesCount); - d_applicationLookups.resize(d_applicationLookupsCount); d_applications.resize(d_nodesCount); d_nodeTriggers.resize(d_nodesCount); d_nodeIndividualTrigger.resize(d_nodesCount); @@ -866,6 +868,9 @@ void EqualityEngine<NotifyClass>::storeApplicationLookup(FunctionApplication& fu d_applicationLookup[funNormalized] = funId; d_applicationLookups.push_back(funNormalized); d_applicationLookupsCount = d_applicationLookupsCount + 1; + Debug("equality::backtrack") << "d_applicationLookupsCount = " << d_applicationLookupsCount << std::endl; + Debug("equality::backtrack") << "d_applicationLookups.size() = " << d_applicationLookups.size() << std::endl; + Assert(d_applicationLookupsCount == d_applicationLookups.size()); } } // Namespace uf |