summaryrefslogtreecommitdiff
path: root/src/expr/term_conversion_proof_generator.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/term_conversion_proof_generator.cpp')
-rw-r--r--src/expr/term_conversion_proof_generator.cpp624
1 files changed, 0 insertions, 624 deletions
diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
deleted file mode 100644
index 0e0ed3165..000000000
--- a/src/expr/term_conversion_proof_generator.cpp
+++ /dev/null
@@ -1,624 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- * Andrew Reynolds, Aina Niemetz
- *
- * 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.
- * ****************************************************************************
- *
- * Implementation of term conversion proof generator utility.
- */
-
-#include "expr/term_conversion_proof_generator.h"
-
-#include <sstream>
-
-#include "expr/proof_checker.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_algorithm.h"
-#include "expr/term_context.h"
-#include "expr/term_context_stack.h"
-
-using namespace cvc5::kind;
-
-namespace cvc5 {
-
-std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol)
-{
- switch (tcpol)
- {
- case TConvPolicy::FIXPOINT: out << "FIXPOINT"; break;
- case TConvPolicy::ONCE: out << "ONCE"; break;
- default: out << "TConvPolicy:unknown"; break;
- }
- return out;
-}
-
-std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol)
-{
- switch (tcpol)
- {
- case TConvCachePolicy::STATIC: out << "STATIC"; break;
- case TConvCachePolicy::DYNAMIC: out << "DYNAMIC"; break;
- case TConvCachePolicy::NEVER: out << "NEVER"; break;
- default: out << "TConvCachePolicy:unknown"; break;
- }
- return out;
-}
-
-TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm,
- context::Context* c,
- TConvPolicy pol,
- TConvCachePolicy cpol,
- std::string name,
- TermContext* tccb,
- bool rewriteOps)
- : d_proof(pnm, nullptr, c, name + "::LazyCDProof"),
- d_preRewriteMap(c ? c : &d_context),
- d_postRewriteMap(c ? c : &d_context),
- d_policy(pol),
- d_cpolicy(cpol),
- d_name(name),
- d_tcontext(tccb),
- d_rewriteOps(rewriteOps)
-{
-}
-
-TConvProofGenerator::~TConvProofGenerator() {}
-
-void TConvProofGenerator::addRewriteStep(Node t,
- Node s,
- ProofGenerator* pg,
- bool isPre,
- PfRule trustId,
- bool isClosed,
- uint32_t tctx)
-{
- Node eq = registerRewriteStep(t, s, tctx, isPre);
- if (!eq.isNull())
- {
- d_proof.addLazyStep(eq, pg, trustId, isClosed);
- }
-}
-
-void TConvProofGenerator::addRewriteStep(
- Node t, Node s, ProofStep ps, bool isPre, uint32_t tctx)
-{
- Node eq = registerRewriteStep(t, s, tctx, isPre);
- if (!eq.isNull())
- {
- d_proof.addStep(eq, ps);
- }
-}
-
-void TConvProofGenerator::addRewriteStep(Node t,
- Node s,
- PfRule id,
- const std::vector<Node>& children,
- const std::vector<Node>& args,
- bool isPre,
- uint32_t tctx)
-{
- Node eq = registerRewriteStep(t, s, tctx, isPre);
- if (!eq.isNull())
- {
- d_proof.addStep(eq, id, children, args);
- }
-}
-
-bool TConvProofGenerator::hasRewriteStep(Node t,
- uint32_t tctx,
- bool isPre) const
-{
- return !getRewriteStep(t, tctx, isPre).isNull();
-}
-
-Node TConvProofGenerator::getRewriteStep(Node t,
- uint32_t tctx,
- bool isPre) const
-{
- Node thash = t;
- if (d_tcontext != nullptr)
- {
- thash = TCtxNode::computeNodeHash(t, tctx);
- }
- return getRewriteStepInternal(thash, isPre);
-}
-
-Node TConvProofGenerator::registerRewriteStep(Node t,
- Node s,
- uint32_t tctx,
- bool isPre)
-{
- Assert(!t.isNull());
- Assert(!s.isNull());
-
- if (t == s)
- {
- return Node::null();
- }
- Node thash = t;
- if (d_tcontext != nullptr)
- {
- thash = TCtxNode::computeNodeHash(t, tctx);
- }
- else
- {
- // don't use term context ids if not using term context
- Assert(tctx == 0);
- }
- // should not rewrite term to two different things
- if (!getRewriteStepInternal(thash, isPre).isNull())
- {
- Assert(getRewriteStepInternal(thash, isPre) == s)
- << identify() << " rewriting " << t << " to both " << s << " and "
- << getRewriteStepInternal(thash, isPre);
- return Node::null();
- }
- NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
- rm[thash] = s;
- if (d_cpolicy == TConvCachePolicy::DYNAMIC)
- {
- // clear the cache
- d_cache.clear();
- }
- return t.eqNode(s);
-}
-
-std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
-{
- Trace("tconv-pf-gen") << "TConvProofGenerator::getProofFor: " << identify()
- << ": " << f << std::endl;
- if (f.getKind() != EQUAL)
- {
- std::stringstream serr;
- serr << "TConvProofGenerator::getProofFor: " << identify()
- << ": fail, non-equality " << f;
- Unhandled() << serr.str();
- Trace("tconv-pf-gen") << serr.str() << std::endl;
- return nullptr;
- }
- // we use the existing proofs
- LazyCDProof lpf(
- d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProof");
- if (f[0] == f[1])
- {
- // assertion failure in debug
- Assert(false) << "TConvProofGenerator::getProofFor: " << identify()
- << ": don't ask for trivial proofs";
- lpf.addStep(f, PfRule::REFL, {}, {f[0]});
- }
- else
- {
- Node conc = getProofForRewriting(f[0], lpf, d_tcontext);
- if (conc != f)
- {
- bool debugTraceEnabled = Trace.isOn("tconv-pf-gen-debug");
- Assert(conc.getKind() == EQUAL && conc[0] == f[0]);
- std::stringstream serr;
- serr << "TConvProofGenerator::getProofFor: " << toStringDebug()
- << ": failed, mismatch";
- if (!debugTraceEnabled)
- {
- serr << " (see -t tconv-pf-gen-debug for details)";
- }
- serr << std::endl;
- serr << " source: " << f[0] << std::endl;
- serr << " requested conclusion: " << f[1] << std::endl;
- serr << "conclusion from generator: " << conc[1] << std::endl;
-
- if (debugTraceEnabled)
- {
- Trace("tconv-pf-gen-debug") << "Printing rewrite steps..." << std::endl;
- for (size_t r = 0; r < 2; r++)
- {
- const NodeNodeMap& rm = r == 0 ? d_preRewriteMap : d_postRewriteMap;
- serr << "Rewrite steps (" << (r == 0 ? "pre" : "post")
- << "):" << std::endl;
- for (NodeNodeMap::const_iterator it = rm.begin(); it != rm.end();
- ++it)
- {
- serr << (*it).first << " -> " << (*it).second << std::endl;
- }
- }
- }
- Unhandled() << serr.str();
- return nullptr;
- }
- }
- std::shared_ptr<ProofNode> pfn = lpf.getProofFor(f);
- Trace("tconv-pf-gen") << "... success" << std::endl;
- Assert (pfn!=nullptr);
- Trace("tconv-pf-gen-debug") << "... proof is " << *pfn << std::endl;
- return pfn;
-}
-
-std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node n)
-{
- LazyCDProof lpf(
- d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProofRew");
- Node conc = getProofForRewriting(n, lpf, d_tcontext);
- if (conc[1] == n)
- {
- // assertion failure in debug
- Assert(false) << "TConvProofGenerator::getProofForRewriting: " << identify()
- << ": don't ask for trivial proofs";
- lpf.addStep(conc, PfRule::REFL, {}, {n});
- }
- std::shared_ptr<ProofNode> pfn = lpf.getProofFor(conc);
- Assert(pfn != nullptr);
- Trace("tconv-pf-gen-debug") << "... proof is " << *pfn << std::endl;
- return pfn;
-}
-
-Node TConvProofGenerator::getProofForRewriting(Node t,
- LazyCDProof& pf,
- TermContext* tctx)
-{
- NodeManager* nm = NodeManager::currentNM();
- // Invariant: if visited[hash(t)] = s or rewritten[hash(t)] = s and t,s are
- // distinct, then pf is able to generate a proof of t=s. We must
- // Node in the domains of the maps below due to hashing creating new (SEXPR)
- // nodes.
-
- // the final rewritten form of terms
- std::unordered_map<Node, Node> visited;
- // the rewritten form of terms we have processed so far
- std::unordered_map<Node, Node> rewritten;
- std::unordered_map<Node, Node>::iterator it;
- std::unordered_map<Node, Node>::iterator itr;
- std::map<Node, std::shared_ptr<ProofNode> >::iterator itc;
- Trace("tconv-pf-gen-rewrite")
- << "TConvProofGenerator::getProofForRewriting: " << toStringDebug()
- << std::endl;
- Trace("tconv-pf-gen-rewrite") << "Input: " << t << std::endl;
- // if provided, we use term context for cache
- std::shared_ptr<TCtxStack> visitctx;
- // otherwise, visit is used if we don't have a term context
- std::vector<TNode> visit;
- Node tinitialHash;
- if (tctx != nullptr)
- {
- visitctx = std::make_shared<TCtxStack>(tctx);
- visitctx->pushInitial(t);
- tinitialHash = TCtxNode::computeNodeHash(t, tctx->initialValue());
- }
- else
- {
- visit.push_back(t);
- tinitialHash = t;
- }
- Node cur;
- uint32_t curCVal = 0;
- Node curHash;
- do
- {
- // pop the top element
- if (tctx != nullptr)
- {
- std::pair<Node, uint32_t> curPair = visitctx->getCurrent();
- cur = curPair.first;
- curCVal = curPair.second;
- curHash = TCtxNode::computeNodeHash(cur, curCVal);
- visitctx->pop();
- }
- else
- {
- cur = visit.back();
- curHash = cur;
- visit.pop_back();
- }
- Trace("tconv-pf-gen-rewrite") << "* visit : " << curHash << std::endl;
- // has the proof for cur been cached?
- itc = d_cache.find(curHash);
- if (itc != d_cache.end())
- {
- Node res = itc->second->getResult();
- Assert(res.getKind() == EQUAL);
- Assert(!res[1].isNull());
- visited[curHash] = res[1];
- pf.addProof(itc->second);
- continue;
- }
- it = visited.find(curHash);
- if (it == visited.end())
- {
- Trace("tconv-pf-gen-rewrite") << "- previsit" << std::endl;
- visited[curHash] = Node::null();
- // did we rewrite the current node (at pre-rewrite)?
- Node rcur = getRewriteStepInternal(curHash, true);
- if (!rcur.isNull())
- {
- Trace("tconv-pf-gen-rewrite")
- << "*** " << curHash << " prerewrites to " << rcur << std::endl;
- // d_proof has a proof of cur = rcur. Hence there is nothing
- // to do here, as pf will reference d_proof to get its proof.
- if (d_policy == TConvPolicy::FIXPOINT)
- {
- // 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[curHash] = rcur;
- if (tctx != nullptr)
- {
- visitctx->push(cur, curCVal);
- visitctx->push(rcur, curCVal);
- }
- else
- {
- visit.push_back(cur);
- visit.push_back(rcur);
- }
- }
- else
- {
- Assert(d_policy == TConvPolicy::ONCE);
- Trace("tconv-pf-gen-rewrite") << "-> (once, prewrite) " << curHash
- << " = " << rcur << std::endl;
- // not rewriting again, rcur is final
- Assert(!rcur.isNull());
- visited[curHash] = rcur;
- doCache(curHash, cur, rcur, pf);
- }
- }
- else if (tctx != nullptr)
- {
- visitctx->push(cur, curCVal);
- // visit operator if apply uf
- if (d_rewriteOps && cur.getKind() == APPLY_UF)
- {
- visitctx->pushOp(cur, curCVal);
- }
- visitctx->pushChildren(cur, curCVal);
- }
- else
- {
- visit.push_back(cur);
- // visit operator if apply uf
- if (d_rewriteOps && cur.getKind() == APPLY_UF)
- {
- visit.push_back(cur.getOperator());
- }
- visit.insert(visit.end(), cur.begin(), cur.end());
- }
- }
- else if (it->second.isNull())
- {
- itr = rewritten.find(curHash);
- if (itr != rewritten.end())
- {
- // only can generate partially rewritten nodes when rewrite again is
- // true.
- Assert(d_policy != TConvPolicy::ONCE);
- // if it was rewritten, check the status of the rewritten node,
- // which should be finished now
- Node rcur = itr->second;
- Trace("tconv-pf-gen-rewrite")
- << "- postvisit, previously rewritten to " << rcur << std::endl;
- Node rcurHash = rcur;
- if (tctx != nullptr)
- {
- rcurHash = TCtxNode::computeNodeHash(rcur, curCVal);
- }
- Assert(cur != rcur);
- // the final rewritten form of cur is the final form of rcur
- Node rcurFinal = visited[rcurHash];
- Assert(!rcurFinal.isNull());
- 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, {});
- }
- Trace("tconv-pf-gen-rewrite")
- << "-> (rewritten postrewrite) " << curHash << " = " << rcurFinal
- << std::endl;
- visited[curHash] = rcurFinal;
- doCache(curHash, cur, rcurFinal, pf);
- }
- else
- {
- Trace("tconv-pf-gen-rewrite") << "- postvisit" << std::endl;
- Node ret = cur;
- Node retHash = curHash;
- bool childChanged = false;
- std::vector<Node> children;
- Kind ck = cur.getKind();
- if (d_rewriteOps && ck == APPLY_UF)
- {
- // the operator of APPLY_UF is visited
- Node cop = cur.getOperator();
- if (tctx != nullptr)
- {
- uint32_t coval = tctx->computeValueOp(cur, curCVal);
- Node coHash = TCtxNode::computeNodeHash(cop, coval);
- it = visited.find(coHash);
- }
- else
- {
- it = visited.find(cop);
- }
- Assert(it != visited.end());
- Assert(!it->second.isNull());
- childChanged = childChanged || cop != it->second;
- children.push_back(it->second);
- }
- else if (cur.getMetaKind() == metakind::PARAMETERIZED)
- {
- // all other parametrized operators are unchanged
- children.push_back(cur.getOperator());
- }
- // get the results of the children
- if (tctx != nullptr)
- {
- for (size_t i = 0, nchild = cur.getNumChildren(); i < nchild; i++)
- {
- Node cn = cur[i];
- uint32_t cnval = tctx->computeValue(cur, curCVal, i);
- Node cnHash = TCtxNode::computeNodeHash(cn, cnval);
- it = visited.find(cnHash);
- Assert(it != visited.end());
- Assert(!it->second.isNull());
- childChanged = childChanged || cn != it->second;
- children.push_back(it->second);
- }
- }
- else
- {
- // can use simple loop if not term-context-sensitive
- 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(ck, children);
- rewritten[curHash] = ret;
- // congruence to show (cur = ret)
- PfRule congRule = PfRule::CONG;
- std::vector<Node> pfChildren;
- std::vector<Node> pfArgs;
- pfArgs.push_back(ProofRuleChecker::mkKindNode(ck));
- if (ck == APPLY_UF && children[0] != cur.getOperator())
- {
- // use HO_CONG if the operator changed
- congRule = PfRule::HO_CONG;
- pfChildren.push_back(cur.getOperator().eqNode(children[0]));
- }
- else if (kind::metaKindOf(ck) == kind::metakind::PARAMETERIZED)
- {
- pfArgs.push_back(cur.getOperator());
- }
- 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]));
- }
- Node result = cur.eqNode(ret);
- pf.addStep(result, congRule, pfChildren, pfArgs);
- // must update the hash
- retHash = ret;
- if (tctx != nullptr)
- {
- retHash = TCtxNode::computeNodeHash(ret, curCVal);
- }
- }
- else if (tctx != nullptr)
- {
- // now we need the hash
- retHash = TCtxNode::computeNodeHash(cur, curCVal);
- }
- // did we rewrite ret (at post-rewrite)?
- Node rret = getRewriteStepInternal(retHash, false);
- if (!rret.isNull() && d_policy == TConvPolicy::FIXPOINT)
- {
- Trace("tconv-pf-gen-rewrite")
- << "*** " << retHash << " postrewrites to " << rret << std::endl;
- // 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[retHash] = rret;
- if (tctx != nullptr)
- {
- if (cur != ret)
- {
- visitctx->push(cur, curCVal);
- }
- visitctx->push(ret, curCVal);
- visitctx->push(rret, curCVal);
- }
- else
- {
- if (cur != ret)
- {
- visit.push_back(cur);
- }
- visit.push_back(ret);
- visit.push_back(rret);
- }
- }
- else
- {
- // If we changed due to congruence, and then rewrote, then we
- // require a trans step to connect here
- if (!rret.isNull() && childChanged)
- {
- std::vector<Node> pfChildren;
- pfChildren.push_back(cur.eqNode(ret));
- pfChildren.push_back(ret.eqNode(rret));
- Node result = cur.eqNode(rret);
- pf.addStep(result, PfRule::TRANS, pfChildren, {});
- }
- // take its rewrite if it rewrote and we have ONCE rewriting policy
- ret = rret.isNull() ? ret : rret;
- Trace("tconv-pf-gen-rewrite")
- << "-> (postrewrite) " << curHash << " = " << ret << std::endl;
- // it is final
- Assert(!ret.isNull());
- visited[curHash] = ret;
- doCache(curHash, cur, ret, pf);
- }
- }
- }
- else
- {
- Trace("tconv-pf-gen-rewrite") << "- already visited" << std::endl;
- }
- } while (!(tctx != nullptr ? visitctx->empty() : visit.empty()));
- Assert(visited.find(tinitialHash) != visited.end());
- Assert(!visited.find(tinitialHash)->second.isNull());
- Trace("tconv-pf-gen-rewrite")
- << "...finished, return " << visited[tinitialHash] << std::endl;
- // return the conclusion of the overall proof
- return t.eqNode(visited[tinitialHash]);
-}
-
-void TConvProofGenerator::doCache(Node curHash,
- Node cur,
- Node r,
- LazyCDProof& pf)
-{
- if (d_cpolicy != TConvCachePolicy::NEVER)
- {
- Node eq = cur.eqNode(r);
- d_cache[curHash] = pf.getProofFor(eq);
- }
-}
-
-Node TConvProofGenerator::getRewriteStepInternal(Node t, bool isPre) const
-{
- const NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
- NodeNodeMap::const_iterator it = rm.find(t);
- if (it == rm.end())
- {
- return Node::null();
- }
- return (*it).second;
-}
-std::string TConvProofGenerator::identify() const { return d_name; }
-
-std::string TConvProofGenerator::toStringDebug() const
-{
- std::stringstream ss;
- ss << identify() << " (policy=" << d_policy << ", cache policy=" << d_cpolicy
- << (d_tcontext != nullptr ? ", term-context-sensitive" : "") << ")";
- return ss.str();
-}
-
-} // namespace cvc5
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback