added model generation to eager bit-blasting and turned abc off by default

11 files changed, 117 insertions, 38 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f82fc86ed..ffe239e2f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3180,8 +3180,11 @@ void SmtEnginePrivate::processAssertions() {
   // everything gets bit-blasted to internal SAT solver
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) {
-      Node eager_atom = NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM, d_assertionsToCheck[i]);
+      TNode atom = d_assertionsToCheck[i];
+      Node eager_atom = NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM, atom);
       d_assertionsToCheck[i] = eager_atom;
+      TheoryModel* m = d_smt.d_theoryEngine->getModel();
+      m->addSubstitution(eager_atom, atom);
     }
   }
 
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 8971d289f..4b0465498 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -57,6 +57,8 @@ namespace bv {
 class BitblastingRegistrar;
 
 typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
+
 class AbstractionModule;
 
 /**
@@ -70,7 +72,7 @@ class TBitblaster {
 protected:
   typedef std::vector<T> Bits;
   typedef __gnu_cxx::hash_map <Node, Bits, NodeHashFunction>  TermDefMap;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>       AtomSet;
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>       TNodeSet;
 
   typedef void  (*TermBBStrategy) (TNode, Bits&, TBitblaster<T>*);
   typedef T     (*AtomBBStrategy) (TNode, TBitblaster<T>*);
@@ -104,8 +106,6 @@ class TheoryBV;
 
 class TLazyBitblaster :  public TBitblaster<Node> {
   typedef std::vector<Node> Bits;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> VarSet;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AtomSet;
   typedef context::CDList<prop::SatLiteral> AssertionList;
   typedef context::CDHashMap<prop::SatLiteral, std::vector<prop::SatLiteral> , prop::SatLiteralHashFunction> ExplanationMap;
   
@@ -138,8 +138,8 @@ class TLazyBitblaster :  public TBitblaster<Node> {
                                      currently asserted by the DPLL SAT solver. */
   ExplanationMap* d_explanations; /**< context dependent list of explanations for the propagated literals.
                                     Only used when bvEagerPropagate option enabled. */
-  VarSet d_variables;
-  AtomSet d_bbAtoms; 
+  TNodeSet d_variables;
+  TNodeSet d_bbAtoms; 
   AbstractionModule* d_abstraction;
   bool d_emptyNotify;
   
@@ -188,7 +188,7 @@ public:
    */
   void collectModelInfo(TheoryModel* m, bool fullModel);
 
-  typedef VarSet::const_iterator vars_iterator;
+  typedef TNodeSet::const_iterator vars_iterator;
   vars_iterator beginVars() { return d_variables.begin(); }
   vars_iterator endVars() { return d_variables.end(); }
 
@@ -239,7 +239,14 @@ class EagerBitblaster : public TBitblaster<Node> {
   BitblastingRegistrar*              d_bitblastingRegistrar;
   context::Context*                  d_nullContext;
   prop::CnfStream*                   d_cnfStream;
-  TNodeSet d_bbAtoms; 
+
+  theory::bv::TheoryBV* d_bv;
+  TNodeSet d_bbAtoms;
+  TNodeSet d_variables;
+
+  Node getVarValue(TNode a, bool fullModel);
+  bool isSharedTerm(TNode node); 
+
 public:
   void addAtom(TNode atom);
   void makeVariable(TNode node, Bits& bits);
@@ -249,10 +256,11 @@ public:
   bool hasBBAtom(TNode atom) const; 
   void bbFormula(TNode formula);
   void storeBBAtom(TNode atom, Node atom_bb);
-  EagerBitblaster(); 
+  EagerBitblaster(theory::bv::TheoryBV* theory_bv); 
   ~EagerBitblaster();
   bool assertToSat(TNode node, bool propagate = true);
-  bool solve(); 
+  bool solve();
+  void collectModelInfo(TheoryModel* m, bool fullModel);
 };
 
 class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index af35c0499..166d43e35 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -24,11 +24,12 @@ using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 
-EagerBitblastSolver::EagerBitblastSolver()
+EagerBitblastSolver::EagerBitblastSolver(TheoryBV* bv)
   : d_assertionSet()
   , d_bitblaster(NULL)
   , d_aigBitblaster(NULL)
   , d_useAig(options::bitvectorAig())
+  , d_bv(bv)
 {}
 
 EagerBitblastSolver::~EagerBitblastSolver() {
@@ -53,7 +54,7 @@ void EagerBitblastSolver::initialize() {
   if (d_useAig) {
     d_aigBitblaster = new AigBitblaster();
   } else {
-    d_bitblaster = new EagerBitblaster();
+    d_bitblaster = new EagerBitblaster(d_bv);
   }
 }
 
@@ -106,3 +107,8 @@ bool EagerBitblastSolver::hasAssertions(const std::vector<TNode> &formulas) {
   }
   return true; 
 }
+
+void EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+  AlwaysAssert(!d_useAig && d_bitblaster);
+  d_bitblaster->collectModelInfo(m, fullModel); 
+}
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 1fb65c9c8..65fddd819 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -16,6 +16,8 @@
 
 #include "cvc4_private.h"
 #include "expr/node.h"
