This requires changing many of the proof interfaces to pass Env instead of ProofNodeManager. This is also work towards simplifying the initialization of our proof infrastructure.
Node n = rewrite(geq.andNode(leq));
assertionsToPreprocess->push_back(n);
- TrustSubstitutionMap tnullMap(&fakeContext, nullptr);
+ TrustSubstitutionMap tnullMap(d_env, &fakeContext);
CVC5_UNUSED SubstitutionMap& nullMap = tnullMap.get();
Theory::PPAssertStatus status CVC5_UNUSED; // just for assertions
status = te->solve(tgeq, tnullMap);
NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
: PreprocessingPass(preprocContext, "non-clausal-simp"),
d_statistics(statisticsRegistry()),
- d_pnm(d_env.getProofNodeManager()),
- d_llpg(d_pnm ? new smt::PreprocessProofGenerator(
+ d_llpg(options().smt.produceProofs ? new smt::PreprocessProofGenerator(
d_env, userContext(), "NonClausalSimp::llpg")
- : nullptr),
- d_llra(d_pnm ? new LazyCDProof(
- d_pnm, nullptr, userContext(), "NonClausalSimp::llra")
- : nullptr),
+ : nullptr),
+ d_llra(options().smt.produceProofs ? new LazyCDProof(
+ d_env, nullptr, userContext(), "NonClausalSimp::llra")
+ : nullptr),
d_tsubsList(userContext())
{
}
// constant propagations
std::shared_ptr<TrustSubstitutionMap> constantPropagations =
std::make_shared<TrustSubstitutionMap>(
- u, d_pnm, "NonClausalSimp::cprop", PfRule::PREPROCESS_LEMMA);
+ d_env, u, "NonClausalSimp::cprop", PfRule::PREPROCESS_LEMMA);
SubstitutionMap& cps = constantPropagations->get();
// new substitutions
std::shared_ptr<TrustSubstitutionMap> newSubstitutions =
std::make_shared<TrustSubstitutionMap>(
- u, d_pnm, "NonClausalSimp::newSubs", PfRule::PREPROCESS_LEMMA);
+ d_env, u, "NonClausalSimp::newSubs", PfRule::PREPROCESS_LEMMA);
SubstitutionMap& nss = newSubstitutions->get();
size_t j = 0;
return PreprocessingPassResult::NO_CONFLICT;
}
-bool NonClausalSimp::isProofEnabled() const { return d_pnm != nullptr; }
+bool NonClausalSimp::isProofEnabled() const
+{
+ return options().smt.produceProofs;
+}
Node NonClausalSimp::processLearnedLit(Node lit,
theory::TrustSubstitutionMap* subs,
Node processRewrittenLearnedLit(TrustNode trn);
/** Is proof enabled? */
bool isProofEnabled() const;
- /** The proof node manager */
- ProofNodeManager* d_pnm;
/** the learned literal preprocess proof generator */
std::unique_ptr<smt::PreprocessProofGenerator> d_llpg;
/**
#include "proof/proof_checker.h"
#include "proof/proof_node_algorithm.h"
#include "proof/proof_node_manager.h"
+#include "smt/env.h"
#include "theory/builtin/proof_checker.h"
#include "util/rational.h"
namespace proof {
AletheProofPostprocessCallback::AletheProofPostprocessCallback(
- ProofNodeManager* pnm, AletheNodeConverter& anc, bool resPivots)
- : d_pnm(pnm), d_anc(anc), d_resPivots(resPivots)
+ Env& env, AletheNodeConverter& anc, bool resPivots)
+ : EnvObj(env), d_anc(anc), d_resPivots(resPivots)
{
NodeManager* nm = NodeManager::currentNM();
d_cl = nm->mkBoundVar("cl", nm->sExprType());
return addAletheStep(rule, res, conclusion, children, args, cdp);
}
-AletheProofPostprocess::AletheProofPostprocess(ProofNodeManager* pnm,
+AletheProofPostprocess::AletheProofPostprocess(Env& env,
AletheNodeConverter& anc,
bool resPivots)
- : d_pnm(pnm), d_cb(d_pnm, anc, resPivots)
+ : EnvObj(env), d_cb(env, anc, resPivots)
{
}
void AletheProofPostprocess::process(std::shared_ptr<ProofNode> pf)
{
// Translate proof node
- ProofNodeUpdater updater(d_pnm, d_cb, false, false);
+ ProofNodeUpdater updater(d_env, d_cb, false, false);
updater.process(pf->getChildren()[0]);
// In the Alethe proof format the final step has to be (cl). However, after
// required.
// The function has the additional purpose of sanitizing the attributes of the
// first SCOPE
- CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", true);
+ CDProof cpf(d_env, nullptr, "ProofNodeUpdater::CDProof", true);
const std::vector<std::shared_ptr<ProofNode>>& cc = pf->getChildren();
std::vector<Node> ccn;
for (const std::shared_ptr<ProofNode>& cp : cc)
// then, update the original proof node based on this one
Trace("pf-process-debug") << "Update node..." << std::endl;
- d_pnm->updateNode(pf.get(), npn.get());
+ d_env.getProofNodeManager()->updateNode(pf.get(), npn.get());
Trace("pf-process-debug") << "...update node finished." << std::endl;
}
}
* A callback class used by the Alethe converter for post-processing proof nodes
* by replacing internal rules by the rules in the Alethe calculus.
*/
-class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback
+class AletheProofPostprocessCallback : protected EnvObj,
+ public ProofNodeUpdaterCallback
{
public:
- AletheProofPostprocessCallback(ProofNodeManager* pnm,
+ AletheProofPostprocessCallback(Env& env,
AletheNodeConverter& anc,
bool resPivots);
~AletheProofPostprocessCallback() {}
CDProof* cdp);
private:
- /** The proof node manager */
- ProofNodeManager* d_pnm;
/** The Alethe node converter */
AletheNodeConverter& d_anc;
/** Whether to keep the pivots in the alguments of the resolution rule */
* The proof postprocessor module. This postprocesses a proof node into one
* using the rules from the Alethe calculus.
*/
-class AletheProofPostprocess
+class AletheProofPostprocess : protected EnvObj
{
public:
- AletheProofPostprocess(ProofNodeManager* pnm,
- AletheNodeConverter& anc,
- bool resPivots);
+ AletheProofPostprocess(Env& env, AletheNodeConverter& anc, bool resPivots);
~AletheProofPostprocess();
/** post-process */
void process(std::shared_ptr<ProofNode> pf);
private:
- /** The proof node manager */
- ProofNodeManager* d_pnm;
/** The post process callback */
AletheProofPostprocessCallback d_cb;
};
namespace cvc5::internal {
-BufferedProofGenerator::BufferedProofGenerator(context::Context* c,
- ProofNodeManager* pnm)
- : ProofGenerator(), d_facts(c), d_pnm(pnm)
+BufferedProofGenerator::BufferedProofGenerator(Env& env, context::Context* c)
+ : EnvObj(env), ProofGenerator(), d_facts(c)
{
}
}
}
Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl;
- CDProof cdp(d_pnm);
+ CDProof cdp(d_env);
cdp.addStep(fact, *(*it).second);
return cdp.getProofFor(fact);
}
#include "context/cdhashmap.h"
#include "proof/proof_generator.h"
+#include "smt/env_obj.h"
namespace cvc5::internal {
* mapping from formulas to proof steps. It does not generate ProofNodes until
* it is asked to provide a proof for a given fact.
*/
-class BufferedProofGenerator : public ProofGenerator
+class BufferedProofGenerator : protected EnvObj, public ProofGenerator
{
typedef context::CDHashMap<Node, std::shared_ptr<ProofStep>> NodeProofStepMap;
public:
- BufferedProofGenerator(context::Context* c, ProofNodeManager* pnm);
+ BufferedProofGenerator(Env& env, context::Context* c);
~BufferedProofGenerator() {}
/** add step
* Unless the overwrite policy is ALWAYS it does not replace previously
private:
/** maps expected to ProofStep */
NodeProofStepMap d_facts;
- /** the proof node manager */
- ProofNodeManager* d_pnm;
};
} // namespace cvc5::internal
return out;
}
-TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm,
+TConvProofGenerator::TConvProofGenerator(Env& env,
context::Context* c,
TConvPolicy pol,
TConvCachePolicy cpol,
std::string name,
TermContext* tccb,
bool rewriteOps)
- : d_proof(pnm, nullptr, c, name + "::LazyCDProof"),
+ : EnvObj(env),
+ d_proof(env, nullptr, c, name + "::LazyCDProof"),
d_preRewriteMap(c ? c : &d_context),
d_postRewriteMap(c ? c : &d_context),
d_policy(pol),
return nullptr;
}
// we use the existing proofs
- LazyCDProof lpf(
- d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProof");
+ LazyCDProof lpf(d_env, &d_proof, nullptr, d_name + "::LazyCDProof");
if (f[0] == f[1])
{
// assertion failure in debug
std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node n)
{
- LazyCDProof lpf(
- d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProofRew");
+ LazyCDProof lpf(d_env, &d_proof, nullptr, d_name + "::LazyCDProofRew");
Node conc = getProofForRewriting(n, lpf, d_tcontext);
if (conc[1] == n)
{
* replayed in the expected way, e.g. the occurrence of (and A B) that is not
* in term position is not rewritten.
*/
-class TConvProofGenerator : public ProofGenerator
+class TConvProofGenerator : protected EnvObj, public ProofGenerator
{
public:
/**
* Constructor, which notice does fixpoint rewriting (since this is the
* most common use case) and never caches.
*
- * @param pnm The proof node manager for constructing ProofNode objects.
+ * @param env Reference to the environment.
* @param c The context that this class depends on. If none is provided,
* this class is context-independent.
* @param tpol The policy for applying rewrite steps of this class. For
* is non-null, then this class stores a term-context-sensitive rewrite
* system. The rewrite steps should be given term context identifiers.
*/
- TConvProofGenerator(ProofNodeManager* pnm,
+ TConvProofGenerator(Env& env,
context::Context* c = nullptr,
TConvPolicy pol = TConvPolicy::FIXPOINT,
TConvCachePolicy cpol = TConvCachePolicy::NEVER,
#include "proof/proof.h"
#include "proof/proof_node.h"
#include "proof/proof_node_manager.h"
+#include "smt/env.h"
namespace cvc5::internal {
-EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm,
+EagerProofGenerator::EagerProofGenerator(Env& env,
context::Context* c,
std::string name)
- : d_pnm(pnm), d_name(name), d_proofs(c == nullptr ? &d_context : c)
+ : EnvObj(env), d_name(name), d_proofs(c == nullptr ? &d_context : c)
{
}
const std::vector<Node>& args,
bool isConflict)
{
+ ProofNodeManager* pnm = d_env.getProofNodeManager();
// if no children, its easy
if (exp.empty())
{
- std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, conc);
+ std::shared_ptr<ProofNode> pf = pnm->mkNode(id, {}, args, conc);
return mkTrustNode(conc, pf, isConflict);
}
// otherwise, we use CDProof + SCOPE
- CDProof cdp(d_pnm);
+ CDProof cdp(d_env);
cdp.addStep(conc, id, exp, args);
std::shared_ptr<ProofNode> pf = cdp.getProofFor(conc);
// We use mkNode instead of mkScope, since there is no reason to check
// whether the free assumptions of pf are in exp, since they are by the
// construction above.
- std::shared_ptr<ProofNode> pfs = d_pnm->mkNode(PfRule::SCOPE, {pf}, exp);
+ std::shared_ptr<ProofNode> pfs = pnm->mkNode(PfRule::SCOPE, {pf}, exp);
return mkTrustNode(pfs->getResult(), pfs, isConflict);
}
const std::vector<Node>& args)
{
Node eq = a.eqNode(b);
- CDProof cdp(d_pnm);
+ CDProof cdp(d_env);
cdp.addStep(eq, id, {}, args);
std::shared_ptr<ProofNode> pf = cdp.getProofFor(eq);
return mkTrustedRewrite(a, b, pf);
#include "proof/proof_generator.h"
#include "proof/proof_rule.h"
#include "proof/trust_node.h"
+#include "smt/env_obj.h"
namespace cvc5::internal {
* storing the proof internally, and the proof output channel is responsible for
* maintaining the map that epg is who to ask for the proof of the conflict.
*/
-class EagerProofGenerator : public ProofGenerator
+class EagerProofGenerator : protected EnvObj, public ProofGenerator
{
typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap;
public:
- EagerProofGenerator(ProofNodeManager* pnm,
+ EagerProofGenerator(Env& env,
context::Context* c = nullptr,
std::string name = "EagerProofGenerator");
~EagerProofGenerator() {}
void setProofForLemma(Node lem, std::shared_ptr<ProofNode> pf);
/** Set that pf is the proof for explained propagation */
void setProofForPropExp(TNode lit, Node exp, std::shared_ptr<ProofNode> pf);
- /** The proof node manager */
- ProofNodeManager* d_pnm;
/** Name identifier */
std::string d_name;
/** A dummy context used by this class if none is provided */
namespace cvc5::internal {
-LazyCDProof::LazyCDProof(ProofNodeManager* pnm,
+LazyCDProof::LazyCDProof(Env& env,
ProofGenerator* dpg,
context::Context* c,
const std::string& name,
bool autoSym,
bool doCache)
- : CDProof(pnm, c, name, autoSym),
+ : CDProof(env, c, name, autoSym),
d_gens(c ? c : &d_context),
d_defaultGen(dpg),
d_doCache(doCache),
{
if (pgc->getRule() == PfRule::SYMM)
{
- d_manager->updateNode(cur, pgc->getChildren()[0].get());
+ getManager()->updateNode(cur, pgc->getChildren()[0].get());
}
else
{
- d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {});
+ getManager()->updateNode(cur, PfRule::SYMM, {pgc}, {});
}
}
else
{
- d_manager->updateNode(cur, pgc.get());
+ getManager()->updateNode(cur, pgc.get());
}
Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for "
<< cfactGen << std::endl;
if (isClosed)
{
Trace("lazy-cdproof-debug") << "Checking closed..." << std::endl;
- pfgEnsureClosed(expected, pg, "lazy-cdproof-debug", ctx);
+ pfgEnsureClosed(options(), expected, pg, "lazy-cdproof-debug", ctx);
}
}
* to getProofFor, even if new steps are provided to this class in the
* meantime.
*/
- LazyCDProof(ProofNodeManager* pnm,
+ LazyCDProof(Env& env,
ProofGenerator* dpg = nullptr,
context::Context* c = nullptr,
const std::string& name = "LazyCDProof",
namespace cvc5::internal {
-LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm,
+LazyCDProofChain::LazyCDProofChain(Env& env,
bool cyclic,
context::Context* c,
ProofGenerator* defGen,
bool defRec,
const std::string& name)
- : CDProof(pnm, c, name, false),
- d_manager(pnm),
+ : CDProof(env, c, name, false),
d_cyclic(cyclic),
d_defRec(defRec),
d_context(),
<< "\n";
}
} while (!visit.empty());
+ ProofNodeManager* pnm = getManager();
// expand all assumptions marked to be connected
for (const std::pair<const Node, std::shared_ptr<ProofNode>>& npfn :
toConnect)
// update each assumption proof node
for (std::shared_ptr<ProofNode> pfn : it->second)
{
- d_manager->updateNode(pfn.get(), npfn.second.get());
+ pnm->updateNode(pfn.get(), npfn.second.get());
}
}
Trace("lazy-cdproofchain") << "===========\n";
}
Trace("lazy-cdproofchain") << "\n";
}
- pfnEnsureClosedWrt(pfn.get(), allowedLeaves, "lazy-cdproofchain", ctx);
+ pfnEnsureClosedWrt(
+ options(), pfn.get(), allowedLeaves, "lazy-cdproofchain", ctx);
}
}
public:
/** Constructor
*
- * @param pnm The proof node manager for constructing ProofNode objects.
+ * @param env Reference to the environment
* @param cyclic Whether this instance is robust to cycles in the chain.
* @param c The context that this class depends on. If none is provided,
* this class is context-independent.
* for a step.
* @param defRec Whether this instance expands proofs from defGen recursively.
*/
- LazyCDProofChain(ProofNodeManager* pnm,
+ LazyCDProofChain(Env& env,
bool cyclic = true,
context::Context* c = nullptr,
ProofGenerator* defGen = nullptr,
* Returns a nullptr when no internal proof stored.
*/
std::shared_ptr<ProofNode> getProofForInternal(Node fact, bool& rec);
-
- /** The proof manager, used for allocating new ProofNode objects */
- ProofNodeManager* d_manager;
/** Whether this instance is robust to cycles in the chain. */
bool d_cyclic;
/** Whether we expand recursively (for the default generator) */
#include "proof/proof_generator.h"
#include "proof/proof_node.h"
#include "proof/proof_node_manager.h"
+#include "smt/env.h"
namespace cvc5::internal {
-LazyTreeProofGenerator::LazyTreeProofGenerator(ProofNodeManager* pnm,
+LazyTreeProofGenerator::LazyTreeProofGenerator(Env& env,
const std::string& name)
- : d_pnm(pnm), d_name(name)
+ : EnvObj(env), d_name(name)
{
d_stack.emplace_back(&d_proof);
}
std::vector<std::shared_ptr<ProofNode>>& scope,
const detail::TreeProofNode& pn) const
{
+ ProofNodeManager* pnm = d_env.getProofNodeManager();
// Store scope size to reset scope afterwards
std::size_t before = scope.size();
std::vector<std::shared_ptr<ProofNode>> children;
{
for (const auto& a : pn.d_args)
{
- scope.emplace_back(d_pnm->mkAssume(a));
+ scope.emplace_back(pnm->mkAssume(a));
}
}
}
for (const auto& p : pn.d_premise)
{
// Add premises as assumptions
- children.emplace_back(d_pnm->mkAssume(p));
+ children.emplace_back(pnm->mkAssume(p));
}
// Reset scope
scope.resize(before);
- return d_pnm->mkNode(pn.d_rule, children, pn.d_args);
+ return pnm->mkNode(pn.d_rule, children, pn.d_args);
}
void LazyTreeProofGenerator::print(std::ostream& os,
#include "expr/node.h"
#include "proof/proof_generator.h"
#include "proof/proof_node_manager.h"
+#include "smt/env_obj.h"
namespace cvc5::internal {
namespace detail {
* To explicitly finish proof construction, we need to call closeChild() one
* additional time.
*/
-class LazyTreeProofGenerator : public ProofGenerator
+class LazyTreeProofGenerator : protected EnvObj, public ProofGenerator
{
public:
friend std::ostream& operator<<(std::ostream& os,
const LazyTreeProofGenerator& ltpg);
- LazyTreeProofGenerator(ProofNodeManager* pnm,
+ LazyTreeProofGenerator(Env& env,
const std::string& name = "LazyTreeProofGenerator");
std::string identify() const override { return d_name; }
const std::string& prefix,
const detail::TreeProofNode& pn) const;
- /** The ProofNodeManager used for constructing ProofNodes */
- ProofNodeManager* d_pnm;
/** The trace to the current node */
std::vector<detail::TreeProofNode*> d_stack;
/** The root node of the proof tree */
#include "proof/proof_node_algorithm.h"
#include "proof/proof_node_manager.h"
#include "proof/proof_node_updater.h"
+#include "smt/env.h"
#include "theory/strings/theory_strings_utils.h"
using namespace cvc5::internal::kind;
namespace proof {
LfscProofPostprocessCallback::LfscProofPostprocessCallback(
- LfscNodeConverter& ltp, ProofNodeManager* pnm)
- : d_pnm(pnm), d_pc(pnm->getChecker()), d_tproc(ltp), d_firstTime(false)
+ Env& env, LfscNodeConverter& ltp)
+ : EnvObj(env),
+ d_pc(env.getProofNodeManager()->getChecker()),
+ d_tproc(ltp),
+ d_firstTime(false)
{
}
return nm->mkBoundVar(nm->booleanType());
}
-LfscProofPostprocess::LfscProofPostprocess(LfscNodeConverter& ltp,
- ProofNodeManager* pnm)
- : d_cb(new proof::LfscProofPostprocessCallback(ltp, pnm)), d_pnm(pnm)
+LfscProofPostprocess::LfscProofPostprocess(Env& env, LfscNodeConverter& ltp)
+ : EnvObj(env), d_cb(new proof::LfscProofPostprocessCallback(env, ltp))
{
}
d_cb->initializeUpdate();
// do not automatically add symmetry steps, since this leads to
// non-termination for example on policy_variable.smt2
- ProofNodeUpdater updater(d_pnm, *(d_cb.get()), false, false);
+ ProofNodeUpdater updater(d_env, *(d_cb.get()), false, false);
updater.process(pf);
}
#include "proof/lfsc/lfsc_node_converter.h"
#include "proof/lfsc/lfsc_util.h"
#include "proof/proof_node_updater.h"
+#include "smt/env_obj.h"
namespace cvc5::internal {
* A callback class used by the Lfsc convereter for post-processing proof nodes
* by replacing internal rules by the rules in the Lfsc calculus.
*/
-class LfscProofPostprocessCallback : public ProofNodeUpdaterCallback
+class LfscProofPostprocessCallback : protected EnvObj,
+ public ProofNodeUpdaterCallback
{
public:
- LfscProofPostprocessCallback(LfscNodeConverter& ltp, ProofNodeManager* pnm);
+ LfscProofPostprocessCallback(Env& env, LfscNodeConverter& ltp);
/**
* Initialize, called once for each new ProofNode to process. This initializes
* static information to be used by successive calls to update.
bool& continueUpdate) override;
private:
- /** The proof node manager */
- ProofNodeManager* d_pnm;
/** The proof checker of d_pnm **/
ProofChecker* d_pc;
/** The term processor */
* The proof postprocessor module. This postprocesses a proof node into one
* using the rules from the Lfsc calculus.
*/
-class LfscProofPostprocess
+class LfscProofPostprocess : protected EnvObj
{
public:
- LfscProofPostprocess(LfscNodeConverter& ltp, ProofNodeManager* pnm);
+ LfscProofPostprocess(Env& env, LfscNodeConverter& ltp);
/** post-process */
void process(std::shared_ptr<ProofNode> pf);
private:
/** The post process callback */
std::unique_ptr<LfscProofPostprocessCallback> d_cb;
- /** The proof node manager */
- ProofNodeManager* d_pnm;
};
} // namespace proof
#include "proof/proof_checker.h"
#include "proof/proof_node.h"
#include "proof/proof_node_manager.h"
+#include "smt/env.h"
using namespace cvc5::internal::kind;
namespace cvc5::internal {
-CDProof::CDProof(ProofNodeManager* pnm,
+CDProof::CDProof(Env& env,
context::Context* c,
const std::string& name,
bool autoSymm)
- : d_manager(pnm),
+ : EnvObj(env),
d_context(),
d_nodes(c ? c : &d_context),
d_name(name),
// add as assumption
std::vector<Node> pargs = {fact};
std::vector<std::shared_ptr<ProofNode>> passume;
+ ProofNodeManager* pnm = getManager();
std::shared_ptr<ProofNode> pfa =
- d_manager->mkNode(PfRule::ASSUME, passume, pargs, fact);
+ pnm->mkNode(PfRule::ASSUME, passume, pargs, fact);
d_nodes.insert(fact, pfa);
return pfa;
}
std::vector<std::shared_ptr<ProofNode>> pschild;
pschild.push_back(pfs);
std::vector<Node> args;
+ ProofNodeManager* pnm = getManager();
if (pf == nullptr)
{
Trace("cdproof") << "...fresh make symm" << std::endl;
- std::shared_ptr<ProofNode> psym = d_manager->mkSymm(pfs, fact);
+ std::shared_ptr<ProofNode> psym = pnm->mkSymm(pfs, fact);
Assert(psym != nullptr);
d_nodes.insert(fact, psym);
return psym;
// if its not an assumption, make the connection
Trace("cdproof") << "...update symm" << std::endl;
// update pf
- bool sret = d_manager->updateNode(pf.get(), PfRule::SYMM, pschild, args);
+ bool sret = pnm->updateNode(pf.get(), PfRule::SYMM, pschild, args);
AlwaysAssert(sret);
}
}
// we will overwrite the existing proof node by updating its contents below
}
// collect the child proofs, for each premise
+ ProofNodeManager* pnm = getManager();
std::vector<std::shared_ptr<ProofNode>> pchildren;
for (const Node& c : children)
{
// otherwise, we initialize it as an assumption
std::vector<Node> pcargs = {c};
std::vector<std::shared_ptr<ProofNode>> pcassume;
- pc = d_manager->mkNode(PfRule::ASSUME, pcassume, pcargs, c);
+ pc = pnm->mkNode(PfRule::ASSUME, pcassume, pcargs, c);
// assumptions never fail to check
Assert(pc != nullptr);
d_nodes.insert(c, pc);
if (pprev == nullptr)
{
Trace("cdproof") << " new node " << expected << "..." << std::endl;
- pthis = d_manager->mkNode(id, pchildren, args, expected);
+ pthis = pnm->mkNode(id, pchildren, args, expected);
if (pthis == nullptr)
{
// failed to construct the node, perhaps due to a proof checking failure
// We return the value of updateNode here. This means this method may return
// false if this call failed, regardless of whether we already have a proof
// step for expected.
- ret = d_manager->updateNode(pthis.get(), id, pchildren, args);
+ ret = pnm->updateNode(pthis.get(), id, pchildren, args);
}
if (ret)
{
// checker than the one of the manager in this class, then it is double
// checked here, so that this class maintains the invariant that all of
// its nodes in d_nodes have been checked by the underlying checker.
- Assert(d_manager->getChecker() == nullptr
- || d_manager->getChecker()->check(pn.get(), curFact) == curFact);
+ Assert(getManager()->getChecker() == nullptr
+ || getManager()->getChecker()->check(pn.get(), curFact)
+ == curFact);
// just store the proof for fact
d_nodes.insert(curFact, pn);
}
// We update cur to have the structure of the top node of pn. Notice that
// the interface to update this node will ensure that the proof apf is a
// proof of the assumption. If it does not, then pn was wrong.
- if (!d_manager->updateNode(
+ if (!getManager()->updateNode(
cur.get(), pn->getRule(), pn->getChildren(), pn->getArguments()))
{
return false;
size_t CDProof::getNumProofNodes() const { return d_nodes.size(); }
-ProofNodeManager* CDProof::getManager() const { return d_manager; }
+ProofNodeManager* CDProof::getManager() const
+{
+ ProofNodeManager* pnm = d_env.getProofNodeManager();
+ Assert(pnm != nullptr);
+ return pnm;
+}
bool CDProof::shouldOverwrite(ProofNode* pn, PfRule newId, CDPOverwrite opol)
{
#include "expr/node.h"
#include "proof/proof_generator.h"
#include "proof/proof_step_buffer.h"
+#include "smt/env_obj.h"
namespace cvc5::internal {
* of ID_2. More generally, CDProof::isSame(F,G) returns true if F and G are
* essentially the same formula according to this class.
*/
-class CDProof : public ProofGenerator
+class CDProof : protected EnvObj, public ProofGenerator
{
public:
/**
* @param autoSymm Whether this proof automatically adds symmetry steps based
* on policy documented above.
*/
- CDProof(ProofNodeManager* pnm,
+ CDProof(Env& env,
context::Context* c = nullptr,
const std::string& name = "CDProof",
bool autoSymm = true);
protected:
typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap;
- /** The proof manager, used for allocating new ProofNode objects */
- ProofNodeManager* d_manager;
/** A dummy context used by this class if none is provided */
context::Context d_context;
/** The nodes of the proof */
* Ensure closed with respect to assumptions, internal version, which
* generalizes the check for a proof generator or a proof node.
*/
-void ensureClosedWrtInternal(Node proven,
+void ensureClosedWrtInternal(const Options& opts,
+ Node proven,
ProofGenerator* pg,
ProofNode* pnp,
const std::vector<Node>& assumps,
const char* ctx,
bool reqGen)
{
- if (!options::produceProofs())
+ if (!opts.smt.produceProofs)
{
// proofs not enabled, do not do check
return;
}
bool isTraceDebug = TraceIsOn(c);
- if (options::proofCheck() != options::ProofCheckMode::EAGER && !isTraceDebug)
+ if (opts.proof.proofCheck != options::ProofCheckMode::EAGER && !isTraceDebug)
{
// trace is off and proof new eager checking is off, do not do check
return;
Trace(c) << "====" << std::endl;
}
-void pfgEnsureClosed(Node proven,
+void pfgEnsureClosed(const Options& opts,
+ Node proven,
ProofGenerator* pg,
const char* c,
const char* ctx,
Assert(!proven.isNull());
// proof generator may be null
std::vector<Node> assumps;
- ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen);
+ ensureClosedWrtInternal(opts, proven, pg, nullptr, assumps, c, ctx, reqGen);
}
-void pfgEnsureClosedWrt(Node proven,
+void pfgEnsureClosedWrt(const Options& opts,
+ Node proven,
ProofGenerator* pg,
const std::vector<Node>& assumps,
const char* c,
{
Assert(!proven.isNull());
// proof generator may be null
- ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen);
+ ensureClosedWrtInternal(opts, proven, pg, nullptr, assumps, c, ctx, reqGen);
}
-void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx)
+void pfnEnsureClosed(const Options& opts,
+ ProofNode* pn,
+ const char* c,
+ const char* ctx)
{
- ensureClosedWrtInternal(Node::null(), nullptr, pn, {}, c, ctx, false);
+ ensureClosedWrtInternal(opts, Node::null(), nullptr, pn, {}, c, ctx, false);
}
-void pfnEnsureClosedWrt(ProofNode* pn,
+void pfnEnsureClosedWrt(const Options& opts,
+ ProofNode* pn,
const std::vector<Node>& assumps,
const char* c,
const char* ctx)
{
- ensureClosedWrtInternal(Node::null(), nullptr, pn, assumps, c, ctx, false);
+ ensureClosedWrtInternal(
+ opts, Node::null(), nullptr, pn, assumps, c, ctx, false);
}
} // namespace cvc5::internal
namespace cvc5::internal {
+class Options;
class ProofGenerator;
class ProofNode;
*
* @param reqGen Whether we consider a null generator to be a failure.
*/
-void pfgEnsureClosed(Node proven,
+void pfgEnsureClosed(const Options& opts,
+ Node proven,
ProofGenerator* pg,
const char* c,
const char* ctx,
*
* @param reqGen Whether we consider a null generator to be a failure.
*/
-void pfgEnsureClosedWrt(Node proven,
+void pfgEnsureClosedWrt(const Options& opts,
+ Node proven,
ProofGenerator* pg,
const std::vector<Node>& assumps,
const char* c,
* assertion failure if pn is not closed. Detailed information is printed
* on trace c. Context ctx is a string used for debugging.
*/
-void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx);
+void pfnEnsureClosed(const Options& opts,
+ ProofNode* pn,
+ const char* c,
+ const char* ctx);
/**
* Same as above, but throws an assertion failure only if the free assumptions
* of pn are not contained in assumps.
*/
-void pfnEnsureClosedWrt(ProofNode* pn,
+void pfnEnsureClosedWrt(const Options& opts,
+ ProofNode* pn,
const std::vector<Node>& assumps,
const char* c,
const char* ctx);
#include "proof/proof_ensure_closed.h"
#include "proof/proof_node_algorithm.h"
#include "proof/proof_node_manager.h"
+#include "smt/env.h"
namespace cvc5::internal {
return false;
}
-ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm,
+ProofNodeUpdater::ProofNodeUpdater(Env& env,
ProofNodeUpdaterCallback& cb,
bool mergeSubproofs,
bool autoSym)
- : d_pnm(pnm),
+ : EnvObj(env),
d_cb(cb),
d_debugFreeAssumps(false),
d_mergeSubproofs(mergeSubproofs),
visit.push_back(pf);
std::map<Node, std::shared_ptr<ProofNode>>::iterator itc;
Node res;
+ ProofNodeManager* pnm = d_env.getProofNodeManager();
+ Assert(pnm != nullptr);
do
{
cur = visit.back();
{
// already have a proof, merge it into this one
visited[cur] = true;
- d_pnm->updateNode(cur.get(), itc->second.get());
+ pnm->updateNode(cur.get(), itc->second.get());
// does not contain free assumptions since the range of resCache does
// not contain free assumptions
cfaMap[cur.get()] = false;
{
PfRule id = cur->getRule();
// use CDProof to open a scope for which the callback updates
- CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", d_autoSym);
+ CDProof cpf(d_env, nullptr, "ProofNodeUpdater::CDProof", d_autoSym);
const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren();
std::vector<Node> ccn;
for (const std::shared_ptr<ProofNode>& cp : cc)
}
// then, update the original proof node based on this one
Trace("pf-process-debug") << "Update node..." << std::endl;
- d_pnm->updateNode(cur.get(), npn.get());
+ d_env.getProofNodeManager()->updateNode(cur.get(), npn.get());
Trace("pf-process-debug") << "...update node finished." << std::endl;
if (d_debugFreeAssumps)
{
// the proof. We can now debug based on the expected set of free
// assumptions.
Trace("pfnu-debug") << "Ensure updated closed..." << std::endl;
- pfnEnsureClosedWrt(
- npn.get(), fullFa, "pfnu-debug", "ProofNodeUpdater:postupdate");
+ pfnEnsureClosedWrt(options(),
+ npn.get(),
+ fullFa,
+ "pfnu-debug",
+ "ProofNodeUpdater:postupdate");
}
Trace("pf-process-debug") << "..finished" << std::endl;
return true;
resCacheNcWaiting.find(res);
if (itnw != resCacheNcWaiting.end())
{
+ ProofNodeManager* pnm = d_env.getProofNodeManager();
for (std::shared_ptr<ProofNode>& ncp : itnw->second)
{
- d_pnm->updateNode(ncp.get(), cur.get());
+ pnm->updateNode(ncp.get(), cur.get());
}
resCacheNcWaiting.erase(res);
}
// assumptions.
Trace("pfnu-debug") << "Ensure update closed..." << std::endl;
pfnEnsureClosedWrt(
- cur.get(), fa, "pfnu-debug", "ProofNodeUpdater:finalize");
+ options(), cur.get(), fa, "pfnu-debug", "ProofNodeUpdater:finalize");
}
}
#include "expr/node.h"
#include "proof/proof_node.h"
+#include "smt/env_obj.h"
namespace cvc5::internal {
* should be filled in the callback for each ProofNode to update. This update
* process is applied in a *pre-order* traversal.
*/
-class ProofNodeUpdater
+class ProofNodeUpdater : protected EnvObj
{
public:
/**
- * @param pnm The proof node manager we are using
+ * @param env Reference to the environment
* @param cb The callback to apply to each node
* @param mergeSubproofs Whether to automatically merge subproofs within
* the same SCOPE that prove the same fact.
* @param autoSym Whether intermediate CDProof objects passed to updater
* callbacks automatically introduce SYMM steps.
*/
- ProofNodeUpdater(ProofNodeManager* pnm,
+ ProofNodeUpdater(Env& env,
ProofNodeUpdaterCallback& cb,
bool mergeSubproofs = false,
bool autoSym = true);
void setDebugFreeAssumptions(const std::vector<Node>& freeAssumps);
private:
- /** The proof node manager */
- ProofNodeManager* d_pnm;
/** The callback */
ProofNodeUpdaterCallback& d_cb;
/**
#include "context/cdlist.h"
#include "context/context.h"
-#include "proof/proof_node_manager.h"
namespace cvc5::internal {
+class Env;
+
/**
* A (context-dependent) set of proofs, which is used for memory
* management purposes.
class CDProofSet
{
public:
- CDProofSet(ProofNodeManager* pnm,
- context::Context* c,
- std::string namePrefix = "Proof")
- : d_pnm(pnm), d_proofs(c), d_namePrefix(namePrefix)
+ CDProofSet(Env& env, context::Context* c, std::string namePrefix = "Proof")
+ : d_env(env), d_proofs(c), d_namePrefix(namePrefix)
{
}
/**
T* allocateProof(Args&&... args)
{
d_proofs.push_back(std::make_shared<T>(
- d_pnm,
+ d_env,
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;
+ /** Reference to env */
+ Env& d_env;
/** A context-dependent list of lazy proofs. */
context::CDList<std::shared_ptr<T>> d_proofs;
/** The name prefix of the lazy proofs */
Node TrustNode::getRewriteProven(TNode n, Node nr) { return n.eqNode(nr); }
-void TrustNode::debugCheckClosed(const char* c,
+void TrustNode::debugCheckClosed(const Options& opts,
+ const char* c,
const char* ctx,
bool reqNullGen)
{
- pfgEnsureClosed(d_proven, d_gen, c, ctx, reqNullGen);
+ pfgEnsureClosed(opts, d_proven, d_gen, c, ctx, reqNullGen);
}
std::string TrustNode::identifyGenerator() const
namespace cvc5::internal {
+class Options;
class ProofGenerator;
class ProofNode;
*
* @param reqNullGen Whether we consider a null generator to be a failure.
*/
- void debugCheckClosed(const char* c, const char* ctx, bool reqNullGen = true);
+ void debugCheckClosed(const Options& opts,
+ const char* c,
+ const char* ctx,
+ bool reqNullGen = true);
private:
TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g = nullptr);
: EnvObj(env),
d_cnfStream(cnfStream),
d_satPM(satPM),
- d_proof(env.getProofNodeManager(),
- nullptr,
- userContext(),
- "ProofCnfStream::LazyCDProof"),
+ d_proof(env, nullptr, userContext(), "ProofCnfStream::LazyCDProof"),
d_blocked(userContext()),
d_optClausesManager(userContext(), &d_proof, d_optClausesPfs)
{
namespace prop {
ProofPostprocessCallback::ProofPostprocessCallback(
- ProofNodeManager* pnm, ProofCnfStream* proofCnfStream)
- : d_pnm(pnm), d_proofCnfStream(proofCnfStream)
+ Env& env, ProofCnfStream* proofCnfStream)
+ : EnvObj(env), d_proofCnfStream(proofCnfStream)
{
}
return true;
}
-ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
- ProofCnfStream* proofCnfStream)
- : d_cb(pnm, proofCnfStream), d_pnm(pnm)
+ProofPostproccess::ProofPostproccess(Env& env, ProofCnfStream* proofCnfStream)
+ : EnvObj(env), d_cb(env, proofCnfStream)
{
}
// how to process, including how to process assumptions in pf.
d_cb.initializeUpdate();
// now, process
- ProofNodeUpdater updater(d_pnm, d_cb);
+ ProofNodeUpdater updater(d_env, d_cb);
updater.process(pf);
}
#include "proof/proof_node_updater.h"
#include "prop/proof_cnf_stream.h"
+#include "smt/env_obj.h"
namespace cvc5::internal {
* assertions and lemmas, with the CNF transformation of these formulas, while
* expanding the generators of lemmas.
*/
-class ProofPostprocessCallback : public ProofNodeUpdaterCallback
+class ProofPostprocessCallback : protected EnvObj,
+ public ProofNodeUpdaterCallback
{
public:
- ProofPostprocessCallback(ProofNodeManager* pnm,
- ProofCnfStream* proofCnfStream);
+ ProofPostprocessCallback(Env& env, ProofCnfStream* proofCnfStream);
~ProofPostprocessCallback() {}
/**
* Initialize, called once for each new ProofNode to process. This initializes
bool& continueUpdate) override;
private:
- /** The proof node manager */
- ProofNodeManager* d_pnm;
/** The cnf stream proof generator */
ProofCnfStream* d_proofCnfStream;
//---------------------------------reset at the begining of each update
* produced by the SAT solver. Its main task is to connect the refutation's
* assumptions to the CNF transformation proof in ProofCnfStream.
*/
-class ProofPostproccess
+class ProofPostproccess : protected EnvObj
{
public:
- ProofPostproccess(ProofNodeManager* pnm, ProofCnfStream* proofCnfStream);
+ ProofPostproccess(Env& env, ProofCnfStream* proofCnfStream);
~ProofPostproccess();
/** post-process
*
private:
/** The post process callback */
ProofPostprocessCallback d_cb;
- /** The proof node manager */
- ProofNodeManager* d_pnm;
};
} // namespace prop
d_satSolver(nullptr),
d_cnfStream(nullptr),
d_pfCnfStream(nullptr),
- d_theoryLemmaPg(d_env.getProofNodeManager(),
- d_env.getUserContext(),
- "PropEngine::ThLemmaPg"),
+ d_theoryLemmaPg(d_env, d_env.getUserContext(), "PropEngine::ThLemmaPg"),
d_ppm(nullptr),
d_interrupted(false),
d_assumptions(d_env.getUserContext())
*d_cnfStream,
static_cast<MinisatSatSolver*>(d_satSolver)->getProofManager()));
d_ppm.reset(
- new PropPfManager(userContext, pnm, d_satSolver, d_pfCnfStream.get()));
+ new PropPfManager(env, userContext, d_satSolver, d_pfCnfStream.get()));
}
}
{
Assert(tplemma.getGenerator() != nullptr);
// ensure closed, make the proof node eagerly here to debug
- tplemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma");
+ tplemma.debugCheckClosed(
+ options(), "te-proof-debug", "TheoryEngine::lemma");
for (theory::SkolemLemma& lem : ppLemmas)
{
Assert(lem.d_lemma.getGenerator() != nullptr);
- lem.d_lemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_new");
+ lem.d_lemma.debugCheckClosed(
+ options(), "te-proof-debug", "TheoryEngine::lemma_new");
}
}
Assert(options().smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS);
std::vector<Node> core;
getUnsatCore(core);
- CDProof cdp(d_env.getProofNodeManager());
+ CDProof cdp(d_env);
Node fnode = NodeManager::currentNM()->mkConst(false);
cdp.addStep(fnode, PfRule::SAT_REFUTATION, core, {});
return cdp.getProofFor(fnode);
#include "proof/proof_node_algorithm.h"
#include "prop/prop_proof_manager.h"
#include "prop/sat_solver.h"
+#include "smt/env.h"
namespace cvc5::internal {
namespace prop {
-PropPfManager::PropPfManager(context::UserContext* userContext,
- ProofNodeManager* pnm,
+PropPfManager::PropPfManager(Env& env,
+ context::UserContext* userContext,
CDCLTSatSolverInterface* satSolver,
ProofCnfStream* cnfProof)
- : d_pnm(pnm),
- d_pfpp(new ProofPostproccess(pnm, cnfProof)),
+ : EnvObj(env),
+ d_pfpp(new ProofPostproccess(env, cnfProof)),
d_satSolver(satSolver),
d_assertions(userContext)
{
d_assertions.push_back(assertion);
}
std::vector<Node> avec{d_assertions.begin(), d_assertions.end()};
- pfnEnsureClosedWrt(
- conflictProof.get(), avec, "sat-proof", "PropPfManager::checkProof");
+ pfnEnsureClosedWrt(options(),
+ conflictProof.get(),
+ avec,
+ "sat-proof",
+ "PropPfManager::checkProof");
}
std::shared_ptr<ProofNode> PropPfManager::getProof()
#include "proof/proof_node_manager.h"
#include "prop/proof_post_processor.h"
#include "prop/sat_proof_manager.h"
+#include "smt/env_obj.h"
namespace cvc5::internal {
* The expected proof to be built is a refutation proof with preprocessed
* assertions as free assumptions.
*/
-class PropPfManager
+class PropPfManager : protected EnvObj
{
public:
- PropPfManager(context::UserContext* userContext,
- ProofNodeManager* pnm,
+ PropPfManager(Env& env,
+ context::UserContext* userContext,
CDCLTSatSolverInterface* satSolver,
ProofCnfStream* cnfProof);
void checkProof(const context::CDList<Node>& assertions);
private:
- /** A node manager */
- ProofNodeManager* d_pnm;
/** The proof post-processor */
std::unique_ptr<prop::ProofPostproccess> d_pfpp;
/**
: EnvObj(env),
d_solver(solver),
d_cnfStream(cnfStream),
- d_resChains(d_env.getProofNodeManager(), true, userContext()),
- d_resChainPg(userContext(), d_env.getProofNodeManager()),
+ d_resChains(d_env, true, userContext()),
+ d_resChainPg(d_env, userContext()),
d_assumptions(userContext()),
d_conflictLit(undefSatVariable),
d_optResLevels(userContext()),
bool ZeroLevelLearner::getSolved(const Node& lit, Subs& subs)
{
context::Context dummyContext;
- theory::TrustSubstitutionMap subsOut(&dummyContext);
+ theory::TrustSubstitutionMap subsOut(d_env, &dummyContext);
TrustNode tlit = TrustNode::mkTrustLemma(lit);
theory::Theory::PPAssertStatus status = d_theoryEngine->solve(tlit, subsOut);
if (status == theory::Theory::PP_ASSERT_STATUS_SOLVED)
d_rewriter(new theory::Rewriter()),
d_evalRew(nullptr),
d_eval(nullptr),
- d_topLevelSubs(new theory::TrustSubstitutionMap(d_userContext.get())),
+ d_topLevelSubs(nullptr),
d_logic(),
d_statisticsRegistry(std::make_unique<StatisticsRegistry>(*this)),
d_options(),
Env::~Env() {}
-void Env::setProofNodeManager(ProofNodeManager* pnm)
+void Env::finishInit(ProofNodeManager* pnm)
{
- Assert(pnm != nullptr);
- Assert(d_proofNodeManager == nullptr);
- d_proofNodeManager = pnm;
- d_rewriter->setProofNodeManager(pnm);
- d_topLevelSubs->setProofNodeManager(pnm);
+ if (pnm != nullptr)
+ {
+ Assert(d_proofNodeManager == nullptr);
+ d_proofNodeManager = pnm;
+ d_rewriter->finishInit(*this);
+ }
+ d_topLevelSubs.reset(
+ new theory::TrustSubstitutionMap(*this, d_userContext.get()));
}
void Env::shutdown()
/* Private initialization ------------------------------------------------- */
/** Set proof node manager if it exists */
- void setProofNodeManager(ProofNodeManager* pnm);
+ void finishInit(ProofNodeManager* pnm);
/* Private shutdown ------------------------------------------------------- */
/**
// initialize if not done already
if (d_tpg == nullptr)
{
- Assert(d_env.getProofNodeManager() != nullptr);
- d_tpg.reset(new TConvProofGenerator(d_env.getProofNodeManager(),
+ d_tpg.reset(new TConvProofGenerator(d_env,
d_env.getUserContext(),
TConvPolicy::FIXPOINT,
TConvCachePolicy::NEVER,
#include "proof/proof.h"
#include "proof/proof_checker.h"
#include "proof/proof_node.h"
+#include "proof/proof_node_manager.h"
#include "smt/env.h"
#include "theory/quantifiers/extended_rewrite.h"
: EnvObj(env),
d_ctx(c ? c : &d_context),
d_src(d_ctx),
- d_helperProofs(env.getProofNodeManager(), d_ctx),
- d_inputPf(env.getProofNodeManager(), c, "InputProof"),
+ d_helperProofs(env, d_ctx),
+ d_inputPf(env, c, "InputProof"),
d_name(name),
d_ra(ra),
d_rpp(rpp)
return nullptr;
}
// make CDProof to construct the proof below
- CDProof cdp(d_env.getProofNodeManager());
+ CDProof cdp(d_env);
Node curr = f;
std::vector<Node> transChildren;
d_pfpp(nullptr),
d_finalProof(nullptr)
{
- // enable proof support in the environment/rewriter
- d_env.setProofNodeManager(d_pnm.get());
// now construct preprocess proof generator
d_pppg = std::make_unique<PreprocessProofGenerator>(
env, env.getUserContext(), "smt::PreprocessProofGenerator");
{
proof::AletheNodeConverter anc;
proof::AletheProofPostprocess vpfpp(
- d_pnm.get(), anc, options().proof.proofAletheResPivots);
+ d_env, anc, options().proof.proofAletheResPivots);
vpfpp.process(fp);
proof::AletheProofPrinter vpp;
vpp.print(out, fp);
std::vector<Node> assertions;
getAssertions(as, assertions);
proof::LfscNodeConverter ltp;
- proof::LfscProofPostprocess lpp(ltp, d_pnm.get());
+ proof::LfscProofPostprocess lpp(d_env, ltp);
lpp.process(fp);
proof::LfscPrinter lp(ltp);
lp.print(out, assertions, fp.get());
Trace("difficulty-proc") << "Make SAT refutation" << std::endl;
// assume a SAT refutation from all input assertions that were marked
// as having a difficulty
- CDProof cdp(d_pnm.get());
+ CDProof cdp(d_env);
Node fnode = NodeManager::currentNM()->mkConst(false);
cdp.addStep(fnode, PfRule::SAT_REFUTATION, ppAsserts, {});
std::shared_ptr<ProofNode> pf = cdp.getProofFor(fnode);
Assert(fpf->getRule() == PfRule::SAT_REFUTATION);
const std::vector<std::shared_ptr<ProofNode>>& children = fpf->getChildren();
DifficultyPostprocessCallback dpc;
- ProofNodeUpdater dpnu(d_pnm.get(), dpc);
+ ProofNodeUpdater dpnu(d_env, dpc);
Trace("difficulty-proc") << "Compute accumulated difficulty" << std::endl;
// For each child of SAT_REFUTATION, we increment the difficulty on all
// "source" free assumptions (see DifficultyPostprocessCallback) by the
rewriter::RewriteDb* rdb,
bool updateScopedAssumptions)
: EnvObj(env),
- d_pnm(env.getProofNodeManager()),
d_pppg(pppg),
d_wfpm(env),
d_updateScopedAssumptions(updateScopedAssumptions)
std::vector<Node> childrenResArgs;
Node resPlaceHolder;
size_t nextGuardedElimPos = eliminators[0];
+ ProofNodeManager* pnm = d_env.getProofNodeManager();
do
{
size_t start = lastElim + 1;
args.begin() + (2 * end) + 1);
Trace("smt-proof-pp-debug2") << "\tres children: " << childrenRes << "\n";
Trace("smt-proof-pp-debug2") << "\tres args: " << childrenResArgs << "\n";
- resPlaceHolder = d_pnm->getChecker()->checkDebug(PfRule::CHAIN_RESOLUTION,
- childrenRes,
- childrenResArgs,
- Node::null(),
- "");
+ resPlaceHolder = pnm->getChecker()->checkDebug(PfRule::CHAIN_RESOLUTION,
+ childrenRes,
+ childrenResArgs,
+ Node::null(),
+ "");
Trace("smt-proof-pp-debug2")
<< "resPlaceHorder: " << resPlaceHolder << "\n";
Trace("smt-proof-pp-debug2") << "-------\n";
// to be handled by the caller
if (end < children.size() - 1)
{
- lastClause = d_pnm->getChecker()->checkDebug(
+ lastClause = pnm->getChecker()->checkDebug(
PfRule::FACTORING, {resPlaceHolder}, {}, Node::null(), "");
if (!lastClause.isNull())
{
else if (id == PfRule::MACRO_RESOLUTION
|| id == PfRule::MACRO_RESOLUTION_TRUST)
{
+ ProofNodeManager* pnm = d_env.getProofNodeManager();
// first generate the naive chain_resolution
std::vector<Node> chainResArgs{args.begin() + 1, args.end()};
- Node chainConclusion = d_pnm->getChecker()->checkDebug(
+ Node chainConclusion = pnm->getChecker()->checkDebug(
PfRule::CHAIN_RESOLUTION, children, chainResArgs, Node::null(), "");
Trace("smt-proof-pp-debug") << "Original conclusion: " << args[0] << "\n";
Trace("smt-proof-pp-debug")
<< "......updated to " << var << " -> " << ss
<< " based on previous substitution" << std::endl;
// make the proof for the tranitivity step
- std::shared_ptr<CDProof> pf = std::make_shared<CDProof>(d_pnm);
+ std::shared_ptr<CDProof> pf = std::make_shared<CDProof>(d_env);
pfs.push_back(pf);
// prove the updated substitution
- TConvProofGenerator tcg(d_pnm,
+ TConvProofGenerator tcg(d_env,
nullptr,
TConvPolicy::ONCE,
TConvCachePolicy::NEVER,
// should be implied by the substitution now
TConvPolicy tcpolicy = ida == MethodId::SBA_FIXPOINT ? TConvPolicy::FIXPOINT
: TConvPolicy::ONCE;
- TConvProofGenerator tcpg(d_pnm,
+ TConvProofGenerator tcpg(d_env,
nullptr,
tcpolicy,
TConvCachePolicy::NEVER,
Assert(!args.empty());
Node eq = args[0];
Assert(eq.getKind() == EQUAL);
+ ProofNodeManager* pnm = d_env.getProofNodeManager();
// try to replay theory rewrite
// first, check that maybe its just an evaluation step
- ProofChecker* pc = d_pnm->getChecker();
+ ProofChecker* pc = pnm->getChecker();
Node ceval =
pc->checkDebug(PfRule::EVALUATE, {}, {eq[0]}, eq, "smt-proof-pp-debug");
if (!ceval.isNull() && ceval == eq)
Trace("macro::arith") << " args: " << args << std::endl;
}
Assert(args.size() == children.size());
+ ProofNodeManager* pnm = d_env.getProofNodeManager();
NodeManager* nm = NodeManager::currentNM();
- ProofStepBuffer steps{d_pnm->getChecker()};
+ ProofStepBuffer steps{pnm->getChecker()};
// Scale all children, accumulating
std::vector<Node> scaledRels;
}
else if (id == PfRule::BV_BITBLAST)
{
- bv::BBProof bb(d_env, nullptr, d_pnm, true);
+ bv::BBProof bb(d_env, nullptr, true);
Node eq = args[0];
Assert(eq.getKind() == EQUAL);
bb.bbAtom(eq[0]);
: EnvObj(env),
d_cb(env, pppg, rdb, updateScopedAssumptions),
// the update merges subproofs
- d_updater(env.getProofNodeManager(), d_cb, options().proof.proofPpMerge),
+ d_updater(env, d_cb, options().proof.proofPpMerge),
d_finalCb(env),
- d_finalizer(env.getProofNodeManager(), d_finalCb)
+ d_finalizer(env, d_finalCb)
{
}
private:
/** Common constants */
Node d_true;
- /** Pointer to the proof node manager */
- ProofNodeManager* d_pnm;
/** The preprocessing proof generator */
ProofGenerator* d_pppg;
/** The witness form proof generator */
SetDefaults sdefaults(*d_env, d_isInternalSubsolver);
sdefaults.setDefaults(d_env->d_logic, getOptions());
+ ProofNodeManager* pnm = nullptr;
if (d_env->getOptions().smt.produceProofs)
{
// ensure bound variable uses canonical bound variables
d_asserts->enableProofs(pppg);
// enabled proofs in the preprocessor
d_smtSolver->getPreprocessor()->enableProofs(pppg);
+ pnm = d_pfManager->getProofNodeManager();
}
+ // enable proof support in the environment/rewriter
+ d_env->finishInit(pnm);
Trace("smt-debug") << "SolverEngine::finishInit" << std::endl;
d_smtSolver->finishInit();
if (pnm != nullptr)
{
d_tpg.reset(
- new TConvProofGenerator(pnm,
+ new TConvProofGenerator(env,
nullptr,
TConvPolicy::FIXPOINT,
TConvCachePolicy::NEVER,
"RemoveTermFormulas::TConvProofGenerator",
&d_rtfc));
d_tpgi.reset(
- new TConvProofGenerator(pnm,
+ new TConvProofGenerator(env,
nullptr,
TConvPolicy::ONCE,
TConvCachePolicy::NEVER,
"RemoveTermFormulas::TConvProofGenerator"));
d_lp.reset(new LazyCDProof(
- pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof"));
+ env, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof"));
}
}
newLem = TrustNode::mkTrustLemma(newAssertion, d_lp.get());
Trace("rtf-proof-debug") << "Checking closed..." << std::endl;
- newLem.debugCheckClosed("rtf-proof-debug",
- "RemoveTermFormulas::run:new_assert");
+ newLem.debugCheckClosed(
+ options(), "rtf-proof-debug", "RemoveTermFormulas::run:new_assert");
}
// The representation is now the skolem
WitnessFormGenerator::WitnessFormGenerator(Env& env)
: d_rewriter(env.getRewriter()),
- d_tcpg(env.getProofNodeManager(),
+ d_tcpg(env,
nullptr,
TConvPolicy::FIXPOINT,
TConvCachePolicy::NEVER,
"WfGenerator::TConvProofGenerator",
nullptr,
true),
- d_wintroPf(env.getProofNodeManager(),
- nullptr,
- nullptr,
- "WfGenerator::LazyCDProof"),
- d_pskPf(
- env.getProofNodeManager(), nullptr, "WfGenerator::PurifySkolemProof")
+ d_wintroPf(env, nullptr, nullptr, "WfGenerator::LazyCDProof"),
+ d_pskPf(env, nullptr, "WfGenerator::PurifySkolemProof")
{
}
BranchAndBound::BranchAndBound(Env& env,
ArithState& s,
InferenceManager& im,
- PreprocessRewriteEq& ppre,
- ProofNodeManager* pnm)
+ PreprocessRewriteEq& ppre)
: EnvObj(env),
d_astate(s),
d_im(im),
d_ppre(ppre),
- d_pfGen(new EagerProofGenerator(pnm, userContext())),
- d_pnm(pnm)
+ d_pfGen(new EagerProofGenerator(env, userContext()))
{
}
Trace("integers") << "l: " << l << std::endl;
if (proofsEnabled())
{
+ ProofNodeManager* pnm = d_env.getProofNodeManager();
Node less = nm->mkNode(LT, var, nm->mkConstInt(nearest));
Node greater = nm->mkNode(GT, var, nm->mkConstInt(nearest));
// TODO (project #37): justify. Thread proofs through *ensureLiteral*.
Trace("integers::pf") << "literal: " << literal << std::endl;
Trace("integers::pf") << "eq: " << eq << std::endl;
Trace("integers::pf") << "rawEq: " << rawEq << std::endl;
- Pf pfNotLit = d_pnm->mkAssume(literal.negate());
+ Pf pfNotLit = pnm->mkAssume(literal.negate());
// rewrite notLiteral to notRawEq, using teq.
Pf pfNotRawEq =
literal == rawEq
? pfNotLit
- : d_pnm->mkNode(
- PfRule::MACRO_SR_PRED_TRANSFORM,
- {pfNotLit,
- teq.getGenerator()->getProofFor(teq.getProven())},
- {rawEq.negate()});
- Pf pfBot = d_pnm->mkNode(
- PfRule::CONTRA,
- {d_pnm->mkNode(PfRule::ARITH_TRICHOTOMY,
- {d_pnm->mkAssume(less.negate()), pfNotRawEq},
- {greater}),
- d_pnm->mkAssume(greater.negate())},
- {});
+ : pnm->mkNode(
+ PfRule::MACRO_SR_PRED_TRANSFORM,
+ {pfNotLit, teq.getGenerator()->getProofFor(teq.getProven())},
+ {rawEq.negate()});
+ Pf pfBot =
+ pnm->mkNode(PfRule::CONTRA,
+ {pnm->mkNode(PfRule::ARITH_TRICHOTOMY,
+ {pnm->mkAssume(less.negate()), pfNotRawEq},
+ {greater}),
+ pnm->mkAssume(greater.negate())},
+ {});
std::vector<Node> assumptions = {
literal.negate(), less.negate(), greater.negate()};
// Proof of (not (and (not (= v i)) (not (< v i)) (not (> v i))))
- Pf pfNotAnd = d_pnm->mkScope(pfBot, assumptions);
- Pf pfL = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
- {d_pnm->mkNode(PfRule::NOT_AND, {pfNotAnd}, {})},
- {l});
+ Pf pfNotAnd = pnm->mkScope(pfBot, assumptions);
+ Pf pfL = pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
+ {pnm->mkNode(PfRule::NOT_AND, {pfNotAnd}, {})},
+ {l});
lem = d_pfGen->mkTrustNode(l, pfL);
}
else
return lem;
}
-bool BranchAndBound::proofsEnabled() const { return d_pnm != nullptr; }
+bool BranchAndBound::proofsEnabled() const
+{
+ return d_env.isTheoryProofProducing();
+}
} // namespace arith
} // namespace theory
BranchAndBound(Env& env,
ArithState& s,
InferenceManager& im,
- PreprocessRewriteEq& ppre,
- ProofNodeManager* pnm);
+ PreprocessRewriteEq& ppre);
~BranchAndBound() {}
/**
* Branch variable, called when integer var has given value
PreprocessRewriteEq& d_ppre;
/** Proof generator. */
std::unique_ptr<EagerProofGenerator> d_pfGen;
- /** Proof node manager */
- ProofNodeManager* d_pnm;
};
} // namespace arith
// Construct d_pfGenEe with the SAT context, since its proof include
// unclosed assumptions of theory literals.
d_pfGenEe(new EagerProofGenerator(
- d_pnm, context(), "ArithCongruenceManager::pfGenEe")),
+ d_env, context(), "ArithCongruenceManager::pfGenEe")),
// Construct d_pfGenEe with the USER context, since its proofs are closed.
d_pfGenExplain(new EagerProofGenerator(
- d_pnm, userContext(), "ArithCongruenceManager::pfGenExplain")),
+ d_env, userContext(), "ArithCongruenceManager::pfGenExplain")),
d_pfee(nullptr)
{
}
d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
: nullptr),
d_checker(),
- d_pfGen(new EagerProofGenerator(d_pnm, userContext())),
+ d_pfGen(new EagerProofGenerator(env, userContext())),
d_constraintDatabase(d_env,
d_partialModel,
d_congruenceManager,
{
if (d_env.isTheoryProofProducing())
{
- d_proof.reset(
- new CoveringsProofGenerator(userContext(), d_env.getProofNodeManager()));
+ d_proof.reset(new CoveringsProofGenerator(env, userContext()));
}
}
} // namespace
-CoveringsProofGenerator::CoveringsProofGenerator(context::Context* ctx,
- ProofNodeManager* pnm)
- : d_pnm(pnm), d_proofs(pnm, ctx), d_current(nullptr)
+CoveringsProofGenerator::CoveringsProofGenerator(Env& env,
+ context::Context* ctx)
+ : EnvObj(env), d_proofs(env, ctx), d_current(nullptr)
{
d_false = NodeManager::currentNM()->mkConst(false);
d_zero = NodeManager::currentNM()->mkConstReal(Rational(0));
#include "expr/node.h"
#include "proof/lazy_tree_proof_generator.h"
#include "proof/proof_set.h"
+#include "smt/env_obj.h"
#include "theory/arith/nl/coverings/cdcac_utils.h"
namespace cvc5::internal {
* It uses a LazyTreeProofGenerator internally to manage the tree-based proof
* construction.
*/
-class CoveringsProofGenerator
+class CoveringsProofGenerator : protected EnvObj
{
public:
friend std::ostream& operator<<(std::ostream& os,
const CoveringsProofGenerator& proof);
- CoveringsProofGenerator(context::Context* ctx, ProofNodeManager* pnm);
+ CoveringsProofGenerator(Env& env, context::Context* ctx);
/** Start a new proof in this proof generator */
void startNewProof();
VariableMapper& vm);
private:
- /** The proof node manager used for the proofs */
- ProofNodeManager* d_pnm;
/** The list of generated proofs */
CDProofSet<LazyTreeProofGenerator> d_proofs;
/** The current proof */
namespace arith {
namespace nl {
-ExtState::ExtState(InferenceManager& im, NlModel& model, Env& env)
- : d_im(im), d_model(model), d_env(env)
+ExtState::ExtState(Env& env, InferenceManager& im, NlModel& model)
+ : EnvObj(env), d_im(im), d_model(model)
{
d_false = NodeManager::currentNM()->mkConst(false);
d_true = NodeManager::currentNM()->mkConst(true);
d_zero = NodeManager::currentNM()->mkConstInt(Rational(0));
d_one = NodeManager::currentNM()->mkConstInt(Rational(1));
d_neg_one = NodeManager::currentNM()->mkConstInt(Rational(-1));
- if (d_env.isTheoryProofProducing())
+ if (env.isTheoryProofProducing())
{
- d_proof.reset(new CDProofSet<CDProof>(
- d_env.getProofNodeManager(), d_env.getUserContext(), "nl-ext"));
+ d_proof.reset(new CDProofSet<CDProof>(env, env.getUserContext(), "nl-ext"));
}
}
class NlModel;
-struct ExtState
+class ExtState : protected EnvObj
{
- ExtState(InferenceManager& im, NlModel& model, Env& env);
+ public:
+ ExtState(Env& env, InferenceManager& im, NlModel& model);
void init(const std::vector<Node>& xts);
InferenceManager& d_im;
/** Reference to the non-linear model object */
NlModel& d_model;
- /** Reference to the environment */
- Env& d_env;
/**
* A CDProofSet that hands out CDProof objects for lemmas.
*/
namespace arith {
namespace nl {
-struct ExtState;
+class ExtState;
class FactoringCheck : protected EnvObj
{
}
// compute if bound is not satisfied, and store what is required
// for a possible refinement
- if (d_data->d_env.getOptions().arith.nlExtTangentPlanes)
+ if (options().arith.nlExtTangentPlanes)
{
if (is_false_lit)
{
: PfRule::ARITH_MULT_NEG,
{},
{mult, simpleeq});
- theory::Rewriter* rew = d_data->d_env.getRewriter();
- if (type == Kind::EQUAL
- && (rew->rewrite(simpleeq) != rew->rewrite(exp[1])))
+ if (type == Kind::EQUAL && (rewrite(simpleeq) != rewrite(exp[1])))
{
// it is not identical under rewriting and we need to do some work here
// The proof looks like this:
{nm->mkConstInt(Rational(1))});
Node lb = nm->mkNode(Kind::GEQ, simpleeq[0], simpleeq[1]);
Node rb = nm->mkNode(Kind::LEQ, simpleeq[0], simpleeq[1]);
- if (rew->rewrite(lb) == rew->rewrite(exp[1][0]))
+ if (rewrite(lb) == rewrite(exp[1][0]))
{
proof->addStep(
lb, PfRule::MACRO_SR_PRED_TRANSFORM, {exp[1][0]}, {lb});
namespace arith {
namespace nl {
-struct ExtState;
+class ExtState;
class MonomialBoundsCheck : protected EnvObj
{
namespace arith {
namespace nl {
-struct ExtState;
+class ExtState;
class MonomialCheck : protected EnvObj
{
namespace arith {
namespace nl {
-struct ExtState;
+class ExtState;
class SplitZeroCheck : protected EnvObj
{
namespace arith {
namespace nl {
-struct ExtState;
+class ExtState;
class TangentPlaneCheck : protected EnvObj
{
d_extTheory(env, d_extTheoryCb, d_im),
d_model(env),
d_trSlv(d_env, d_astate, d_im, d_model),
- d_extState(d_im, d_model, d_env),
+ d_extState(d_env, d_im, d_model),
d_factoringSlv(d_env, &d_extState),
d_monomialBoundsSlv(d_env, &d_extState),
d_monomialSlv(d_env, &d_extState),
#include "expr/skolem_manager.h"
#include "proof/proof.h"
+#include "proof/proof_node_manager.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/inference_manager.h"
#include "theory/arith/nl/nl_model.h"
d_neg_one = NodeManager::currentNM()->mkConstInt(Rational(-1));
if (d_env.isTheoryProofProducing())
{
- d_proof.reset(new CDProofSet<CDProof>(
- d_env.getProofNodeManager(), d_env.getUserContext(), "nl-trans"));
+ d_proof.reset(
+ new CDProofSet<CDProof>(d_env, d_env.getUserContext(), "nl-trans"));
d_proofChecker.reset(new TranscendentalProofRuleChecker());
d_proofChecker->registerTo(d_env.getProofNodeManager()->getChecker());
}
namespace theory {
namespace arith {
-OperatorElim::OperatorElim(Env& env)
- : EnvObj(env), EagerProofGenerator(d_env.getProofNodeManager())
-{
-}
+OperatorElim::OperatorElim(Env& env) : EagerProofGenerator(env) {}
void OperatorElim::checkNonLinearLogic(Node term)
{
SkolemLemma OperatorElim::mkSkolemLemma(Node lem, Node k)
{
TrustNode tlem;
- if (d_pnm != nullptr)
+ if (d_env.isTheoryProofProducing())
{
tlem = mkTrustNode(lem, PfRule::THEORY_PREPROCESS_LEMMA, {}, {lem});
}
namespace theory {
namespace arith {
-class OperatorElim : protected EnvObj, public EagerProofGenerator
+class OperatorElim : public EagerProofGenerator
{
public:
OperatorElim(Env& env);
namespace arith {
PreprocessRewriteEq::PreprocessRewriteEq(Env& env)
- : EnvObj(env),
- d_ppPfGen(d_env.getProofNodeManager(), context(), "Arith::ppRewrite")
+ : EnvObj(env), d_ppPfGen(env, context(), "Arith::ppRewrite")
{
}
d_astate(env, valuation),
d_im(env, *this, d_astate),
d_ppre(d_env),
- d_bab(env, d_astate, d_im, d_ppre, d_pnm),
+ d_bab(env, d_astate, d_im, d_ppre),
d_eqSolver(nullptr),
d_internal(new linear::TheoryArithPrivate(*this, env, d_bab)),
d_nonlinearExtension(nullptr),
InferenceManager::InferenceManager(Env& env, Theory& t, TheoryState& state)
: TheoryInferenceManager(env, t, state, "theory::arrays::", false),
- d_lemmaPg(isProofEnabled()
- ? new EagerProofGenerator(env.getProofNodeManager(),
- userContext(),
- "ArrayLemmaProofGenerator")
- : nullptr)
+ d_lemmaPg(isProofEnabled() ? new EagerProofGenerator(
+ env, userContext(), "ArrayLemmaProofGenerator")
+ : nullptr)
{
}
name + "number of setModelVal conflicts")),
d_ppEqualityEngine(d_env, userContext(), name + "pp", true),
d_ppFacts(userContext()),
- d_rewriter(env.getRewriter(), d_pnm),
+ d_rewriter(env),
d_state(env, valuation),
d_im(env, *this, d_state),
d_literalsToPropagate(context()),
#include "expr/attribute.h"
#include "proof/conv_proof_generator.h"
#include "proof/eager_proof_generator.h"
+#include "smt/env.h"
#include "theory/arrays/skolem_cache.h"
#include "theory/type_enumerator.h"
#include "util/cardinality.h"
return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count);
}
-TheoryArraysRewriter::TheoryArraysRewriter(Rewriter* rewriter,
- ProofNodeManager* pnm)
- : d_rewriter(rewriter), d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr)
+TheoryArraysRewriter::TheoryArraysRewriter(Env& env)
+ : d_rewriter(env.getRewriter()),
+ d_epg(env.isTheoryProofProducing() ? new EagerProofGenerator(env)
+ : nullptr)
{
}
namespace cvc5::internal {
class EagerProofGenerator;
+class Env;
namespace theory {
-class Rewriter;
-
namespace arrays {
Node getMostFrequentValue(TNode store);
class TheoryArraysRewriter : public TheoryRewriter
{
public:
- TheoryArraysRewriter(Rewriter* rewriter, ProofNodeManager* pnm);
+ TheoryArraysRewriter(Env& env);
/** Normalize a constant whose index type has cardinality indexCard */
static Node normalizeConstant(TNode node, Cardinality indexCard);
d_forwardPropagation(enableForward),
d_backwardPropagation(enableBackward),
d_needsFinish(false),
- d_pnm(nullptr),
d_epg(nullptr),
d_proofInternal(nullptr),
d_proofExternal(nullptr)
}
else if (assertion.getKind() == kind::AND)
{
- ProofCircuitPropagatorBackward prover{d_pnm, assertion, true};
+ ProofCircuitPropagatorBackward prover{
+ d_env.getProofNodeManager(), assertion, true};
if (isProofEnabled())
{
addProof(assertion, prover.assume(assertion));
// Assign the given assertion to true
assignAndEnqueue(assertion,
true,
- isProofEnabled() ? d_pnm->mkAssume(assertion) : nullptr);
+ isProofEnabled()
+ ? d_env.getProofNodeManager()->mkAssume(assertion)
+ : nullptr);
}
}
{
return;
}
- ProofCircuitPropagator pcp(d_pnm);
+ ProofCircuitPropagator pcp(d_env.getProofNodeManager());
if (n == bfalse)
{
d_epg->setProofFor(bfalse, pcp.assume(bfalse));
{
Trace("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent
<< ", " << parentAssignment << ")" << endl;
- ProofCircuitPropagatorBackward prover{d_pnm, parent, parentAssignment};
+ ProofCircuitPropagatorBackward prover{
+ d_env.getProofNodeManager(), parent, parentAssignment};
// backward rules
switch (parent.getKind())
Trace("circuit-prop") << "Parent: " << parent << endl;
Assert(expr::hasSubterm(parent, child));
- ProofCircuitPropagatorForward prover{d_pnm, child, childAssignment, parent};
+ ProofCircuitPropagatorForward prover{
+ d_env.getProofNodeManager(), child, childAssignment, parent};
// Forward rules
switch (parent.getKind())
void CircuitPropagator::enableProofs(context::Context* ctx,
ProofGenerator* defParent)
{
- d_pnm = d_env.getProofNodeManager();
- Assert(d_pnm != nullptr);
- d_epg.reset(new EagerProofGenerator(d_pnm, ctx));
+ d_epg.reset(new EagerProofGenerator(d_env, ctx));
d_proofInternal.reset(new LazyCDProofChain(
- d_pnm, true, ctx, d_epg.get(), true, "CircuitPropInternalLazyChain"));
+ d_env, true, ctx, d_epg.get(), true, "CircuitPropInternalLazyChain"));
if (defParent != nullptr)
{
// If we provide a parent proof generator (defParent), we want the ASSUME
// leafs of proofs provided by this class to call the getProofFor method on
// the parent. To do this, we use a LazyCDProofChain.
d_proofExternal.reset(new LazyCDProofChain(
- d_pnm, true, ctx, defParent, false, "CircuitPropExternalLazyChain"));
+ d_env, true, ctx, defParent, false, "CircuitPropExternalLazyChain"));
}
}
/** Adds a new proof for f, or drops it if we already have a proof */
void addProof(TNode f, std::shared_ptr<ProofNode> pf);
- /** A pointer to the proof manager */
- ProofNodeManager* d_pnm;
/** Eager proof generator that actually stores the proofs */
std::unique_ptr<EagerProofGenerator> d_epg;
/** Connects the proofs to subproofs internally */
namespace bv {
BitblastProofGenerator::BitblastProofGenerator(Env& env,
- ProofNodeManager* pnm,
TConvProofGenerator* tcpg)
- : EnvObj(env), d_pnm(pnm), d_tcpg(tcpg)
+ : EnvObj(env), d_tcpg(tcpg)
{
}
{
const auto& [t, bbt] = d_cache.at(eq);
- CDProof cdp(d_pnm);
+ CDProof cdp(d_env);
/* Coarse-grained bit-blast step. */
if (t.isNull())
{
{
public:
BitblastProofGenerator(Env& env,
- ProofNodeManager* pnm,
TConvProofGenerator* tcpg);
~BitblastProofGenerator(){};
void addBitblastStep(TNode t, TNode bbt, TNode eq);
private:
- /** The associated proof node manager. */
- ProofNodeManager* d_pnm;
/**
* The associated term conversion proof generator, which tracks the
* individual bit-blast steps.
namespace theory {
namespace bv {
-BBProof::BBProof(Env& env,
- TheoryState* state,
- ProofNodeManager* pnm,
- bool fineGrained)
+BBProof::BBProof(Env& env, TheoryState* state, bool fineGrained)
: EnvObj(env),
d_bb(new NodeBitblaster(env, state)),
- d_pnm(pnm),
d_tcontext(new TheoryLeafTermContext(theory::THEORY_BV)),
- d_tcpg(pnm ? new TConvProofGenerator(
- pnm,
- nullptr,
- /* ONCE to visit each term only once, post-order. FIXPOINT
- * could lead to infinite loops due to terms being rewritten
- * to terms that contain themselves */
- TConvPolicy::ONCE,
- /* STATIC to get the same ProofNode for a shared subterm. */
- TConvCachePolicy::STATIC,
- "BBProof::TConvProofGenerator",
- d_tcontext.get(),
- false)
- : nullptr),
- d_bbpg(pnm ? new BitblastProofGenerator(env, pnm, d_tcpg.get())
- : nullptr),
+ d_tcpg(new TConvProofGenerator(
+ env,
+ nullptr,
+ /* ONCE to visit each term only once, post-order. FIXPOINT
+ * could lead to infinite loops due to terms being rewritten
+ * to terms that contain themselves */
+ TConvPolicy::ONCE,
+ /* STATIC to get the same ProofNode for a shared subterm. */
+ TConvCachePolicy::STATIC,
+ "BBProof::TConvProofGenerator",
+ d_tcontext.get(),
+ false)),
+ d_bbpg(new BitblastProofGenerator(env, d_tcpg.get())),
d_recordFineGrainedProofs(fineGrained)
{
}
BitblastProofGenerator* BBProof::getProofGenerator() { return d_bbpg.get(); }
-bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; }
+bool BBProof::isProofsEnabled() const { return d_env.isTheoryProofProducing(); }
} // namespace bv
} // namespace theory
public:
BBProof(Env& env,
TheoryState* state,
- ProofNodeManager* pnm,
bool fineGrained);
~BBProof();
/** The associated simple bit-blaster. */
std::unique_ptr<NodeBitblaster> d_bb;
- /** The associated proof node manager. */
- ProofNodeManager* d_pnm;
/** Term context for d_tcpg to not rewrite below BV leafs. */
std::unique_ptr<TermContext> d_tcontext;
/** Term conversion proof generator for bit-blast steps. */
BVSolverBitblast::BVSolverBitblast(Env& env,
TheoryState* s,
- TheoryInferenceManager& inferMgr,
- ProofNodeManager* pnm)
+ TheoryInferenceManager& inferMgr)
: BVSolver(env, *s, inferMgr),
d_bitblaster(new NodeBitblaster(env, s)),
d_bbRegistrar(new BBRegistrar(d_bitblaster.get())),
d_bbInputFacts(context()),
d_assumptions(context()),
d_assertions(context()),
- d_epg(pnm ? new EagerProofGenerator(pnm, userContext(), "") : nullptr),
+ d_epg(env.isTheoryProofProducing()
+ ? new EagerProofGenerator(env, userContext(), "")
+ : nullptr),
d_factLiteralCache(context()),
d_literalFactCache(context()),
d_propagate(options().bv.bitvectorPropagate),
d_resetNotify(new NotifyResetAssertions(userContext()))
{
- if (pnm != nullptr)
+ if (env.isTheoryProofProducing())
{
- d_bvProofChecker.registerTo(pnm->getChecker());
+ d_bvProofChecker.registerTo(env.getProofNodeManager()->getChecker());
}
initSatSolver();
public:
BVSolverBitblast(Env& env,
TheoryState* state,
- TheoryInferenceManager& inferMgr,
- ProofNodeManager* pnm);
+ TheoryInferenceManager& inferMgr);
~BVSolverBitblast() = default;
bool needsEqualityEngine(EeSetupInfo& esi) override { return true; }
} // namespace
BVSolverBitblastInternal::BVSolverBitblastInternal(
- Env& env,
- TheoryState* s,
- TheoryInferenceManager& inferMgr,
- ProofNodeManager* pnm)
+ Env& env, TheoryState* s, TheoryInferenceManager& inferMgr)
: BVSolver(env, *s, inferMgr),
- d_pnm(pnm),
- d_bitblaster(new BBProof(env, s, pnm, false)),
- d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr)
+ d_bitblaster(new BBProof(env, s, false)),
+ d_epg(new EagerProofGenerator(d_env))
{
}
Node atom_bb = d_bitblaster->getStoredBBAtom(fact);
Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);
- if (d_pnm == nullptr)
+ if (!d_env.isTheoryProofProducing())
{
d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA);
}
NodeManager* nm = NodeManager::currentNM();
Node lemma = nm->mkNode(kind::EQUAL, fact, n);
- if (d_pnm == nullptr)
+ if (!d_env.isTheoryProofProducing())
{
d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
}
public:
BVSolverBitblastInternal(Env& env,
TheoryState* state,
- TheoryInferenceManager& inferMgr,
- ProofNodeManager* pnm);
+ TheoryInferenceManager& inferMgr);
~BVSolverBitblastInternal() = default;
bool needsEqualityEngine(EeSetupInfo& esi) override;
*/
void addBBLemma(TNode fact);
- /** Proof node manager. */
- ProofNodeManager* d_pnm;
/** Bit-blaster used to bit-blast atoms/terms. */
std::unique_ptr<BBProof> d_bitblaster;
/** Proof rule checker */
switch (options().bv.bvSolver)
{
case options::BVSolver::BITBLAST:
- d_internal.reset(new BVSolverBitblast(env, &d_state, d_im, d_pnm));
+ d_internal.reset(new BVSolverBitblast(env, &d_state, d_im));
break;
default:
AlwaysAssert(options().bv.bvSolver == options::BVSolver::BITBLAST_INTERNAL);
- d_internal.reset(
- new BVSolverBitblastInternal(d_env, &d_state, d_im, d_pnm));
+ d_internal.reset(new BVSolverBitblastInternal(d_env, &d_state, d_im));
}
d_theoryState = &d_state;
d_inferManager = &d_im;
: EnvObj(env),
d_te(te),
d_valuation(&te),
- d_pnm(env.isTheoryProofProducing() ? env.getProofNodeManager() : nullptr),
d_logicInfo(env.getLogicInfo()),
d_paraTheories(paraTheories),
d_eemanager(nullptr),
d_mmanager(nullptr),
d_sharedSolver(nullptr),
- d_cmbsPg(d_pnm ? new EagerProofGenerator(d_pnm, env.getUserContext())
- : nullptr)
+ d_cmbsPg(env.isTheoryProofProducing()
+ ? new EagerProofGenerator(env, env.getUserContext())
+ : nullptr)
{
// create the equality engine, model manager, and shared solver
if (options().theory.eeMode == options::EqEngineMode::DISTRIBUTED)
TheoryEngine& d_te;
/** Valuation for the engine */
Valuation d_valuation;
- /** The proof node manager */
- ProofNodeManager* d_pnm;
/** Logic info of theory engine (cached) */
const LogicInfo& d_logicInfo;
/** List of parametric theories of theory engine */
namespace theory {
namespace datatypes {
-InferProofCons::InferProofCons(context::Context* c, ProofNodeManager* pnm)
- : d_pnm(pnm), d_lazyFactMap(c == nullptr ? &d_context : c)
+InferProofCons::InferProofCons(Env& env, context::Context* c)
+ : EnvObj(env), d_lazyFactMap(c == nullptr ? &d_context : c)
{
- Assert(d_pnm != nullptr);
}
void InferProofCons::notifyFact(const std::shared_ptr<DatatypesInference>& di)
{
Trace("dt-ipc") << "dt-ipc: Ask proof for " << fact << std::endl;
// temporary proof
- CDProof pf(d_pnm);
+ CDProof pf(d_env);
// get the inference
NodeDatatypesInferenceMap::iterator it = d_lazyFactMap.find(fact);
if (it == d_lazyFactMap.end())
#include "context/cdhashmap.h"
#include "expr/node.h"
#include "proof/proof_generator.h"
+#include "smt/env_obj.h"
#include "theory/datatypes/inference.h"
namespace cvc5::internal {
-
-class ProofNodeManager;
-
namespace theory {
namespace datatypes {
* The main (private) method of this class is convert below, which is
* called when we need to construct a proof node from an InferInfo.
*/
-class InferProofCons : public ProofGenerator
+class InferProofCons : protected EnvObj, public ProofGenerator
{
typedef context::CDHashMap<Node, std::shared_ptr<DatatypesInference>>
NodeDatatypesInferenceMap;
public:
- InferProofCons(context::Context* c, ProofNodeManager* pnm);
+ InferProofCons(Env& env, context::Context* c);
~InferProofCons() {}
/**
* This is called to notify that di is an inference that may need a proof
void convert(InferenceId infer, TNode conc, TNode exp, CDProof* cdp);
/** A dummy context used by this class if none is provided */
context::Context d_context;
- /** the proof node manager */
- ProofNodeManager* d_pnm;
/** The lazy fact map */
NodeDatatypesInferenceMap d_lazyFactMap;
};
InferenceManager::InferenceManager(Env& env, Theory& t, TheoryState& state)
: InferenceManagerBuffered(env, t, state, "theory::datatypes::"),
- d_ipc(isProofEnabled()
- ? new InferProofCons(context(), env.getProofNodeManager())
- : nullptr),
- d_lemPg(isProofEnabled()
- ? new EagerProofGenerator(env.getProofNodeManager(),
- userContext(),
- "datatypes::lemPg")
- : nullptr)
+ d_ipc(isProofEnabled() ? new InferProofCons(env, context()) : nullptr),
+ d_lemPg(isProofEnabled() ? new EagerProofGenerator(
+ env, userContext(), "datatypes::lemPg")
+ : nullptr)
{
d_false = NodeManager::currentNM()->mkConst(false);
}
std::shared_ptr<InferProofCons> ipcl;
if (isProofEnabled())
{
- ipcl =
- std::make_shared<InferProofCons>(nullptr, d_env.getProofNodeManager());
+ ipcl = std::make_shared<InferProofCons>(d_env, nullptr);
}
conc = prepareDtInference(conc, exp, id, ipcl.get());
// send it as a lemma
: EnvObj(env),
d_termCanon(),
d_aedb(userContext(), &d_termCanon, true),
- d_pnm(env.getProofNodeManager()),
- d_pfAlpha(d_pnm ? new EagerProofGenerator(d_pnm) : nullptr)
+ d_pfAlpha(env.isTheoryProofProducing() ? new EagerProofGenerator(env)
+ : nullptr)
{
}
Trace("alpha-eq") << "subs: " << vars[i] << " -> " << subs[i]
<< std::endl;
}
- CDProof cdp(d_pnm);
+ CDProof cdp(d_env);
Node sret =
ret.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
std::vector<Node> transEq;
expr::TermCanonize d_termCanon;
/** the database of quantified formulas registered to this class */
AlphaEquivalenceDb d_aedb;
- /** Pointer to the proof node manager */
- ProofNodeManager* d_pnm;
/** An eager proof generator storing alpha equivalence proofs.*/
std::unique_ptr<EagerProofGenerator> d_pfAlpha;
/** Are proofs enabled for this object? */
d_treg(tr),
d_insts(userContext()),
d_c_inst_match_trie_dom(userContext()),
- d_pfInst(isProofEnabled() ? new CDProof(env.getProofNodeManager(),
- userContext(),
- "Instantiate::pfInst")
- : nullptr)
+ d_pfInst(isProofEnabled()
+ ? new CDProof(env, userContext(), "Instantiate::pfInst")
+ : nullptr)
{
}
std::shared_ptr<LazyCDProof> pfTmp;
if (isProofEnabled())
{
- pfTmp.reset(new LazyCDProof(d_env.getProofNodeManager(),
- nullptr,
- nullptr,
- "Instantiate::LazyCDProof::tmp"));
+ pfTmp.reset(new LazyCDProof(
+ d_env, nullptr, nullptr, "Instantiate::LazyCDProof::tmp"));
}
// construct the instantiation
d_skolemized(userContext()),
d_epg(!isProofEnabled()
? nullptr
- : new EagerProofGenerator(env.getProofNodeManager(),
- userContext(),
- "Skolemize::epg"))
+ : new EagerProofGenerator(env, userContext(), "Skolemize::epg"))
{
}
Node existsq = nm->mkNode(EXISTS, echildren);
Node res = skm->mkSkolemize(existsq, d_skolem_constants[q], "skv");
Node qnot = q.notNode();
- CDProof cdp(pnm);
+ CDProof cdp(d_env);
cdp.addStep(res, PfRule::SKOLEMIZE, {qnot}, {});
std::shared_ptr<ProofNode> pf = cdp.getProofFor(res);
std::vector<Node> assumps;
return TrustNode::mkTrustRewrite(node, ret, d_tpg.get());
}
-void Rewriter::setProofNodeManager(ProofNodeManager* pnm)
+void Rewriter::finishInit(Env& env)
{
// if not already initialized with proof support
if (d_tpg == nullptr)
{
- Trace("rewriter") << "Rewriter::setProofNodeManager" << std::endl;
+ Trace("rewriter") << "Rewriter::finishInit" << std::endl;
// the rewriter is staticly determinstic, thus use static cache policy
// for the term conversion proof generator
- d_tpg.reset(new TConvProofGenerator(pnm,
+ d_tpg.reset(new TConvProofGenerator(env,
nullptr,
TConvPolicy::FIXPOINT,
TConvCachePolicy::STATIC,
TrustNode rewriteWithProof(TNode node,
bool isExtEq = false);
- /** Set proof node manager */
- void setProofNodeManager(ProofNodeManager* pnm);
+ /** Finish init, which sets up the proof manager if applicable */
+ void finishInit(Env& env);
/**
* Registers a theory rewriter with this rewriter. The rewriter does not own
TermRegistry::TermRegistry(Env& env,
SolverState& state,
InferenceManager& im,
- SkolemCache& skc,
- ProofNodeManager* pnm)
+ SkolemCache& skc)
: EnvObj(env),
d_im(im),
d_skCache(skc),
d_proxy(userContext()),
d_proxy_to_term(userContext()),
- d_epg(
- pnm ? new EagerProofGenerator(pnm, nullptr, "sets::TermRegistry::epg")
- : nullptr)
+ d_epg(env.isTheoryProofProducing() ? new EagerProofGenerator(
+ env, nullptr, "sets::TermRegistry::epg")
+ : nullptr)
{
}
TermRegistry(Env& env,
SolverState& state,
InferenceManager& im,
- SkolemCache& skc,
- ProofNodeManager* pnm);
+ SkolemCache& skc);
/** get the proxy variable for set n
*
* Proxy variables are used to communicate information that otherwise would
d_state(env, valuation, d_skCache),
d_im(env, *this, d_state),
d_cpacb(*this),
- d_internal(new TheorySetsPrivate(
- env, *this, d_state, d_im, d_skCache, d_pnm, d_cpacb)),
+ d_internal(
+ new TheorySetsPrivate(env, *this, d_state, d_im, d_skCache, d_cpacb)),
d_notify(*d_internal.get(), d_im)
{
// use the official theory state and inference manager objects
SolverState& state,
InferenceManager& im,
SkolemCache& skc,
- ProofNodeManager* pnm,
CarePairArgumentCallback& cpacb)
: EnvObj(env),
d_deq(context()),
d_state(state),
d_im(im),
d_skCache(skc),
- d_treg(d_env, state, im, skc, pnm),
+ d_treg(d_env, state, im, skc),
d_rels(new TheorySetsRels(d_env, state, im, skc, d_treg)),
d_cardSolver(new CardinalityExtension(d_env, state, im, d_treg)),
d_rels_enabled(false),
SolverState& state,
InferenceManager& im,
SkolemCache& skc,
- ProofNodeManager* pnm,
CarePairArgumentCallback& cpacb);
~TheorySetsPrivate();
namespace theory {
namespace strings {
-InferProofCons::InferProofCons(context::Context* c,
- ProofNodeManager* pnm,
+InferProofCons::InferProofCons(Env& env,
+ context::Context* c,
SequencesStatistics& statistics)
- : d_pnm(pnm), d_lazyFactMap(c), d_statistics(statistics)
+ : EnvObj(env), d_lazyFactMap(c), d_statistics(statistics)
{
- Assert(d_pnm != nullptr);
}
void InferProofCons::notifyFact(const InferInfo& ii)
Assert(ii->d_conc == fact);
// make a placeholder proof using STRINGS_INFERENCE, which is reconstructed
// during post-process
- CDProof pf(d_pnm);
+ CDProof pf(d_env);
std::vector<Node> args;
packArgs(ii->d_conc, ii->getId(), ii->d_idRev, ii->d_premises, args);
// must flatten
#include "proof/proof_checker.h"
#include "proof/proof_rule.h"
#include "proof/theory_proof_step_buffer.h"
+#include "smt/env_obj.h"
#include "theory/builtin/proof_checker.h"
#include "theory/strings/infer_info.h"
#include "theory/strings/sequences_stats.h"
* returns applications of the rule STRING_INFERENCE, which store the arguments
* to the proof conversion routine "convert" below.
*/
-class InferProofCons : public ProofGenerator
+class InferProofCons : protected EnvObj, public ProofGenerator
{
typedef context::CDHashMap<Node, std::shared_ptr<InferInfo>> NodeInferInfoMap;
public:
- InferProofCons(context::Context* c,
- ProofNodeManager* pnm,
+ InferProofCons(Env& env,
+ context::Context* c,
SequencesStatistics& statistics);
~InferProofCons() {}
/**
* in termsToPurify.
*/
static Node maybePurifyTerm(Node n, std::unordered_set<Node>& termsToPurify);
- /** the proof node manager */
- ProofNodeManager* d_pnm;
/** The lazy fact map */
NodeInferInfoMap d_lazyFactMap;
/** Reference to the statistics for the theory of strings/sequences. */
d_termReg(tr),
d_extt(e),
d_statistics(statistics),
- d_ipc(isProofEnabled()
- ? new InferProofCons(
- context(), env.getProofNodeManager(), d_statistics)
- : nullptr),
- d_ipcl(isProofEnabled()
- ? new InferProofCons(
- context(), env.getProofNodeManager(), d_statistics)
- : nullptr)
+ d_ipc(isProofEnabled() ? new InferProofCons(env, context(), d_statistics)
+ : nullptr),
+ d_ipcl(isProofEnabled() ? new InferProofCons(env, context(), d_statistics)
+ : nullptr)
{
NodeManager* nm = NodeManager::currentNM();
d_zero = nm->mkConstInt(Rational(0));
#include "expr/bound_var_manager.h"
#include "options/strings_options.h"
#include "proof/proof_node_manager.h"
+#include "smt/env.h"
#include "theory/rewriter.h"
#include "theory/strings/regexp_entail.h"
#include "theory/strings/theory_strings_utils.h"
typedef expr::Attribute<ReElimStarIndexAttributeId, Node>
ReElimStarIndexAttribute;
-RegExpElimination::RegExpElimination(bool isAgg,
- ProofNodeManager* pnm,
- context::Context* c)
- : d_isAggressive(isAgg),
- d_pnm(pnm),
- d_epg(pnm == nullptr
+RegExpElimination::RegExpElimination(Env& env, bool isAgg, context::Context* c)
+ : EnvObj(env),
+ d_isAggressive(isAgg),
+ d_epg(!env.isTheoryProofProducing()
? nullptr
- : new EagerProofGenerator(pnm, c, "RegExpElimination::epg"))
+ : new EagerProofGenerator(env, c, "RegExpElimination::epg"))
{
}
// Currently aggressive doesnt work due to fresh bound variables
if (isProofEnabled() && !d_isAggressive)
{
+ ProofNodeManager* pnm = d_env.getProofNodeManager();
Node eq = atom.eqNode(eatom);
Node aggn = NodeManager::currentNM()->mkConst(d_isAggressive);
std::shared_ptr<ProofNode> pn =
- d_pnm->mkNode(PfRule::RE_ELIM, {}, {atom, aggn}, eq);
+ pnm->mkNode(PfRule::RE_ELIM, {}, {atom, aggn}, eq);
d_epg->setProofFor(eq, pn);
return TrustNode::mkTrustRewrite(atom, eatom, d_epg.get());
}
<< "." << std::endl;
return atomElim;
}
-bool RegExpElimination::isProofEnabled() const { return d_pnm != nullptr; }
+bool RegExpElimination::isProofEnabled() const
+{
+ return d_env.isTheoryProofProducing();
+}
} // namespace strings
} // namespace theory
#include "expr/node.h"
#include "proof/eager_proof_generator.h"
#include "proof/trust_node.h"
+#include "smt/env_obj.h"
namespace cvc5::internal {
namespace theory {
*
* It is used by TheoryStrings during ppRewrite.
*/
-class RegExpElimination
+class RegExpElimination : protected EnvObj
{
public:
/**
* @param pnm The proof node manager to use (for proofs)
* @param c The context to use (for proofs)
*/
- RegExpElimination(bool isAgg = false,
- ProofNodeManager* pnm = nullptr,
+ RegExpElimination(Env& env,
+ bool isAgg = false,
context::Context* c = nullptr);
/** eliminate membership
*
bool isProofEnabled() const;
/** Are aggressive eliminations enabled? */
bool d_isAggressive;
- /** Pointer to the proof node manager */
- ProofNodeManager* d_pnm;
/** An eager proof generator for storing proofs in eliminate trusted above */
std::unique_ptr<EagerProofGenerator> d_epg;
}; /* class RegExpElimination */
TermRegistry::TermRegistry(Env& env,
Theory& t,
SolverState& s,
- SequencesStatistics& statistics,
- ProofNodeManager* pnm)
+ SequencesStatistics& statistics)
: EnvObj(env),
d_theory(t),
d_state(s),
d_proxyVar(userContext()),
d_proxyVarToLength(userContext()),
d_lengthLemmaTermsCache(userContext()),
- d_epg(pnm ? new EagerProofGenerator(
- pnm,
- userContext(),
- "strings::TermRegistry::EagerProofGenerator")
- : nullptr)
+ d_epg(
+ env.isTheoryProofProducing() ? new EagerProofGenerator(
+ env, userContext(), "strings::TermRegistry::EagerProofGenerator")
+ : nullptr)
{
NodeManager* nm = NodeManager::currentNM();
d_zero = nm->mkConstInt(Rational(0));
TermRegistry(Env& env,
Theory& t,
SolverState& s,
- SequencesStatistics& statistics,
- ProofNodeManager* pnm);
+ SequencesStatistics& statistics);
~TermRegistry();
/** get the cardinality of the alphabet used, based on the options */
uint32_t getAlphabetCardinality() const;
d_notify(*this),
d_statistics(),
d_state(env, d_valuation),
- d_termReg(env, *this, d_state, d_statistics, d_pnm),
+ d_termReg(env, *this, d_state, d_statistics),
d_rewriter(env.getRewriter(),
&d_statistics.d_rewrites,
d_termReg.getAlphabetCardinality()),
d_rsolver(
env, d_state, d_im, d_termReg, d_csolver, d_esolver, d_statistics),
d_regexp_elim(
+ env,
options().strings.regExpElim == options::RegExpElimMode::AGG,
- d_pnm,
userContext()),
d_stringsFmf(env, valuation, d_termReg),
d_strat(d_env),
TheoryEngine::TheoryEngine(Env& env)
: EnvObj(env),
d_propEngine(nullptr),
- d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
- : nullptr),
- d_lazyProof(
- d_pnm != nullptr ? new LazyCDProof(
- d_pnm, nullptr, userContext(), "TheoryEngine::LazyCDProof")
- : nullptr),
- d_tepg(new TheoryEngineProofGenerator(d_pnm, userContext())),
+ d_lazyProof(env.isTheoryProofProducing() ? new LazyCDProof(
+ env, nullptr, userContext(), "TheoryEngine::LazyCDProof")
+ : nullptr),
+ d_tepg(new TheoryEngineProofGenerator(env, userContext())),
d_tc(nullptr),
d_sharedSolver(nullptr),
d_quantEngine(nullptr),
if (isProofEnabled())
{
texplanation.debugCheckClosed(
- "te-proof-exp", "texplanation no share", false);
+ options(), "te-proof-exp", "texplanation no share", false);
// check if no generator, if so, add THEORY_LEMMA
if (texplanation.getGenerator() == nullptr)
{
tlemma = TrustNode::mkTrustLemma(lemma, d_lazyProof.get());
}
// ensure closed
- tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_initial");
+ tlemma.debugCheckClosed(
+ options(), "te-proof-debug", "TheoryEngine::lemma_initial");
}
// assert the lemma
Trace("te-proof-debug") << "Check closed conflict" << std::endl;
// doesn't require proof generator, yet, since THEORY_LEMMA is added below
tconflict.debugCheckClosed(
- "te-proof-debug", "TheoryEngine::conflict_initial", false);
+ options(), "te-proof-debug", "TheoryEngine::conflict_initial", false);
Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl;
{
Trace("te-proof-debug")
<< "Check closed conflict explained with sharing" << std::endl;
- tncExp.debugCheckClosed("te-proof-debug",
+ tncExp.debugCheckClosed(options(),
+ "te-proof-debug",
"TheoryEngine::conflict_explained_sharing");
Trace("te-proof-debug") << "Process conflict: " << conflict << std::endl;
Trace("te-proof-debug") << "Conflict " << tconflict << " from "
Trace("te-proof-debug") << "add lazy step " << tncExp.identifyGenerator()
<< " for " << proven << std::endl;
d_lazyProof->addLazyStep(proven, tncExp.getGenerator());
- pfgEnsureClosed(proven,
+ pfgEnsureClosed(options(),
+ proven,
d_lazyProof.get(),
"te-proof-debug",
"TheoryEngine::conflict_during");
<< "Check closed conflict with sharing" << std::endl;
if (isProofEnabled())
{
- tconf.debugCheckClosed("te-proof-debug", "TheoryEngine::conflict:sharing");
+ tconf.debugCheckClosed(
+ options(), "te-proof-debug", "TheoryEngine::conflict:sharing");
}
lemma(tconf, LemmaProperty::REMOVABLE);
}
// communicating arrangements between shared terms, and the rewriter
// for arithmetic equalities does not preserve terms, e.g. x=y may become
// x+-1*y=0.
- lcp.reset(new LazyCDProof(d_pnm,
+ lcp.reset(new LazyCDProof(d_env,
nullptr,
nullptr,
"TheoryEngine::LazyCDProof::getExplanation",
d_sharedSolver->explain(toExplain.d_node, toExplain.d_theory);
if (lcp != nullptr)
{
- texplanation.debugCheckClosed("te-proof-exp", "texplanation", false);
+ texplanation.debugCheckClosed(
+ options(), "te-proof-exp", "texplanation", false);
Trace("te-proof-exp")
<< "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node
<< " by " << texplanation.getNode() << std::endl;
*/
theory::Theory* d_theoryTable[theory::THEORY_LAST];
- //--------------------------------- new proofs
- /** Proof node manager used by this theory engine, if proofs are enabled */
- ProofNodeManager* d_pnm;
+ //--------------------------------- proofs
/** The lazy proof object
*
* This stores instructions for how to construct proofs for all theory lemmas.
std::shared_ptr<LazyCDProof> d_lazyProof;
/** The proof generator */
std::shared_ptr<TheoryEngineProofGenerator> d_tepg;
- //--------------------------------- end new proofs
+ //--------------------------------- end proofs
/** The combination manager we are using */
std::unique_ptr<theory::CombinationEngine> d_tc;
/** The shared solver of the above combination engine. */
#include <sstream>
#include "proof/proof_node.h"
+#include "smt/env.h"
using namespace cvc5::internal::kind;
namespace cvc5::internal {
-TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm,
+TheoryEngineProofGenerator::TheoryEngineProofGenerator(Env& env,
context::Context* c)
- : d_pnm(pnm), d_proofs(c)
+ : EnvObj(env), d_proofs(c)
{
d_false = NodeManager::currentNM()->mkConst(false);
}
std::shared_ptr<ProofNode> pfb = lcp->getProofFor(conclusion);
Trace("tepg-debug") << "...mkScope" << std::endl;
// call the scope method of proof node manager
- std::shared_ptr<ProofNode> pf = d_pnm->mkScope(pfb, scopeAssumps);
+ ProofNodeManager* pnm = d_env.getProofNodeManager();
+ std::shared_ptr<ProofNode> pf = pnm->mkScope(pfb, scopeAssumps);
if (pf->getResult() != f)
{
#include "proof/proof_generator.h"
#include "proof/proof_node_manager.h"
#include "proof/trust_node.h"
+#include "smt/env_obj.h"
namespace cvc5::internal {
* Notice that this class could be made general purpose. Its main feature is
* storing lazy proofs for facts in a context-dependent manner.
*/
-class TheoryEngineProofGenerator : public ProofGenerator
+class TheoryEngineProofGenerator : protected EnvObj, public ProofGenerator
{
typedef context::CDHashMap<Node, std::shared_ptr<LazyCDProof>>
NodeLazyCDProofMap;
public:
- TheoryEngineProofGenerator(ProofNodeManager* pnm, context::Context* c);
+ TheoryEngineProofGenerator(Env& env, context::Context* c);
~TheoryEngineProofGenerator() {}
/**
* Make trust explanation. Called when lpf has a proof of lit from free
std::string identify() const override;
private:
- /** The proof manager, used for allocating new ProofNode objects */
- ProofNodeManager* d_pnm;
/** Map from formulas to lazy CD proofs */
NodeLazyCDProofMap d_proofs;
/** The false node */
context::UserContext* u = userContext();
ProofNodeManager* pnm = env.getProofNodeManager();
d_defaultPg.reset(
- new EagerProofGenerator(pnm, u, statsName + "EagerProofGenerator"));
+ new EagerProofGenerator(env, u, statsName + "EagerProofGenerator"));
if (options().proof.proofAnnotate)
{
d_iipa.reset(new InferenceIdProofAnnotator(pnm, u));
{
context::Context* u = userContext();
d_tpg.reset(
- new TConvProofGenerator(pnm,
+ new TConvProofGenerator(env,
u,
TConvPolicy::FIXPOINT,
TConvCachePolicy::NEVER,
"TheoryPreprocessor::preprocess_rewrite",
&d_rtfc));
- d_tpgRew.reset(new TConvProofGenerator(pnm,
+ d_tpgRew.reset(new TConvProofGenerator(env,
u,
TConvPolicy::ONCE,
TConvCachePolicy::NEVER,
"TheoryPreprocessor::pprew"));
d_lp.reset(
- new LazyCDProof(pnm, nullptr, u, "TheoryPreprocessor::LazyCDProof"));
+ new LazyCDProof(env, nullptr, u, "TheoryPreprocessor::LazyCDProof"));
// Make the main term conversion sequence generator, which tracks up to
// three conversions made in succession:
// (1) rewriting
// node -> irNode via rewriting
// irNode -> ppNode via theory-preprocessing + rewriting + tf removal
tret = d_tspg->mkTrustRewriteSequence(cterms);
- tret.debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_ret");
+ tret.debugCheckClosed(
+ options(), "tpp-debug", "TheoryPreprocessor::lemma_ret");
}
else
{
{
Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (generator) "
<< term << " -> " << termr << std::endl;
- trn.debugCheckClosed("tpp-debug",
- "TheoryPreprocessor::preprocessWithProof");
+ trn.debugCheckClosed(
+ options(), "tpp-debug", "TheoryPreprocessor::preprocessWithProof");
// always use term context hash 0 (default)
pg->addRewriteStep(
term, termr, trn.getGenerator(), isPre, PfRule::ASSUME, true, tctx);
#include "theory/trust_substitutions.h"
+#include "smt/env.h"
#include "theory/rewriter.h"
namespace cvc5::internal {
namespace theory {
-TrustSubstitutionMap::TrustSubstitutionMap(context::Context* c,
- ProofNodeManager* pnm,
+TrustSubstitutionMap::TrustSubstitutionMap(Env& env,
+ context::Context* c,
std::string name,
PfRule trustId,
MethodId ids)
- : d_ctx(c),
+ : EnvObj(env),
+ d_ctx(c),
d_subs(c),
d_tsubs(c),
d_tspb(nullptr),
d_ids(ids),
d_eqtIndex(c)
{
- setProofNodeManager(pnm);
-}
-
-void TrustSubstitutionMap::setProofNodeManager(ProofNodeManager* pnm)
-{
+ ProofNodeManager* pnm = d_env.getProofNodeManager();
if (pnm != nullptr)
{
- // should not set the proof node manager more than once
- Assert(d_tspb == nullptr);
- d_tspb.reset(new TheoryProofStepBuffer(pnm->getChecker())),
- d_subsPg.reset(new LazyCDProof(
- pnm, nullptr, d_ctx, "TrustSubstitutionMap::subsPg"));
+ d_tspb.reset(new TheoryProofStepBuffer(pnm->getChecker()));
+ d_subsPg.reset(
+ new LazyCDProof(env, nullptr, d_ctx, "TrustSubstitutionMap::subsPg"));
d_applyPg.reset(
- new LazyCDProof(pnm, nullptr, d_ctx, "TrustSubstitutionMap::applyPg"));
- d_helperPf.reset(new CDProofSet<LazyCDProof>(pnm, d_ctx));
+ new LazyCDProof(env, nullptr, d_ctx, "TrustSubstitutionMap::applyPg"));
+ d_helperPf.reset(new CDProofSet<LazyCDProof>(env, d_ctx));
}
}
/**
* A layer on top of SubstitutionMap that tracks proofs.
*/
-class TrustSubstitutionMap : public ProofGenerator
+class TrustSubstitutionMap : protected EnvObj, public ProofGenerator
{
using NodeUIntMap = context::CDHashMap<Node, size_t>;
public:
- TrustSubstitutionMap(context::Context* c,
- ProofNodeManager* pnm = nullptr,
+ TrustSubstitutionMap(Env& env,
+ context::Context* c,
std::string name = "TrustSubstitutionMap",
PfRule trustId = PfRule::PREPROCESS_LEMMA,
MethodId ids = MethodId::SB_DEFAULT);
- /** Set proof node manager */
- void setProofNodeManager(ProofNodeManager* pnm);
/** Gets a reference to the underlying substitution map */
SubstitutionMap& get();
/**
: EnvObj(env),
d_lifted(userContext()),
d_lambdaMap(userContext()),
- d_epg(env.isTheoryProofProducing() ? new EagerProofGenerator(
- env.getProofNodeManager(), userContext(), "LambdaLift::epg")
- : nullptr)
+ d_epg(env.isTheoryProofProducing()
+ ? new EagerProofGenerator(env, userContext(), "LambdaLift::epg")
+ : nullptr)
{
}
namespace eq {
ProofEqEngine::ProofEqEngine(Env& env, EqualityEngine& ee)
- : EnvObj(env),
- EagerProofGenerator(env.getProofNodeManager(),
- env.getUserContext(),
- "pfee::" + ee.identify()),
+ : EagerProofGenerator(env, env.getUserContext(), "pfee::" + ee.identify()),
d_ee(ee),
- d_factPg(env.getContext(), env.getProofNodeManager()),
+ d_factPg(env, env.getContext()),
d_assumpPg(env.getProofNodeManager()),
- d_pnm(env.getProofNodeManager()),
- d_proof(env.getProofNodeManager(),
+ d_proof(env,
nullptr,
env.getContext(),
"pfee::LazyCDProof::" + ee.identify()),
<< ", exp = " << exp << ", noExplain = " << noExplain
<< ", args = " << args << std::endl;
Assert(conc != d_true);
- LazyCDProof tmpProof(d_pnm, &d_proof);
+ LazyCDProof tmpProof(d_env, &d_proof);
LazyCDProof* curr;
TrustNodeKind tnk;
// same policy as above: for conflicts, use existing lazy proof
explainVecWithProof(tnk, assumps, exp, noExplain, curr);
// Register the proof step. We use a separate lazy CDProof which will make
// calls to curr above for the proofs of the literals in exp.
- LazyCDProof outer(d_pnm, curr);
+ LazyCDProof outer(d_env, curr);
if (!outer.addStep(conc, id, exp, args))
{
// a step went wrong, e.g. during checking
Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp
<< ", noExplain = " << noExplain << " via generator"
<< std::endl;
- LazyCDProof tmpProof(d_pnm, &d_proof);
+ LazyCDProof tmpProof(d_env, &d_proof);
LazyCDProof* curr;
TrustNodeKind tnk;
// same policy as above: for conflicts, use existing lazy proof
// "skeleton" that is the base of the proof we are constructing. The call to
// LazyCDProofChain::getProofFor will expand the leaves of this proof via
// calls to curr.
- LazyCDProofChain outer(d_pnm, true, nullptr, curr, false);
+ LazyCDProofChain outer(d_env, true, nullptr, curr, false);
outer.addLazyStep(conc, pg);
return ensureProofForFact(conc, assumps, tnk, &outer);
}
TrustNode ProofEqEngine::explain(Node conc)
{
Trace("pfee") << "pfee::explain " << conc << std::endl;
- LazyCDProof tmpProof(d_pnm, &d_proof);
+ LazyCDProof tmpProof(d_env, &d_proof);
std::vector<TNode> assumps;
explainWithProof(conc, assumps, &tmpProof);
return ensureProofForFact(conc, assumps, TrustNodeKind::PROP_EXP, &tmpProof);
return TrustNode::null();
}
// clone it so that we have a fresh copy
- pfBody = d_pnm->clone(pfBody);
+ ProofNodeManager* pnm = d_env.getProofNodeManager();
+ pfBody = pnm->clone(pfBody);
Trace("pfee-proof") << "pfee::ensureProofForFact: add scope" << std::endl;
// The free assumptions must be closed by assumps, which should be passed
// as arguments of SCOPE. However, some of the free assumptions may not
}
// Scope the proof constructed above, and connect the formula with the proof
// minimize the assumptions.
- pf = d_pnm->mkScope(pfBody, scopeAssumps, true, true);
+ pf = pnm->mkScope(pfBody, scopeAssumps, true, true);
// If we have no assumptions, and are proving an explanation for propagation
if (scopeAssumps.empty() && tnk == TrustNodeKind::PROP_EXP)
{
// minimize here, since we already ensured the proof was closed above, and
// we do not want to minimize, or else "true" would be omitted.
scopeAssumps.push_back(nm->mkConst(true));
- pf = d_pnm->mkScope(pf, scopeAssumps, false);
+ pf = pnm->mkScope(pf, scopeAssumps, false);
}
exp = nm->mkAnd(scopeAssumps);
// Make the lemma or conflict node. This must exactly match the conclusion
* - explain, for explaining why a literal is true in the current state.
* Details on these methods can be found below.
*/
-class ProofEqEngine : protected EnvObj, public EagerProofGenerator
+class ProofEqEngine : public EagerProofGenerator
{
typedef context::CDHashSet<Node> NodeSet;
typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofMap;
/** common nodes */
Node d_true;
Node d_false;
- /** the proof node manager */
- ProofNodeManager* d_pnm;
/** The SAT-context-dependent proof object */
LazyCDProof d_proof;
/**
opts.writeSmt().produceProofs = true;
Env env(NodeManager::currentNM(), &opts);
smt::PfManager pfm(env);
+ env.finishInit(pfm.getProofNodeManager());
EXPECT_TRUE(env.isTheoryProofProducing());
// register checkers that we need
builtin::BuiltinProofRuleChecker btchecker(env);
projects / cvc5.git / commitdiff