Changes to the combination mechanism, lots of details. Not done yet, there are still the AUFBV wrong results, but it seems better.

http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5

1 files changed, 96 insertions, 62 deletions

diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index c044097ff..1a38d7332 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -18,12 +18,14 @@
 
 #include "expr/node.h"
 #include "theory/theory.h"
-#include "context/context.h"
-#include "util/stats.h"
 #include "theory/uf/equality_engine.h"
+#include "util/stats.h"
+#include "context/cdhashset.h"
 
 namespace CVC4 {
 
+class TheoryEngine;
+
 class SharedTermsDatabase : public context::ContextNotifyObj {
 
 public:
@@ -54,51 +56,20 @@ private:
   /** Context-dependent size of the d_addedSharedTerms list */
   context::CDO<unsigned> d_addedSharedTermsSize;
   
-  typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap;
-
   /** A map from atoms and subterms to the theories that use it */
+  typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap;
   SharedTermsTheoriesMap d_termsToTheories;
 
-  typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap;
-
   /** Map from term to theories that have already been notified about the shared term */
+  typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap;
   AlreadyNotifiedMap d_alreadyNotifiedMap;
 
-public:
-
-  /** Class for notifications about new shared term equalities */
-  class SharedTermsNotifyClass {
-    public:
-      SharedTermsNotifyClass() {}
-      virtual ~SharedTermsNotifyClass() {}
-      virtual void notify(TNode literal, TNode original, theory::TheoryId theory) = 0;
-  };
+  /** The registered equalities for propagation */
+  typedef context::CDHashSet<TNode, TNodeHashFunction> RegisteredEqualitiesSet;
+  RegisteredEqualitiesSet d_registeredEqualities;
 
 private:
 
-  // Instance of class to send shared term notifications to
-  SharedTermsNotifyClass& d_sharedNotify;
-
-  // Type for list of theory, node pairs: theory is theory to be notified,
-  // node is the representative for this equivalence class known to the
-  // theory that will be notified
-  typedef context::CDHashMap<theory::TheoryId, TNode, __gnu_cxx::hash<unsigned> > NotifyList;
-  typedef context::CDHashMap<TNode, NotifyList*, TNodeHashFunction> TermToNotifyList;
-
-  // Map from terms (only valid for reps) to their notify lists
-  // Note that theory, term pairs only need to be in the notify list if the
-  // representative term is not a valid shared term for the theory.
-  TermToNotifyList d_termToNotifyList;
-
-  // List of allocated NotifyList* objects
-  std::vector<NotifyList*> d_allocatedNL;
-
-  // Total number of allocated NotifyList* objects
-  unsigned d_allocatedNLSize;
-
-  // Size of portion of d_allocatedNL that is currently in use
-  context::CDO<unsigned> d_allocatedNLNext;
-
   /** This method removes all the un-necessary stuff from the maps */
   void backtrack();
 
@@ -108,7 +79,7 @@ private:
   public:
     EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {}
     bool eqNotifyTriggerEquality(TNode equality, bool value) {
-      Unreachable();
+      d_sharedTerms.propagateEquality(equality, value);
       return true;
     }
 
@@ -118,14 +89,12 @@ private:
     }
 
     bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) {
-      if (value) {
-        d_sharedTerms.mergeSharedTerms(t1, t2);
-      }
-      return true;
+      return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value);
     }
 
     bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
-      return true;
+      d_sharedTerms.conflict(t1, t2, true);
+      return false;
     }
   };
 
@@ -135,24 +104,83 @@ private:
   /** Equality engine */
   theory::eq::EqualityEngine d_equalityEngine;
 
