diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-04-09 11:01:23 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-09 13:01:23 -0500 |
commit | 9ece5fa56493692aff1a17c73e0039fd1b232a06 (patch) | |
tree | ff0783ad27e6eed8989cee105e9fdc76f8f58efd | |
parent | 40abcb2a5cdd63b331446da6feae0148ad8bb2c5 (diff) |
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
-rw-r--r-- | src/theory/booleans/circuit_propagator.cpp | 4 | ||||
-rw-r--r-- | src/theory/theory.cpp | 17 | ||||
-rw-r--r-- | 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 |