From 3f94a7cacbdf22c26c406b411da3a220ef5520d1 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Sat, 16 Jun 2012 23:58:07 +0000 Subject: [PATCH] small change to equality assertions so that one doesn't get x = y and y = x --- src/theory/theory_engine.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) 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) -- 2.30.2