From f3bf9af12eb6af487e61c585fa9639f1d1485220 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 21 Oct 2021 12:10:26 -0700 Subject: [PATCH] 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. --- src/theory/booleans/proof_circuit_propagator.cpp | 6 ++++-- test/regress/CMakeLists.txt | 3 ++- ...-ite.smt2 => proj-issue305-circuit-prop-ite-a.smt2} | 0 .../preprocess/proj-issue305-circuit-prop-ite-b.smt2 | 10 ++++++++++ 4 files changed, 16 insertions(+), 3 deletions(-) rename test/regress/regress0/preprocess/{proj-issue305-circuit-prop-ite.smt2 => proj-issue305-circuit-prop-ite-a.smt2} (100%) create mode 100644 test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 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 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 similarity index 100% rename from test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite.smt2 rename to 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 -- 2.30.2