From: Dejan Jovanović <dejan@cs.nyu.edu>
Date: Wed, 3 Apr 2013 21:55:58 +0000 (-0400)
Subject: * changing the bitblast-eager to bitblast on pre-register
X-Git-Tag: cvc5-1.0.0~7329
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bb6c74a7bb306de8b7c5d7e9701b3524eda68f4a;p=cvc5.git

* 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
---

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 032788806..6bbe4bb3e 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -88,8 +88,8 @@ void BVMinisatSatSolver::popAssumption() {
   d_minisat->popAssumption();
 }
 
-SatVariable BVMinisatSatSolver::newVar(bool freeze){
-  return d_minisat->newVar(true, true, freeze);
+SatVariable BVMinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){
+  return d_minisat->newVar(true, true, !canErase);
 }
 
 void BVMinisatSatSolver::markUnremovable(SatLiteral lit){
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 0dd208088..ebf4a44b4 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -80,7 +80,7 @@ public:
 
   SatValue propagate();
 
-  SatVariable newVar(bool theoryAtom = false);
+  SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true);
 
   SatVariable trueVar() { return d_minisat->trueVar(); }
   SatVariable falseVar() { return d_minisat->falseVar(); }
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 983669da3..4be58bdef 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -26,6 +26,7 @@
 #include "expr/command.h"
 #include "expr/expr.h"
 #include "prop/theory_proxy.h"
+#include "theory/bv/options.h"
 
 #include <queue>
 
@@ -151,8 +152,8 @@ void TseitinCnfStream::ensureLiteral(TNode n) {
   Debug("ensureLiteral") << "CnfStream::ensureLiteral(): out lit is " << lit << std::endl;
 }
 
-SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
-  Debug("cnf") << "newLiteral(" << node << ", " << theoryLiteral << ")" << endl;
+SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister, bool canEliminate) {
+  Debug("cnf") << "newLiteral(" << node << ", " << isTheoryAtom << ")" << endl;
   Assert(node.getKind() != kind::NOT);
 
   // Get the literal for this node
@@ -166,7 +167,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
         lit = SatLiteral(d_satSolver->falseVar());
       }
     } else {
-      lit = SatLiteral(d_satSolver->newVar(theoryLiteral));
+      lit = SatLiteral(d_satSolver->newVar(isTheoryAtom, preRegister, canEliminate));
     }
     d_nodeToLiteralMap.insert(node, lit);
     d_nodeToLiteralMap.insert(node.notNode(), ~lit);
@@ -175,7 +176,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
   }
 
   // If it's a theory literal, need to store it for back queries