+#include "theory/theory_model.h"
+#include "theory/bv/theory_bv.h"
 #include <vector>
 #pragma once
 
@@ -37,8 +39,9 @@ class EagerBitblastSolver {
   EagerBitblaster* d_bitblaster;
   AigBitblaster* d_aigBitblaster;
   bool d_useAig;
+  TheoryBV* d_bv; 
 public:
-  EagerBitblastSolver(); 
+  EagerBitblastSolver(theory::bv::TheoryBV* bv); 
   ~EagerBitblastSolver();
   bool checkSat();
   void assertFormula(TNode formula);
@@ -48,6 +51,7 @@ public:
   void turnOffAig();
   bool isInitialized();
   void initialize();
+  void collectModelInfo(theory::TheoryModel* m, bool fullModel);
 };
 
 }
diff --git a/src/theory/bv/eager_bitblaster.h b/src/theory/bv/eager_bitblaster.h
index da73c7f09..91ef866bd 100644
--- a/src/theory/bv/eager_bitblaster.h
+++ b/src/theory/bv/eager_bitblaster.h
@@ -20,11 +20,13 @@
 #define __CVC4__EAGER__BITBLASTER_H
 
 
-#include "bitblaster_template.h"
 #include "theory/theory_registrar.h"
+#include "theory/bv/bitblaster_template.h"
+#include "theory/bv/options.h"
+#include "theory/theory_model.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver_factory.h"
-#include "theory/bv/options.h"
+
 
 namespace CVC4 {
 namespace theory {
@@ -43,9 +45,11 @@ public:
 
 };/* class Registrar */
 
-EagerBitblaster::EagerBitblaster()
+EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
   : TBitblaster<Node>()
+  , d_bv(theory_bv)
   , d_bbAtoms()
+  , d_variables()
 {
   d_bitblastingRegistrar = new BitblastingRegistrar(this); 
   d_nullContext = new context::Context();
@@ -126,6 +130,7 @@ void EagerBitblaster::makeVariable(TNode var, Bits& bits) {
   for (unsigned i = 0; i < utils::getSize(var); ++i) {
     bits.push_back(utils::mkBitOf(var, i)); 
   }
+  d_variables.insert(var); 
 }
 
 Node EagerBitblaster::getBBAtom(TNode node) const {
@@ -154,6 +159,68 @@ bool EagerBitblaster::solve() {
 }
 
 
+/**
+ * Returns the value a is currently assigned to in the SAT solver
+ * or null if the value is completely unassigned.
+ *
+ * @param a
+ * @param fullModel whether to create a "full model," i.e., add
+ * constants to equivalence classes that don't already have them
+ *
+ * @return
+ */
+Node EagerBitblaster::getVarValue(TNode a, bool fullModel) {
+  if (!hasBBTerm(a)) {
+    Assert(isSharedTerm(a));
+    return Node();
+  }
+  Bits bits;
+  getBBTerm(a, bits);
+  Integer value(0);
+  for (int i = bits.size() -1; i >= 0; --i) {
+    prop::SatValue bit_value;
+    if (d_cnfStream->hasLiteral(bits[i])) {
+      prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
+      bit_value = d_satSolver->value(bit);
+      Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
+    } else {
+      // the bit is unconstrainted so we can give it an arbitrary value
+      bit_value = prop::SAT_VALUE_FALSE;
+    }
+    Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
+    value = value * 2 + bit_int;
+  }
+  return utils::mkConst(BitVector(bits.size(), value));
+}
+
+
+void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
+  TNodeSet::const_iterator it = d_variables.begin();
+  for (; it!= d_variables.end(); ++it) {
+    TNode var = *it;
+    if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var))  {
+      Node const_value = getVarValue(var, fullModel);
+      if(const_value == Node()) {
+        if( fullModel ){
+          // if the value is unassigned just set it to zero
+          const_value = utils::mkConst(BitVector(utils::getSize(var), 0u));
+        }
+      }
+      if(const_value != Node()) {
+        Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
+                                 << var << " "
+                                 << const_value << "))\n";
+        m->assertEquality(var, const_value, true);
+      }
+    }
+  }
+}
+
+bool EagerBitblaster::isSharedTerm(TNode node) {
+  return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
+}
+
+
 } /*bv namespace */
 } /* theory namespace */
 } /* CVC4 namespace*/
diff --git a/src/theory/bv/lazy_bitblaster.h b/src/theory/bv/lazy_bitblaster.h
index 570549866..e11254dbb 100644
--- a/src/theory/bv/lazy_bitblaster.h
+++ b/src/theory/bv/lazy_bitblaster.h
@@ -453,7 +453,7 @@ Node TLazyBitblaster::getVarValue(TNode a, bool fullModel) {
 }
 
 void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
