diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-10-21 12:10:26 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-21 19:10:26 +0000 |
| commit | f3bf9af12eb6af487e61c585fa9639f1d1485220 (patch) | |
| tree | 8cae4300799cb7a102fb51acfb273a00eec8fe45 | |
| parent | 2da1033d731495b4925087f06a082a81cadf97a9 (diff) | |
Fix symmetric proof issue for ITE in circuit propagator (#7452)
This PR goes back to #7446 and implements a proper fix that handles both symmetrical cases.
| -rw-r--r-- | src/theory/booleans/proof_circuit_propagator.cpp | 6 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2 (renamed from test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite.smt2) | 0 | ||||
| -rw-r--r-- | test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 | 10 |
4 files changed, 16 insertions, 3 deletions
diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index 3b1e40667..fa48f7638 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -396,8 +396,10 @@ std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteIsCase(unsigned c) } if (d_parentAssignment) { - return mkResolution( - mkProof(PfRule::ITE_ELIM2, {assume(d_parent)}), d_parent[c + 1], true); + return mkResolution(mkProof(c == 0 ? PfRule::ITE_ELIM1 : PfRule::ITE_ELIM2, + {assume(d_parent)}), + d_parent[c + 1], + true); } return mkResolution( mkProof(PfRule::NOT_ITE_ELIM2, {assume(d_parent.notNode())}), diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fe7c3fdaf..1ed42dd77 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -835,7 +835,8 @@ set(regress_0_tests regress0/preprocess/preprocess_14.cvc.smt2 regress0/preprocess/preprocess_15.cvc.smt2 regress0/preprocess/proj-issue304-circuit-prop-xor.smt2 - regress0/preprocess/proj-issue305-circuit-prop-ite.smt2 + regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2 + regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 regress0/print_define_fun_internal.smt2 regress0/print_lambda.cvc.smt2 regress0/print_model.cvc.smt2 diff --git a/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite.smt2 b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2 index 6760bdf4d..6760bdf4d 100644 --- a/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite.smt2 +++ b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2 diff --git a/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 new file mode 100644 index 000000000..fcb26054e --- /dev/null +++ b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 @@ -0,0 +1,10 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :check-proofs true) +(declare-fun a () Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) +(assert c) +(assert (not b)) +(assert (ite a b c)) +(check-sat)
\ No newline at end of file |