1 files changed, 35 insertions, 34 deletions

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 8fc57eb48..5ff8ee4dc 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -187,20 +187,6 @@ private:
   /** A context-dependents count of nodes */
   context::CDO<DefaultSizeType> d_nodesCount;
 
-  /**
-   * At time of addition a function application can already normalize to something, so
-   * we keep both the original, and the normalized version.
-   */
-  struct FunctionApplicationPair {
-    FunctionApplication original;
-    FunctionApplication normalized;
-    FunctionApplicationPair() {}
-    FunctionApplicationPair(const FunctionApplication& original, const FunctionApplication& normalized)
-    : original(original), normalized(normalized) {}
-    bool isNull() const {
-      return !original.isApplication();
-    }
-  };
   /** Map from ids to the applications */
   std::vector<FunctionApplicationPair> d_applications;
 
@@ -336,16 +322,6 @@ private:
    */
   std::vector<Trigger> d_equalityTriggers;
 
-  struct TriggerInfo {
-    /** The trigger itself */
-    Node trigger;
-    /** Polarity of the trigger */
-    bool polarity;
-    TriggerInfo() {}
-    TriggerInfo(Node trigger, bool polarity)
-    : trigger(trigger), polarity(polarity) {}
-  };
-
   /**
    * Vector of original equalities of the triggers.
    */
@@ -515,6 +491,31 @@ private:
    */
   std::vector<TriggerTermSetRef> d_nodeIndividualTrigger;
 
+  typedef std::hash_map<EqualityPair, DisequalityReasonRef, EqualityPairHashFunction> DisequalityReasonsMap;
+
+  /**
+   * A map from pairs of disequal terms, to the reason why we deduced they are disequal.
+   */
+  DisequalityReasonsMap d_disequalityReasonsMap;
+
+  /**
+   * A list of all the disequalities we deduced.
+   */
+  std::vector<EqualityPair> d_deducedDisequalities;
+
+  /**
+   * Context dependent size of the deduced disequalities
+   */
+  context::CDO<size_t> d_deducedDisequalitiesSize;
+
+  /**
+   * For each disequality deduced, we add the pairs of equivalences needed to explain it.
+   */
+  std::vector<EqualityPair> d_deducedDisequalityReasons;
+
+
+  bool storePropagatedDisequality(TNode lhs, TNode rhs, unsigned reasonsCount) const;
+
 public:
 
   /**
@@ -594,23 +595,18 @@ public:
   void getUseListTerms(TNode t, std::set<TNode>& output);
 
   /**
-   * Returns true if the two nodes are in the same equivalence class.
-   */
-  bool areEqual(TNode t1, TNode t2) const;
-
-  /**
    * Get an explanation of the equality t1 = t2 begin true of false. 
    * Returns the reasons (added when asserting) that imply it
    * in the assertions vector.
    */
-  void explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& assertions);
+  void explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& assertions) const;
 
   /**
    * Get an explanation of the predicate being true or false. 
    * Returns the reasons (added when asserting) that imply imply it
    * in the assertions vector.
    */
-  void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions);
+  void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions) const;
 
   /**
    * Add term to the set of trigger terms with a corresponding tag. The notify class will get
@@ -652,14 +648,14 @@ public:
   void addTriggerPredicate(TNode predicate);
 
   /**
-   * Check whether the two terms are equal.
+   * Returns true if the two are currently in the database and equal.
    */
-  bool areEqual(TNode t1, TNode t2);
+  bool areEqual(TNode t1, TNode t2) const;
 
   /**
    * Check whether the two term are dis-equal.
    */
-  bool areDisequal(TNode t1, TNode t2);
+  bool areDisequal(TNode t1, TNode t2, bool ensureProof) const;
 
   /**
    * Return the number of nodes in the equivalence class containing t
@@ -667,6 +663,11 @@ public:
    */
   size_t getSize(TNode t);
 
+  /**
+   * Returns true if the engine is in a consistents state.
+   */
+  bool consistent() const { return !d_done; }
+
 };
 
 } // Namespace uf