diff options
| -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 |