-  if ( theoryLiteral || d_fullLitToNodeMap ||
+  if ( isTheoryAtom || d_fullLitToNodeMap ||
        ( CVC4_USE_REPLAY && options::replayLog() != NULL ) ||
        (Dump.isOn("clauses")) ) {
 
@@ -184,7 +185,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
   }
 
   // If a theory literal, we pre-register it
-  if (theoryLiteral) {
+  if (preRegister) {
     bool backup = d_removable;
     d_registrar->preRegister(node);
     d_removable = backup;
@@ -214,13 +215,27 @@ SatLiteral CnfStream::convertAtom(TNode node) {
 
   Assert(!hasLiteral(node), "atom already mapped!");
 
+  bool theoryLiteral = false;
+  bool canEliminate = true;
+  bool preRegister = false;
+
   // Is this a variable add it to the list
   if (node.isVar()) {
     d_booleanVariables.push_back(node);
+  } else {
+    theoryLiteral = true;
+    canEliminate = false;
+    preRegister = true;
+
+    if (options::bitvectorEagerBitblast() && theory::Theory::theoryOf(node) == theory::THEORY_BV) {
+      // All BV atoms are treated as boolean except for equality
+      theoryLiteral = false;
+      canEliminate = true;
+    }
   }
 
   // Make a new literal (variables are not considered theory literals)
-  SatLiteral lit = newLiteral(node, !node.isVar());
+  SatLiteral lit = newLiteral(node, theoryLiteral, preRegister, canEliminate);
 
   // Return the resulting literal
   return lit;
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
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; }
 
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 886dc0f72..960f2ad62 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -140,8 +140,8 @@ void MinisatSatSolver::addClause(SatClause& clause, bool removable) {
   d_minisat->addClause(minisat_clause, removable);
 }
 
-SatVariable MinisatSatSolver::newVar(bool theoryAtom) {
-  return d_minisat->newVar(true, true, theoryAtom);
+SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) {
+  return d_minisat->newVar(true, true, isTheoryAtom, preRegister, canErase);
 }
 
 SatValue MinisatSatSolver::solve(unsigned long& resource) {
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 723f257f7..37e471846 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -57,7 +57,7 @@ public:
 
   void addClause(SatClause& clause, bool removable);
 
-  SatVariable newVar(bool theoryAtom = false);
+  SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase);
   SatVariable trueVar() { return d_minisat->trueVar(); }
   SatVariable falseVar() { return d_minisat->falseVar(); }
 
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index ed2dc04b9..9c3e59954 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -95,11 +95,11 @@ SimpSolver::~SimpSolver()
 }
 
 
-Var SimpSolver::newVar(bool sign, bool dvar, bool theoryAtom) {
-    Var v = Solver::newVar(sign, dvar,theoryAtom);
+Var SimpSolver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bool canErase) {
+    Var v = Solver::newVar(sign, dvar, isTheoryAtom, preRegister, canErase);
 
     if (use_simplification){
-        frozen    .push((char)theoryAtom);
+        frozen    .push((char)(!canErase));
         eliminated.push((char)false);
         n_occ     .push(0);
         n_occ     .push(0);
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index e9116001f..878d799a5 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -46,7 +46,7 @@ class SimpSolver : public Solver {
 
     // Problem specification:
     //
-    Var     newVar    (bool polarity = true, bool dvar = true, bool theoryAtom = false);
+    Var     newVar    (bool polarity = true, bool dvar = true, bool isTheoryAtom = false, bool preRegister = false, bool canErase = true);
     bool    addClause (const vec<Lit>& ps, bool removable);
     bool    addEmptyClause(bool removable);                  // Add the empty clause to the solver.
     bool    addClause (Lit p, bool removable);               // Add a unit clause to the solver.
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;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 18636a486..55000c94d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -59,6 +59,7 @@
 #include "theory/substitutions.h"
 #include "theory/uf/options.h"
 #include "theory/arith/options.h"
+#include "theory/bv/options.h"
 #include "theory/theory_traits.h"
 #include "theory/logic_info.h"
 #include "theory/options.h"
@@ -674,6 +675,11 @@ void SmtEngine::finalOptionsAreSet() {
     return;
   }
 
+  if (options::bitvectorEagerBitblast()) {
+    // Eager solver should use the internal decision strategy
+    options::decisionMode.set(DECISION_STRATEGY_INTERNAL);
+  }
+
   if(options::checkModels()) {
     if(! options::produceModels()) {
       Notice() << "SmtEngine: turning on produce-models to support check-model" << endl;
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index cf841bb56..ad62ade38 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -104,6 +104,7 @@ void Bitblaster::bbAtom(TNode node) {
     d_bitblastedAtoms.insert(node);
   } else {
     d_bvOutput->lemma(atom_definition, false);
+    d_bitblastedAtoms.insert(node);
   }
 }
 
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 237b04172..d8a784544 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -54,7 +54,11 @@ void BitblastSolver::preRegister(TNode node) {
        node.getKind() == kind::BITVECTOR_SLT ||
        node.getKind() == kind::BITVECTOR_SLE) &&
       !d_bitblaster->hasBBAtom(node)) {
-    d_bitblastQueue.push_back(node);
+    if (options::bitvectorEagerBitblast()) {
+      d_bitblaster->bbAtom(node);
+    } else {
+      d_bitblastQueue.push_back(node);
+    }
   }
 }
 
@@ -62,29 +66,23 @@ void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
   d_bitblaster->explain(literal, assumptions);
 }
 
+void BitblastSolver::bitblastQueue() {
+  while (!d_bitblastQueue.empty()) {
+    TNode atom = d_bitblastQueue.front();
+    d_bitblaster->bbAtom(atom);
+    d_bitblastQueue.pop();
+  }
+}
 
 bool BitblastSolver::check(Theory::Effort e) {
   Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n"; 
+  Assert(!options::bitvectorEagerBitblast());
+
   ++(d_statistics.d_numCallstoCheck); 
-  //// Eager bit-blasting
-  if (options::bitvectorEagerBitblast()) {
-    while (!done()) {
-      TNode assertion = get(); 
-      TNode atom = assertion.getKind() == kind::NOT ? assertion[0] : assertion;
-      if (atom.getKind() != kind::BITVECTOR_BITOF) {
-        d_bitblaster->bbAtom(atom);
-      }
-      return true;
-    }
-  }
 
   //// Lazy bit-blasting
   // bit-blast enqueued nodes
-  while (!d_bitblastQueue.empty()) {
-    TNode atom = d_bitblastQueue.front();
-    d_bitblaster->bbAtom(atom);
-    d_bitblastQueue.pop();
-  }
+  bitblastQueue();
 
   // Processing assertions  
   while (!done()) {
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 1eef61daf..1fab621cd 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -52,6 +52,7 @@ public:
   void collectModelInfo(TheoryModel* m); 
   Node getModelValue(TNode node);
   bool isComplete() { return true; }
+  void bitblastQueue();
 };
 
 }
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 228a4d8a3..433223308 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -102,6 +102,7 @@ void TheoryBV::preRegisterTerm(TNode node) {
 
   if (options::bitvectorEagerBitblast()) {
     // don't use the equality engine in the eager bit-blasting
+    d_subtheoryMap[SUB_BITBLAST]->preRegister(node);
     return;
   }
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
@@ -124,6 +125,10 @@ void TheoryBV::sendConflict() {
 void TheoryBV::check(Effort e)
 {
   Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
+  if (options::bitvectorEagerBitblast()) {
+    return;
+  }
+
   if (Theory::fullEffort(e)) {
     ++(d_statistics.d_numCallsToCheckFullEffort); 
   } else {
@@ -186,6 +191,10 @@ Node TheoryBV::getModelValue(TNode var) {
 void TheoryBV::propagate(Effort e) {
   Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
 
+  if (options::bitvectorEagerBitblast()) {
+    return;
+  }
+
   if (inConflict()) {
     return;
   }