From f1db161860d0283cb5537ad8847e0b52d1485e28 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 22 Oct 2021 14:37:54 -0700 Subject: [PATCH] Fix another double negation proof issue (#7468) This PR fixes another subtle proof issue in the circuit propagator concerning negated ites. Fixes cvc5/cvc5-projects#309. --- src/theory/booleans/proof_circuit_propagator.cpp | 9 +++++---- test/regress/CMakeLists.txt | 1 + .../preprocess/proj-issue309-circuit-prop-ite.smt2 | 9 +++++++++ 3 files changed, 15 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress0/preprocess/proj-issue309-circuit-prop-ite.smt2 diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index 71fb2a56f..e462414d1 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -382,10 +382,11 @@ std::shared_ptr ProofCircuitPropagatorBackward::iteC(bool c) d_parent[0], !c); } - return mkResolution(mkProof(c ? PfRule::NOT_ITE_ELIM1 : PfRule::NOT_ITE_ELIM2, - {assume(d_parent.notNode())}), - d_parent[0], - !c); + return mkNot( + mkResolution(mkProof(c ? PfRule::NOT_ITE_ELIM1 : PfRule::NOT_ITE_ELIM2, + {assume(d_parent.notNode())}), + d_parent[0], + !c)); } std::shared_ptr ProofCircuitPropagatorBackward::iteIsCase(unsigned c) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1c81316c3..ab449dc13 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -839,6 +839,7 @@ set(regress_0_tests regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2 regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2 regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2 + regress0/preprocess/proj-issue309-circuit-prop-ite.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-issue309-circuit-prop-ite.smt2 b/test/regress/regress0/preprocess/proj-issue309-circuit-prop-ite.smt2 new file mode 100644 index 000000000..09626896d --- /dev/null +++ b/test/regress/regress0/preprocess/proj-issue309-circuit-prop-ite.smt2 @@ -0,0 +1,9 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :check-proofs true) +(declare-fun a () Bool) +(declare-fun c () Bool) +(declare-fun d () Bool) +(assert (not a)) +(assert (not (ite a d (not c)))) +(check-sat) -- 2.30.2