* 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, 4 insertions, 3 deletions

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index cbcca5e85..1c66be911 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -146,11 +146,12 @@ protected:
    * Acquires a new variable from the SAT solver to represent the node
    * and inserts the necessary data it into the mapping tables.
    * @param node a formula
-   * @param theoryLiteral whether this literal a theory literal (and
-   * therefore the theory is to be informed when set to true/false)
+   * @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 canEliminate whether the sat solver can safely eliminate this variable
    * @return the literal corresponding to the formula
    */
-  SatLiteral newLiteral(TNode node, bool theoryLiteral = false);
+  SatLiteral newLiteral(TNode node, bool isTheoryAtom = false, bool preRegister = false, bool canEliminate = true);
 
   /**
    * Constructs a new literal for an atom and returns it.  Calls