From ad87bbc615944514fcfcb3689768aab60a9cc9d6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 11 Jun 2020 12:47:30 -0500 Subject: (proof-new) Add lazy proof utility (#4589) Adds an extension of CDProof where facts can be mapped to (lazy) proof generators. --- src/expr/CMakeLists.txt | 2 + src/expr/lazy_proof.cpp | 179 ++++++++++++++++++++++++++++++++++++++++++++++++ src/expr/lazy_proof.h | 101 +++++++++++++++++++++++++++ 3 files changed, 282 insertions(+) create mode 100644 src/expr/lazy_proof.cpp create mode 100644 src/expr/lazy_proof.h diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 2e02586ce..3d74d0bad 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -15,6 +15,8 @@ libcvc4_add_sources( expr_sequence.cpp expr_sequence.h kind_map.h + lazy_proof.cpp + lazy_proof.h match_trie.cpp match_trie.h node.cpp diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp new file mode 100644 index 000000000..ae0ddbbfa --- /dev/null +++ b/src/expr/lazy_proof.cpp @@ -0,0 +1,179 @@ +/********************* */ +/*! \file lazy_proof.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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.h" + +using namespace CVC4::kind; + +namespace CVC4 { + +LazyCDProof::LazyCDProof(ProofNodeManager* pnm, + ProofGenerator* dpg, + context::Context* c) + : CDProof(pnm, c), d_gens(c ? c : &d_context), d_defaultGen(dpg) +{ +} + +LazyCDProof::~LazyCDProof() {} + +std::shared_ptr LazyCDProof::mkProof(Node fact) +{ + Trace("lazy-cdproof") << "LazyCDProof::mkLazyProof " << fact << std::endl; + // make the proof, which should always be non-null, since we construct an + // assumption in the worst case. + std::shared_ptr opf = CDProof::mkProof(fact); + Assert(opf != nullptr); + if (!hasGenerators()) + { + Trace("lazy-cdproof") << "...no generators, finished" << std::endl; + // optimization: no generators, we are done + return opf; + } + // otherwise, we traverse the proof opf and fill in the ASSUME leafs that + // have generators + std::unordered_set visited; + std::unordered_set::iterator it; + std::vector visit; + ProofNode* cur; + visit.push_back(opf.get()); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + + if (it == visited.end()) + { + visited.insert(cur); + if (cur->getRule() == PfRule::ASSUME) + { + Node afact = cur->getResult(); + bool isSym = false; + ProofGenerator* pg = getGeneratorFor(afact, 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: Failed added fact for " + << afactGen << std::endl; + Assert(false) << "Proof generator " << pg->identify() + << " could not add proof for fact " << afactGen + << std::endl; + } + else + { + Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for " + << afactGen << std::endl; + } + } + else + { + Trace("lazy-cdproof") + << "LazyCDProof: No generator for " << afact << 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 + // the proofs from provided proof generators are final and need + // no further modification by this class. + } + else + { + const std::vector>& cc = cur->getChildren(); + for (const std::shared_ptr& cp : cc) + { + visit.push_back(cp.get()); + } + } + } + } while (!visit.empty()); + // we have now updated the ASSUME leafs of opf, return it + Trace("lazy-cdproof") << "...finished" << std::endl; + return opf; +} + +void LazyCDProof::addLazyStep(Node expected, + ProofGenerator* pg, + bool forceOverwrite) +{ + Assert(pg != nullptr); + if (!forceOverwrite) + { + NodeProofGeneratorMap::const_iterator it = d_gens.find(expected); + if (it != d_gens.end()) + { + // don't overwrite something that is already there + return; + } + } + // just store now + d_gens.insert(expected, pg); +} + +ProofGenerator* LazyCDProof::getGeneratorFor(Node fact, + bool& isSym) +{ + isSym = false; + NodeProofGeneratorMap::const_iterator it = d_gens.find(fact); + if (it != d_gens.end()) + { + return (*it).second; + } + Node factSym = CDProof::getSymmFact(fact); + // could be symmetry + if (factSym.isNull()) + { + // can't be symmetry, return the default generator + return d_defaultGen; + } + it = d_gens.find(factSym); + if (it != d_gens.end()) + { + isSym = true; + return (*it).second; + } + // return the default generator + return d_defaultGen; +} + +bool LazyCDProof::hasGenerators() const +{ + return !d_gens.empty() || d_defaultGen != nullptr; +} + +bool LazyCDProof::hasGenerator(Node fact) const +{ + if (d_defaultGen != nullptr) + { + return true; + } + NodeProofGeneratorMap::const_iterator it = d_gens.find(fact); + if (it != d_gens.end()) + { + return true; + } + // maybe there is a symmetric fact? + Node factSym = CDProof::getSymmFact(fact); + if (!factSym.isNull()) + { + it = d_gens.find(factSym); + } + return it != d_gens.end(); +} + +} // namespace CVC4 diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h new file mode 100644 index 000000000..d12aa1ac8 --- /dev/null +++ b/src/expr/lazy_proof.h @@ -0,0 +1,101 @@ +/********************* */ +/*! \file lazy_proof.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__LAZY_PROOF_H +#define CVC4__EXPR__LAZY_PROOF_H + +#include +#include + +#include "expr/proof.h" +#include "expr/proof_generator.h" +#include "expr/proof_node_manager.h" + +namespace CVC4 { + +/** + * A (context-dependent) lazy proof. This class is an extension of CDProof + * that additionally maps facts to proof generators in a context-dependent + * manner. It extends CDProof with an additional method, addLazyStep for adding + * steps to a proof via a given proof generator. + */ +class LazyCDProof : public CDProof +{ + public: + /** Constructor + * + * @param pnm The proof node manager for constructing ProofNode objects. + * @param dpg The (optional) default proof generator, which is called + * for facts that have no explicitly provided generator. + * @param c The context that this class depends on. If none is provided, + * this class is context-independent. + */ + LazyCDProof(ProofNodeManager* pnm, + ProofGenerator* dpg = nullptr, + context::Context* c = nullptr); + ~LazyCDProof(); + /** + * Get lazy proof for fact, or nullptr if it does not exist. This may + * additionally call proof generators to generate proofs for ASSUME nodes that + * don't yet have a concrete proof. + */ + std::shared_ptr mkProof(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). + * + * It is important to note that pg is asked to provide a proof for expected + * only when no other call for the fact expected is provided via the addStep + * method of this class. In particular, pg is asked to prove expected when it + * appears as the conclusion of an ASSUME leaf within CDProof::mkProof. + * + * @param expected The fact that can be proven. + * @param pg The generator that can proof expected. + * @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 forceOverwrite = false); + /** + * Does this have any proof generators? This method always returns true + * if the default is non-null. + */ + bool hasGenerators() const; + /** Does the given fact have an explicitly provided generator? */ + bool hasGenerator(Node fact) const; + + protected: + typedef context::CDHashMap + NodeProofGeneratorMap; + /** Maps facts that can be proven to generators */ + NodeProofGeneratorMap d_gens; + /** The default proof generator */ + ProofGenerator* d_defaultGen; + /** + * Get generator for fact, or nullptr if it doesnt exist. This method is + * robust to symmetry of (dis)equality. It updates isSym to true if a + * proof generator for the symmetric form of fact was provided. + */ + ProofGenerator* getGeneratorFor(Node fact, bool& isSym); +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__LAZY_PROOF_H */ -- cgit v1.2.3