* changing the bitblast-eager to bitblast on pre-register

* the newVar interface of the sat solver now changed to include (isTheoryLiteral, preRegister, canEliminate)
* when bitblast-eager all bv atoms are (theory=false, prereg = true, canelim = true)
* bitblast-eager implies decision=internal

2 files changed, 4 insertions, 4 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index f7d67d445..c7f1780b6 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -150,7 +150,7 @@ Solver::~Solver()
 // Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be
 // used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
 //
-Var Solver::newVar(bool sign, bool dvar, bool theoryAtom)
+Var Solver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bool canErase)
 {
     int v = nVars();
 
@@ -163,12 +163,12 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom)
     polarity .push(sign);
     decision .push();
     trail    .capacity(v+1);
-    theory   .push(theoryAtom);
+    theory   .push(isTheoryAtom);
 
     setDecisionVar(v, dvar);
 
     // If the variable is introduced at non-zero level, we need to reintroduce it on backtracks
-    if (theoryAtom) {
+    if (preRegister) {
       variables_to_register.push(VarIntroInfo(v, decisionLevel()));
     }
 
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 0dad68a08..9338f9b55 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -117,7 +117,7 @@ public:
 
     // Problem specification:
     //
-    Var     newVar    (bool polarity = true, bool dvar = true, bool theoryAtom = false); // Add a new variable with parameters specifying variable mode.
+    Var     newVar    (bool polarity = true, bool dvar = true, bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); // Add a new variable with parameters specifying variable mode.
     Var     trueVar() const { return varTrue; }
     Var     falseVar() const { return varFalse; }