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.
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)
{
}
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<ProofNode> 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
} 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)
{
// 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
}
// 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,
return it != d_gens.end();
}
-std::string LazyCDProof::identify() const { return "LazyCDProof"; }
-
} // namespace CVC4
*/
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
*
* @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.
*/
void addLazyStep(Node expected,
ProofGenerator* pg,
+ bool isClosed = true,
+ const char* ctx = "LazyCDProof::addLazyStep",
bool forceOverwrite = false,
PfRule trustId = PfRule::ASSUME);
/**
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<Node, ProofGenerator*, NodeHashFunction>
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)
{
}
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());
return polarity ? symFact : symFact.notNode();
}
-std::string CDProof::identify() const { return "CDProof"; }
+std::string CDProof::identify() const { return d_name; }
} // 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.
* 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<ProofNode> getProof(Node fact) const;
/**
* Get symmetric fact (a g such that isSame returns true for isSame(f,g)), or
* null if none exist.
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<ProofNode> getProof(Node fact) const;
+ /** Name identifier */
+ std::string d_name;
/** Ensure fact sym */
std::shared_ptr<ProofNode> getProofSymm(Node fact);
/**
#include "expr/proof_generator.h"
#include "expr/proof.h"
+#include "expr/proof_node_algorithm.h"
+#include "options/smt_options.h"
namespace CVC4 {
return false;
}
+void pfgEnsureClosed(Node proven,
+ ProofGenerator* pg,
+ const char* c,
+ const char* ctx,
+ bool reqGen)
+{
+ std::vector<Node> assumps;
+ pfgEnsureClosedWrt(proven, pg, assumps, c, ctx, reqGen);
+}
+
+void pfgEnsureClosedWrt(Node proven,
+ ProofGenerator* pg,
+ const std::vector<Node>& 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<ProofNode> 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<Node> 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
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<Node>& assumps,
+ const char* c,
+ const char* ctx,
+ bool reqGen = true);
+
} // namespace CVC4
#endif /* CVC4__EXPR__PROOF_GENERATOR_H */
return out;
}
+size_t PfRuleHashFunction::operator()(PfRule id) const
+{
+ return static_cast<size_t>(id);
+}
+
} // namespace CVC4
*/
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 */
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)
{
}
return Node::null();
}
d_rewriteMap[t] = s;
+ if (d_cpolicy == TConvCachePolicy::DYNAMIC)
+ {
+ // clear the cache
+ d_cache.clear();
+ }
return t.eqNode(s);
}
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)
{
std::unordered_map<TNode, Node, TNodeHashFunction> rewritten;
std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
std::unordered_map<TNode, Node, TNodeHashFunction>::iterator itr;
+ std::map<Node, std::shared_ptr<ProofNode> >::iterator itc;
std::vector<TNode> visit;
TNode cur;
visit.push_back(t);
{
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();
Assert(d_policy == TConvPolicy::ONCE);
// not rewriting again, rcur is final
visited[cur] = rcur;
+ doCache(cur, rcur, pf);
}
}
else
pf.addStep(result, PfRule::TRANS, pfChildren, {});
}
visited[cur] = rcurFinal;
+ doCache(cur, rcurFinal, pf);
}
else
{
{
// it is final
visited[cur] = ret;
+ doCache(cur, ret, 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);
}
return (*it).second;
}
-std::string TConvProofGenerator::identify() const
-{
- return "TConvProofGenerator";
-}
+std::string TConvProofGenerator::identify() const { return d_name; }
} // namespace CVC4
/** 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.
*
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.
* 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<Node, std::shared_ptr<ProofNode> > 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
* 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
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"
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"));
}
}
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
static bool hasNestedTermChildren( TNode node );
/** A proof node manager */
- std::unique_ptr<ProofNodeManager> d_pnm;
+ ProofNodeManager* d_pnm;
/**
* A proof generator for the term conversion.
*/
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")
{
}
// (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);
}
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)
{
}
const std::vector<Node>& args,
bool isConflict)
{
- std::vector<std::shared_ptr<ProofNode>> children;
- std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, children, args, n);
+ std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, n);
return mkTrustNode(n, pf, isConflict);
}
{
// make the lemma
Node lem = f.orNode(f.notNode());
- std::vector<Node> 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
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<ProofNode> getProofFor(Node f) override;
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 */
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 */
context::Context d_context;
/**
projects / cvc5.git / commitdiff