-  __gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin();
+  TNodeSet::iterator it = d_variables.begin();
   for (; it!= d_variables.end(); ++it) {
     TNode var = *it;
     if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var))  {
diff --git a/src/theory/bv/options b/src/theory/bv/options
index b5a4fea93..81d88421b 100644
--- a/src/theory/bv/options
+++ b/src/theory/bv/options
@@ -5,14 +5,14 @@
 
 module BV "theory/bv/options.h" Bitvector theory
 
-# Option to set the bit-blasting mode (lazy, eager, eager-aig)
+# Option to set the bit-blasting mode (lazy, eager)
 
 option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :handler CVC4::theory::bv::stringToBitblastMode :default CVC4::theory::bv::BITBLAST_MODE_LAZY :read-write :include "theory/bv/bitblast_mode.h" :handler-include "theory/bv/options_handlers.h"
  choose bitblasting mode, see --bitblast=help
 
 # Options for eager bit-blasting
  
-option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::theory::bv::abcEnabledBuild :predicate-include "theory/bv/options_handlers.h" :read-write :link --bitblast=eager
+option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::theory::bv::abcEnabledBuild :predicate-include "theory/bv/options_handlers.h" :read-write :link --bitblast=eager :link --bv-aig-simp="balance;drw"
  bitblast by first converting to AIG (only if --bitblast=eager)
 
 expert-option bitvectorAigSimplifications --bv-aig-simp=FILE std::string :default "" :predicate CVC4::theory::bv::abcEnabledBuild :read-write :link --bitblast-aig
diff --git a/src/theory/bv/options_handlers.h b/src/theory/bv/options_handlers.h
index 5d85a1be0..7cdd4aac5 100644
--- a/src/theory/bv/options_handlers.h
+++ b/src/theory/bv/options_handlers.h
@@ -56,9 +56,6 @@ lazy (default)\n\
 \n\
 eager\n\
 + Bitblast eagerly to bv SAT solver\n\
-\n\
-aig\n\
-+ Bitblast eagerly to bv SAT solver by converting to AIG\n\
 ";
 
 inline BitblastMode stringToBitblastMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
@@ -70,7 +67,8 @@ inline BitblastMode stringToBitblastMode(std::string option, std::string optarg,
       options::bitvectorEqualitySolver.set(true);
     }
     if (!options::bitvectorEqualitySlicer.wasSetByUser()) {
-      if (options::incrementalSolving()) {
+      if (options::incrementalSolving() ||
+          options::produceModels()) {
         options::bitvectorEqualitySlicer.set(BITVECTOR_SLICER_OFF);
       } else {
         options::bitvectorEqualitySlicer.set(BITVECTOR_SLICER_AUTO);
@@ -85,10 +83,6 @@ inline BitblastMode stringToBitblastMode(std::string option, std::string optarg,
     }
     return BITBLAST_MODE_LAZY;
   } else if(optarg == "eager") {
-    if (options::produceModels()) {
-      throw OptionException(std::string("Eager bit-blasting does not currently support model generation. \n\
-                                         Try --bitblast=lazy")); 
-    }
 
     if (options::incrementalSolving() &&
         options::incrementalSolving.wasSetByUser()) {
@@ -96,14 +90,6 @@ inline BitblastMode stringToBitblastMode(std::string option, std::string optarg,
                                          Try --bitblast=lazy"));
     }
     
-    if (!options::bitvectorAig.wasSetByUser()) {
-      options::bitvectorAig.set(true);
-      abcEnabledBuild("--bitblast-aig", true, NULL); 
-    }
-    if (!options::bitvectorAigSimplifications.wasSetByUser()) {
-      // due to a known bug in abc switching to using drw instead of rw
-      options::bitvectorAigSimplifications.set("balance;drw");
-    }
     if (!options::bitvectorToBool.wasSetByUser()) {
       options::bitvectorToBool.set(true);
     }
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index d3da10a90..4b5333e46 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -61,7 +61,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
 {
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    d_eagerSolver = new EagerBitblastSolver();
+    d_eagerSolver = new EagerBitblastSolver(this);
     return; 
   }
 
@@ -434,7 +434,9 @@ void TheoryBV::check(Effort e)
 
 void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
   Assert(!inConflict());
-
+  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+    d_eagerSolver->collectModelInfo(m, fullModel); 
+  }
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     if (d_subtheories[i]->isComplete()) {
       d_subtheories[i]->collectModelInfo(m, fullModel);
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 683f002cf..e96df8df2 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -209,6 +209,7 @@ private:
  
   friend class LazyBitblaster;
   friend class TLazyBitblaster;
+  friend class EagerBitblaster;
   friend class BitblastSolver;
   friend class EqualitySolver;
   friend class CoreSolver;
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 6c0018c05..46eb5606b 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -152,7 +152,9 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
       Unreachable();
     }
 
-    if (n.getNumChildren() > 0) {
+    if (n.getNumChildren() > 0 &&
+        n.getKind() != kind::BITVECTOR_ACKERMANIZE_UDIV &&
+        n.getKind() != kind::BITVECTOR_ACKERMANIZE_UREM) {
       std::vector<Node> children;
       if (n.getKind() == APPLY_UF) {
         Node op = getModelValue(n.getOperator(), hasBoundVars);