From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 9 Apr 2021 18:01:23 +0000 (-0700)
Subject: Learn equalities involving Boolean variables (#6323)
X-Git-Tag: cvc5-1.0.0~1934
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9ece5fa56493692aff1a17c73e0039fd1b232a06;p=cvc5.git

Learn equalities involving Boolean variables (#6323)

Previously, the circuit propagator was not learning literals of the form (= x t) where x is Boolean, since this term was not treated as a theory literal.
This commit changes that, which improves performance significantly, since it
allows the elimination of Boolean variables, which, in turn, can make the
justification heuristic much more effective.

Signed-off-by: Andres Noetzli noetzli@amazon.com
---

diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index aa400a750..df50bccac 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -716,7 +716,9 @@ TrustNode CircuitPropagator::propagate()
                     && (current[0].isVar() && current[1].isVar()));
 
     // If an atom, add to the list for simplification
-    if (atom)
+    if (atom
+        || (current.getKind() == kind::EQUAL
+            && (current[0].isVar() || current[1].isVar())))
     {
       Debug("circuit-prop")
           << "CircuitPropagator::propagate(): adding to learned: "
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index c15652eef..55ce4f292 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -405,6 +405,23 @@ Theory::PPAssertStatus Theory::ppAssert(TrustNode tin,
       }
     }
   }
+  else if (in.getKind() == kind::NOT && in[0].getKind() == kind::EQUAL
+           && in[0][0].getType().isBoolean())
+  {
+    TNode eq = in[0];
+    if (eq[0].isVar())
+    {
+      Node res = eq[0].eqNode(eq[1].notNode());
+      TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr);
+      return ppAssert(tn, outSubstitutions);
+    }
+    else if (eq[1].isVar())
+    {
+      Node res = eq[1].eqNode(eq[0].notNode());
+      TrustNode tn = TrustNode::mkTrustRewrite(in, res, nullptr);
+      return ppAssert(tn, outSubstitutions);
+    }
+  }
 
   return PP_ASSERT_STATUS_UNSOLVED;
 }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 048372c69..38748b757 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1581,7 +1581,6 @@ set(regress_1_tests
   regress1/nl/disj-eval.smt2
   regress1/nl/dist-big.smt2
   regress1/nl/div-mod-partial.smt2
-  regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2
   regress1/nl/exp-4.5-lt.smt2
   regress1/nl/exp-approx.smt2
   regress1/nl/exp-soundness-bound.smt2
@@ -2541,6 +2540,8 @@ set(regression_disabled_tests
   regress1/ho/hoa0102.smt2
   # slow on some builds after changes to tangent planes
   regress1/nl/approx-sqrt-unsat.smt2
+  # times out after update to circuit propagator
+  regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2
   # times out after update to tangent planes
   regress1/nl/NAVIGATION2.smt2
   # sat or unknown in different builds