From 5b65d0f80d56731fd7d07f491973bad14a85566e Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 9 Oct 2012 13:22:28 +0000
Subject: [PATCH] * Add assertion in TheoryModel code to ensure we don't get
 inconsistent   substitutions for solved variables.  Related to bug 418 (and
 might   resolve it).

* Respect phase-locking in Minisat (one phase-saving site was unguarded).

(this commit was certified error- and warning-free by the test-and-commit script.)
---
 src/prop/minisat/core/Solver.cc |  3 ++-
 src/theory/model.cpp            | 13 +++++++++++++
 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.
-- 
2.30.2