Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastructure to BV collectModelInfo in preparation for bug fix.

1 files changed, 97 insertions, 92 deletions

diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 7960b0320..47aac4370 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -12,7 +12,7 @@
  ** \brief [[ Add one-line brief description here ]]
  **
  ** [[ Add lengthier description here ]]
- ** 
+ **
  **/
 
 #include "bitblaster.h"
@@ -29,7 +29,7 @@
 using namespace std;
 
 using namespace CVC4::theory::bv::utils;
-using namespace CVC4::context; 
+using namespace CVC4::context;
 using namespace CVC4::prop;
 
 namespace CVC4 {
@@ -37,20 +37,20 @@ namespace theory {
 namespace bv{
 
 std::string toString(Bits&  bits) {
-  ostringstream os; 
+  ostringstream os;
   for (int i = bits.size() - 1; i >= 0; --i) {
     TNode bit = bits[i];
     if (bit.getKind() == kind::CONST_BOOLEAN) {
       os << (bit.getConst<bool>() ? "1" : "0");
     } else {
-      os << bit<< " ";   
+      os << bit<< " ";
     }
   }
   os <<"\n";
-  
-  return os.str(); 
+
+  return os.str();
 }
-/////// Bitblaster 
+/////// Bitblaster
 
 Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) :
     d_bv(bv),
@@ -64,35 +64,35 @@ Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) :
     d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar(), new Context());
 
     MinisatNotify* notify = new MinisatNotify(d_cnfStream, bv);
-    d_satSolver->setNotify(notify); 
+    d_satSolver->setNotify(notify);
     // initializing the bit-blasting strategies
-    initAtomBBStrategies(); 
-    initTermBBStrategies(); 
+    initAtomBBStrategies();
+    initTermBBStrategies();
   }
 
 Bitblaster::~Bitblaster() {
   delete d_cnfStream;
-  delete d_satSolver; 
+  delete d_satSolver;
 }
 
 
-/** 
+/**
  * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
  * NOTE: duplicate clauses are not detected because of marker literal
  * @param node the atom to be bitblasted
- * 
+ *
  */
 void Bitblaster::bbAtom(TNode node) {
   node = node.getKind() == kind::NOT?  node[0] : node;
-  
+
   if (hasBBAtom(node)) {
-    return; 
+    return;
   }
 
   // make sure it is marked as an atom
-  addAtom(node); 
+  addAtom(node);
 
-  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
+  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
   ++d_statistics.d_numAtoms;
   // the bitblasted definition of the atom
   Node normalized = Rewriter::rewrite(node);
@@ -126,14 +126,14 @@ void Bitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
 
-  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
+  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
   ++d_statistics.d_numTerms;
 
   d_termBBStrategies[node.getKind()] (node, bits,this);
-  
+
   Assert (bits.size() == utils::getSize(node));
 
-  cacheTermDef(node, bits); 
+  cacheTermDef(node, bits);
 }
 
 Node Bitblaster::bbOptimize(TNode node) {
@@ -142,21 +142,21 @@ Node Bitblaster::bbOptimize(TNode node) {
    if (node.getKind() == kind::BITVECTOR_PLUS) {
     if (RewriteRule<BBPlusNeg>::applies(node)) {
       Node res = RewriteRule<BBPlusNeg>::run<false>(node);
-      return res; 
+      return res;
     }
     //  if (RewriteRule<BBFactorOut>::applies(node)) {
     //   Node res = RewriteRule<BBFactorOut>::run<false>(node);
-    //   return res; 
-    // } 
+    //   return res;
+    // }
 
   } else if (node.getKind() == kind::BITVECTOR_MULT) {
     if (RewriteRule<MultPow2>::applies(node)) {
       Node res = RewriteRule<MultPow2>::run<false>(node);
-      return res; 
+      return res;
     }
   }
-  
-  return node; 
+
+  return node;
 }
 
 /// Public methods
@@ -173,31 +173,31 @@ void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
   std::vector<SatLiteral> literal_explanation;
   d_satSolver->explain(d_cnfStream->getLiteral(atom), literal_explanation);
   for (unsigned i = 0; i < literal_explanation.size(); ++i) {
-    explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); 
+    explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
   }
 }
 
 
