From 109f17375661cc29f8125d289c4a776514c23e33 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 21 Oct 2021 09:48:47 -0700 Subject: [PATCH] Add regression (#7447) This PR fixes a proof for an xor term that failed to eliminate a double negation. Fixes cvc5/cvc5-projects#304 --- src/theory/booleans/proof_circuit_propagator.cpp | 4 ++-- test/regress/CMakeLists.txt | 1 + .../preprocess/proj-issue304-circuit-prop-xor.smt2 | 8 ++++++++ 3 files changed, 11 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/preprocess/proj-issue304-circuit-prop-xor.smt2 diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index 0ddfb741d..3b1e40667 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -223,11 +223,11 @@ std::shared_ptr ProofCircuitPropagator::xorYFromX(bool negated, } if (x) { - return mkResolution( + return mkNot(mkResolution( mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM2, {assume(negated ? parent.notNode() : Node(parent))}), parent[0], - false); + false)); } return mkNot( mkResolution(mkProof(negated ? PfRule::NOT_XOR_ELIM1 : PfRule::XOR_ELIM1, diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index eda397da0..8ef4ed362 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -834,6 +834,7 @@ set(regress_0_tests regress0/preprocess/preprocess_13.cvc.smt2 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/print_define_fun_internal.smt2 regress0/print_lambda.cvc.smt2 diff --git a/test/regress/regress0/preprocess/proj-issue304-circuit-prop-xor.smt2 b/test/regress/regress0/preprocess/proj-issue304-circuit-prop-xor.smt2 new file mode 100644 index 000000000..9e4bd285c --- /dev/null +++ b/test/regress/regress0/preprocess/proj-issue304-circuit-prop-xor.smt2 @@ -0,0 +1,8 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :check-proofs true) +(declare-const a Bool) +(declare-const b Bool) +(assert b) +(assert (xor b (not a))) +(check-sat) -- 2.30.2