From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Wed, 14 Dec 2011 09:31:21 +0000 (+0000)
Subject: some more bug fixes (TNode -> Node, normalize literals in explanations)
X-Git-Tag: cvc5-1.0.0~8358
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ee64b3fa49a22b89ffb3e62d8d7144fc9b99754e;p=cvc5.git

some more bug fixes (TNode -> Node, normalize literals in explanations)
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 4c289b5c1..d08e79c8e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -570,16 +570,16 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
     d_propagatedLiterals.push_back(literal);
   } else {
     // Otherwise it might be a shared-term (dis-)equality
-    Node normalizedEquality = Rewriter::rewrite(literal);
-    if (d_propEngine->isSatLiteral(normalizedEquality)) {
+    Node normalizedLiteral = Rewriter::rewrite(literal);
+    if (d_propEngine->isSatLiteral(normalizedLiteral)) {
       // If there is a literal, just enqueue it, same as above
       bool value;
-      if (d_propEngine->hasValue(normalizedEquality, value)) {
+      if (d_propEngine->hasValue(normalizedLiteral, value)) {
         // if we are propagting something that already has a sat value we better be the same
-        Debug("theory") << "literal " << literal << " (" << normalizedEquality << ") propagated by " << theory << " but already has a sat value" << std::endl;
-        Assert((value && (literal.getKind() != kind::NOT)) || (!value && literal.getKind() == kind::NOT));
+        Debug("theory") << "literal " << literal << " (" << normalizedLiteral << ") propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl;
+        Assert(value);
       } else {
-        d_propagatedLiterals.push_back(normalizedEquality);
+        d_propagatedLiterals.push_back(normalizedLiteral);
       }
     }
     // Otherwise, we assert it to all interested theories
@@ -708,7 +708,7 @@ void TheoryEngine::explainEquality(TheoryId theoryId, TNode eqLiteral, NodeBuild
   SharedAssertionsMap::iterator find = d_sharedAssertions.find(NodeTheoryPair(eqLiteral, theoryId));
   if (find == d_sharedAssertions.end()) {
     // Not a shared assertion, just add it since it must be SAT literal
-    builder << eqLiteral;
+    builder << Rewriter::rewrite(eqLiteral);
   } else {
     TheoryId explainingTheory = (*find).second.theory;
     if (explainingTheory == theory::THEORY_LAST) {
@@ -721,4 +721,3 @@ void TheoryEngine::explainEquality(TheoryId theoryId, TNode eqLiteral, NodeBuild
     }
   }
 }
-
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index e2462f244..2344adc70 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -137,9 +137,10 @@ void TheoryUF::propagate(Effort level) {
       } else {
         if (!satValue) {
           Debug("uf") << "TheoryUF::propagate(): in conflict" << std::endl;
+          Node negatedLiteral;
           std::vector<TNode> assumptions;
           if (literal != d_false) {
-            TNode negatedLiteral = literal.getKind() == kind::NOT ? literal[0] : (TNode) literal.notNode();
+            negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode();
             assumptions.push_back(negatedLiteral);
           }
           explain(literal, assumptions);
@@ -206,8 +207,9 @@ bool TheoryUF::propagate(TNode literal) {
     } else {
       Debug("uf") << "TheoryUF::propagate(" << literal << ") => conflict" << std::endl;
       std::vector<TNode> assumptions;
+      Node negatedLiteral;
       if (literal != d_false) {
-        TNode negatedLiteral = literal.getKind() == kind::NOT ? literal[0] : (TNode) literal.notNode();
+        negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode();
         assumptions.push_back(negatedLiteral);
       }
       explain(literal, assumptions);