From: Andrew Reynolds Date: Wed, 30 Sep 2020 13:20:03 +0000 (-0500) Subject: (proof-new) Add the term conversion sequence generator (#5097) X-Git-Tag: cvc5-1.0.0~2784 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0cf0dc3b3661e668f8c03113faad5078d91cea98;p=cvc5.git (proof-new) Add the term conversion sequence generator (#5097) This class will be used in the theory preprocessor and is planned to be used in other preprocessing passes that can be understood as sequences of rewrite systems. --- diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 1cc4e9a33..8742612ad 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -75,6 +75,8 @@ libcvc4_add_sources( skolem_manager.h symbol_table.cpp symbol_table.h + tconv_seq_proof_generator.cpp + tconv_seq_proof_generator.h term_canonize.cpp term_canonize.h term_context.cpp diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index eb298cc83..9f60a49e4 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -56,6 +56,18 @@ std::shared_ptr ProofNodeManager::mkAssume(Node fact) return mkNode(PfRule::ASSUME, {}, {fact}, fact); } +std::shared_ptr ProofNodeManager::mkTrans( + const std::vector>& children, Node expected) +{ + Assert(!children.empty()); + if (children.size() == 1) + { + Assert(expected.isNull() || children[0]->getResult() == expected); + return children[0]; + } + return mkNode(PfRule::TRANS, children, {}, expected); +} + std::shared_ptr ProofNodeManager::mkScope( std::shared_ptr pf, std::vector& assumps, diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h index 47fdf3ebd..7d7993146 100644 --- a/src/expr/proof_node_manager.h +++ b/src/expr/proof_node_manager.h @@ -80,6 +80,15 @@ class ProofNodeManager * @return The ASSUME proof of fact. */ std::shared_ptr mkAssume(Node fact); + /** + * Make transitivity proof, where children contains one or more proofs of + * equalities that form an ordered chain. In other words, the vector children + * is a legal set of children for an application of TRANS. + */ + std::shared_ptr mkTrans( + const std::vector>& children, + Node expected = Node::null()); + /** * Make scope having body pf and arguments (assumptions-to-close) assumps. * If ensureClosed is true, then this method throws an assertion failure if diff --git a/src/expr/tconv_seq_proof_generator.cpp b/src/expr/tconv_seq_proof_generator.cpp new file mode 100644 index 000000000..b22170b38 --- /dev/null +++ b/src/expr/tconv_seq_proof_generator.cpp @@ -0,0 +1,167 @@ +/********************* */ +/*! \file tconv_seq_proof_generator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 Term conversion sequence proof generator utility + **/ + +#include "expr/tconv_seq_proof_generator.h" + +namespace CVC4 { + +TConvSeqProofGenerator::TConvSeqProofGenerator( + ProofNodeManager* pnm, + const std::vector& ts, + context::Context* c, + std::string name) + : d_pnm(pnm), d_converted(c), d_name(name) +{ + d_tconvs.insert(d_tconvs.end(), ts.begin(), ts.end()); + AlwaysAssert(!d_tconvs.empty()) + << "TConvSeqProofGenerator::TConvSeqProofGenerator: expecting non-empty " + "sequence"; +} + +TConvSeqProofGenerator::~TConvSeqProofGenerator() {} + +void TConvSeqProofGenerator::registerConvertedTerm(Node t, Node s, size_t index) +{ + if (t == s) + { + // no need + return; + } + std::pair key = std::pair(t, index); + d_converted[key] = s; +} + +std::shared_ptr TConvSeqProofGenerator::getProofFor(Node f) +{ + Trace("tconv-seq-pf-gen") + << "TConvSeqProofGenerator::getProofFor: " << identify() << ": " << f + << std::endl; + return getSubsequenceProofFor(f, 0, d_tconvs.size() - 1); +} + +std::shared_ptr TConvSeqProofGenerator::getSubsequenceProofFor( + Node f, size_t start, size_t end) +{ + Assert(end < d_tconvs.size()); + if (f.getKind() != kind::EQUAL) + { + std::stringstream serr; + serr << "TConvSeqProofGenerator::getProofFor: " << identify() + << ": fail, non-equality " << f; + Unhandled() << serr.str(); + Trace("tconv-seq-pf-gen") << serr.str() << std::endl; + return nullptr; + } + // start with the left hand side of the equality + Node curr = f[0]; + // proofs forming transitivity chain + std::vector> transChildren; + std::pair currKey; + NodeIndexNodeMap::iterator itc; + // convert the term in sequence + for (size_t i = start; i <= end; i++) + { + currKey = std::pair(curr, i); + itc = d_converted.find(currKey); + // if we provided a conversion at this index via registerConvertedTerm + if (itc != d_converted.end()) + { + Node next = (*itc).second; + Trace("tconv-seq-pf-gen") << "...convert to " << next << std::endl; + Node eq = curr.eqNode(next); + std::shared_ptr pf = d_tconvs[i]->getProofFor(eq); + transChildren.push_back(pf); + curr = next; + } + } + // should end up with the right hand side of the equality + if (curr != f[1]) + { + // unexpected + std::stringstream serr; + serr << "TConvSeqProofGenerator::getProofFor: " << identify() + << ": failed, mismatch (see -t tconv-seq-pf-gen-debug for details)" + << std::endl; + serr << " source: " << f[0] << std::endl; + serr << "expected after conversions: " << f[1] << std::endl; + serr << " actual after conversions: " << curr << std::endl; + + if (Trace.isOn("tconv-seq-pf-gen-debug")) + { + Trace("tconv-pf-gen-debug") + << "Printing conversion steps..." << std::endl; + serr << "Conversions: " << std::endl; + for (NodeIndexNodeMap::const_iterator it = d_converted.begin(); + it != d_converted.end(); + ++it) + { + serr << "(" << (*it).first.first << ", " << (*it).first.second + << ") -> " << (*it).second << std::endl; + } + } + Unhandled() << serr.str(); + return nullptr; + } + // otherwise, make transitivity + return d_pnm->mkTrans(transChildren, f); +} + +theory::TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence( + const std::vector& cterms) +{ + Assert(cterms.size() == d_tconvs.size() + 1); + if (cterms[0] == cterms[cterms.size() - 1]) + { + return theory::TrustNode::null(); + } + bool useThis = false; + ProofGenerator* pg = nullptr; + for (size_t i = 0, nconvs = d_tconvs.size(); i < nconvs; i++) + { + if (cterms[i] == cterms[i + 1]) + { + continue; + } + else if (pg == nullptr) + { + // Maybe the i^th generator can explain it alone, which must be the case + // if there is only one position in the sequence where the term changes. + // We may overwrite pg with this class if another step is encountered in + // this loop. + pg = d_tconvs[i]; + } + else + { + // need more than a single generator, use this class + useThis = true; + break; + } + } + if (useThis) + { + pg = this; + // if more than two steps, we must register each conversion step + for (size_t i = 0, nconvs = d_tconvs.size(); i < nconvs; i++) + { + registerConvertedTerm(cterms[i], cterms[i + 1], i); + } + } + Assert(pg != nullptr); + return theory::TrustNode::mkTrustRewrite( + cterms[0], cterms[cterms.size() - 1], pg); +} + +std::string TConvSeqProofGenerator::identify() const { return d_name; } + +} // namespace CVC4 diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h new file mode 100644 index 000000000..95499d6b8 --- /dev/null +++ b/src/expr/tconv_seq_proof_generator.h @@ -0,0 +1,119 @@ +/********************* */ +/*! \file tconv_seq_proof_generator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 Term conversion sequence proof generator utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H +#define CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H + +#include "context/cdhashmap.h" +#include "expr/node.h" +#include "expr/proof_generator.h" +#include "expr/proof_node_manager.h" +#include "theory/trust_node.h" + +namespace CVC4 { + +/** + * 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& 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 getProofFor(Node f) override; + /** + * Get subsequence proof for f, with given start and end steps (inclusive). + */ + std::shared_ptr 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& cterms); + + protected: + using NodeIndexPairHashFunction = + PairHashFunction; + typedef context:: + CDHashMap, Node, NodeIndexPairHashFunction> + NodeIndexNodeMap; + /** The proof node manager */ + ProofNodeManager* d_pnm; + /** The term conversion generators */ + std::vector d_tconvs; + /** the set of converted terms */ + NodeIndexNodeMap d_converted; + /** Name identifier */ + std::string d_name; +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H */