From 2174ab36023326cd998565bbf35d31c38bc10594 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 12 Aug 2020 14:48:31 -0500 Subject: [PATCH] (proof-new) Improve interfaces to proof generators (#4803) This includes configurable naming and a caching policy for term conversion proof generator. Also corrects a subtle issue in LazyCDProof related to making getProofFor idempotent using the notion of owned proofs. --- src/expr/lazy_proof.cpp | 66 +++++++++----- src/expr/lazy_proof.h | 10 ++- src/expr/proof.cpp | 14 +-- src/expr/proof.h | 10 ++- src/expr/proof_generator.cpp | 91 ++++++++++++++++++++ src/expr/proof_generator.h | 27 ++++++ src/expr/proof_rule.cpp | 5 ++ src/expr/proof_rule.h | 6 ++ src/expr/term_conversion_proof_generator.cpp | 59 +++++++++++-- src/expr/term_conversion_proof_generator.h | 31 ++++++- src/options/smt_options.toml | 9 ++ src/smt/term_formula_removal.cpp | 14 ++- src/smt/term_formula_removal.h | 6 +- src/smt/witness_form.cpp | 15 +++- src/theory/eager_proof_generator.cpp | 13 +-- src/theory/eager_proof_generator.h | 8 +- 16 files changed, 323 insertions(+), 61 deletions(-) diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp index df0258af7..dc984438c 100644 --- a/src/expr/lazy_proof.cpp +++ b/src/expr/lazy_proof.cpp @@ -20,8 +20,9 @@ namespace CVC4 { LazyCDProof::LazyCDProof(ProofNodeManager* pnm, ProofGenerator* dpg, - context::Context* c) - : CDProof(pnm, c), d_gens(c ? c : &d_context), d_defaultGen(dpg) + context::Context* c, + std::string name) + : CDProof(pnm, c, name), d_gens(c ? c : &d_context), d_defaultGen(dpg) { } @@ -56,36 +57,47 @@ std::shared_ptr LazyCDProof::getProofFor(Node fact) if (it == visited.end()) { visited.insert(cur); - if (cur->getRule() == PfRule::ASSUME) + Node cfact = cur->getResult(); + if (getProof(cfact).get() != cur) + { + // We don't own this proof, skip it. This is to ensure that this method + // is idempotent, since it may be the case that a previous call to + // getProofFor connected a proof from a proof generator as a child of + // a ProofNode in the range of the map in CDProof. Thus, this ensures + // we don't touch such proofs. + Trace("lazy-cdproof") << "...skip unowned proof" << std::endl; + } + else if (cur->getRule() == PfRule::ASSUME) { - Node afact = cur->getResult(); bool isSym = false; - ProofGenerator* pg = getGeneratorFor(afact, isSym); + ProofGenerator* pg = getGeneratorFor(cfact, isSym); if (pg != nullptr) { - Trace("lazy-cdproof") << "LazyCDProof: Call generator for assumption " - << afact << std::endl; - Node afactGen = isSym ? CDProof::getSymmFact(afact) : afact; - Assert(!afactGen.isNull()); - // use the addProofTo interface - if (!pg->addProofTo(afactGen, this)) + Trace("lazy-cdproof") + << "LazyCDProof: Call generator " << pg->identify() + << " for assumption " << cfact << std::endl; + Node cfactGen = isSym ? CDProof::getSymmFact(cfact) : cfact; + Assert(!cfactGen.isNull()); + // Do not use the addProofTo interface, instead use the update node + // interface, since this ensures that we don't take ownership for + // the current proof. Instead, it is only linked, and ignored on + // future calls to getProofFor due to the check above. + std::shared_ptr pgc = pg->getProofFor(cfactGen); + if (isSym) { - Trace("lazy-cdproof") << "LazyCDProof: Failed added fact for " - << afactGen << std::endl; - Assert(false) << "Proof generator " << pg->identify() - << " could not add proof for fact " << afactGen - << std::endl; + d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {}); } else { - Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for " - << afactGen << std::endl; + d_manager->updateNode(cur, pgc.get()); } + Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for " + << cfactGen << std::endl; } else { - Trace("lazy-cdproof") - << "LazyCDProof: No generator for " << afact << std::endl; + Trace("lazy-cdproof") << "LazyCDProof: " << identify() + << " : No generator for " << cfact << std::endl; } // Notice that we do not traverse the proofs that have been generated // lazily by the proof generators here. In other words, we assume that @@ -104,11 +116,14 @@ std::shared_ptr LazyCDProof::getProofFor(Node fact) } while (!visit.empty()); // we have now updated the ASSUME leafs of opf, return it Trace("lazy-cdproof") << "...finished" << std::endl; + Assert(opf->getResult() == fact); return opf; } void LazyCDProof::addLazyStep(Node expected, ProofGenerator* pg, + bool isClosed, + const char* ctx, bool forceOverwrite, PfRule idNull) { @@ -117,7 +132,8 @@ void LazyCDProof::addLazyStep(Node expected, // null generator, should have given a proof rule if (idNull == PfRule::ASSUME) { - Assert(false); + Unreachable() << "LazyCDProof::addLazyStep: " << identify() + << ": failed to provide proof generator for " << expected; return; } Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected @@ -138,6 +154,12 @@ void LazyCDProof::addLazyStep(Node expected, } // just store now d_gens.insert(expected, pg); + // debug checking + if (isClosed) + { + Trace("lazy-cdproof-debug") << "Checking closed..." << std::endl; + pfgEnsureClosed(expected, pg, "lazy-cdproof-debug", ctx); + } } ProofGenerator* LazyCDProof::getGeneratorFor(Node fact, @@ -191,6 +213,4 @@ bool LazyCDProof::hasGenerator(Node fact) const return it != d_gens.end(); } -std::string LazyCDProof::identify() const { return "LazyCDProof"; } - } // namespace CVC4 diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h index 1f68a3ccb..4368cbb85 100644 --- a/src/expr/lazy_proof.h +++ b/src/expr/lazy_proof.h @@ -45,7 +45,8 @@ class LazyCDProof : public CDProof */ LazyCDProof(ProofNodeManager* pnm, ProofGenerator* dpg = nullptr, - context::Context* c = nullptr); + context::Context* c = nullptr, + std::string name = "LazyCDProof"); ~LazyCDProof(); /** * Get lazy proof for fact, or nullptr if it does not exist. This may @@ -66,6 +67,9 @@ class LazyCDProof : public CDProof * * @param expected The fact that can be proven. * @param pg The generator that can proof expected. + * @param isClosed Whether to expect that pg can provide a closed proof for + * this fact. + * @param ctx The context we are in (for debugging). * @param forceOverwrite If this flag is true, then this call overwrites * an existing proof generator provided for expected, if one was provided * via a previous call to addLazyStep in the current context. @@ -76,6 +80,8 @@ class LazyCDProof : public CDProof */ void addLazyStep(Node expected, ProofGenerator* pg, + bool isClosed = true, + const char* ctx = "LazyCDProof::addLazyStep", bool forceOverwrite = false, PfRule trustId = PfRule::ASSUME); /** @@ -85,8 +91,6 @@ class LazyCDProof : public CDProof bool hasGenerators() const; /** Does the given fact have an explicitly provided generator? */ bool hasGenerator(Node fact) const; - /** identify */ - std::string identify() const override; protected: typedef context::CDHashMap diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp index 20e8e29e2..a9e6d6940 100644 --- a/src/expr/proof.cpp +++ b/src/expr/proof.cpp @@ -18,8 +18,8 @@ using namespace CVC4::kind; namespace CVC4 { -CDProof::CDProof(ProofNodeManager* pnm, context::Context* c) - : d_manager(pnm), d_context(), d_nodes(c ? c : &d_context) +CDProof::CDProof(ProofNodeManager* pnm, context::Context* c, std::string name) + : d_manager(pnm), d_context(), d_nodes(c ? c : &d_context), d_name(name) { } @@ -111,9 +111,13 @@ bool CDProof::addStep(Node expected, bool ensureChildren, CDPOverwrite opolicy) { - Trace("cdproof") << "CDProof::addStep: " << id << " " << expected - << ", ensureChildren = " << ensureChildren + Trace("cdproof") << "CDProof::addStep: " << identify() << " : " << id << " " + << expected << ", ensureChildren = " << ensureChildren << ", overwrite policy = " << opolicy << std::endl; + Trace("cdproof-debug") << "CDProof::addStep: " << identify() + << " : children: " << children << "\n"; + Trace("cdproof-debug") << "CDProof::addStep: " << identify() + << " : args: " << args << "\n"; // We must always provide expected to this method Assert(!expected.isNull()); @@ -424,6 +428,6 @@ Node CDProof::getSymmFact(TNode f) return polarity ? symFact : symFact.notNode(); } -std::string CDProof::identify() const { return "CDProof"; } +std::string CDProof::identify() const { return d_name; } } // namespace CVC4 diff --git a/src/expr/proof.h b/src/expr/proof.h index ff6b8bbf1..5fbcc4ec8 100644 --- a/src/expr/proof.h +++ b/src/expr/proof.h @@ -134,7 +134,9 @@ namespace CVC4 { class CDProof : public ProofGenerator { public: - CDProof(ProofNodeManager* pnm, context::Context* c = nullptr); + CDProof(ProofNodeManager* pnm, + context::Context* c = nullptr, + std::string name = "CDProof"); virtual ~CDProof(); /** * Make proof for fact. @@ -224,6 +226,8 @@ class CDProof : public ProofGenerator * f suffices as a proof for g according to this class. */ static bool isSame(TNode f, TNode g); + /** Get proof for fact, or nullptr if it does not exist. */ + std::shared_ptr getProof(Node fact) const; /** * Get symmetric fact (a g such that isSame returns true for isSame(f,g)), or * null if none exist. @@ -241,8 +245,8 @@ class CDProof : public ProofGenerator context::Context d_context; /** The nodes of the proof */ NodeProofNodeMap d_nodes; - /** Get proof for fact, or nullptr if it does not exist. */ - std::shared_ptr getProof(Node fact) const; + /** Name identifier */ + std::string d_name; /** Ensure fact sym */ std::shared_ptr getProofSymm(Node fact); /** diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp index be2c22c1e..7a480fa97 100644 --- a/src/expr/proof_generator.cpp +++ b/src/expr/proof_generator.cpp @@ -15,6 +15,8 @@ #include "expr/proof_generator.h" #include "expr/proof.h" +#include "expr/proof_node_algorithm.h" +#include "options/smt_options.h" namespace CVC4 { @@ -66,4 +68,93 @@ bool ProofGenerator::addProofTo(Node f, CDProof* pf, CDPOverwrite opolicy) return false; } +void pfgEnsureClosed(Node proven, + ProofGenerator* pg, + const char* c, + const char* ctx, + bool reqGen) +{ + std::vector assumps; + pfgEnsureClosedWrt(proven, pg, assumps, c, ctx, reqGen); +} + +void pfgEnsureClosedWrt(Node proven, + ProofGenerator* pg, + const std::vector& assumps, + const char* c, + const char* ctx, + bool reqGen) +{ + if (!options::proofNew()) + { + // proofs not enabled, do not do check + return; + } + bool isTraceDebug = Trace.isOn(c); + if (!options::proofNewEagerChecking() && !isTraceDebug) + { + // trace is off and proof new eager checking is off, do not do check + return; + } + std::stringstream ss; + ss << "ProofGenerator: " << (pg == nullptr ? "null" : pg->identify()) + << " in context " << ctx; + std::stringstream sdiag; + bool isTraceOn = Trace.isOn(c); + if (!isTraceOn) + { + sdiag << ", use -t " << c << " for details"; + } + Trace(c) << "=== pfgEnsureClosed: " << ss.str() << std::endl; + Trace(c) << "Proven: " << proven << std::endl; + if (pg == nullptr) + { + // only failure if flag is true + if (reqGen) + { + Unreachable() << "...pfgEnsureClosed: no generator in context " << ctx + << sdiag.str(); + } + Trace(c) << "...pfgEnsureClosed: no generator in context " << ctx + << std::endl; + return; + } + std::shared_ptr pn = pg->getProofFor(proven); + Trace(c) << " Proof: " << *pn.get() << std::endl; + if (pn == nullptr) + { + AlwaysAssert(false) << "...pfgEnsureClosed: null proof from " << ss.str() + << sdiag.str(); + } + std::vector fassumps; + expr::getFreeAssumptions(pn.get(), fassumps); + bool isClosed = true; + std::stringstream ssf; + for (const Node& fa : fassumps) + { + if (std::find(assumps.begin(), assumps.end(), fa) == assumps.end()) + { + isClosed = false; + ssf << "- " << fa << std::endl; + } + } + if (!isClosed) + { + Trace(c) << "Free assumptions:" << std::endl; + Trace(c) << ssf.str(); + if (!assumps.empty()) + { + Trace(c) << "Expected assumptions:" << std::endl; + for (const Node& a : assumps) + { + Trace(c) << "- " << a << std::endl; + } + } + } + AlwaysAssert(isClosed) << "...pfgEnsureClosed: open proof from " << ss.str() + << sdiag.str(); + Trace(c) << "...pfgEnsureClosed: success" << std::endl; + Trace(c) << "====" << std::endl; +} + } // namespace CVC4 diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h index 35f94194f..298f9b4c6 100644 --- a/src/expr/proof_generator.h +++ b/src/expr/proof_generator.h @@ -105,6 +105,33 @@ class ProofGenerator virtual std::string identify() const = 0; }; +/** + * Debug check closed on Trace c. Context ctx is string for debugging. + * This method throws an assertion failure if pg cannot provide a closed + * proof for fact proven. This is checked only if --proof-new-eager-checking + * is enabled or the Trace c is enabled. + * + * @param reqGen Whether we consider a null generator to be a failure. + */ +void pfgEnsureClosed(Node proven, + ProofGenerator* pg, + const char* c, + const char* ctx, + bool reqGen = true); + +/** + * Debug check closed with Trace c. Context ctx is string for debugging and + * assumps is the set of allowed open assertions. + * + * @param reqGen Whether we consider a null generator to be a failure. + */ +void pfgEnsureClosedWrt(Node proven, + ProofGenerator* pg, + const std::vector& assumps, + const char* c, + const char* ctx, + bool reqGen = true); + } // namespace CVC4 #endif /* CVC4__EXPR__PROOF_GENERATOR_H */ diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 9713adbec..c4b72208e 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -134,4 +134,9 @@ std::ostream& operator<<(std::ostream& out, PfRule id) return out; } +size_t PfRuleHashFunction::operator()(PfRule id) const +{ + return static_cast(id); +} + } // namespace CVC4 diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 3d468d08e..beff92bd4 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -851,6 +851,12 @@ const char* toString(PfRule id); */ std::ostream& operator<<(std::ostream& out, PfRule id); +/** Hash function for proof rules */ +struct PfRuleHashFunction +{ + size_t operator()(PfRule id) const; +}; /* struct PfRuleHashFunction */ + } // namespace CVC4 #endif /* CVC4__EXPR__PROOF_RULE_H */ diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index bad163375..1c4baeed7 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -29,10 +29,28 @@ std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol) return out; } +std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol) +{ + switch (tcpol) + { + case TConvCachePolicy::STATIC: out << "STATIC"; break; + case TConvCachePolicy::DYNAMIC: out << "DYNAMIC"; break; + case TConvCachePolicy::NEVER: out << "NEVER"; break; + default: out << "TConvCachePolicy:unknown"; break; + } + return out; +} + TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm, context::Context* c, - TConvPolicy tpol) - : d_proof(pnm, nullptr, c), d_rewriteMap(c ? c : &d_context), d_policy(tpol) + TConvPolicy pol, + TConvCachePolicy cpol, + std::string name) + : d_proof(pnm, nullptr, c, name + "::LazyCDProof"), + d_rewriteMap(c ? c : &d_context), + d_policy(pol), + d_cpolicy(cpol), + d_name(name) { } @@ -87,6 +105,11 @@ Node TConvProofGenerator::registerRewriteStep(Node t, Node s) return Node::null(); } d_rewriteMap[t] = s; + if (d_cpolicy == TConvCachePolicy::DYNAMIC) + { + // clear the cache + d_cache.clear(); + } return t.eqNode(s); } @@ -101,7 +124,8 @@ std::shared_ptr TConvProofGenerator::getProofFor(Node f) return nullptr; } // we use the existing proofs - LazyCDProof lpf(d_proof.getManager(), &d_proof); + LazyCDProof lpf( + d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProof"); Node conc = getProofForRewriting(f[0], lpf); if (conc != f) { @@ -125,6 +149,7 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf) std::unordered_map rewritten; std::unordered_map::iterator it; std::unordered_map::iterator itr; + std::map >::iterator itc; std::vector visit; TNode cur; visit.push_back(t); @@ -132,8 +157,17 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf) { cur = visit.back(); visit.pop_back(); + // has the proof for cur been cached? + itc = d_cache.find(cur); + if (itc != d_cache.end()) + { + Node res = itc->second->getResult(); + Assert(res.getKind() == EQUAL); + visited[cur] = res[1]; + pf.addProof(itc->second); + continue; + } it = visited.find(cur); - if (it == visited.end()) { visited[cur] = Node::null(); @@ -157,6 +191,7 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf) Assert(d_policy == TConvPolicy::ONCE); // not rewriting again, rcur is final visited[cur] = rcur; + doCache(cur, rcur, pf); } } else @@ -189,6 +224,7 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf) pf.addStep(result, PfRule::TRANS, pfChildren, {}); } visited[cur] = rcurFinal; + doCache(cur, rcurFinal, pf); } else { @@ -259,6 +295,7 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf) { // it is final visited[cur] = ret; + doCache(cur, ret, pf); } } } @@ -269,6 +306,15 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf) return t.eqNode(visited[t]); } +void TConvProofGenerator::doCache(Node cur, Node r, LazyCDProof& pf) +{ + if (d_cpolicy != TConvCachePolicy::NEVER) + { + Node eq = cur.eqNode(r); + d_cache[cur] = pf.getProofFor(eq); + } +} + Node TConvProofGenerator::getRewriteStep(Node t) const { NodeNodeMap::const_iterator it = d_rewriteMap.find(t); @@ -278,9 +324,6 @@ Node TConvProofGenerator::getRewriteStep(Node t) const } return (*it).second; } -std::string TConvProofGenerator::identify() const -{ - return "TConvProofGenerator"; -} +std::string TConvProofGenerator::identify() const { return d_name; } } // namespace CVC4 diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h index d7ff6e8f6..e634b8a83 100644 --- a/src/expr/term_conversion_proof_generator.h +++ b/src/expr/term_conversion_proof_generator.h @@ -35,6 +35,19 @@ enum class TConvPolicy : uint32_t /** Writes a term conversion policy name to a stream. */ std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol); +/** A policy for how proofs are cached in TConvProofGenerator */ +enum class TConvCachePolicy : uint32_t +{ + // proofs are statically cached + STATIC, + // proofs are dynamically cached, cleared when a new rewrite is added + DYNAMIC, + // proofs are never cached + NEVER, +}; +/** Writes a term conversion cache policy name to a stream. */ +std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol); + /** * The term conversion proof generator. * @@ -75,17 +88,23 @@ std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol); class TConvProofGenerator : public ProofGenerator { public: - /** Constructor + /** + * 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 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 * details, see d_policy. + * @param cpol The caching policy for this generator. + * @param name The name of this generator (for debugging). */ TConvProofGenerator(ProofNodeManager* pnm, context::Context* c = nullptr, - TConvPolicy pol = TConvPolicy::FIXPOINT); + TConvPolicy pol = TConvPolicy::FIXPOINT, + TConvCachePolicy cpol = TConvCachePolicy::NEVER, + std::string name = "TConvProofGenerator"); ~TConvProofGenerator(); /** * Add rewrite step t --> s based on proof generator. @@ -136,6 +155,12 @@ class TConvProofGenerator : public ProofGenerator * f(a,c) = f(f(c),d) if d_policy is ONCE. */ TConvPolicy d_policy; + /** The cache policy */ + TConvCachePolicy d_cpolicy; + /** Name identifier */ + std::string d_name; + /** The cache for terms */ + std::map > d_cache; /** * Adds a proof of t = t' to the proof pf where t' is the result of rewriting * t based on the rewrite steps registered to this class. This method then @@ -147,6 +172,8 @@ class TConvProofGenerator : public ProofGenerator * and a rewrite step has not already been registered for t. */ Node registerRewriteStep(Node t, Node s); + /** cache that r is the rewritten form of cur, pf can provide a proof */ + void doCache(Node cur, Node r, LazyCDProof& pf); }; } // namespace CVC4 diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index d14a8e1cf..6b5bee6bb 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -182,6 +182,15 @@ header = "options/smt_options.h" default = "false" help = "check pedantic levels eagerly (during proof rule construction) instead of during final proof construction" +[[option]] + name = "proofNewEagerChecking" + category = "regular" + long = "proof-new-eager-checking" + type = "bool" + default = "false" + read_only = true + help = "check proofs eagerly with proof-new for local debugging" + [[option]] name = "dumpInstantiations" category = "regular" diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 3f44e592e..5da190a3d 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -422,13 +422,19 @@ Node RemoveTermFormulas::getAxiomFor(Node n) return Node::null(); } -void RemoveTermFormulas::setProofChecker(ProofChecker* pc) +void RemoveTermFormulas::setProofNodeManager(ProofNodeManager* pnm) { if (d_tpg == nullptr) { - d_pnm.reset(new ProofNodeManager(pc)); - d_tpg.reset(new TConvProofGenerator(d_pnm.get())); - d_lp.reset(new LazyCDProof(d_pnm.get())); + d_pnm = pnm; + d_tpg.reset( + new TConvProofGenerator(d_pnm, + nullptr, + TConvPolicy::FIXPOINT, + TConvCachePolicy::NEVER, + "RemoveTermFormulas::TConvProofGenerator")); + d_lp.reset(new LazyCDProof( + d_pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof")); } } diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index d4c22b78b..78d5899d0 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -106,10 +106,10 @@ class RemoveTermFormulas { void garbageCollect(); /** - * Set proof checker, which signals this class to enable proofs using the + * Set proof node manager, which signals this class to enable proofs using the * given checker. */ - void setProofChecker(ProofChecker* pc); + void setProofNodeManager(ProofNodeManager* pnm); /** * Get axiom for term n. This returns the axiom that this class uses to @@ -166,7 +166,7 @@ class RemoveTermFormulas { static bool hasNestedTermChildren( TNode node ); /** A proof node manager */ - std::unique_ptr d_pnm; + ProofNodeManager* d_pnm; /** * A proof generator for the term conversion. */ diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index 891c0f731..19795119d 100644 --- a/src/smt/witness_form.cpp +++ b/src/smt/witness_form.cpp @@ -21,7 +21,12 @@ namespace CVC4 { namespace smt { WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm) - : d_tcpg(pnm), d_wintroPf(pnm) + : d_tcpg(pnm, + nullptr, + TConvPolicy::FIXPOINT, + TConvCachePolicy::NEVER, + "WfGenerator::TConvProofGenerator"), + d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof") { } @@ -89,7 +94,13 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t) // (exists ((x T)) (P x)) // --------------------------- WITNESS_INTRO // k = (witness ((x T)) (P x)) - d_wintroPf.addLazyStep(exists, pg, false, PfRule::WITNESS_AXIOM); + d_wintroPf.addLazyStep( + exists, + pg, + true, + "WitnessFormGenerator::convertToWitnessForm:witness_axiom", + false, + PfRule::WITNESS_AXIOM); d_wintroPf.addStep(eq, PfRule::WITNESS_INTRO, {exists}, {}); d_tcpg.addRewriteStep(cur, curw, &d_wintroPf); } diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp index 9c25fb3e4..09f02708b 100644 --- a/src/theory/eager_proof_generator.cpp +++ b/src/theory/eager_proof_generator.cpp @@ -20,8 +20,9 @@ namespace CVC4 { namespace theory { EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm, - context::Context* c) - : d_pnm(pnm), d_proofs(c == nullptr ? &d_context : c) + context::Context* c, + std::string name) + : d_pnm(pnm), d_name(name), d_proofs(c == nullptr ? &d_context : c) { } @@ -97,8 +98,7 @@ TrustNode EagerProofGenerator::mkTrustNode(Node n, const std::vector& args, bool isConflict) { - std::vector> children; - std::shared_ptr pf = d_pnm->mkNode(id, children, args, n); + std::shared_ptr pf = d_pnm->mkNode(id, {}, args, n); return mkTrustNode(n, pf, isConflict); } @@ -117,9 +117,10 @@ TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f) { // make the lemma Node lem = f.orNode(f.notNode()); - std::vector args; - return mkTrustNode(lem, PfRule::SPLIT, args, false); + return mkTrustNode(lem, PfRule::SPLIT, {f}, false); } +std::string EagerProofGenerator::identify() const { return d_name; } + } // namespace theory } // namespace CVC4 diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h index 9a00f3612..226750a91 100644 --- a/src/theory/eager_proof_generator.h +++ b/src/theory/eager_proof_generator.h @@ -86,7 +86,9 @@ class EagerProofGenerator : public ProofGenerator NodeProofNodeMap; public: - EagerProofGenerator(ProofNodeManager* pnm, context::Context* c = nullptr); + EagerProofGenerator(ProofNodeManager* pnm, + context::Context* c = nullptr, + std::string name = "EagerProofGenerator"); ~EagerProofGenerator() {} /** Get the proof for formula f. */ std::shared_ptr getProofFor(Node f) override; @@ -152,7 +154,7 @@ class EagerProofGenerator : public ProofGenerator TrustNode mkTrustNodeSplit(Node f); //--------------------------------------- end common proofs /** identify */ - std::string identify() const override { return "EagerProofGenerator"; } + std::string identify() const override; protected: /** Set that pf is the proof for conflict conf */ @@ -163,6 +165,8 @@ class EagerProofGenerator : public ProofGenerator void setProofForPropExp(TNode lit, Node exp, std::shared_ptr 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 */ context::Context d_context; /** -- 2.30.2