From 20007b739555fe27a6600fcb4d156173bcc0eee3 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 20 Nov 2020 20:04:37 +0100 Subject: [PATCH] (proof-new) Replace LazyCDProofSet by generic CDProofSet (#5487) This PR replaces the LazyCDProofSet, that was hardcoded to use LazyCDProof objects, by a templated CDProofSet. --- src/expr/CMakeLists.txt | 3 +- src/expr/lazy_proof_set.cpp | 39 -------------- src/expr/lazy_proof_set.h | 67 ----------------------- src/expr/proof_set.h | 75 ++++++++++++++++++++++++++ src/smt/preprocess_proof_generator.cpp | 7 +-- src/smt/preprocess_proof_generator.h | 6 ++- src/theory/trust_substitutions.cpp | 7 +-- src/theory/trust_substitutions.h | 6 ++- 8 files changed, 92 insertions(+), 118 deletions(-) delete mode 100644 src/expr/lazy_proof_set.cpp delete mode 100644 src/expr/lazy_proof_set.h create mode 100644 src/expr/proof_set.h diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 430303f6b..18de83e90 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -32,8 +32,6 @@ libcvc4_add_sources( lazy_proof.h lazy_proof_chain.cpp lazy_proof_chain.h - lazy_proof_set.cpp - lazy_proof_set.h match_trie.cpp match_trie.h node.cpp @@ -72,6 +70,7 @@ libcvc4_add_sources( proof_node_updater.h proof_rule.cpp proof_rule.h + proof_set.h proof_step_buffer.cpp proof_step_buffer.h skolem_manager.cpp diff --git a/src/expr/lazy_proof_set.cpp b/src/expr/lazy_proof_set.cpp deleted file mode 100644 index be6abbbc9..000000000 --- a/src/expr/lazy_proof_set.cpp +++ /dev/null @@ -1,39 +0,0 @@ -/********************* */ -/*! \file lazy_proof_set.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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.\endverbatim - ** - ** \brief Lazy proof set utility - **/ - -#include "expr/lazy_proof_set.h" - -namespace CVC4 { - -LazyCDProofSet::LazyCDProofSet(ProofNodeManager* pnm, - context::Context* c, - std::string namePrefix) - : d_pnm(pnm), - d_contextUse(c ? c : &d_context), - d_pfs(d_contextUse), - d_namePrefix(namePrefix) -{ -} - -LazyCDProof* LazyCDProofSet::allocateProof(bool isCd) -{ - std::stringstream ss; - ss << d_namePrefix << "_" << d_pfs.size(); - std::shared_ptr pf = std::make_shared( - d_pnm, nullptr, isCd ? d_contextUse : nullptr, ss.str()); - d_pfs.push_back(pf); - return pf.get(); -} - -} // namespace CVC4 diff --git a/src/expr/lazy_proof_set.h b/src/expr/lazy_proof_set.h deleted file mode 100644 index 3501aabb5..000000000 --- a/src/expr/lazy_proof_set.h +++ /dev/null @@ -1,67 +0,0 @@ -/********************* */ -/*! \file lazy_proof_set.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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.\endverbatim - ** - ** \brief Lazy proof set utility - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__EXPR__LAZY_PROOF_SET_H -#define CVC4__EXPR__LAZY_PROOF_SET_H - -#include - -#include "context/cdlist.h" -#include "context/context.h" -#include "expr/lazy_proof.h" - -namespace CVC4 { - -/** - * A (context-dependent) set of lazy proofs, which is used for memory - * management purposes. - */ -class LazyCDProofSet -{ - public: - LazyCDProofSet(ProofNodeManager* pnm, - context::Context* c = nullptr, - std::string namePrefix = "LazyCDProof"); - ~LazyCDProofSet() {} - /** - * Allocate a lazy proof. This returns a fresh lazy proof object that - * remains alive in the context given to this class. Internally, this adds a - * LazyCDProof to the list d_pfs below. - * - * @param isCd Whether the proof is context-dependent (using the same context - * that is provided to this class). - */ - LazyCDProof* allocateProof(bool isCd = false); - - protected: - /** The proof node manager */ - ProofNodeManager* d_pnm; - /** A dummy context used by this class if none is provided */ - context::Context d_context; - /** - * The context we are using (either the one provided in the constructor or - * d_context). - */ - context::Context* d_contextUse; - /** A context-dependent list of lazy proofs. */ - context::CDList > d_pfs; - /** The name prefix of the lazy proofs */ - std::string d_namePrefix; -}; - -} // namespace CVC4 - -#endif /* CVC4__EXPR__LAZY_PROOF_SET_H */ diff --git a/src/expr/proof_set.h b/src/expr/proof_set.h new file mode 100644 index 000000000..20ef67efe --- /dev/null +++ b/src/expr/proof_set.h @@ -0,0 +1,75 @@ +/********************* */ +/*! \file proof_set.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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.\endverbatim + ** + ** \brief Proof set utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__PROOF_SET_H +#define CVC4__EXPR__PROOF_SET_H + +#include + +#include "context/cdlist.h" +#include "context/context.h" +#include "expr/proof_node_manager.h" + +namespace CVC4 { + +/** + * A (context-dependent) set of proofs, which is used for memory + * management purposes. + */ +template +class CDProofSet +{ + public: + CDProofSet(ProofNodeManager* pnm, + context::Context* c, + std::string namePrefix = "Proof") + : d_pnm(pnm), d_proofs(c), d_namePrefix(namePrefix) + { + } + /** + * Allocate a new proof. + * + * This returns a fresh proof object that remains alive in the context given + * to this class. Internally, this adds a new proof of type T to a + * context-dependent list of proofs and passes the following arguments to the + * T constructor: + * pnm, args..., name + * where pnm is the proof node manager + * provided to this proof set upon construction, args... are the arguments to + * allocateProof() and name is the namePrefix with an appended index. + */ + template + T* allocateProof(Args&&... args) + { + d_proofs.push_back(std::make_shared( + d_pnm, + std::forward(args)..., + d_namePrefix + "_" + std::to_string(d_proofs.size()))); + return d_proofs.back().get(); + } + + protected: + /** The proof node manager */ + ProofNodeManager* d_pnm; + /** A context-dependent list of lazy proofs. */ + context::CDList> d_proofs; + /** The name prefix of the lazy proofs */ + std::string d_namePrefix; +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__LAZY_PROOF_SET_H */ diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 465e7a471..bab56a0d2 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -28,8 +28,9 @@ PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm, PfRule ra, PfRule rpp) : d_pnm(pnm), - d_src(c ? c : &d_context), - d_helperProofs(pnm, c ? c : &d_context), + d_ctx(c ? c : &d_context), + d_src(d_ctx), + d_helperProofs(pnm, d_ctx), d_inputPf(pnm, nullptr), d_name(name), d_ra(ra), @@ -227,7 +228,7 @@ ProofNodeManager* PreprocessProofGenerator::getManager() { return d_pnm; } LazyCDProof* PreprocessProofGenerator::allocateHelperProof() { - return d_helperProofs.allocateProof(); + return d_helperProofs.allocateProof(nullptr, d_ctx); } std::string PreprocessProofGenerator::identify() const { return d_name; } diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h index a0c090ad7..41add5583 100644 --- a/src/smt/preprocess_proof_generator.h +++ b/src/smt/preprocess_proof_generator.h @@ -22,7 +22,7 @@ #include "context/cdhashmap.h" #include "context/cdlist.h" #include "expr/lazy_proof.h" -#include "expr/lazy_proof_set.h" +#include "expr/proof_set.h" #include "expr/proof_generator.h" #include "expr/proof_node_manager.h" #include "theory/eager_proof_generator.h" @@ -118,6 +118,8 @@ class PreprocessProofGenerator : public ProofGenerator ProofNodeManager* d_pnm; /** A dummy context used by this class if none is provided */ context::Context d_context; + /** The context used here */ + context::Context* d_ctx; /** * The trust node that was the source of each node constructed during * preprocessing. For each n, d_src[n] is a trust node whose node is n. This @@ -127,7 +129,7 @@ class PreprocessProofGenerator : public ProofGenerator */ NodeTrustNodeMap d_src; /** A context-dependent list of LazyCDProof, allocated for conjoin steps */ - LazyCDProofSet d_helperProofs; + CDProofSet d_helperProofs; /** * A cd proof for input assertions, this is an empty proof that intentionally * returns (ASSUME f) for all f. diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp index 27159f964..aaa3b44f7 100644 --- a/src/theory/trust_substitutions.cpp +++ b/src/theory/trust_substitutions.cpp @@ -24,7 +24,8 @@ TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c, std::string name, PfRule trustId, MethodId ids) - : d_subs(c), + : d_ctx(c), + d_subs(c), d_pnm(pnm), d_tsubs(c), d_tspb(pnm ? new TheoryProofStepBuffer(pnm->getChecker()) : nullptr), @@ -68,7 +69,7 @@ void TrustSubstitutionMap::addSubstitution(TNode x, addSubstitution(x, t, nullptr); return; } - LazyCDProof* stepPg = d_helperPf.allocateProof(); + LazyCDProof* stepPg = d_helperPf.allocateProof(nullptr, d_ctx); Node eq = x.eqNode(t); stepPg->addStep(eq, id, {}, args); addSubstitution(x, t, stepPg); @@ -99,7 +100,7 @@ ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x, Trace("trust-subs") << "...use generator directly" << std::endl; return tn.getGenerator(); } - LazyCDProof* solvePg = d_helperPf.allocateProof(); + LazyCDProof* solvePg = d_helperPf.allocateProof(nullptr, d_ctx); // Try to transform tn.getProven() to (= x t) here, if necessary if (!d_tspb->applyPredTransform(proven, eq, {})) { diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index d7f48d054..c316f08c5 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -20,8 +20,8 @@ #include "context/cdlist.h" #include "context/context.h" #include "expr/lazy_proof.h" -#include "expr/lazy_proof_set.h" #include "expr/proof_node_manager.h" +#include "expr/proof_set.h" #include "expr/term_conversion_proof_generator.h" #include "theory/eager_proof_generator.h" #include "theory/substitutions.h" @@ -94,6 +94,8 @@ class TrustSubstitutionMap * Moreover, it ensures that d_subsPg has a proof of the returned value. */ Node getCurrentSubstitution(); + /** The context used here */ + context::Context* d_ctx; /** The substitution map */ SubstitutionMap d_subs; /** The proof node manager */ @@ -109,7 +111,7 @@ class TrustSubstitutionMap /** * A context-dependent list of LazyCDProof, allocated for internal steps. */ - LazyCDProofSet d_helperPf; + CDProofSet d_helperPf; /** * The formula corresponding to the current substitution. This is of the form * (and (= x1 t1) ... (= xn tn)) -- 2.30.2