fixed model generation bug; commented out attempt at inequality propagation

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 811e9a200e2690b15d2ce55580ae12bd747d42b6..c4f1b1b86b25a6467c2cd85fdae3cb016a4409b3 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -243,7 +243,7 @@ void CoreSolver::buildModel() {
     if  (repr.getKind() == kind::CONST_BITVECTOR) {
       // must check if it's just the constant
       eq::EqClassIterator it(repr, &d_equalityEngine);
-      if (!(++it).isFinished()) {
+      if (!(++it).isFinished() || true) {
         constants.insert(repr);
         constants_in_eq_engine.insert(repr); 
       }

diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index d6539f3edb0c0f68c4f4c327828db4765ce83522..9f7760608f8570fb59984058995cccaa8d3e9574 100644 (file)
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -49,6 +49,12 @@ bool InequalitySolver::check(Theory::Effort e) {
       TNode a = fact[0][1];
       TNode b = fact[0][0]; 
       ok = d_inequalityGraph.addInequality(a, b, true, fact);
+      // propagate
+      // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
+      //   Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b)); 
+      //   d_bv->storePropagation(neq, SUB_INEQUALITY);
+      //   d_explanations[neq] = fact;
+      // }
     } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULT) {
       TNode a = fact[0][1];
       TNode b = fact[0][0]; 
@@ -57,6 +63,12 @@ bool InequalitySolver::check(Theory::Effort e) {
       TNode a = fact[0];
       TNode b = fact[1]; 
       ok = d_inequalityGraph.addInequality(a, b, true, fact);
+      // propagate
+      // if (d_bv->isSharedTerm(a) && d_bv->isSharedTerm(b)) {
+      //   Node neq = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, a, b)); 
+      //   d_bv->storePropagation(neq, SUB_INEQUALITY);
+      //   d_explanations[neq] = fact;
+      // }
     } else if (fact.getKind() == kind::BITVECTOR_ULE) {
       TNode a = fact[0];
       TNode b = fact[1]; 
@@ -147,7 +159,10 @@ bool InequalitySolver::isInequalityOnly(TNode node) {
 }
 
 void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
-  Assert (false); 
+  Assert (d_explanations.find(literal) != d_explanations.end());
+  TNode explanation = d_explanations[literal];
+  assumptions.push_back(explanation);
+  Debug("bv-inequality-explain") << "InequalitySolver::explain " << literal << " with " << explanation <<"\n"; 
 }
 
 void InequalitySolver::propagate(Theory::Effort e) {

diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index b19ebb381ba30f3c577d4a014337ceb07780b5e4..b02233b746770eab4fa7f78add15dbb3c3fd2fbc 100644 (file)
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -36,6 +36,7 @@ class InequalitySolver: public SubtheorySolver {
 
   context::CDHashSet<Node, NodeHashFunction> d_assertionSet; 
   InequalityGraph d_inequalityGraph;
+  context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations; 
   context::CDO<bool> d_isComplete;
   __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_ineqTermCache; 
   bool isInequalityOnly(TNode node); 
@@ -45,6 +46,7 @@ public:
     : SubtheorySolver(c, bv),
       d_assertionSet(c),
       d_inequalityGraph(c),
+      d_explanations(c),
       d_isComplete(c, true),
       d_ineqTermCache(),
       d_statistics()

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 8245fdbdcc9f1b3bc128d60fc1b5c096e2041bb8..502d49f58ffe4f077bead2eb49632ad8180b84db 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -275,6 +275,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
       // Safe to ignore this one, subtheory should produce a conflict
       return true;
     }
+ 
     d_propagatedBy[literal] = subtheory;
   }
 

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 6bc4bdaf6c22e735e8b4bc7cb867c59a39a7757f..ff8b3a8b1b82a9430b0911e21cf02e36c4352313 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -123,6 +123,8 @@ private:
 
   void addSharedTerm(TNode t);
 
+  bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); }
+  
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
   Node getModelValue(TNode var);