From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Sat, 16 Jun 2012 23:58:07 +0000 (+0000)
Subject: small change to equality assertions so that one doesn't get x = y and y = x
X-Git-Tag: cvc5-1.0.0~7989
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3f94a7cacbdf22c26c406b411da3a220ef5520d1;p=cvc5.git

small change to equality assertions so that one doesn't get x = y and y = x
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 92e4b17df..161d0febd 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -894,13 +894,17 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId,
     }
   }
 
-  // Normalize to lhs < rhs
+  // Normalize to lhs < rhs if not a sat literal
   Assert(atom.getKind() == kind::EQUAL);
   Assert(atom[0] != atom[1]);
+  
   Node normalizedAtom = atom;
-  if (atom[0] > atom[1]) {
-    normalizedAtom = atom[1].eqNode(atom[0]);
-  }
+  if (!d_propEngine->isSatLiteral(normalizedAtom)) {
+    Node reverse = atom[1].eqNode(atom[0]);
+    if (d_propEngine->isSatLiteral(reverse) || atom[0] > atom[1]) {
+      normalizedAtom = reverse;
+    }  
+  } 
   Node normalizedAssertion = polarity ? normalizedAtom : normalizedAtom.notNode();
 
   // Try and assert (note that we assert the non-normalized one)