diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-25 08:41:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-25 08:41:13 -0500 |
commit | 87a64143f02c919df14baeb3c1acdd1295df50e9 (patch) | |
tree | 8a60d9db3d7b37f5436caf456719d4fbc340ef98 /src/proof/conv_seq_proof_generator.h | |
parent | 23c30f6961f9b19d656a3fb513134ce6c50b82ac (diff) | |
parent | 8e1eac35d265eacfbeb5f16be61e5d4caf45d1af (diff) |
Merge branch 'master' into issue6453issue6453
Diffstat (limited to 'src/proof/conv_seq_proof_generator.h')
-rw-r--r-- | src/proof/conv_seq_proof_generator.h | 121 |
1 files changed, 121 insertions, 0 deletions
diff --git a/src/proof/conv_seq_proof_generator.h b/src/proof/conv_seq_proof_generator.h new file mode 100644 index 000000000..8d4417134 --- /dev/null +++ b/src/proof/conv_seq_proof_generator.h @@ -0,0 +1,121 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, 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. + * **************************************************************************** + * + * Term conversion sequence proof generator utility. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__CONV_SEQ_PROOF_GENERATOR_H +#define CVC5__PROOF__CONV_SEQ_PROOF_GENERATOR_H + +#include "context/cdhashmap.h" +#include "expr/node.h" +#include "proof/proof_generator.h" +#include "proof/trust_node.h" + +namespace cvc5 { + +class ProofNodeManager; + +/** + * The term conversion sequence proof generator. This is used for maintaining + * a fixed sequence of proof generators that provide proofs for rewrites + * (equalities). We call these the "component generators" of this sequence, + * which are typically TConvProofGenerator. + */ +class TConvSeqProofGenerator : public ProofGenerator +{ + public: + /** + * @param pnm The proof node manager for constructing ProofNode objects. + * @param ts The list of component term conversion generators that are + * applied in sequence + * @param c The context that this class depends on. If none is provided, + * this class is context-independent. + * @param name The name of this generator (for debugging). + */ + TConvSeqProofGenerator(ProofNodeManager* pnm, + const std::vector<ProofGenerator*>& ts, + context::Context* c = nullptr, + std::string name = "TConvSeqProofGenerator"); + ~TConvSeqProofGenerator(); + /** + * Indicate that the index^th proof generator converts term t to s. This + * should be called for a unique s for each (t, index). It must be the + * case that d_tconv[index] can provide a proof for t = s in the remainder + * of the context maintained by this class. + */ + void registerConvertedTerm(Node t, Node s, size_t index); + /** + * Get the proof for formula f. It should be the case that f is of the form + * t_0 = t_n, where it must be the case that t_n is obtained by the following: + * For each i=0, ... n, let t_{i+1} be the term such that + * registerConvertedTerm(t_i, t_{i+1}, i) + * was called. Otherwise t_{i+1} = t_i. + * In other words, t_n is obtained by converting t_0, in order, based on the + * calls to registerConvertedTerm. + * + * @param f The equality fact to get the proof for. + * @return The proof for f. + */ + std::shared_ptr<ProofNode> getProofFor(Node f) override; + /** + * Get subsequence proof for f, with given start and end steps (inclusive). + */ + std::shared_ptr<ProofNode> getSubsequenceProofFor(Node f, + size_t start, + size_t end); + /** Identify this generator (for debugging, etc..) */ + std::string identify() const override; + + /** + * Make trust node from a sequence of converted terms. The number of + * terms in cterms should be 1 + the number of component proof generators + * maintained by this class. This selects a proof generator that is capable + * of proving cterms[0] = cterms[cterms.size()-1], which is either this + * generator, or one of the component proof generators, if only one step + * rewrote. In the former case, all steps are registered to this class. + * Using a component generator is an optimization that saves having to + * save the conversion steps or use this class. For example, if we have 2 + * term conversion components, and call this method on: + * { a, b, c } + * then this method calls: + * registerConvertedTerm( a, b, 0 ) + * registerConvertedTerm( b, c, 1 ) + * and returns a trust node proving (= a c) with this class as the proof + * generator. On the other hand, if we call this method on: + * { d, d, e } + * then we return a trust node proving (= d e) with the 2nd component proof + * generator, as it alone is capable of proving this equality. + */ + theory::TrustNode mkTrustRewriteSequence(const std::vector<Node>& cterms); + + protected: + using NodeIndexPairHashFunction = + PairHashFunction<Node, size_t, std::hash<Node>>; + typedef context:: + CDHashMap<std::pair<Node, size_t>, Node, NodeIndexPairHashFunction> + NodeIndexNodeMap; + /** The proof node manager */ + ProofNodeManager* d_pnm; + /** The term conversion generators */ + std::vector<ProofGenerator*> d_tconvs; + /** the set of converted terms */ + NodeIndexNodeMap d_converted; + /** Name identifier */ + std::string d_name; +}; + +} // namespace cvc5 + +#endif /* CVC5__PROOF__CONV_SEQ_PROOF_GENERATOR_H */ |