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, 10 insertions, 9 deletions

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 1dfcb86f0..0d35d57d8 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -55,7 +55,7 @@ public:
     }
 
     bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
-      Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+      Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
       if (value) {
         return d_uf.propagate(predicate);
       } else {
@@ -64,7 +64,7 @@ public:
     }
 
     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
-      Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << std::endl;
+      Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
       if (value) {
         return d_uf.propagate(t1.eqNode(t2));
       } else {
@@ -73,12 +73,9 @@ public:
     }
 
     bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
-      Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
-      if (Theory::theoryOf(t1) == THEORY_BOOL) {
-        return d_uf.propagate(t1.iffNode(t2));
-      } else {
-        return d_uf.propagate(t1.eqNode(t2));
-      }
+      Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
+      d_uf.conflict(t1, t2);
+      return false;
     }
   };
 
@@ -119,13 +116,15 @@ private:
   /** Symmetry analyzer */
   SymmetryBreaker d_symb;
 
+  /** Conflict when merging two constants */
+  void conflict(TNode a, TNode b);
+
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
   TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
 
   void check(Effort);
-  void propagate(Effort);
   void preRegisterTerm(TNode term);
   Node explain(TNode n);
 
@@ -135,6 +134,8 @@ public:
   void addSharedTerm(TNode n);
   void computeCareGraph();
 
+  void propagate(Effort effort) {}
+
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
   std::string identify() const {