several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify and now term notify handles boolean constants; fixed bug 328

4 files changed, 67 insertions, 33 deletions

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index d53507def..41c0c4ac9 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -101,6 +101,7 @@ Solver::Solver(CVC4::context::Context* c) :
   , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
   , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
 
+  , need_to_propagate(false)
   , only_bcp(false)
   , clause_added(false)
   , ok                 (true)
@@ -187,13 +188,12 @@ bool Solver::addClause_(vec<Lit>& ps)
     else if (ps.size() == 1){
         uncheckedEnqueue(ps[0]);
         return ok = (propagate() == CRef_Undef);
-    }else{
+    } else {
         CRef cr = ca.alloc(ps, false);
         clauses.push(cr);
         attachClause(cr);
     }
-
-    return true;
+    return ok; 
 }
 
 void Solver::attachClause(CRef cr) {
@@ -514,8 +514,8 @@ void Solver::popAssumption() {
 }
 
 lbool Solver::assertAssumption(Lit p, bool propagate) {
-
-  assert(marker[var(p)] == 1);
+  
+  // assert(marker[var(p)] == 1);
 
   if (decisionLevel() > assumptions.size()) {
     cancelUntil(assumptions.size());
@@ -759,7 +759,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
               analyzeFinal(p, conflict);
               return l_False;
             }
-
+            
             varDecayActivity();
             claDecayActivity();
 
@@ -927,7 +927,6 @@ lbool Solver::solve_()
 // 
 
 void Solver::explain(Lit p, std::vector<Lit>& explanation) {
-
   vec<Lit> queue;
   queue.push(p);
 
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index ae5efd81e..ea8e98c4c 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -190,6 +190,7 @@ public:
       marker[var] = 1;
     }
 
+    bool need_to_propagate;             // true if we added new clauses, set to true in propagation 
     bool only_bcp;                      // solving mode in which only boolean constraint propagation is done
     void setOnlyBCP (bool val) { only_bcp = val;}
     void explain(Lit l, std::vector<Lit>& explanation);
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index bbbfdc1ad..5ca1594ee 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -39,6 +39,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
   : Theory(THEORY_BV, c, u, out, valuation, logicInfo),
     d_context(c),
     d_assertions(c),
+    d_bitblastQueue(c),
     d_bitblaster(new Bitblaster(c, this) ),
     d_alreadyPropagatedSet(c),
     d_sharedTermsSet(c),
@@ -114,12 +115,13 @@ void TheoryBV::preRegisterTerm(TNode node) {
     return;
   }
 
-  if (node.getKind() == kind::EQUAL ||
-      node.getKind() == kind::BITVECTOR_ULT ||
-      node.getKind() == kind::BITVECTOR_ULE ||
-      node.getKind() == kind::BITVECTOR_SLT ||
-      node.getKind() == kind::BITVECTOR_SLE) {
-    d_bitblaster->bbAtom(node);
+  if ((node.getKind() == kind::EQUAL ||
+       node.getKind() == kind::BITVECTOR_ULT ||
+       node.getKind() == kind::BITVECTOR_ULE ||
+       node.getKind() == kind::BITVECTOR_SLT ||
+       node.getKind() == kind::BITVECTOR_SLE) &&
+      !d_bitblaster->hasBBAtom(node)) {
+    d_bitblastQueue.push_back(node); 
   }
 
   if (d_useEqualityEngine) {
@@ -157,11 +159,21 @@ void TheoryBV::check(Effort e)
     return;
   }
 
+  // getting the new assertions
+  
+  std::vector<TNode> new_assertions; 
   while (!done() && !d_conflict) {
     Assertion assertion = get();
     TNode fact = assertion.assertion;
-
+    new_assertions.push_back(fact);
     BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; 
+  }
+
+  // sending assertions to equality engine first
+
+  for (unsigned i = 0; i < new_assertions.size(); ++i) {
+    TNode fact = new_assertions[i];
+    TypeNode factType = fact[0].getType(); 
 
     // Notify the equality engine
     if (d_useEqualityEngine && !d_conflict && !propagatedBy(fact, SUB_EQUALITY) ) {
@@ -183,7 +195,24 @@ void TheoryBV::check(Effort e)
       }
     }
 
-    // Bit-blaster
+    // checking for a conflict 
+    if (d_conflict) {
+      BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
+      d_out->conflict(d_conflictNode);
+      return;
+    }
+  }
+
+  // bit-blasting atoms on queue
+
+  for (unsigned i = 0; i < d_bitblastQueue.size(); ++i) {
+    d_bitblaster->bbAtom(d_bitblastQueue[i]);
+    // would be nice to clear the bitblastQueue?
+  }
+  
+  // bit-blaster propagation 
+  for (unsigned i = 0; i < new_assertions.size(); ++i) {
+    TNode fact = new_assertions[i];
     if (!d_conflict && !propagatedBy(fact, SUB_BITBLASTER)) {
       // Some atoms have not been bit-blasted yet
       d_bitblaster->bbAtom(fact);
@@ -202,7 +231,7 @@ void TheoryBV::check(Effort e)
 
   // If in conflict, output the conflict
   if (d_conflict) {
-    BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode;
+    BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
     d_out->conflict(d_conflictNode);
     return;
   }
@@ -242,7 +271,7 @@ Node TheoryBV::getValue(TNode n) {
 
 
 void TheoryBV::propagate(Effort e) {
-  BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate()" << std::endl;
+  BVDebug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
 
   if (d_conflict) {
     return;
@@ -266,7 +295,7 @@ void TheoryBV::propagate(Effort e) {
         // check if we already propagated the negation
         Node negLiteral = literal.getKind() == kind::NOT ? (Node)literal[0] : mkNot(literal);
         if (d_alreadyPropagatedSet.find(negLiteral) != d_alreadyPropagatedSet.end()) {
-          Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict " << literal << " and its negation both propagated \n"; 
+          Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict " << literal << " and its negation both propagated \n"; 
           // we are in conflict
           std::vector<TNode> assumptions;
           explain(literal, assumptions);
@@ -276,11 +305,11 @@ void TheoryBV::propagate(Effort e) {
           return;
         }
         
-        BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): " << literal << std::endl;
+        BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << literal << std::endl;
         d_out->propagate(literal);
         d_alreadyPropagatedSet.insert(literal); 
       } else {
-        Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
+        Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
         
         Node negatedLiteral;
         std::vector<TNode> assumptions;
@@ -324,11 +353,11 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
 
 bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 {
-  Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal  << ")" << std::endl;
+  Debug("bitvector") << indent() << "TheoryBV::storePropagation(" << literal  << ")" << std::endl;
 
   // If already in conflict, no more propagation
   if (d_conflict) {
-    Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << "): already in conflict" << std::endl;
+    Debug("bitvector") << indent() << "TheoryBV::storePropagation(" << literal << "): already in conflict" << std::endl;
     return false;
   }
 
@@ -346,7 +375,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 
   // If asserted, we might be in conflict
   if (hasSatValue && !satValue) {
-    Debug("bitvector-prop") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ") => conflict" << std::endl;
+    Debug("bitvector-prop") << indent() << "TheoryBV::storePropagation(" << literal << ") => conflict" << std::endl;
     std::vector<TNode> assumptions;
     Node negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode();
     assumptions.push_back(negatedLiteral);
@@ -357,7 +386,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
   }
 
   // Nothing, just enqueue it for propagation and mark it as asserted already
-  Debug("bitvector-prop") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ") => enqueuing for propagation" << std::endl;
+  Debug("bitvector-prop") << indent() << "TheoryBV::storePropagation(" << literal << ") => enqueuing for propagation" << std::endl;
   d_literalsToPropagate.push_back(literal);
 
   // No conflict
@@ -399,7 +428,7 @@ Node TheoryBV::explain(TNode node) {
 
 
 void TheoryBV::addSharedTerm(TNode t) {
-  Debug("bitvector::sharing") << spaces(getSatContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
+  Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
   d_sharedTermsSet.insert(t); 
   if (!Options::current()->bitvectorEagerBitblast && d_useEqualityEngine) {
     d_equalityEngine.addTriggerTerm(t);
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index e46d052f8..6ef9d18dd 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -42,12 +42,6 @@ namespace bv {
 /// forward declarations 
 class Bitblaster;
 
-static inline std::string spaces(int level)
-{
-  std::string indentStr(level, ' ');
-  return indentStr;
-}
-
 class TheoryBV : public Theory {
 
 
@@ -61,7 +55,9 @@ private:
   
   /** Bitblaster */
   Bitblaster* d_bitblaster; 
-    
+
+  context::CDList<TNode> d_bitblastQueue; 
+  
   /** Context dependent set of atoms we already propagated */
   context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet;
   context::CDHashSet<TNode, TNodeHashFunction> d_sharedTermsSet;
@@ -119,7 +115,7 @@ private:
       if (value) {
         return d_bv.storePropagation(predicate, SUB_EQUALITY);
       } else {
-       return d_bv.storePropagation(predicate, SUB_EQUALITY);
+        return d_bv.storePropagation(predicate.notNode(), SUB_EQUALITY);
       }
     }
 
@@ -134,6 +130,9 @@ private:
 
     bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
       Debug("bitvector") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
+      if (Theory::theoryOf(t1) == THEORY_BOOL) {
+        return d_bv.storePropagation(t1.iffNode(t2), SUB_EQUALITY);
+      }
       return d_bv.storePropagation(t1.eqNode(t2), SUB_EQUALITY);
     }
   };
@@ -190,6 +189,12 @@ private:
 
   friend class Bitblaster;
 
+  inline std::string indent()
+  {
+    std::string indentStr(getSatContext()->getLevel(), ' ');
+    return indentStr;
+  }
+  
 public:
 
   void propagate(Effort e);