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

1 files changed, 70 insertions, 3 deletions

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