* 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

1 files changed, 8 insertions, 2 deletions

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index d55788298..18a1dcf68 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -40,8 +40,14 @@ public:
   /** Assert a clause in the solver. */
   virtual void addClause(SatClause& clause, bool removable) = 0;
 
-  /** Create a new boolean variable in the solver. */
-  virtual SatVariable newVar(bool theoryAtom = false) = 0;
+  /**
+   * Create a new boolean variable in the solver.
+   * @param isTheoryAtom is this a theory atom that needs to be asserted to theory
+   * @param preRegister whether to preregister the atom with the theory
+   * @param canErase whether the sat solver can safely eliminate this variable
+   *
+   */
+  virtual SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) = 0;
 
   /** Create a new (or return an existing) boolean variable representing the constant true */
   virtual SatVariable trueVar() = 0;