* Changing pre-registration to be context dependent -- it is called from the SAT solver on every backtrack

* Updated UF to handle the context dependent pre-registration
* Additionally some small changes in order to satisfy warnings of the eclipse code analysis tool

5 files changed, 40 insertions, 3 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 629e44e3e..9b0c4847b 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -98,7 +98,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
   SatLiteral lit;
   if (!hasLiteral(node)) {
     // If no literal, well make one
-    lit = Minisat::mkLit(d_satSolver->newVar(theoryLiteral));
+    lit = variableToLiteral(d_satSolver->newVar(theoryLiteral));
     d_translationCache[node].literal = lit;
     d_translationCache[node.notNode()].literal = ~lit;
   } else {
@@ -411,6 +411,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
         //Node atomic = handleNonAtomicNode(node);
         //return isCached(atomic) ? lookupInCache(atomic) : convertAtom(atomic);
       }
+      break;
     }
   }
 
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 7ca117c2e..711379519 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -148,6 +148,11 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom)
 
     setDecisionVar(v, dvar);
 
+    // If the variable is introduced at non-zero level, we need to reintroduce it on backtracks
+    if (theoryAtom) {
+      variables_to_register.push(VarIntroInfo(v, decisionLevel()));
+    }
+
     return v;
 }
 
@@ -295,6 +300,13 @@ void Solver::cancelUntil(int level) {
         qhead = trail_lim[level];
         trail.shrink(trail.size() - trail_lim[level]);
         trail_lim.shrink(trail_lim.size() - level);
+
+        // Register variables that have not been registered yet
+        int currentLevel = decisionLevel();
+        for(int i = variables_to_register.size() - 1; i >= 0 && variables_to_register[i].level > currentLevel; --i) {
+          variables_to_register[i].level = currentLevel;
+          proxy->variableNotify(variables_to_register[i].var);
+        }
     }
 }
 
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 1141e53c4..4c6e98a2e 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -80,12 +80,23 @@ protected:
   /** True if we are currently solving. */
   bool minisat_busy;
 
+  // Information about registration of variables
+  struct VarIntroInfo {
+    Var var;
+    int level;
+    VarIntroInfo(Var var, int level)
+    : var(var), level(level) {}
+  };
+
+  /** Variables to re-register with theory solvers on backtracks */
+  vec<VarIntroInfo> variables_to_register;
+
 public:
 
     // Constructor/Destructor:
     //
     Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bool enableIncremental = false);
-    CVC4_PUBLIC ~Solver();
+    CVC4_PUBLIC virtual ~Solver();
 
     // Problem specification:
     //
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 62558cac1..a7eced6f2 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -27,6 +27,10 @@
 namespace CVC4 {
 namespace prop {
 
+void SatSolver::variableNotify(SatVariable var) {
+  d_theoryEngine->preRegister(getNode(variableToLiteral(var)));
+}
+
 void SatSolver::theoryCheck(theory::Theory::Effort effort) {
   d_theoryEngine->check(effort);
 }
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 2521f3ee7..39977a96b 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -70,6 +70,10 @@ inline SatVariable literalToVariable(SatLiteral lit) {
   return Minisat::var(lit);
 }
 
+inline SatLiteral variableToLiteral(SatVariable var) {
+  return Minisat::mkLit(var);
+}
+
 inline bool literalSign(SatLiteral lit) {
   return Minisat::sign(lit);
 }
@@ -208,7 +212,7 @@ public:
             TheoryEngine* theoryEngine,
             context::Context* context);
 
-  ~SatSolver();
+  virtual ~SatSolver();
 
   bool solve();
 
@@ -242,6 +246,11 @@ public:
 
   void removeClausesAboveLevel(int level);
 
+  /**
+   * Notifies of a new variable at a decision level.
+   */
+  void variableNotify(SatVariable var);
+
   void unregisterVar(SatLiteral lit);
 
   void renewVar(SatLiteral lit, int level = -1);