-/** 
+/**
  * Asserts the clauses corresponding to the atom to the Sat Solver
  * by turning on the marker literal (i.e. setting it to false)
  * @param node the atom to be asserted
- * 
+ *
  */
- 
+
 bool Bitblaster::propagate() {
   return d_satSolver->propagate() == prop::SAT_VALUE_TRUE;
 }
 
 bool Bitblaster::assertToSat(TNode lit, bool propagate) {
   // strip the not
-  TNode atom; 
+  TNode atom;
   if (lit.getKind() == kind::NOT) {
-    atom = lit[0]; 
+    atom = lit[0];
   } else {
-    atom = lit; 
+    atom = lit;
   }
-  
+
   Assert (hasBBAtom(atom));
 
   SatLiteral markerLit = d_cnfStream->getLiteral(atom);
@@ -205,9 +205,9 @@ bool Bitblaster::assertToSat(TNode lit, bool propagate) {
   if(lit.getKind() == kind::NOT) {
     markerLit = ~markerLit;
   }
-  
+
   Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n";
-  Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal:   " << markerLit << "\n";  
+  Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal:   " << markerLit << "\n";
 
   SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
 
@@ -217,13 +217,13 @@ bool Bitblaster::assertToSat(TNode lit, bool propagate) {
   return ret == prop::SAT_VALUE_TRUE;
 }
 
-/** 
- * Calls the solve method for the Sat Solver. 
+/**
+ * Calls the solve method for the Sat Solver.
  * passing it the marker literals to be asserted
- * 
+ *
  * @return true for sat, and false for unsat
  */
- 
+
 bool Bitblaster::solve(bool quick_solve) {
   if (Trace.isOn("bitvector")) {
     Trace("bitvector") << "Bitblaster::solve() asserted atoms ";
@@ -232,24 +232,24 @@ bool Bitblaster::solve(bool quick_solve) {
       Trace("bitvector") << "     " << d_cnfStream->getNode(*it) << "\n";
     }
   }
-  Debug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; 
-  return SAT_VALUE_TRUE == d_satSolver->solve(); 
+  Debug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n";
+  return SAT_VALUE_TRUE == d_satSolver->solve();
 }
 
 void Bitblaster::getConflict(std::vector<TNode>& conflict) {
   SatClause conflictClause;
   d_satSolver->getUnsatCore(conflictClause);
-  
+
   for (unsigned i = 0; i < conflictClause.size(); i++) {
-    SatLiteral lit = conflictClause[i]; 
+    SatLiteral lit = conflictClause[i];
     TNode atom = d_cnfStream->getNode(lit);
-    Node  not_atom; 
+    Node  not_atom;
     if (atom.getKind() == kind::NOT) {
       not_atom = atom[0];
     } else {
-      not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom); 
+      not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom);
     }
-    conflict.push_back(not_atom); 
+    conflict.push_back(not_atom);
   }
 }
 
