fixes for bug347

it was an issue with constants being merged, which influenced explanations of disequalities. when constants are attempted to be merged, equality engine now enters conflict mode immediately

2 files changed, 29 insertions, 16 deletions

diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index 98678a9b4..afb4a8b4a 100644
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -29,7 +29,7 @@ using namespace CVC4::theory::bv::utils;
 
 EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
-    d_notify(bv),
+    d_notify(*this),
     d_equalityEngine(d_notify, c, "theory::bv::TheoryBV")
 {
   if (d_useEqualityEngine) {
@@ -127,34 +127,41 @@ bool EqualitySolver::addAssertions(const std::vector<TNode>& assertions, Theory:
 bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
   BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
   if (value) {
-    return d_bv->storePropagation(equality, TheoryBV::SUB_EQUALITY);
+    return d_solver.storePropagation(equality);
   } else {
-    return d_bv->storePropagation(equality.notNode(), TheoryBV::SUB_EQUALITY);
+    return d_solver.storePropagation(equality.notNode());
   }
 }
 
 bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
   BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
   if (value) {
-    return d_bv->storePropagation(predicate, TheoryBV::SUB_EQUALITY);
+    return d_solver.storePropagation(predicate);
   } else {
-    return d_bv->storePropagation(predicate.notNode(), TheoryBV::SUB_EQUALITY);
+    return d_solver.storePropagation(predicate.notNode());
   }
 }
 
 bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
   Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
   if (value) {
-    return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY);
+    return d_solver.storePropagation(t1.eqNode(t2));
   } else {
-    return d_bv->storePropagation(t1.eqNode(t2).notNode(), TheoryBV::SUB_EQUALITY);
+    return d_solver.storePropagation(t1.eqNode(t2).notNode());
   }
 }
 
-bool EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
-  Debug("bitvector::equality") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
-  if (Theory::theoryOf(t1) == THEORY_BOOL) {
-    return d_bv->storePropagation(t1.iffNode(t2), TheoryBV::SUB_EQUALITY);
-  }
-  return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY);
+void EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+  d_solver.conflict(t1, t2);
+}
+
+bool EqualitySolver::storePropagation(TNode literal) {
+  return d_bv->storePropagation(literal, TheoryBV::SUB_EQUALITY);
 }
+  
+void EqualitySolver::conflict(TNode a, TNode b) {
+  std::vector<TNode> assumptions;
+  d_equalityEngine.explainEquality(a, b, true, assumptions);
+  d_bv->setConflict(mkAnd(assumptions));
+}
+
diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h
index 356d12a06..d4239ff13 100644
--- a/src/theory/bv/bv_subtheory_eq.h
+++ b/src/theory/bv/bv_subtheory_eq.h
@@ -32,14 +32,14 @@ class EqualitySolver : public SubtheorySolver {
   // NotifyClass: handles call-back from congruence closure module
 
   class NotifyClass : public eq::EqualityEngineNotify {
-    TheoryBV* d_bv;
+    EqualitySolver& d_solver;
 
   public:
-    NotifyClass(TheoryBV* bv): d_bv(bv) {}
+    NotifyClass(EqualitySolver& solver): d_solver(solver) {}
     bool eqNotifyTriggerEquality(TNode equality, bool value);
     bool eqNotifyTriggerPredicate(TNode predicate, bool value);
     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
-    bool eqNotifyConstantTermMerge(TNode t1, TNode t2);
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2);
 };
 
 
@@ -49,6 +49,12 @@ class EqualitySolver : public SubtheorySolver {
   /** Equality engine */
   eq::EqualityEngine d_equalityEngine;
 
+  /** Store a propagation to the bv solver */
+  bool storePropagation(TNode literal);
+  
+  /** Store a conflict from merging two constants */
+  void conflict(TNode a, TNode b);
+
 public:
 
   EqualitySolver(context::Context* c, TheoryBV* bv);