diff options
Diffstat (limited to 'src/expr/term_conversion_proof_generator.cpp')
-rw-r--r-- | src/expr/term_conversion_proof_generator.cpp | 351 |
1 files changed, 273 insertions, 78 deletions
diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index 1c4baeed7..8cd7561b4 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -14,6 +14,8 @@ #include "expr/term_conversion_proof_generator.h" +#include "expr/term_context_stack.h" + using namespace CVC4::kind; namespace CVC4 { @@ -45,31 +47,38 @@ TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm, context::Context* c, TConvPolicy pol, TConvCachePolicy cpol, - std::string name) + std::string name, + TermContext* tccb) : d_proof(pnm, nullptr, c, name + "::LazyCDProof"), d_rewriteMap(c ? c : &d_context), d_policy(pol), d_cpolicy(cpol), - d_name(name) + d_name(name), + d_tcontext(tccb) { } TConvProofGenerator::~TConvProofGenerator() {} -void TConvProofGenerator::addRewriteStep(Node t, Node s, ProofGenerator* pg) +void TConvProofGenerator::addRewriteStep( + Node t, Node s, ProofGenerator* pg, bool isClosed, uint32_t tctx) { - Node eq = registerRewriteStep(t, s); + Node eq = registerRewriteStep(t, s, tctx); if (!eq.isNull()) { - d_proof.addLazyStep(eq, pg); + d_proof.addLazyStep(eq, pg, isClosed); } } -void TConvProofGenerator::addRewriteStep(Node t, Node s, ProofStep ps) +void TConvProofGenerator::addRewriteStep(Node t, + Node s, + ProofStep ps, + uint32_t tctx) { - Node eq = registerRewriteStep(t, s); + Node eq = registerRewriteStep(t, s, tctx); if (!eq.isNull()) { + AlwaysAssert(ps.d_rule != PfRule::ASSUME); d_proof.addStep(eq, ps); } } @@ -78,33 +87,55 @@ void TConvProofGenerator::addRewriteStep(Node t, Node s, PfRule id, const std::vector<Node>& children, - const std::vector<Node>& args) + const std::vector<Node>& args, + uint32_t tctx) { - Node eq = registerRewriteStep(t, s); + Node eq = registerRewriteStep(t, s, tctx); if (!eq.isNull()) { + AlwaysAssert(id != PfRule::ASSUME); d_proof.addStep(eq, id, children, args); } } -bool TConvProofGenerator::hasRewriteStep(Node t) const +bool TConvProofGenerator::hasRewriteStep(Node t, uint32_t tctx) const { - return !getRewriteStep(t).isNull(); + return !getRewriteStep(t, tctx).isNull(); } -Node TConvProofGenerator::registerRewriteStep(Node t, Node s) +Node TConvProofGenerator::getRewriteStep(Node t, uint32_t tctx) const +{ + Node thash = t; + if (d_tcontext != nullptr) + { + thash = TCtxNode::computeNodeHash(t, tctx); + } + return getRewriteStepInternal(thash); +} + +Node TConvProofGenerator::registerRewriteStep(Node t, Node s, uint32_t tctx) { 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 (!getRewriteStep(t).isNull()) + if (!getRewriteStepInternal(thash).isNull()) { - Assert(getRewriteStep(t) == s); + Assert(getRewriteStepInternal(thash) == s); return Node::null(); } - d_rewriteMap[t] = s; + d_rewriteMap[thash] = s; if (d_cpolicy == TConvCachePolicy::DYNAMIC) { // clear the cache @@ -115,66 +146,140 @@ Node TConvProofGenerator::registerRewriteStep(Node t, Node s) std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f) { - Trace("tconv-pf-gen") << "TConvProofGenerator::getProofFor: " << f - << std::endl; + Trace("tconv-pf-gen") << "TConvProofGenerator::getProofFor: " << identify() + << ": " << f << std::endl; if (f.getKind() != EQUAL) { - Trace("tconv-pf-gen") << "... fail, non-equality" << std::endl; - Assert(false); + 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"); - Node conc = getProofForRewriting(f[0], lpf); - if (conc != f) + if (f[0] == f[1]) { - Trace("tconv-pf-gen") << "...failed, mismatch: returned proof concludes " - << conc << ", expected " << f << std::endl; - Assert(false); - return nullptr; + // 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) + { + Assert(conc.getKind() == EQUAL && conc[0] == f[0]); + std::stringstream serr; + serr << "TConvProofGenerator::getProofFor: " << toStringDebug() + << ": failed, mismatch (see -t tconv-pf-gen-debug for details)" + << std::endl; + serr << " source: " << f[0] << std::endl; + serr << "expected after rewriting: " << f[1] << std::endl; + serr << " actual after rewriting: " << conc[1] << std::endl; + + if (Trace.isOn("tconv-pf-gen-debug")) + { + Trace("tconv-pf-gen-debug") << "Printing rewrite steps..." << std::endl; + serr << "Rewrite steps: " << std::endl; + for (NodeNodeMap::const_iterator it = d_rewriteMap.begin(); + it != d_rewriteMap.end(); + ++it) + { + serr << (*it).first << " -> " << (*it).second << std::endl; + } + } + Unhandled() << serr.str(); + return nullptr; + } } Trace("tconv-pf-gen") << "... success" << std::endl; return lpf.getProofFor(f); } -Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf) +Node TConvProofGenerator::getProofForRewriting(Node t, + LazyCDProof& pf, + TermContext* tctx) { 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. + // 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<TNode, Node, TNodeHashFunction> visited; + std::unordered_map<Node, 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::unordered_map<Node, Node, TNodeHashFunction> rewritten; + std::unordered_map<Node, Node, TNodeHashFunction>::iterator it; + std::unordered_map<Node, Node, TNodeHashFunction>::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; - TNode cur; - visit.push_back(t); + 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 { - cur = visit.back(); - visit.pop_back(); + // 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(cur); + itc = d_cache.find(curHash); if (itc != d_cache.end()) { Node res = itc->second->getResult(); Assert(res.getKind() == EQUAL); - visited[cur] = res[1]; + Assert(!res[1].isNull()); + visited[curHash] = res[1]; pf.addProof(itc->second); continue; } - it = visited.find(cur); + it = visited.find(curHash); if (it == visited.end()) { - visited[cur] = Node::null(); + Trace("tconv-pf-gen-rewrite") << "- previsit" << std::endl; + visited[curHash] = Node::null(); // did we rewrite the current node (possibly at pre-rewrite)? - Node rcur = getRewriteStep(cur); + Node rcur = getRewriteStepInternal(curHash); 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) @@ -182,18 +287,34 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf) // 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); + 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 - visited[cur] = rcur; - doCache(cur, rcur, pf); + Assert(!rcur.isNull()); + visited[curHash] = rcur; + doCache(curHash, cur, rcur, pf); } } + else if (tctx != nullptr) + { + visitctx->push(cur, curCVal); + visitctx->pushChildren(cur, curCVal); + } else { visit.push_back(cur); @@ -202,7 +323,7 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf) } else if (it->second.isNull()) { - itr = rewritten.find(cur); + itr = rewritten.find(curHash); if (itr != rewritten.end()) { // only can generate partially rewritten nodes when rewrite again is @@ -211,9 +332,17 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf) // 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[rcur]; + Node rcurFinal = visited[rcurHash]; + Assert(!rcurFinal.isNull()); if (rcurFinal != rcur) { // must connect via TRANS @@ -223,30 +352,54 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf) Node result = cur.eqNode(rcurFinal); pf.addStep(result, PfRule::TRANS, pfChildren, {}); } - visited[cur] = rcurFinal; - doCache(cur, rcurFinal, pf); + 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; if (cur.getMetaKind() == metakind::PARAMETERIZED) { children.push_back(cur.getOperator()); } - for (const Node& cn : cur) + // 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 { - it = visited.find(cn); - Assert(it != visited.end()); - Assert(!it->second.isNull()); - childChanged = childChanged || cn != it->second; - children.push_back(it->second); + // 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(cur.getKind(), children); - rewritten[cur] = ret; + rewritten[curHash] = ret; // congruence to show (cur = ret) std::vector<Node> pfChildren; for (size_t i = 0, size = cur.getNumChildren(); i < size; i++) @@ -260,62 +413,96 @@ Node TConvProofGenerator::getProofForRewriting(Node t, LazyCDProof& pf) } std::vector<Node> pfArgs; Kind k = cur.getKind(); + pfArgs.push_back(ProofRuleChecker::mkKindNode(k)); 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); + // 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; // only if not ONCE policy, which only does pre-rewrite if (d_policy != TConvPolicy::ONCE) { - rret = getRewriteStep(ret); + rret = getRewriteStepInternal(retHash); } if (!rret.isNull()) { - if (cur != ret) - { - visit.push_back(cur); - } + 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[ret] = rret; - visit.push_back(ret); - visit.push_back(rret); + 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 { + Trace("tconv-pf-gen-rewrite") + << "-> (postrewrite) " << curHash << " = " << ret << std::endl; // it is final - visited[cur] = ret; - doCache(cur, ret, pf); + Assert(!ret.isNull()); + visited[curHash] = ret; + doCache(curHash, cur, ret, pf); } } } - } while (!visit.empty()); - Assert(visited.find(t) != visited.end()); - Assert(!visited.find(t)->second.isNull()); + 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[t]); + return t.eqNode(visited[tinitialHash]); } -void TConvProofGenerator::doCache(Node cur, Node r, LazyCDProof& pf) +void TConvProofGenerator::doCache(Node curHash, + Node cur, + Node r, + LazyCDProof& pf) { if (d_cpolicy != TConvCachePolicy::NEVER) { Node eq = cur.eqNode(r); - d_cache[cur] = pf.getProofFor(eq); + d_cache[curHash] = pf.getProofFor(eq); } } -Node TConvProofGenerator::getRewriteStep(Node t) const +Node TConvProofGenerator::getRewriteStepInternal(Node t) const { NodeNodeMap::const_iterator it = d_rewriteMap.find(t); if (it == d_rewriteMap.end()) @@ -326,4 +513,12 @@ Node TConvProofGenerator::getRewriteStep(Node t) const } 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 CVC4 |