@@ -259,9 +259,9 @@ void Bitblaster::getConflict(std::vector<TNode>& conflict) {
 
 void Bitblaster::initAtomBBStrategies() {
   for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
-    d_atomBBStrategies[i] = UndefinedAtomBBStrategy; 
+    d_atomBBStrategies[i] = UndefinedAtomBBStrategy;
   }
-  
+
   /// setting default bb strategies for atoms
   d_atomBBStrategies [ kind::EQUAL ]           = DefaultEqBB;
   d_atomBBStrategies [ kind::BITVECTOR_ULT ]   = DefaultUltBB;
@@ -272,7 +272,7 @@ void Bitblaster::initAtomBBStrategies() {
   d_atomBBStrategies [ kind::BITVECTOR_SLE ]   = DefaultSleBB;
   d_atomBBStrategies [ kind::BITVECTOR_SGT ]   = DefaultSgtBB;
   d_atomBBStrategies [ kind::BITVECTOR_SGE ]   = DefaultSgeBB;
-  
+
 }
 
 void Bitblaster::initTermBBStrategies() {
@@ -281,7 +281,7 @@ void Bitblaster::initTermBBStrategies() {
   for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
     d_termBBStrategies[i] = DefaultVarBB;
   }
-  
+
   /// setting default bb strategies for terms:
   //  d_termBBStrategies [ kind::VARIABLE ]               = DefaultVarBB;
   d_termBBStrategies [ kind::CONST_BITVECTOR ]        = DefaultConstBB;
@@ -298,13 +298,13 @@ void Bitblaster::initTermBBStrategies() {
   d_termBBStrategies [ kind::BITVECTOR_PLUS ]         = DefaultPlusBB;
   d_termBBStrategies [ kind::BITVECTOR_SUB ]          = DefaultSubBB;
   d_termBBStrategies [ kind::BITVECTOR_NEG ]          = DefaultNegBB;
-  d_termBBStrategies [ kind::BITVECTOR_UDIV ]         = UndefinedTermBBStrategy; 
-  d_termBBStrategies [ kind::BITVECTOR_UREM ]         = UndefinedTermBBStrategy; 
+  d_termBBStrategies [ kind::BITVECTOR_UDIV ]         = UndefinedTermBBStrategy;
+  d_termBBStrategies [ kind::BITVECTOR_UREM ]         = UndefinedTermBBStrategy;
   d_termBBStrategies [ kind::BITVECTOR_UDIV_TOTAL ]   = DefaultUdivBB;
   d_termBBStrategies [ kind::BITVECTOR_UREM_TOTAL ]   = DefaultUremBB;
-  d_termBBStrategies [ kind::BITVECTOR_SDIV ]         = UndefinedTermBBStrategy; 
-  d_termBBStrategies [ kind::BITVECTOR_SREM ]         = UndefinedTermBBStrategy; 
-  d_termBBStrategies [ kind::BITVECTOR_SMOD ]         = UndefinedTermBBStrategy; 
+  d_termBBStrategies [ kind::BITVECTOR_SDIV ]         = UndefinedTermBBStrategy;
+  d_termBBStrategies [ kind::BITVECTOR_SREM ]         = UndefinedTermBBStrategy;
+  d_termBBStrategies [ kind::BITVECTOR_SMOD ]         = UndefinedTermBBStrategy;
   d_termBBStrategies [ kind::BITVECTOR_SHL ]          = DefaultShlBB;
   d_termBBStrategies [ kind::BITVECTOR_LSHR ]         = DefaultLshrBB;
   d_termBBStrategies [ kind::BITVECTOR_ASHR ]         = DefaultAshrBB;
@@ -316,22 +316,22 @@ void Bitblaster::initTermBBStrategies() {
   d_termBBStrategies [ kind::BITVECTOR_ROTATE_LEFT ]  = DefaultRotateLeftBB;
 
 }
- 
+
 bool Bitblaster::hasBBAtom(TNode atom) const {
   return d_bitblastedAtoms.find(atom) != d_bitblastedAtoms.end();
 }
 
 void Bitblaster::cacheTermDef(TNode term, Bits def) {
   Assert (d_termCache.find(term) == d_termCache.end());
-  d_termCache[term] = def; 
+  d_termCache[term] = def;
 }
 
 bool Bitblaster::hasBBTerm(TNode node) const {
-  return d_termCache.find(node) != d_termCache.end(); 
+  return d_termCache.find(node) != d_termCache.end();
 }
 
 void Bitblaster::getBBTerm(TNode node, Bits& bits) const {
-  Assert (hasBBTerm(node)); 
+  Assert (hasBBTerm(node));
   // copy?
   bits = d_termCache.find(node)->second;
 }
@@ -340,7 +340,7 @@ Bitblaster::Statistics::Statistics() :
   d_numTermClauses("theory::bv::NumberOfTermSatClauses", 0),
   d_numAtomClauses("theory::bv::NumberOfAtomSatClauses", 0),
   d_numTerms("theory::bv::NumberOfBitblastedTerms", 0),
-  d_numAtoms("theory::bv::NumberOfBitblastedAtoms", 0), 
+  d_numAtoms("theory::bv::NumberOfBitblastedAtoms", 0),
   d_bitblastTimer("theory::bv::BitblastTimer")
 {
   StatisticsRegistry::registerStat(&d_numTermClauses);
@@ -377,7 +377,7 @@ void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) {
 };
 
 void Bitblaster::MinisatNotify::safePoint() {
-  d_bv->d_out->safePoint(); 
+  d_bv->d_out->safePoint();
 }
 
 EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) {
@@ -420,70 +420,75 @@ EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) {
 
 
 bool Bitblaster::isSharedTerm(TNode node) {
-  return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); 
+  return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
 }
 
 bool Bitblaster::hasValue(TNode a) {
-  Assert (d_termCache.find(a) != d_termCache.end()); 
+  Assert (d_termCache.find(a) != d_termCache.end());
   Bits bits = d_termCache[a];
   for (int i = bits.size() -1; i >= 0; --i) {
-    SatValue bit_value; 
-    if (d_cnfStream->hasLiteral(bits[i])) { 
+    SatValue bit_value;
+    if (d_cnfStream->hasLiteral(bits[i])) {
       SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
       bit_value = d_satSolver->value(bit);
       if (bit_value == SAT_VALUE_UNKNOWN)
-        return false; 
+        return false;
     } else {
-      return false; 
+      return false;
     }
   }
-  return true; 
+  return true;
 }
-/** 
+/**
  * Returns the value a is currently assigned to in the SAT solver
- * or null if the value is completely unassigned. 
- * 
- * @param a 
- * 
- * @return 
+ * or null if the value is completely unassigned.
+ *
+ * @param a
+ *
+ * @return
  */
-Node Bitblaster::getVarValue(TNode a) {
+Node Bitblaster::getVarValue(TNode a, bool fullModel) {
   if (d_termCache.find(a) == d_termCache.end()) {
     Assert(isSharedTerm(a));
-    return Node(); 
+    return Node();
   }
   Bits bits = d_termCache[a];
-  Integer value(0); 
+  Integer value(0);
   for (int i = bits.size() -1; i >= 0; --i) {
     SatValue bit_value;
-    if (d_cnfStream->hasLiteral(bits[i])) { 
+    if (d_cnfStream->hasLiteral(bits[i])) {
       SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
       bit_value = d_satSolver->value(bit);
-      Assert (bit_value != SAT_VALUE_UNKNOWN); 
+      Assert (bit_value != SAT_VALUE_UNKNOWN);
     } else {
-      // the bit is unconstrainted so we can give it an arbitrary value 
+      //TODO: return Node() if fullModel=false?
+      // the bit is unconstrainted so we can give it an arbitrary value
       bit_value = SAT_VALUE_FALSE;
     }
-    Integer bit_int = bit_value == SAT_VALUE_TRUE ? Integer(1) : Integer(0); 
-    value = value * 2 + bit_int;  
+    Integer bit_int = bit_value == SAT_VALUE_TRUE ? Integer(1) : Integer(0);
+    value = value * 2 + bit_int;
   }
-  return utils::mkConst(BitVector(bits.size(), value));  
+  return utils::mkConst(BitVector(bits.size(), value));
 }
 
-void Bitblaster::collectModelInfo(TheoryModel* m) {
+void Bitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
   __gnu_cxx::hash_set<TNode, TNodeHashFunction>::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);
+      Node const_value = getVarValue(var, fullModel);
       if(const_value == Node()) {
-        // if the value is unassigned just set it to zero
-        const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); 
+        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") << "Bitblaster::collectModelInfo (assert (= "
+                                  << var << " "
+                                  << const_value << "))\n";
+        m->assertEquality(var, const_value, true);
       }
-      Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= "
-                                << var << " "
-                                << const_value << "))\n";
-      m->assertEquality(var, const_value, true); 
     }
   }
 }