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.
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
return mkNode(PfRule::ASSUME, {}, {fact}, fact);
}
+std::shared_ptr<ProofNode> ProofNodeManager::mkTrans(
+ const std::vector<std::shared_ptr<ProofNode>>& 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<ProofNode> ProofNodeManager::mkScope(
std::shared_ptr<ProofNode> pf,
std::vector<Node>& assumps,
* @return The ASSUME proof of fact.
*/
std::shared_ptr<ProofNode> 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<ProofNode> mkTrans(
+ const std::vector<std::shared_ptr<ProofNode>>& 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
--- /dev/null
+/********************* */
+/*! \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<ProofGenerator*>& 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<Node, size_t> key = std::pair<Node, size_t>(t, index);
+ d_converted[key] = s;
+}
+
+std::shared_ptr<ProofNode> 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<ProofNode> 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<std::shared_ptr<ProofNode>> transChildren;
+ std::pair<Node, size_t> currKey;
+ NodeIndexNodeMap::iterator itc;
+ // convert the term in sequence
+ for (size_t i = start; i <= end; i++)
+ {
+ currKey = std::pair<Node, size_t>(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<ProofNode> 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<Node>& 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
--- /dev/null
+/********************* */
+/*! \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<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, NodeHashFunction>;
+ 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 CVC4
+
+#endif /* CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H */
projects / cvc5.git / commitdiff