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

1 files changed, 28 insertions, 5 deletions

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index ac6f458e9..8cf159cd7 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -78,12 +78,13 @@ public:
   virtual bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) = 0;
 
   /**
-   * Notifies about the merge of two constant terms.
+   * Notifies about the merge of two constant terms. After this, all work is suspended and all you 
+   * can do is ask for explanations.
    *
    * @param t1 a constant term
    * @param t2 a constnat term
    */
-  virtual bool eqNotifyConstantTermMerge(TNode t1, TNode t2) = 0;
+  virtual void eqNotifyConstantTermMerge(TNode t1, TNode t2) = 0;
 };
 
 /**
@@ -95,7 +96,7 @@ public:
   bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
   bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
   bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
-  bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { return true; }
+  void eqNotifyConstantTermMerge(TNode t1, TNode t2) { }
 };
 
 
@@ -521,9 +522,31 @@ private:
   std::vector<EqualityPair> d_deducedDisequalityReasons;
 
   /**
-   * Stores a propagated disequality for explanation purpooses and remembers the reasons.
+   * Size of the memory for disequality reasons.
    */
-  bool storePropagatedDisequality(TNode lhs, TNode rhs, unsigned reasonsCount) const;
+  context::CDO<size_t> d_deducedDisequalityReasonsSize;
+
+  /**
+   * Map from equalities to the tags that have received the notification.
+   */
+  typedef context::CDHashMap<EqualityPair, Theory::Set, EqualityPairHashFunction> PropagatedDisequalitiesMap;
+  PropagatedDisequalitiesMap d_propagatedDisequalities;
+
+  /**
+   * Has this equality been propagated to anyone.
+   */
+  bool hasPropagatedDisequality(EqualityNodeId lhsId, EqualityNodeId rhsId) const;
+
+  /**
+   * Has this equality been propagated to the tag owner.
+   */
+  bool hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId) const;
+
+  /**
+   * Stores a propagated disequality for explanation purpooses and remembers the reasons. The
+   * reasons should be pushed on the reasons vector.
+   */
+  void storePropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId);
   
   /**
    * An equality tagged with a set of tags.