diff options
Diffstat (limited to 'src/proof/eager_proof_generator.h')
-rw-r--r-- | src/proof/eager_proof_generator.h | 197 |
1 files changed, 197 insertions, 0 deletions
diff --git a/src/proof/eager_proof_generator.h b/src/proof/eager_proof_generator.h new file mode 100644 index 000000000..ada48d893 --- /dev/null +++ b/src/proof/eager_proof_generator.h @@ -0,0 +1,197 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Alex Ozdemir, Gereon Kremer + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * The eager proof generator class. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__EAGER_PROOF_GENERATOR_H +#define CVC5__PROOF__EAGER_PROOF_GENERATOR_H + +#include "context/cdhashmap.h" +#include "expr/node.h" +#include "proof/proof_generator.h" +#include "proof/proof_rule.h" +#include "proof/trust_node.h" + +namespace cvc5 { + +class ProofNode; +class ProofNodeManager; + +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<ProofNode> 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<ProofNode> 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<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap; + + public: + 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; + /** 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<ProofNode> 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<ProofNode> pf, + bool isConflict = false); + /** + * Make trust node from a single step proof. This is a convenience function + * that avoids the need to explictly construct ProofNode by the caller. + * + * @param conc The conclusion of the rule, + * @param id The rule of the proof concluding conc + * @param exp The explanation (premises) to the proof concluding conc, + * @param args The arguments to the proof concluding conc, + * @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 (exp => conc), or of conc if exp is empty. + */ + TrustNode mkTrustNode(Node conc, + PfRule id, + const std::vector<Node>& exp, + const std::vector<Node>& 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<ProofNode> pf); + /** + * Make trust node: `a = b` as a Rewrite trust node + * + * @param a the original + * @param b what is rewrites to + * @param pf The proof of a = b, + * @return The trust node corresponding to the fact that this generator has + * a proof of a = b + */ + TrustNode mkTrustedRewrite(Node a, Node b, std::shared_ptr<ProofNode> 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; + + protected: + /** Set that pf is the proof for conflict conf */ + void setProofForConflict(Node conf, std::shared_ptr<ProofNode> pf); + /** Set that pf is the proof for lemma lem */ + void setProofForLemma(Node lem, std::shared_ptr<ProofNode> pf); + /** Set that pf is the proof for explained propagation */ + 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; + /** + * 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 cvc5 + +#endif /* CVC5__PROOF__PROOF_GENERATOR_H */ |