From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 28 Aug 2018 20:25:12 +0000 (-0500)
Subject: Solve equalities between Boolean variables in presolve. (#2390)
X-Git-Tag: cvc5-1.0.0~4705
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2978e5fa3434b80d3ca440ec482d5fe07bf5d368;p=cvc5.git

Solve equalities between Boolean variables in presolve. (#2390)
---

diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index d04b71ee1..2548cf5c3 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -368,7 +368,9 @@ bool CircuitPropagator::propagate() {
     Debug("circuit-prop") << "CircuitPropagator::propagate(): assigned to " << (assignment ? "true" : "false") << std::endl;
 
     // Is this an atom
-    bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.isVar();
+    bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.isVar()
+                || (current.getKind() == kind::EQUAL
+                    && (current[0].isVar() && current[1].isVar()));
 
     // If an atom, add to the list for simplification
     if (atom) {
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 3c6801f28..d025c4966 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -40,20 +40,20 @@ Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubsti
 
   // Add the substitution from the variable to its value
   if (in.getKind() == kind::NOT) {
-    if (in[0].getKind() == kind::VARIABLE) {
+    if (in[0].isVar())
+    {
       outSubstitutions.addSubstitution(in[0], NodeManager::currentNM()->mkConst<bool>(false));
-    } else {
-      return PP_ASSERT_STATUS_UNSOLVED;
+      return PP_ASSERT_STATUS_SOLVED;
     }
   } else {
-    if (in.getKind() == kind::VARIABLE) {
+    if (in.isVar())
+    {
       outSubstitutions.addSubstitution(in, NodeManager::currentNM()->mkConst<bool>(true));
-    } else {
-      return PP_ASSERT_STATUS_UNSOLVED;
+      return PP_ASSERT_STATUS_SOLVED;
     }
   }
 
-  return PP_ASSERT_STATUS_SOLVED;
+  return Theory::ppAssert(in, outSubstitutions);
 }
 
 /*