-  /** Attach a new notify list to an equivalence class representative */
-  NotifyList* getNewNotifyList();
+  /**
+   * Method called by equalityEngine when a becomes (dis-)equal to b and a and b are shared with
+   * the theory. Returns false if there is a direct conflict (via rewrite for example).
+   */
+  bool propagateSharedEquality(theory::TheoryId theory, TNode a, TNode b, bool value);
+
+  /**
+   * Called from the equality engine when a trigger equality is deduced.
+   */
+  bool propagateEquality(TNode equality, bool polarity);
+
+  /** Theory engine */
+  TheoryEngine* d_theoryEngine;  
+
+  /** Are we in conflict */
+  context::CDO<bool> d_inConflict;
+  
+  /** Conflicting terms, if any */
+  Node d_conflictLHS, d_conflictRHS;
+  
+  /** Polarity of the conflict */
+  bool d_conflictPolarity;
+
+  /** Called by the equality engine notify to mark the conflict */
+  void conflict(TNode lhs, TNode rhs, bool polarity) {
+    if (!d_inConflict) {
+      // Only remember it if we're not already in conflict
+      d_inConflict = true;
+      d_conflictLHS = lhs;
+      d_conflictRHS = rhs;
+      d_conflictPolarity = polarity;
+    }
+  }
 
-  /** Method called by equalityEngine when a becomes equal to b */
-  void mergeSharedTerms(TNode a, TNode b);
+  /**
+   * Should be called before any public non-const method in order to
+   * enqueue the conflict to the theory engine.
+   */
+  void checkForConflict();
 
 public:
 
-  SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context);
+  SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context);
   ~SharedTermsDatabase() throw(AssertionException);
   
   /**
+   * Asserts the equality to the shared terms database,
+   */
+  void assertEquality(TNode equality, bool polarity, TNode reason);
+
+  /**
+   * Return whether the equality is alreday known to the engine
+   */
+  bool isKnown(TNode literal) const;
+
+  /** 
+   * Returns an explanation of the propagation that came from the database.
+   */
+  Node explain(TNode literal) const;
+
+  /**
+   * Add an equality to propagate.
+   */
+  void addEqualityToPropagate(TNode equality);
+  
+  /**
    * Add a shared term to the database. The shared term is a subterm of the atom and 
    * should be associated with the given theory. 
    */
   void addSharedTerm(TNode atom, TNode term, theory::Theory::Set theories);
 
   /**
+   * Mark that the given theories have been notified of the given shared term.
+   */
+  void markNotified(TNode term, theory::Theory::Set theories);
+
+  /**
    * Returns true if the atom contains any shared terms, false otherwise.
    */
   bool hasSharedTerms(TNode atom) const;
@@ -176,26 +204,32 @@ public:
    * Get the theories that share the term and have been notified already.
    */
   theory::Theory::Set getNotifiedTheories(TNode term) const;
-
-  // Notify theory about a new equality between shared terms
-  void assertEq(TNode equality, theory::TheoryId theory);
-
+   
   /**
-   * Mark that the given theories have been notified of the given shared term.
+   * Returns true if the term is currently registered as shared with some theory.
    */
-  void markNotified(TNode term, theory::Theory::Set theories);
-   
   bool isShared(TNode term) const {
-    return d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end();
+    return term.isConst() || d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end();
   }
 
-  bool areEqual(TNode a, TNode b);
-
-  bool areDisequal(TNode a, TNode b);
+  /**
+   * Returns true if the literal is an (dis-)equality with both sides registered as shared with
+   * some theory.
+   */
+  bool isSharedEquality(TNode literal) const {
+    TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
+    return atom.getKind() == kind::EQUAL && isShared(atom[0]) && isShared(atom[1]);
+  }
 
-  void processSharedLiteral(TNode literal, TNode reason);
+  /**
+   * Returns true if the shared terms a and b are known to be equal.
+   */
+  bool areEqual(TNode a, TNode b) const;
 
-  Node explain(TNode literal);
+  /**
+   * Retursn true if the shared terms a and b are known to be dis-equal.
+   */
+  bool areDisequal(TNode a, TNode b) const;
 
 protected: