adding disequality propagation

relevant comparison http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2602&reference_id=2590&p=5

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 0776ecf0d721f570d3cd7cb645cc1ec5353c2dc1..a3eeec633a85836292423ee2c51f7bdc4ac381cc 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -67,7 +67,7 @@ void TheoryUF::check(Effort level) {
       if (assertion[0].getKind() == kind::APPLY_UF) {
         d_equalityEngine.addEquality(assertion[0], d_false, assertion);
       } else {
-        // disequality
+        // Disequality check
         TNode equality = assertion[0];
         if (d_equalityEngine.getRepresentative(equality[0]) == d_equalityEngine.getRepresentative(equality[1])) {
           std::vector<TNode> assumptions;
@@ -76,6 +76,8 @@ void TheoryUF::check(Effort level) {
           d_conflictNode = mkAnd(assumptions);
           d_conflict = true;
         }
+        // Assert the dis-equality
+        d_equalityEngine.addEquality(assertion[0], d_false, assertion);
       }
       break;
     default:
@@ -136,8 +138,11 @@ void TheoryUF::preRegisterTerm(TNode node) {
     // Add the terms
     d_equalityEngine.addTerm(node[0]);
     d_equalityEngine.addTerm(node[1]);
-    // Add the trigger
+    // Add the trigger for equality
     d_equalityEngine.addTriggerEquality(node[0], node[1], node);
+       // Add the disequality terms and triggers
+       d_equalityEngine.addTerm(node);
+       d_equalityEngine.addTriggerEquality(node, d_false, node.notNode());
     break;
   case kind::APPLY_UF:
     // Function applications/predicates

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index d78504dc896b74281ba1185f87eb44f1018ad6e4..de8e70a49e4f462b5fef0f00574dd58509eb6121 100644 (file)
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -103,6 +103,7 @@ public:
   {
     // The kinds we are treating as function application in congruence
     d_equalityEngine.addFunctionKind(kind::APPLY_UF);
+    d_equalityEngine.addFunctionKind(kind::EQUAL);
 
     // The boolean constants
     d_true = NodeManager::currentNM()->mkConst<bool>(true);