From 007e93702d91c02954180cd601741aa19bf2a127 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 30 Aug 2021 15:44:32 -0500 Subject: [PATCH] Fix proof equality engine for "no-explain" premises (#7079) There was an inconsistency between when the equality engine would explain a literal and when we would provide a proof for it. This led to rare cases where we over zealously provided a proof for a fact that should have been an assumption in the theory lemma proof. This corrects the issue by ensuring that no-explain premises are explicitly marked via a new helper proof generator "AssumptionProofGenerator" which always supplies (ASSUME f) as the proof for f. This corrects some proof checking errors on string benchmarks. --- src/CMakeLists.txt | 2 + src/proof/assumption_proof_generator.cpp | 36 +++++++++++++++ src/proof/assumption_proof_generator.h | 46 +++++++++++++++++++ src/theory/uf/proof_equality_engine.cpp | 7 ++- src/theory/uf/proof_equality_engine.h | 3 ++ test/regress/CMakeLists.txt | 2 + .../regress1/strings/instance3303-delta.smt2 | 6 +++ .../regress1/strings/instance7075-delta.smt2 | 6 +++ 8 files changed, 106 insertions(+), 2 deletions(-) create mode 100644 src/proof/assumption_proof_generator.cpp create mode 100644 src/proof/assumption_proof_generator.h create mode 100644 test/regress/regress1/strings/instance3303-delta.smt2 create mode 100644 test/regress/regress1/strings/instance7075-delta.smt2 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 306420a2c..4bce6f0d2 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -159,6 +159,8 @@ libcvc5_add_sources( printer/smt2/smt2_printer.h printer/tptp/tptp_printer.cpp printer/tptp/tptp_printer.h + proof/assumption_proof_generator.cpp + proof/assumption_proof_generator.h proof/buffered_proof_generator.cpp proof/buffered_proof_generator.h proof/conv_proof_generator.cpp diff --git a/src/proof/assumption_proof_generator.cpp b/src/proof/assumption_proof_generator.cpp new file mode 100644 index 000000000..84adb676e --- /dev/null +++ b/src/proof/assumption_proof_generator.cpp @@ -0,0 +1,36 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The assumption proof generator class. + */ + +#include "proof/assumption_proof_generator.h" + +#include "proof/proof_node_manager.h" + +namespace cvc5 { + +AssumptionProofGenerator::AssumptionProofGenerator(ProofNodeManager* pnm) + : d_pnm(pnm) +{ +} + +std::shared_ptr AssumptionProofGenerator::getProofFor(Node f) +{ + return d_pnm->mkAssume(f); +} +std::string AssumptionProofGenerator::identify() const +{ + return "AssumptionProofGenerator"; +} + +} // namespace cvc5 diff --git a/src/proof/assumption_proof_generator.h b/src/proof/assumption_proof_generator.h new file mode 100644 index 000000000..218e5ffc0 --- /dev/null +++ b/src/proof/assumption_proof_generator.h @@ -0,0 +1,46 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The assumption proof generator class. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__ASSUMPTION_PROOF_GENERATOR_H +#define CVC5__PROOF__ASSUMPTION_PROOF_GENERATOR_H + +#include "proof/proof_generator.h" + +namespace cvc5 { + +class ProofNodeManager; + +/** + * A proof generator which always returns (ASSUME f) for getProofFor(f). + */ +class AssumptionProofGenerator : public ProofGenerator +{ + public: + AssumptionProofGenerator(ProofNodeManager* pnm); + /** Get the proof for formula f */ + std::shared_ptr getProofFor(Node f) override; + /** Identify this generator (for debugging, etc..) */ + std::string identify() const override; + + private: + /** The proof manager, used for allocating new ProofNode objects */ + ProofNodeManager* d_pnm; +}; + +} // namespace cvc5 + +#endif /* CVC5__PROOF__ASSUMPTION_PROOF_GENERATOR_H */ diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index b4522d9df..ca8b3f740 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -36,6 +36,7 @@ ProofEqEngine::ProofEqEngine(context::Context* c, : EagerProofGenerator(pnm, u, "pfee::" + ee.identify()), d_ee(ee), d_factPg(c, pnm), + d_assumpPg(pnm), d_pnm(pnm), d_proof(pnm, nullptr, c, "pfee::LazyCDProof::" + ee.identify()), d_keep(c) @@ -225,7 +226,7 @@ TrustNode ProofEqEngine::assertLemma(Node conc, LazyCDProof* curr; TrustNodeKind tnk; // same policy as above: for conflicts, use existing lazy proof - if (conc == d_false) + if (conc == d_false && noExplain.empty()) { curr = &d_proof; tnk = TrustNodeKind::CONFLICT; @@ -264,7 +265,7 @@ TrustNode ProofEqEngine::assertLemma(Node conc, LazyCDProof* curr; TrustNodeKind tnk; // same policy as above: for conflicts, use existing lazy proof - if (conc == d_false) + if (conc == d_false && noExplain.empty()) { curr = &d_proof; tnk = TrustNodeKind::CONFLICT; @@ -314,6 +315,8 @@ void ProofEqEngine::explainVecWithProof(TrustNodeKind& tnk, assumps.push_back(e); // it is not a conflict, since it may involve new literals tnk = TrustNodeKind::LEMMA; + // ensure this is an assumption + curr->addLazyStep(e, &d_assumpPg); } } } diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 0c093d4b2..baf155dac 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -23,6 +23,7 @@ #include "context/cdhashmap.h" #include "context/cdhashset.h" #include "expr/node.h" +#include "proof/assumption_proof_generator.h" #include "proof/buffered_proof_generator.h" #include "proof/eager_proof_generator.h" #include "proof/lazy_proof.h" @@ -278,6 +279,8 @@ class ProofEqEngine : public EagerProofGenerator eq::EqualityEngine& d_ee; /** The default proof generator (for simple facts) */ BufferedProofGenerator d_factPg; + /** The no-explain proof generator */ + AssumptionProofGenerator d_assumpPg; /** common nodes */ Node d_true; Node d_false; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index dca8860fd..0d8ec19dc 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2131,6 +2131,8 @@ set(regress_1_tests regress1/strings/idof-neg-index.smt2 regress1/strings/idof-triv.smt2 regress1/strings/ilc-l-nt.smt2 + regress1/strings/instance3303-delta.smt2 + regress1/strings/instance7075-delta.smt2 regress1/strings/issue1105.smt2 regress1/strings/issue1684-regex.smt2 regress1/strings/issue2060.smt2 diff --git a/test/regress/regress1/strings/instance3303-delta.smt2 b/test/regress/regress1/strings/instance3303-delta.smt2 new file mode 100644 index 000000000..b42974774 --- /dev/null +++ b/test/regress/regress1/strings/instance3303-delta.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_S) +(set-info :status unsat) +(declare-const X String) +(assert (str.in_re X (re.++ (re.range "1" "9") ((_ re.loop 0 2) (re.range "0" "9")) (str.to_re "}")))) +(assert (not (str.in_re X (re.++ (re.union (re.range "0" "9") (re.++ (re.range "1" "9") (re.range "0" "9")) (re.++ (re.range "1" "9") (re.range "0" "9") (re.range "0" "9"))) (str.to_re "}"))))) +(check-sat) diff --git a/test/regress/regress1/strings/instance7075-delta.smt2 b/test/regress/regress1/strings/instance7075-delta.smt2 new file mode 100644 index 000000000..54cd2cd9c --- /dev/null +++ b/test/regress/regress1/strings/instance7075-delta.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_S) +(set-info :status sat) +(declare-const X String) +(assert (not (str.in_re X (re.++ (re.range "0" "9") ((_ re.loop 1 2) (re.range "0" "9")))))) +(assert (str.in_re X (re.union (re.++ (re.range "0" "9") ((_ re.loop 1 6) (re.range "0" "9"))) (str.to_re "")))) +(check-sat) -- 2.30.2