From 5557985d7320668b2625f1559f907488e2a85590 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 16 Sep 2020 13:25:33 -0300 Subject: [PATCH] [proof-new] Adds Lazy CDProof chain data-structure (#5060) 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. --- src/expr/CMakeLists.txt | 2 + src/expr/lazy_proof_chain.cpp | 239 ++++++++++++++++++++++++++++++ src/expr/lazy_proof_chain.h | 135 +++++++++++++++++ src/expr/proof_node_algorithm.cpp | 28 ++-- src/expr/proof_node_algorithm.h | 5 +- src/expr/proof_node_manager.cpp | 11 +- 6 files changed, 401 insertions(+), 19 deletions(-) create mode 100644 src/expr/lazy_proof_chain.cpp create mode 100644 src/expr/lazy_proof_chain.h diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 3e3b569af..7fa8b12e7 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -17,6 +17,8 @@ libcvc4_add_sources( 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 diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp new file mode 100644 index 000000000..a01d541eb --- /dev/null +++ b/src/expr/lazy_proof_chain.cpp @@ -0,0 +1,239 @@ +/********************* */ +/*! \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 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, NodeHashFunction> + toConnect; + // leaves of proof node links in the chain, i.e. assumptions, yet to be + // expanded + std::unordered_map>, + NodeHashFunction> + assumptionsToExpand; + // invariant of the loop below, the first iteration notwhistanding: + // visit = domain(assumptionsToExpand) \ domain(toConnect) + std::vector visit{fact}; + std::unordered_map 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 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>> 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>>& + 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>& 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 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& 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 pfn = pg->getProofFor(expected); + std::vector allowedLeaves{assumptions.begin(), assumptions.end()}; + // add all current links in the chain + for (const std::pair& 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 diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h new file mode 100644 index 000000000..7fa49bccc --- /dev/null +++ b/src/expr/lazy_proof_chain.h @@ -0,0 +1,135 @@ +/********************* */ +/*! \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 +#include + +#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 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& 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 d_gens; +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__LAZY_PROOF_CHAIN_H */ diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp index 9e1018024..984379d54 100644 --- a/src/expr/proof_node_algorithm.cpp +++ b/src/expr/proof_node_algorithm.cpp @@ -19,22 +19,26 @@ namespace expr { void getFreeAssumptions(ProofNode* pn, std::vector& assump) { - std::map> amap; - getFreeAssumptionsMap(pn, amap); - for (const std::pair>& p : amap) + std::map>> amap; + std::shared_ptr spn = std::make_shared( + pn->getRule(), pn->getChildren(), pn->getArguments()); + getFreeAssumptionsMap(spn, amap); + for (const std::pair>>& p : + amap) { assump.push_back(p.first); } } -void getFreeAssumptionsMap(ProofNode* pn, - std::map>& amap) +void getFreeAssumptionsMap( + std::shared_ptr pn, + std::map>>& amap) { // proof should not be cyclic // visited set false after preorder traversal, true after postorder traversal std::unordered_map visited; std::unordered_map::iterator it; - std::vector visit; + std::vector> 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. @@ -54,17 +58,17 @@ void getFreeAssumptionsMap(ProofNode* pn, // after postvisiting SCOPE2: {} // std::unordered_map scopeDepth; - ProofNode* cur; + std::shared_ptr cur; visit.push_back(pn); do { cur = visit.back(); visit.pop_back(); - it = visited.find(cur); + it = visited.find(cur.get()); const std::vector& cargs = cur->getArguments(); if (it == visited.end()) { - visited[cur] = true; + visited[cur.get()] = true; PfRule id = cur->getRule(); if (id == PfRule::ASSUME) { @@ -85,7 +89,7 @@ void getFreeAssumptionsMap(ProofNode* pn, 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 @@ -93,13 +97,13 @@ void getFreeAssumptionsMap(ProofNode* pn, const std::vector>& cs = cur->getChildren(); for (const std::shared_ptr& 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) diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h index bc44d7314..aec098e17 100644 --- a/src/expr/proof_node_algorithm.h +++ b/src/expr/proof_node_algorithm.h @@ -49,8 +49,9 @@ void getFreeAssumptions(ProofNode* pn, std::vector& assump); * @param amap The mapping to add the free asumptions of pn and their * corresponding proof nodes to. */ -void getFreeAssumptionsMap(ProofNode* pn, - std::map>& amap); +void getFreeAssumptionsMap( + std::shared_ptr pn, + std::map>>& amap); } // namespace expr } // namespace CVC4 diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index 0d13531a5..54315ee05 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -75,10 +75,11 @@ std::shared_ptr ProofNodeManager::mkScope( bool computedAcr = false; // The free assumptions of the proof - std::map> famap; - expr::getFreeAssumptionsMap(pf.get(), famap); + std::map>> famap; + expr::getFreeAssumptionsMap(pf, famap); std::unordered_set acu; - for (const std::pair>& fa : famap) + for (const std::pair>>& + fa : famap) { Node a = fa.first; if (ac.find(a) != ac.end()) @@ -135,10 +136,10 @@ std::shared_ptr ProofNodeManager::mkScope( children.push_back(pfaa); std::vector args; args.push_back(a); - for (ProofNode* pfs : fa.second) + for (std::shared_ptr 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); -- 2.30.2