A proof generator to facilitate connection of locally independent but globally dependent proofs. In particular this will be used to model the resolution chains done in Minisat.
kind_map.h
lazy_proof.cpp
lazy_proof.h
+ lazy_proof_chain.cpp
+ lazy_proof_chain.h
match_trie.cpp
match_trie.h
node.cpp
--- /dev/null
+/********************* */
+/*! \file lazy_proof_chain.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of lazy proof utility
+ **/
+
+#include "expr/lazy_proof_chain.h"
+
+#include "expr/proof.h"
+#include "expr/proof_node_algorithm.h"
+#include "options/smt_options.h"
+
+namespace CVC4 {
+
+LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm,
+ bool cyclic,
+ context::Context* c)
+ : d_manager(pnm), d_cyclic(cyclic), d_context(), d_gens(c ? c : &d_context)
+{
+}
+
+LazyCDProofChain::~LazyCDProofChain() {}
+
+std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
+{
+ Trace("lazy-cdproofchain")
+ << "LazyCDProofChain::getProofFor " << fact << "\n";
+ // which facts have had proofs retrieved for. This is maintained to avoid
+ // cycles. It also saves the proof node of the fact
+ std::unordered_map<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
+ toConnect;
+ // leaves of proof node links in the chain, i.e. assumptions, yet to be
+ // expanded
+ std::unordered_map<Node,
+ std::vector<std::shared_ptr<ProofNode>>,
+ NodeHashFunction>
+ assumptionsToExpand;
+ // invariant of the loop below, the first iteration notwhistanding:
+ // visit = domain(assumptionsToExpand) \ domain(toConnect)
+ std::vector<Node> visit{fact};
+ std::unordered_map<Node, bool, NodeHashFunction> visited;
+ Node cur;
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ auto itVisited = visited.find(cur);
+ // pre-traversal
+ if (itVisited == visited.end())
+ {
+ Trace("lazy-cdproofchain")
+ << "LazyCDProofChain::getProofFor: check " << cur << "\n";
+ ProofGenerator* pg = getGeneratorFor(cur);
+ if (!pg)
+ {
+ Trace("lazy-cdproofchain")
+ << "LazyCDProofChain::getProofFor: nothing to do\n";
+ // nothing to do for this fact, it'll be a leaf in the final proof node,
+ // don't post-traverse.
+ visited[cur] = true;
+ continue;
+ }
+ Trace("lazy-cdproofchain")
+ << "LazyCDProofChain::getProofFor: Call generator " << pg->identify()
+ << " for chain link " << cur << "\n";
+ std::shared_ptr<ProofNode> curPfn = pg->getProofFor(cur);
+ Trace("lazy-cdproofchain-debug")
+ << "LazyCDProofChain::getProofFor: stored proof: " << *curPfn.get()
+ << "\n";
+ // retrieve free assumptions and their respective proof nodes
+ std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
+ expr::getFreeAssumptionsMap(curPfn, famap);
+ if (Trace.isOn("lazy-cdproofchain"))
+ {
+ Trace("lazy-cdproofchain")
+ << "LazyCDProofChain::getProofFor: free assumptions:\n";
+ for (auto fap : famap)
+ {
+ Trace("lazy-cdproofchain")
+ << "LazyCDProofChain::getProofFor: - " << fap.first << "\n";
+ }
+ }
+ // map node whose proof node must be expanded to the respective poof node
+ toConnect[cur] = curPfn;
+ // mark for post-traversal if we are controlling cycles
+ if (d_cyclic)
+ {
+ visit.push_back(cur);
+ visited[cur] = false;
+ Trace("lazy-cdproofchain") << push;
+ Trace("lazy-cdproofchain-debug") << push;
+ }
+ else
+ {
+ visited[cur] = true;
+ }
+ // enqueue free assumptions to process
+ for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
+ fap : famap)
+ {
+ // check cycles, which are cases in which the assumption has already
+ // been marked to be connected but we have not finished processing the
+ // nodes it depends on
+ if (d_cyclic && toConnect.find(fap.first) != toConnect.end()
+ && std::find(visit.begin(), visit.end(), fap.first) != visit.end())
+ {
+ // Since we have a cycle with an assumption, this fact will be an
+ // assumption in the final proof node produced by this method. This we
+ // mark the proof node it results on, i.e. its value in the toConnect
+ // map, as an assumption proof node. Note that we don't assign
+ // visited[fap.first] to true so that we properly pop the traces
+ // previously pushed.
+ Trace("lazy-cdproofchain")
+ << "LazyCDProofChain::getProofFor: removing cyclic assumption "
+ << fap.first << " from expansion\n";
+ toConnect[fap.first] = fap.second[0];
+ continue;
+ }
+ // only process further the assumptions not already in the map
+ auto it = assumptionsToExpand.find(fap.first);
+ if (it == assumptionsToExpand.end())
+ {
+ visit.push_back(fap.first);
+ }
+ // add assumption proof nodes to be updated
+ assumptionsToExpand[fap.first].insert(
+ assumptionsToExpand[fap.first].end(),
+ fap.second.begin(),
+ fap.second.end());
+ }
+ }
+ else if (!itVisited->second)
+ {
+ visited[cur] = true;
+ Trace("lazy-cdproofchain") << pop;
+ Trace("lazy-cdproofchain-debug") << pop;
+ }
+ } while (!visit.empty());
+ // expand all assumptions marked to be connected
+ for (const std::pair<const Node, std::shared_ptr<ProofNode>>& npfn :
+ toConnect)
+ {
+ auto it = assumptionsToExpand.find(npfn.first);
+ if (it == assumptionsToExpand.end())
+ {
+ Assert(npfn.first == fact);
+ continue;
+ }
+ Trace("lazy-cdproofchain")
+ << "LazyCDProofChain::getProofFor: expand assumption " << npfn.first
+ << "\n";
+ Trace("lazy-cdproofchain-debug")
+ << "LazyCDProofChain::getProofFor: ...expand to " << *npfn.second.get()
+ << "\n";
+ // update each assumption proof node
+ for (std::shared_ptr<ProofNode> pfn : it->second)
+ {
+ d_manager->updateNode(pfn.get(), npfn.second.get());
+ }
+ }
+ // final proof of fact
+ auto it = toConnect.find(fact);
+ if (it == toConnect.end())
+ {
+ return nullptr;
+ }
+ return it->second;
+}
+
+void LazyCDProofChain::addLazyStep(Node expected, ProofGenerator* pg)
+{
+ Assert(pg != nullptr);
+ Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
+ << " set to generator " << pg->identify() << "\n";
+ // note this will replace the generator for expected, if any
+ d_gens.insert(expected, pg);
+}
+
+void LazyCDProofChain::addLazyStep(Node expected,
+ ProofGenerator* pg,
+ const std::vector<Node>& assumptions,
+ const char* ctx)
+{
+ Assert(pg != nullptr);
+ Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected
+ << " set to generator " << pg->identify() << "\n";
+ // note this will rewrite the generator for expected, if any
+ d_gens.insert(expected, pg);
+ // check if chain is closed if options::proofNewEagerChecking() is on
+ if (options::proofNewEagerChecking())
+ {
+ Trace("lazy-cdproofchain")
+ << "LazyCDProofChain::addLazyStep: Checking closed proof...\n";
+ std::shared_ptr<ProofNode> pfn = pg->getProofFor(expected);
+ std::vector<Node> allowedLeaves{assumptions.begin(), assumptions.end()};
+ // add all current links in the chain
+ for (const std::pair<const Node, ProofGenerator*>& link : d_gens)
+ {
+ allowedLeaves.push_back(link.first);
+ }
+ if (Trace.isOn("lazy-cdproofchain"))
+ {
+ Trace("lazy-cdproofchain") << "Checking relative to leaves...\n";
+ for (const Node& n : allowedLeaves)
+ {
+ Trace("lazy-cdproofchain") << " - " << n << "\n";
+ }
+ Trace("lazy-cdproofchain") << "\n";
+ }
+ pfnEnsureClosedWrt(pfn.get(), allowedLeaves, "lazy-cdproofchain", ctx);
+ }
+}
+
+bool LazyCDProofChain::hasGenerator(Node fact) const
+{
+ return d_gens.find(fact) != d_gens.end();
+}
+
+ProofGenerator* LazyCDProofChain::getGeneratorFor(Node fact)
+{
+ auto it = d_gens.find(fact);
+ if (it != d_gens.end())
+ {
+ return (*it).second;
+ }
+ return nullptr;
+}
+
+std::string LazyCDProofChain::identify() const { return "LazyCDProofChain"; }
+
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file lazy_proof_chain.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Lazy proof chain utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__LAZY_PROOF_CHAIN_H
+#define CVC4__EXPR__LAZY_PROOF_CHAIN_H
+
+#include <unordered_map>
+#include <vector>
+
+#include "context/cdhashmap.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
+
+namespace CVC4 {
+
+/**
+ * A (context-dependent) lazy generator for proof chains. This class is an
+ * extension of ProofGenerator that additionally that maps facts to proof
+ * generators in a context-dependent manner. The map is built with the addition
+ * of lazy steps mapping facts to proof generators. More importantly, its
+ * getProofFor method expands the proof generators registered to this class by
+ * connecting, for the proof generated to one fact, assumptions to the proofs
+ * generated for those assumptinos that are registered in the chain.
+ */
+class LazyCDProofChain : public ProofGenerator
+{
+ public:
+ /** Constructor
+ *
+ * @param pnm The proof node manager for constructing ProofNode objects.
+ * @param cyclic Whether this instance is robust to cycles in the cahin.
+ * @param c The context that this class depends on. If none is provided,
+ * this class is context-independent.
+ */
+ LazyCDProofChain(ProofNodeManager* pnm,
+ bool cyclic = true,
+ context::Context* c = nullptr);
+ ~LazyCDProofChain();
+ /**
+ * Get lazy proof for fact, or nullptr if it does not exist, by connecting the
+ * proof nodes generated for each intermediate relevant fact registered in the
+ * chain (i.e., in the domain of d_gens).
+ *
+ * For example, if d_gens consists of the following pairs
+ *
+ * --- (A, PG1)
+ * --- (B, PG2)
+ * --- (C, PG3)
+ *
+ * and getProofFor(A) is called, with PG1 generating a proof with assumptions
+ * B and D, then B is expanded, with its assumption proof node being updated
+ * to the expanded proof node, while D is not. Assuming PG2 provides a proof
+ * with assumptions C and E, then C is expanded and E is not. Suppose PG3
+ * gives a closed proof, thus the call getProofFor(A) produces a proof node
+ *
+ * A : ( ... B : ( ... C : (...), ... ASSUME( E ) ), ... ASSUME( D ) )
+ *
+ * Note that the expansions are done directly on the proof nodes produced by
+ * the generators.
+ *
+ * If this instance has been set to be robust to cyclic proofs (i.e., d_cyclic
+ * is true), then the construction of the proof chain checks that there are no
+ * cycles, i.e., a given fact would have itself as an assumption when
+ * connecting the chain links. If such a cycle were to be detected then the
+ * fact will be marked as an assumption and not expanded in the final proof
+ * node. The method does not fail.
+ */
+ std::shared_ptr<ProofNode> getProofFor(Node fact) override;
+ /** Add step by generator
+ *
+ * This method stores that expected can be proven by proof generator pg if
+ * it is required to do so. This mapping is maintained in the remainder of
+ * the current context (according to the context c provided to this class).
+ *
+ * Moreover the lazy steps of this class are expected to fulfill the
+ * requirement that pg.getProofFor(expected) generates a proof node closed
+ * with relation to
+ * (1) a fixed set F1, ..., Fn,
+ * (2) formulas in the current domain of d_gens.
+ *
+ * This is so that we only add links to the chain that depend on a fixed set
+ * of assumptions or in other links.
+ *
+ * @param expected The fact that can be proven.
+ * @param pg The generator that can proof expected.
+ * @param assumptions The fixed set of assumptions with relation to which the
+ * chain, now augmented with expect, must be closed.
+ * @param ctx The context we are in (for debugging).
+ */
+ void addLazyStep(Node expected,
+ ProofGenerator* pg,
+ const std::vector<Node>& assumptions,
+ const char* ctx = "LazyCDProofChain::addLazyStep");
+
+ /** As above but does not do the closedness check. */
+ void addLazyStep(Node expected, ProofGenerator* pg);
+
+ /** Does the given fact have an explicitly provided generator? */
+ bool hasGenerator(Node fact) const;
+
+ /**
+ * Get generator for fact, or nullptr if it doesnt exist.
+ */
+ ProofGenerator* getGeneratorFor(Node fact);
+
+ /** identify */
+ std::string identify() const override;
+
+ private:
+ /** 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;
+ /** A dummy context used by this class if none is provided */
+ context::Context d_context;
+ /** Maps facts that can be proven to generators */
+ context::CDHashMap<Node, ProofGenerator*, NodeHashFunction> d_gens;
+};
+
+} // namespace CVC4
+
+#endif /* CVC4__EXPR__LAZY_PROOF_CHAIN_H */
void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump)
{
- std::map<Node, std::vector<ProofNode*>> amap;
- getFreeAssumptionsMap(pn, amap);
- for (const std::pair<const Node, std::vector<ProofNode*>>& p : amap)
+ std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amap;
+ std::shared_ptr<ProofNode> spn = std::make_shared<ProofNode>(
+ pn->getRule(), pn->getChildren(), pn->getArguments());
+ getFreeAssumptionsMap(spn, amap);
+ for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& p :
+ amap)
{
assump.push_back(p.first);
}
}
-void getFreeAssumptionsMap(ProofNode* pn,
- std::map<Node, std::vector<ProofNode*>>& amap)
+void getFreeAssumptionsMap(
+ std::shared_ptr<ProofNode> pn,
+ std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap)
{
// proof should not be cyclic
// visited set false after preorder traversal, true after postorder traversal
std::unordered_map<ProofNode*, bool> visited;
std::unordered_map<ProofNode*, bool>::iterator it;
- std::vector<ProofNode*> visit;
+ std::vector<std::shared_ptr<ProofNode>> visit;
// Maps a bound assumption to the number of bindings it is under
// e.g. in (SCOPE (SCOPE (ASSUME x) (x y)) (y)), y would be mapped to 2 at
// (ASSUME x), and x would be mapped to 1.
// after postvisiting SCOPE2: {}
//
std::unordered_map<Node, uint32_t, NodeHashFunction> scopeDepth;
- ProofNode* cur;
+ std::shared_ptr<ProofNode> cur;
visit.push_back(pn);
do
{
cur = visit.back();
visit.pop_back();
- it = visited.find(cur);
+ it = visited.find(cur.get());
const std::vector<Node>& cargs = cur->getArguments();
if (it == visited.end())
{
- visited[cur] = true;
+ visited[cur.get()] = true;
PfRule id = cur->getRule();
if (id == PfRule::ASSUME)
{
scopeDepth[a] += 1;
}
// will need to unbind the variables below
- visited[cur] = false;
+ visited[cur.get()] = false;
visit.push_back(cur);
}
// The following loop cannot be merged with the loop above because the
const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
for (const std::shared_ptr<ProofNode>& cp : cs)
{
- visit.push_back(cp.get());
+ visit.push_back(cp);
}
}
}
else if (!it->second)
{
- visited[cur] = true;
+ visited[cur.get()] = true;
Assert(cur->getRule() == PfRule::SCOPE);
// unbind its assumptions
for (const Node& a : cargs)
* @param amap The mapping to add the free asumptions of pn and their
* corresponding proof nodes to.
*/
-void getFreeAssumptionsMap(ProofNode* pn,
- std::map<Node, std::vector<ProofNode*>>& amap);
+void getFreeAssumptionsMap(
+ std::shared_ptr<ProofNode> pn,
+ std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap);
} // namespace expr
} // namespace CVC4
bool computedAcr = false;
// The free assumptions of the proof
- std::map<Node, std::vector<ProofNode*>> famap;
- expr::getFreeAssumptionsMap(pf.get(), famap);
+ std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
+ expr::getFreeAssumptionsMap(pf, famap);
std::unordered_set<Node, NodeHashFunction> acu;
- for (const std::pair<const Node, std::vector<ProofNode*>>& fa : famap)
+ for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
+ fa : famap)
{
Node a = fa.first;
if (ac.find(a) != ac.end())
children.push_back(pfaa);
std::vector<Node> args;
args.push_back(a);
- for (ProofNode* pfs : fa.second)
+ for (std::shared_ptr<ProofNode> pfs : fa.second)
{
Assert(pfs->getResult() == a);
- updateNode(pfs, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
+ updateNode(pfs.get(), PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
}
Trace("pnm-scope") << "...finished" << std::endl;
acu.insert(aMatch);
projects / cvc5.git / commitdiff