From 9e1e48ad560408667f6972979c6123ebc7b615d2 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 28 Oct 2021 15:03:07 -0700 Subject: [PATCH] Fix proof for xor in circuit propagator (#7525) This PR fixes another double negation issue in the circuit propagator. Fixes cvc5/cvc5-projects#332. --- src/theory/booleans/proof_circuit_propagator.cpp | 10 +++++----- test/regress/CMakeLists.txt | 1 + .../preprocess/proj-issue332-circuit-prop-xor.smt2 | 9 +++++++++ 3 files changed, 15 insertions(+), 5 deletions(-) create mode 100644 test/regress/regress0/preprocess/proj-issue332-circuit-prop-xor.smt2 diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index e462414d1..1ec8f7b67 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -206,11 +206,11 @@ std::shared_ptr ProofCircuitPropagator::xorXFromY(bool negated, parent[1], false)); } - return mkResolution( - mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM1, - {assume(negated ? parent.notNode() : Node(parent))}), - parent[1], - true); + return mkNot( + mkResolution(mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM1, + {assume(negated ? parent.notNode() : Node(parent))}), + parent[1], + true)); } std::shared_ptr ProofCircuitPropagator::xorYFromX(bool negated, diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 2430eb13f..8b8a6a926 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -846,6 +846,7 @@ set(regress_0_tests 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/preprocess/proj-issue332-circuit-prop-xor.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-issue332-circuit-prop-xor.smt2 b/test/regress/regress0/preprocess/proj-issue332-circuit-prop-xor.smt2 new file mode 100644 index 000000000..841e7392b --- /dev/null +++ b/test/regress/regress0/preprocess/proj-issue332-circuit-prop-xor.smt2 @@ -0,0 +1,9 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :check-proofs true) +(declare-const x Real) +(declare-const x4 Real) +(declare-const x8 Bool) +(assert (<= x4 x)) +(assert (not (xor (> x4 x) x8))) +(check-sat) -- 2.30.2