From 9ece5fa56493692aff1a17c73e0039fd1b232a06 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 9 Apr 2021 11:01:23 -0700 Subject: [PATCH] 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 --- src/theory/booleans/circuit_propagator.cpp | 4 +++- src/theory/theory.cpp | 17 +++++++++++++++++ test/regress/CMakeLists.txt | 3 ++- 3 files changed, 22 insertions(+), 2 deletions(-) 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 -- 2.30.2