fixed model generation bug; commented out attempt at inequality propagation

5 files changed, 22 insertions, 2 deletions

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 811e9a200..c4f1b1b86 100644
--- 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 d6539f3ed..9f7760608 100644
--- 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 b19ebb381..b02233b74 100644
--- 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 8245fdbdc..502d49f58 100644
--- 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 6bc4bdaf6..ff8b3a8b1 100644
--- 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);