summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/CMakeLists.txt2
-rw-r--r--src/expr/term_conversion_proof_generator.cpp250
-rw-r--r--src/expr/term_conversion_proof_generator.h123
3 files changed, 375 insertions, 0 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 3d74d0bad..00eeaecea 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -61,6 +61,8 @@ libcvc4_add_sources(
symbol_table.h
term_canonize.cpp
term_canonize.h
+ term_conversion_proof_generator.cpp
+ term_conversion_proof_generator.h
type.cpp
type.h
type_checker.h
diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
new file mode 100644
index 000000000..59faaf632
--- /dev/null
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -0,0 +1,250 @@
+/********************* */
+/*! \file term_conversion_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 term conversion proof generator utility
+ **/
+
+#include "expr/term_conversion_proof_generator.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm,
+ context::Context* c)
+ : d_proof(pnm, nullptr, c), d_rewriteMap(c ? c : &d_context)
+{
+}
+
+TConvProofGenerator::~TConvProofGenerator() {}
+
+void TConvProofGenerator::addRewriteStep(Node t, Node s, ProofGenerator* pg)
+{
+ // should not rewrite term more than once
+ Assert(!hasRewriteStep(t));
+ Node eq = t.eqNode(s);
+ d_proof.addLazyStep(eq, pg);
+ d_rewriteMap[t] = s;
+}
+
+void TConvProofGenerator::addRewriteStep(Node t, Node s, ProofStep ps)
+{
+ // should not rewrite term more than once
+ Assert(!hasRewriteStep(t));
+ Node eq = t.eqNode(s);
+ d_proof.addStep(eq, ps);
+ d_rewriteMap[t] = s;
+}
+
+void TConvProofGenerator::addRewriteStep(Node t,
+ Node s,
+ PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args)
+{
+ // should not rewrite term more than once
+ Assert(!hasRewriteStep(t));
+ Node eq = t.eqNode(s);
+ d_proof.addStep(eq, id, children, args);
+ d_rewriteMap[t] = s;
+}
+
+bool TConvProofGenerator::hasRewriteStep(Node t) const
+{
+ return !getRewriteStep(t).isNull();
+}
+
+std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
+{
+ Trace("tconv-pf-gen") << "TConvProofGenerator::getProofFor: " << f
+ << std::endl;
+ if (f.getKind() != EQUAL)
+ {
+ Trace("tconv-pf-gen") << "... fail, non-equality" << std::endl;
+ Assert(false);
+ return nullptr;
+ }
+ std::shared_ptr<ProofNode> pf = getProofForRewriting(f[0]);
+ if (pf == nullptr)
+ {
+ // failed to generate proof
+ Trace("tconv-pf-gen") << "...failed to get proof" << std::endl;
+ Assert(false);
+ return pf;
+ }
+ if (pf->getResult() != f)
+ {
+ Trace("tconv-pf-gen") << "...failed, mismatch: returned proof concludes "
+ << pf->getResult() << std::endl;
+ Assert(false);
+ return nullptr;
+ }
+ Trace("tconv-pf-gen") << "... success" << std::endl;
+ return pf;
+}
+
+std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node t)
+{
+ // we use the existing proofs
+ PRefProofGenerator prg(&d_proof);
+ LazyCDProof pf(d_proof.getManager(), &prg);
+ NodeManager* nm = NodeManager::currentNM();
+ // Invariant: if visited[t] = s or rewritten[t] = s and t,s are distinct,
+ // then pf is able to generate a proof of t=s.
+ // the final rewritten form of terms
+ std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+ // the rewritten form of terms we have processed so far
+ std::unordered_map<TNode, Node, TNodeHashFunction> rewritten;
+ std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::unordered_map<TNode, Node, TNodeHashFunction>::iterator itr;
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(t);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ it = visited.find(cur);
+
+ if (it == visited.end())
+ {
+ visited[cur] = Node::null();
+ // did we rewrite the current node (possibly at pre-rewrite)?
+ Node rcur = getRewriteStep(cur);
+ if (!rcur.isNull())
+ {
+ // d_proof should have a proof of cur = rcur. Hence there is nothing
+ // to do here, as pf will reference prg to get the proof from d_proof.
+ // It may be the case that rcur also rewrites, thus we cannot assign
+ // the final rewritten form for cur yet. Instead we revisit cur after
+ // finishing visiting rcur.
+ rewritten[cur] = rcur;
+ visit.push_back(cur);
+ visit.push_back(rcur);
+ }
+ else
+ {
+ visit.push_back(cur);
+ visit.insert(visit.end(), cur.begin(), cur.end());
+ }
+ }
+ else if (it->second.isNull())
+ {
+ itr = rewritten.find(cur);
+ if (itr != rewritten.end())
+ {
+ // if it was rewritten, check the status of the rewritten node,
+ // which should be finished now
+ Node rcur = itr->second;
+ Assert(cur != rcur);
+ // the final rewritten form of cur is the final form of rcur
+ Node rcurFinal = visited[rcur];
+ if (rcurFinal != rcur)
+ {
+ // must connect via TRANS
+ std::vector<Node> pfChildren;
+ pfChildren.push_back(cur.eqNode(rcur));
+ pfChildren.push_back(rcur.eqNode(rcurFinal));
+ Node result = cur.eqNode(rcurFinal);
+ pf.addStep(result, PfRule::TRANS, pfChildren, {});
+ }
+ visited[cur] = rcurFinal;
+ }
+ else
+ {
+ Node ret = cur;
+ bool childChanged = false;
+ std::vector<Node> children;
+ if (cur.getMetaKind() == metakind::PARAMETERIZED)
+ {
+ children.push_back(cur.getOperator());
+ }
+ for (const Node& cn : cur)
+ {
+ it = visited.find(cn);
+ Assert(it != visited.end());
+ Assert(!it->second.isNull());
+ childChanged = childChanged || cn != it->second;
+ children.push_back(it->second);
+ }
+ if (childChanged)
+ {
+ ret = nm->mkNode(cur.getKind(), children);
+ rewritten[cur] = ret;
+ // congruence to show (cur = ret)
+ std::vector<Node> pfChildren;
+ for (size_t i = 0, size = cur.getNumChildren(); i < size; i++)
+ {
+ if (cur[i] == ret[i])
+ {
+ // ensure REFL proof for unchanged children
+ pf.addStep(cur[i].eqNode(cur[i]), PfRule::REFL, {}, {cur[i]});
+ }
+ pfChildren.push_back(cur[i].eqNode(ret[i]));
+ }
+ std::vector<Node> pfArgs;
+ Kind k = cur.getKind();
+ if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED)
+ {
+ pfArgs.push_back(cur.getOperator());
+ }
+ else
+ {
+ pfArgs.push_back(nm->operatorOf(k));
+ }
+ Node result = cur.eqNode(ret);
+ pf.addStep(result, PfRule::CONG, pfChildren, pfArgs);
+ }
+ // did we rewrite ret (at post-rewrite)?
+ Node rret = getRewriteStep(ret);
+ if (!rret.isNull())
+ {
+ if (cur != ret)
+ {
+ visit.push_back(cur);
+ }
+ // d_proof should have a proof of ret = rret, hence nothing to do
+ // here, for the same reasons as above. It also may be the case that
+ // rret rewrites, hence we must revisit ret.
+ rewritten[ret] = rret;
+ visit.push_back(ret);
+ visit.push_back(rret);
+ }
+ else
+ {
+ // it is final
+ visited[cur] = ret;
+ }
+ }
+ }
+ } while (!visit.empty());
+ Assert(visited.find(t) != visited.end());
+ Assert(!visited.find(t)->second.isNull());
+ // make the overall proof
+ Node teq = t.eqNode(visited[t]);
+ return pf.mkProof(teq);
+}
+
+Node TConvProofGenerator::getRewriteStep(Node t) const
+{
+ NodeNodeMap::const_iterator it = d_rewriteMap.find(t);
+ if (it == d_rewriteMap.end())
+ {
+ return Node::null();
+ }
+ return (*it).second;
+}
+std::string TConvProofGenerator::identify() const
+{
+ return "TConvProofGenerator";
+}
+
+} // namespace CVC4
diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h
new file mode 100644
index 000000000..2af4250d2
--- /dev/null
+++ b/src/expr/term_conversion_proof_generator.h
@@ -0,0 +1,123 @@
+/********************* */
+/*! \file term_conversion_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 Term conversion proof generator utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H
+#define CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H
+
+#include "context/cdhashmap.h"
+#include "expr/lazy_proof.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
+
+namespace CVC4 {
+
+/**
+ * The term conversion proof generator.
+ *
+ * This class is used for proofs of t = t', where t' is obtained from t by
+ * applying (context-free) small step rewrites on subterms of t. Its main
+ * interface functions are:
+ * (1) addRewriteStep(t,s,<justification>) which notifies this class that t
+ * rewrites to s, where justification is either a proof generator or proof
+ * step,
+ * (2) getProofFor(f) where f is any equality that can be justified by the
+ * rewrite steps given above.
+ *
+ * For example, say we make the following calls:
+ * addRewriteStep(a,b,P1)
+ * addRewriteStep(f(a),c,P2)
+ * addRewriteStep(c,d,P3)
+ * where P1 and P2 are proof steps. Afterwards, this class may justify any
+ * equality t = s where s is obtained by applying the rewrites a->b, f(a)->c,
+ * c->d, based on the strategy outlined below [***]. For example, the call to:
+ * getProofFor(g(f(a),h(a),f(e)) = g(d,h(b),f(e)))
+ * will return the proof:
+ * CONG(
+ * TRANS(P2,P3), ; f(a)=d
+ * CONG(P1 :args h), ; h(a)=h(b)
+ * REFL(:args f(e)) ; f(e)=f(e)
+ * :args g)
+ *
+ * [***] This class traverses the left hand side of a given equality-to-prove
+ * (the term g(f(a),h(a),e) in the above example) and "replays" the rewrite
+ * steps to obtain its rewritten form. To do so, it applies any available
+ * rewrite step both at pre-rewrite (pre-order traversal) and post-rewrite
+ * (post-order traversal). It thus does not require the user of this class to
+ * distinguish whether a rewrite is a pre-rewrite or a post-rewrite during
+ * addRewriteStep. In particular, notice that in the above example, we realize
+ * that f(a) --> c at pre-rewrite instead of post-rewriting a --> b and then
+ * ending with f(a)=f(b).
+ */
+class TConvProofGenerator : public ProofGenerator
+{
+ public:
+ /** Constructor
+ *
+ * @param pnm The proof node manager for constructing ProofNode objects.
+ * @param c The context that this class depends on. If none is provided,
+ * this class is context-independent.
+ */
+ TConvProofGenerator(ProofNodeManager* pnm, context::Context* c = nullptr);
+ ~TConvProofGenerator();
+ /**
+ * Add rewrite step t --> s based on proof generator.
+ */
+ void addRewriteStep(Node t, Node s, ProofGenerator* pg);
+ /** Same as above, for a single step */
+ void addRewriteStep(Node t, Node s, ProofStep ps);
+ /** Same as above, with explicit arguments */
+ void addRewriteStep(Node t,
+ Node s,
+ PfRule id,
+ const std::vector<Node>& children,
+ const std::vector<Node>& args);
+ /** Has rewrite step for term t */
+ bool hasRewriteStep(Node t) const;
+ /**
+ * Get rewrite step for term t, returns the s provided in a call to
+ * addRewriteStep if one exists, or null otherwise.
+ */
+ Node getRewriteStep(Node t) const;
+ /**
+ * Get the proof for formula f. It should be the case that f is of the form
+ * t = t', where t' is the result of rewriting t based on the rewrite steps
+ * registered to this class.
+ *
+ * @param f The fact to get the proof for.
+ * @return The proof for f.
+ */
+ std::shared_ptr<ProofNode> getProofFor(Node f) override;
+ /** Identify this generator (for debugging, etc..) */
+ std::string identify() const override;
+
+ protected:
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+ /** A dummy context used by this class if none is provided */
+ context::Context d_context;
+ /** The (lazy) context dependent proof object. */
+ LazyCDProof d_proof;
+ /** map to rewritten forms */
+ NodeNodeMap d_rewriteMap;
+ /**
+ * Get the proof for term t. Returns a proof of t = t' where t' is the
+ * result of rewriting t based on the rewrite steps registered to this class.
+ */
+ std::shared_ptr<ProofNode> getProofForRewriting(Node t);
+};
+
+} // namespace CVC4
+
+#endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback