From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Mon, 11 Jul 2011 12:45:16 +0000 (+0000)
Subject: adding disequality propagation
X-Git-Tag: cvc5-1.0.0~8508
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e72fdcf6333d575e9c737a6274aa627dc9c54b47;p=cvc5.git

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 0776ecf0d..a3eeec633 100644
--- 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 d78504dc8..de8e70a49 100644
--- 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);