diff options
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 3 | ||||
| -rw-r--r-- | src/theory/model.cpp | 13 | ||||
| -rw-r--r-- | src/theory/substitutions.h | 21 |
3 files changed, 32 insertions, 5 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index e36589ba8..fbaef61f2 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -1443,7 +1443,8 @@ void Solver::pop() Var x = var(trail.last()); assigns [x] = l_Undef; vardata[x].trail_index = -1; - polarity[x] = sign(trail.last()); + if(phase_saving >= 1 && (polarity[x] & 0x2) == 0) + polarity[x] = sign(trail.last()); if(intro_level(x) != -1) {// might be unregistered insertVarOrder(x); } diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 82d602017..f218332ac 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -260,6 +260,19 @@ Node TheoryModel::getNewDomainValue( TypeNode tn ){ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ if( !d_substitutions.hasSubstitution( x ) ){ d_substitutions.addSubstitution( x, t, invalidateCache ); + } else { +#ifdef CVC4_ASSERTIONS + Node oldX = d_substitutions.getSubstitution(x); + // check that either the old substitution is the same, or it now maps to the new substitution + if(oldX != t && d_substitutions.apply(oldX) != d_substitutions.apply(t)) { + stringstream ss; + ss << "Two incompatible substitutions added to TheoryModel:\n" + << "the term: " << x << "\n" + << "old mapping: " << d_substitutions.apply(oldX) << "\n" + << "new mapping: " << d_substitutions.apply(t); + InternalError(ss.str()); + } +#endif /* CVC4_ASSERTIONS */ } } diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index cf751b69e..5cb8c5e2f 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -108,14 +108,27 @@ public: /** * Adds a substitution from x to t. */ - void addSubstitution(TNode x, TNode t, - bool invalidateCache = true); + void addSubstitution(TNode x, TNode t, bool invalidateCache = true); /** * Returns true iff x is in the substitution map */ - bool hasSubstitution(TNode x) - { return d_substitutions.find(x) != d_substitutions.end(); } + bool hasSubstitution(TNode x) const { + return d_substitutions.find(x) != d_substitutions.end(); + } + + /** + * Returns the substitution mapping that was given for x via + * addSubstitution(). Note that the returned value might itself + * be in the map; for the actual substitution that would be + * performed for x, use .apply(x). This getSubstitution() function + * is mainly intended for constructing assertions about what has + * already been put in the map. + */ + TNode getSubstitution(TNode x) const { + AssertArgument(hasSubstitution(x), x, "element not in this substitution map"); + return (*d_substitutions.find(x)).second; + } /** * Apply the substitutions to the node. |