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

2 files changed, 10 insertions, 8 deletions

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);
 }
 
 /*