This PR replaces the LazyCDProofSet, that was hardcoded to use LazyCDProof objects, by a templated CDProofSet.
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
proof_node_updater.h
proof_rule.cpp
proof_rule.h
+ proof_set.h
proof_step_buffer.cpp
proof_step_buffer.h
skolem_manager.cpp
+++ /dev/null
-/********************* */
-/*! \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<LazyCDProof> pf = std::make_shared<LazyCDProof>(
- d_pnm, nullptr, isCd ? d_contextUse : nullptr, ss.str());
- d_pfs.push_back(pf);
- return pf.get();
-}
-
-} // namespace CVC4
+++ /dev/null
-/********************* */
-/*! \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 <memory>
-
-#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<std::shared_ptr<LazyCDProof> > d_pfs;
- /** The name prefix of the lazy proofs */
- std::string d_namePrefix;
-};
-
-} // namespace CVC4
-
-#endif /* CVC4__EXPR__LAZY_PROOF_SET_H */
--- /dev/null
+/********************* */
+/*! \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 <memory>
+
+#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 <typename T>
+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 <typename... Args>
+ T* allocateProof(Args&&... args)
+ {
+ d_proofs.push_back(std::make_shared<T>(
+ d_pnm,
+ std::forward<Args>(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<std::shared_ptr<T>> d_proofs;
+ /** The name prefix of the lazy proofs */
+ std::string d_namePrefix;
+};
+
+} // namespace CVC4
+
+#endif /* CVC4__EXPR__LAZY_PROOF_SET_H */
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),
LazyCDProof* PreprocessProofGenerator::allocateHelperProof()
{
- return d_helperProofs.allocateProof();
+ return d_helperProofs.allocateProof(nullptr, d_ctx);
}
std::string PreprocessProofGenerator::identify() const { return d_name; }
#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"
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
*/
NodeTrustNodeMap d_src;
/** A context-dependent list of LazyCDProof, allocated for conjoin steps */
- LazyCDProofSet d_helperProofs;
+ CDProofSet<LazyCDProof> d_helperProofs;
/**
* A cd proof for input assertions, this is an empty proof that intentionally
* returns (ASSUME f) for all f.
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),
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);
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, {}))
{
#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"
* 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 */
/**
* A context-dependent list of LazyCDProof, allocated for internal steps.
*/
- LazyCDProofSet d_helperPf;
+ CDProofSet<LazyCDProof> d_helperPf;
/**
* The formula corresponding to the current substitution. This is of the form
* (and (= x1 t1) ... (= xn tn))
projects / cvc5.git / commitdiff