From 40fd0e4c958b215a3eba9da17f6f194cacb021be Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 10 Jun 2020 19:44:33 -0500 Subject: [PATCH] (proof-new) Add eager proof generator utility. (#4592) Adds the eager proof generator. This lives in theory/ since it has utilities for generating TrustNode, which is specific to theory/. --- src/CMakeLists.txt | 2 + src/theory/eager_proof_generator.cpp | 125 +++++++++++++++++++ src/theory/eager_proof_generator.h | 178 +++++++++++++++++++++++++++ 3 files changed, 305 insertions(+) create mode 100644 src/theory/eager_proof_generator.cpp create mode 100644 src/theory/eager_proof_generator.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0ed3934a7..3872e2b42 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -432,6 +432,8 @@ libcvc4_add_sources( theory/decision_manager.h theory/decision_strategy.cpp theory/decision_strategy.h + theory/eager_proof_generator.cpp + theory/eager_proof_generator.h theory/evaluator.cpp theory/evaluator.h theory/ext_theory.cpp diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp new file mode 100644 index 000000000..27bc9f5ca --- /dev/null +++ b/src/theory/eager_proof_generator.cpp @@ -0,0 +1,125 @@ +/********************* */ +/*! \file eager_proof_generator.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 the abstract proof generator class + **/ + +#include "theory/eager_proof_generator.h" + +#include "expr/proof_node_manager.h" + +namespace CVC4 { +namespace theory { + +EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm, + context::Context* c) + : d_pnm(pnm), d_proofs(c == nullptr ? &d_context : c) +{ +} + +void EagerProofGenerator::setProofFor(Node f, std::shared_ptr pf) +{ + // pf should prove f + Assert(pf->getResult() == f); + d_proofs[f] = pf; +} +void EagerProofGenerator::setProofForConflict(Node conf, + std::shared_ptr pf) +{ + // Normalize based on key + Node ckey = TrustNode::getConflictProven(conf); + setProofFor(ckey, pf); +} + +void EagerProofGenerator::setProofForLemma(Node lem, + std::shared_ptr pf) +{ + // Normalize based on key + Node lkey = TrustNode::getLemmaProven(lem); + setProofFor(lkey, pf); +} + +void EagerProofGenerator::setProofForPropExp(TNode lit, + Node exp, + std::shared_ptr pf) +{ + // Normalize based on key + Node pekey = TrustNode::getPropExpProven(lit, exp); + setProofFor(pekey, pf); +} + +std::shared_ptr EagerProofGenerator::getProofFor(Node f) +{ + NodeProofNodeMap::iterator it = d_proofs.find(f); + if (it == d_proofs.end()) + { + return nullptr; + } + return (*it).second; +} + +bool EagerProofGenerator::hasProofFor(Node f) +{ + return d_proofs.find(f) != d_proofs.end(); +} + +TrustNode EagerProofGenerator::mkTrustNode(Node n, + std::shared_ptr pf, + bool isConflict) +{ + if (pf == nullptr) + { + return TrustNode::null(); + } + if (isConflict) + { + // this shouldnt modify the key + setProofForConflict(n, pf); + // we can now return the trust node + return TrustNode::mkTrustConflict(n, this); + } + // this shouldnt modify the key + setProofForLemma(n, pf); + // we can now return the trust node + return TrustNode::mkTrustLemma(n, this); +} + +TrustNode EagerProofGenerator::mkTrustNode(Node n, + PfRule id, + const std::vector& args, + bool isConflict) +{ + std::vector> children; + std::shared_ptr pf = d_pnm->mkNode(id, children, args, n); + return mkTrustNode(n, pf, isConflict); +} + +TrustNode EagerProofGenerator::mkTrustedPropagation( + Node n, Node exp, std::shared_ptr pf) +{ + if (pf == nullptr) + { + return TrustNode::null(); + } + setProofForPropExp(n, exp, pf); + return TrustNode::mkTrustPropExp(n, exp, this); +} + +TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f) +{ + // make the lemma + Node lem = f.orNode(f.notNode()); + std::vector args; + return mkTrustNode(lem, PfRule::SPLIT, args, false); +} + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h new file mode 100644 index 000000000..aef377bf0 --- /dev/null +++ b/src/theory/eager_proof_generator.h @@ -0,0 +1,178 @@ +/********************* */ +/*! \file eager_proof_generator.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 The eager proof generator class + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__EAGER_PROOF_GENERATOR_H +#define CVC4__THEORY__EAGER_PROOF_GENERATOR_H + +#include "context/cdhashmap.h" +#include "expr/node.h" +#include "expr/proof_generator.h" +#include "expr/proof_node.h" +#include "theory/trust_node.h" + +namespace CVC4 { +namespace theory { + +/** + * An eager proof generator, with explicit proof caching. + * + * The intended use of this class is to store proofs for lemmas and conflicts + * at the time they are sent out on the ProofOutputChannel. This means that the + * getProofForConflict and getProofForLemma methods are lookups in a + * (user-context depedent) map, the field d_proofs below. + * + * In detail, the method setProofForConflict(conf, pf) should be called prior to + * calling ProofOutputChannel(TrustNode(conf,X)), where X is this generator. + * Similarly for setProofForLemma. + * + * The intended usage of this class in combination with OutputChannel is + * the following: + * //----------------------------------------------------------- + * class MyEagerProofGenerator : public EagerProofGenerator + * { + * public: + * TrustNode getProvenConflictByMethodX(...) + * { + * // construct a conflict + * Node conf = [construct conflict]; + * // construct a proof for conf + * std::shared_ptr pf = [construct the proof for conf]; + * // wrap the conflict in a trust node + * return mkTrustNode(conf,pf); + * } + * }; + * // [1] Make objects given user context u and output channel out. + * + * MyEagerProofGenerator epg(u); + * OutputChannel out; + * + * // [2] Assume epg realizes there is a conflict. We have it store the proof + * // internally and return the conflict node paired with epg. + * + * TrustNode pconf = epg.getProvenConflictByMethodX(...); + * + * // [3] Send the conflict on the output channel. + * + * out.trustedConflict(pconf); + * + * // [4] The trust node has information about what is proven and who can + * // prove it, where this association is valid in the remainder of the user + * // context. + * + * Node conf = pconf.getProven(); + * ProofGenerator * pg = pconf.getGenerator(); + * std::shared_ptr pf = pg->getProofForConflict(conf); + * //----------------------------------------------------------- + * In other words, the proof generator epg is responsible for creating and + * storing the proof internally, and the proof output channel is responsible for + * maintaining the map that epg is who to ask for the proof of the conflict. + */ +class EagerProofGenerator : public ProofGenerator +{ + typedef context::CDHashMap, NodeHashFunction> + NodeProofNodeMap; + + public: + EagerProofGenerator(ProofNodeManager* pnm, context::Context* c = nullptr); + ~EagerProofGenerator() {} + /** Get the proof for formula f. */ + std::shared_ptr getProofFor(Node f) override; + /** Can we give the proof for formula f? */ + bool hasProofFor(Node f) override; + /** + * Set proof for fact f, called when pf is a proof of f. + * + * @param f The fact proven by pf, + * @param pf The proof to store in this class. + */ + void setProofFor(Node f, std::shared_ptr pf); + /** + * Make trust node: wrap n in a trust node with this generator, and have it + * store the proof pf to lemma or conflict n. + * + * @param n The proven node, + * @param pf The proof of n, + * @param isConflict Whether the returned trust node is a conflict (otherwise + * it is a lemma), + * @return The trust node corresponding to the fact that this generator has + * a proof of n. + */ + TrustNode mkTrustNode(Node n, + std::shared_ptr pf, + bool isConflict = false); + /** + * Make trust node from a single step proof (with no premises). This is a + * convenience function that avoids the need to explictly construct ProofNode + * by the caller. + * + * @param n The proven node, + * @param id The rule of the proof concluding n + * @param args The arguments to the proof concluding n, + * @param isConflict Whether the returned trust node is a conflict (otherwise + * it is a lemma), + * @return The trust node corresponding to the fact that this generator has + * a proof of n. + */ + TrustNode mkTrustNode(Node n, + PfRule id, + const std::vector& args, + bool isConflict = false); + /** + * Make trust node: wrap `exp => n` in a trust node with this generator, and + * have it store the proof `pf` too. + * + * @param n The implication + * @param exp A conjunction of literals that imply it + * @param pf The proof of exp => n, + * @return The trust node corresponding to the fact that this generator has + * a proof of exp => n. + */ + TrustNode mkTrustedPropagation(Node n, + Node exp, + std::shared_ptr pf); + //--------------------------------------- common proofs + /** + * This returns the trust node corresponding to the splitting lemma + * (or f (not f)) and this generator. The method registers its proof in the + * map maintained by this class. + */ + TrustNode mkTrustNodeSplit(Node f); + //--------------------------------------- end common proofs + /** identify */ + std::string identify() const override { return "EagerProofGenerator"; } + + protected: + /** Set that pf is the proof for conflict conf */ + void setProofForConflict(Node conf, std::shared_ptr pf); + /** Set that pf is the proof for lemma lem */ + void setProofForLemma(Node lem, std::shared_ptr pf); + /** Set that pf is the proof for explained propagation */ + void setProofForPropExp(TNode lit, Node exp, std::shared_ptr pf); + /** The proof node manager */ + ProofNodeManager* d_pnm; + /** A dummy context used by this class if none is provided */ + context::Context d_context; + /** + * A user-context-dependent map from lemmas and conflicts to proofs provided + * by calls to setProofForConflict and setProofForLemma above. + */ + NodeProofNodeMap d_proofs; +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__PROOF_GENERATOR_H */ -- 2.30.2