diff options
Diffstat (limited to 'src/proof')
43 files changed, 9031 insertions, 3 deletions
diff --git a/src/proof/buffered_proof_generator.cpp b/src/proof/buffered_proof_generator.cpp new file mode 100644 index 000000000..d6f54fb34 --- /dev/null +++ b/src/proof/buffered_proof_generator.cpp @@ -0,0 +1,103 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa + * + * 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 a proof generator for buffered proof steps. + */ + +#include "proof/buffered_proof_generator.h" + +#include "proof/proof.h" +#include "proof/proof_node_manager.h" + +namespace cvc5 { + +BufferedProofGenerator::BufferedProofGenerator(context::Context* c, + ProofNodeManager* pnm) + : ProofGenerator(), d_facts(c), d_pnm(pnm) +{ +} + +bool BufferedProofGenerator::addStep(Node fact, + ProofStep ps, + CDPOverwrite opolicy) +{ + // check duplicates if we are not always overwriting + if (opolicy != CDPOverwrite::ALWAYS) + { + if (d_facts.find(fact) != d_facts.end()) + { + // duplicate + return false; + } + Node symFact = CDProof::getSymmFact(fact); + if (!symFact.isNull()) + { + if (d_facts.find(symFact) != d_facts.end()) + { + // duplicate due to symmetry + return false; + } + } + } + // note that this replaces the value fact is mapped to if there is already one + d_facts.insert(fact, std::make_shared<ProofStep>(ps)); + return true; +} + +std::shared_ptr<ProofNode> BufferedProofGenerator::getProofFor(Node fact) +{ + Trace("pfee-fact-gen") << "BufferedProofGenerator::getProofFor: " << fact + << std::endl; + NodeProofStepMap::iterator it = d_facts.find(fact); + if (it == d_facts.end()) + { + Node symFact = CDProof::getSymmFact(fact); + if (symFact.isNull()) + { + Trace("pfee-fact-gen") << "...cannot find step" << std::endl; + Assert(false); + return nullptr; + } + it = d_facts.find(symFact); + if (it == d_facts.end()) + { + Assert(false); + Trace("pfee-fact-gen") << "...cannot find step (no sym)" << std::endl; + return nullptr; + } + } + Trace("pfee-fact-gen") << "...return via step " << *(*it).second << std::endl; + CDProof cdp(d_pnm); + cdp.addStep(fact, *(*it).second); + return cdp.getProofFor(fact); +} + +bool BufferedProofGenerator::hasProofFor(Node f) +{ + NodeProofStepMap::iterator it = d_facts.find(f); + if (it == d_facts.end()) + { + Node symFact = CDProof::getSymmFact(f); + if (symFact.isNull()) + { + return false; + } + it = d_facts.find(symFact); + if (it == d_facts.end()) + { + return false; + } + } + return true; +} + +} // namespace cvc5 diff --git a/src/proof/buffered_proof_generator.h b/src/proof/buffered_proof_generator.h new file mode 100644 index 000000000..9d13faff4 --- /dev/null +++ b/src/proof/buffered_proof_generator.h @@ -0,0 +1,64 @@ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Andrew Reynolds, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * A proof generator for buffered proof steps. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__BUFFERED_PROOF_GENERATOR_H +#define CVC5__PROOF__BUFFERED_PROOF_GENERATOR_H + +#include "context/cdhashmap.h" +#include "proof/proof_generator.h" + +namespace cvc5 { + +class ProofNodeManager; +class ProofStep; + +/** + * The proof generator for buffered steps. This class is a context-dependent + * mapping from formulas to proof steps. It does not generate ProofNodes until + * it is asked to provide a proof for a given fact. + */ +class BufferedProofGenerator : public ProofGenerator +{ + typedef context::CDHashMap<Node, std::shared_ptr<ProofStep>> NodeProofStepMap; + + public: + BufferedProofGenerator(context::Context* c, ProofNodeManager* pnm); + ~BufferedProofGenerator() {} + /** add step + * Unless the overwrite policy is ALWAYS it does not replace previously + * registered steps (modulo (dis)equality symmetry). + */ + bool addStep(Node fact, + ProofStep ps, + CDPOverwrite opolicy = CDPOverwrite::NEVER); + /** Get proof for. It is robust to (dis)equality symmetry. */ + std::shared_ptr<ProofNode> getProofFor(Node f) override; + /** Whether a step has been registered for f. */ + bool hasProofFor(Node f) override; + /** identify */ + std::string identify() const override { return "BufferedProofGenerator"; } + + private: + /** maps expected to ProofStep */ + NodeProofStepMap d_facts; + /** the proof node manager */ + ProofNodeManager* d_pnm; +}; + +} // namespace cvc5 + +#endif /* CVC5__PROOF__BUFFERED_PROOF_GENERATOR_H */ diff --git a/src/proof/conv_proof_generator.cpp b/src/proof/conv_proof_generator.cpp new file mode 100644 index 000000000..3635f3dea --- /dev/null +++ b/src/proof/conv_proof_generator.cpp @@ -0,0 +1,624 @@ +/****************************************************************************** + * 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 "proof/conv_proof_generator.h" + +#include <sstream> + +#include "expr/term_context.h" +#include "expr/term_context_stack.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" +#include "proof/proof_node_algorithm.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 diff --git a/src/proof/conv_proof_generator.h b/src/proof/conv_proof_generator.h new file mode 100644 index 000000000..f23a661ae --- /dev/null +++ b/src/proof/conv_proof_generator.h @@ -0,0 +1,256 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Term conversion proof generator utility. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__CONV_PROOF_GENERATOR_H +#define CVC5__PROOF__CONV_PROOF_GENERATOR_H + +#include "context/cdhashmap.h" +#include "proof/lazy_proof.h" +#include "proof/proof_generator.h" + +namespace cvc5 { + +class ProofNodeManager; +class TermContext; + +/** A policy for how rewrite steps are applied in TConvProofGenerator */ +enum class TConvPolicy : uint32_t +{ + // steps are applied to fix-point, common use case is PfRule::REWRITE + FIXPOINT, + // steps are applied once at pre-rewrite, common use case is PfRule::SUBS + ONCE, +}; +/** Writes a term conversion policy name to a stream. */ +std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol); + +/** A policy for how proofs are cached in TConvProofGenerator */ +enum class TConvCachePolicy : uint32_t +{ + // proofs are statically cached + STATIC, + // proofs are dynamically cached, cleared when a new rewrite is added + DYNAMIC, + // proofs are never cached + NEVER, +}; +/** Writes a term conversion cache policy name to a stream. */ +std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol); + +/** + * 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 at pre-rewrite (pre-order traversal) and post-rewrite + * (post-order traversal) based on whether the user specified pre-rewrite or a + * post-rewrite during addRewriteStep. + * + * This class may additionally be used for term-context-sensitive rewrite + * systems. An example is the term formula removal pass which rewrites + * terms dependending on whether they occur in a "term position", for details + * see RtfTermContext in expr/term_context.h. To use this class in a way + * that takes into account term contexts, the user of the term conversion + * proof generator should: + * (1) Provide a term context callback to the constructor of this class (tccb), + * (2) Register rewrite steps that indicate the term context identifier of + * the rewrite, which is a uint32_t. + * + * For example, RtfTermContext uses hash value 2 to indicate we are in a "term + * position". Say the user of this class calls: + * addRewriteStep( (and A B), BOOLEAN_TERM_VARIABLE_1, pg, true, 2) + * This indicates that (and A B) should rewrite to BOOLEAN_TERM_VARIABLE_1 if + * (and A B) occurs in a term position, where pg is a proof generator that can + * provide a closed proof of: + * (= (and A B) BOOLEAN_TERM_VARIABLE_1) + * Subsequently, this class may respond to a call to getProofFor on: + * (= + * (or (and A B) (P (and A B))) + * (or (and A B) (P BOOLEAN_TERM_VARIABLE_1))) + * where P is a predicate Bool -> Bool. The proof returned by this class + * involves congruence and pg's proof of the equivalence above. In particular, + * assuming its proof of the equivalence is P1, this proof is: + * (CONG{=} (CONG{or} (REFL (and A B)) (CONG{P} P1))) + * Notice the callback provided to this class ensures that the rewrite is + * replayed in the expected way, e.g. the occurrence of (and A B) that is not + * in term position is not rewritten. + */ +class TConvProofGenerator : public ProofGenerator +{ + public: + /** + * Constructor, which notice does fixpoint rewriting (since this is the + * most common use case) and never caches. + * + * @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. + * @param tpol The policy for applying rewrite steps of this class. For + * details, see d_policy. + * @param cpol The caching policy for this generator. + * @param name The name of this generator (for debugging). + * @param tccb The term context callback that this class depends on. If this + * is non-null, then this class stores a term-context-sensitive rewrite + * system. The rewrite steps should be given term context identifiers. + */ + TConvProofGenerator(ProofNodeManager* pnm, + context::Context* c = nullptr, + TConvPolicy pol = TConvPolicy::FIXPOINT, + TConvCachePolicy cpol = TConvCachePolicy::NEVER, + std::string name = "TConvProofGenerator", + TermContext* tccb = nullptr, + bool rewriteOps = false); + ~TConvProofGenerator(); + /** + * Add rewrite step t --> s based on proof generator. + * + * @param isPre Whether the rewrite is applied at prerewrite (pre-order + * traversal). + * @param trustId If a null proof generator is provided, we add a step to + * the proof that has trustId as the rule and expected as the sole argument. + * @param isClosed whether to expect that pg can provide a closed proof for + * this fact. + * @param tctx The term context identifier for the rewrite step. This + * value should correspond to one generated by the term context callback + * class provided in the argument tccb provided to the constructor of this + * class. + */ + void addRewriteStep(Node t, + Node s, + ProofGenerator* pg, + bool isPre = false, + PfRule trustId = PfRule::ASSUME, + bool isClosed = false, + uint32_t tctx = 0); + /** Same as above, for a single step */ + void addRewriteStep( + Node t, Node s, ProofStep ps, bool isPre = false, uint32_t tctx = 0); + /** Same as above, with explicit arguments */ + void addRewriteStep(Node t, + Node s, + PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args, + bool isPre = false, + uint32_t tctx = 0); + /** Has rewrite step for term t */ + bool hasRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) 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, uint32_t tctx = 0, bool isPre = false) 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 equality 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; + /** + * Get the proof for how term n would rewrite. This is in contrast to the + * above method where the user provides an equality (= n n'). The motivation + * for this method is when it may be expensive to compute n', and hence it + * is preferred that the proof checker computes the rewritten form of + * n, instead of verifying that n has rewritten form n'. + */ + std::shared_ptr<ProofNode> getProofForRewriting(Node n); + + protected: + typedef context::CDHashMap<Node, Node> 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_preRewriteMap; + NodeNodeMap d_postRewriteMap; + /** + * Policy for how rewrites are applied to terms. As a simple example, say we + * have registered the rewrite steps: + * addRewriteStep( a, f(c), p1 ) + * addRewriteStep( c, d, p2 ) + * Then getProofForRewriting(f(a,c),pf) returns a proof of: + * f(a,c) = f(f(d),d) if d_policy is FIXPOINT, + * f(a,c) = f(f(c),d) if d_policy is ONCE. + */ + TConvPolicy d_policy; + /** The cache policy */ + TConvCachePolicy d_cpolicy; + /** Name identifier */ + std::string d_name; + /** The cache for terms */ + std::map<Node, std::shared_ptr<ProofNode> > d_cache; + /** An (optional) term context object */ + TermContext* d_tcontext; + /** + * Whether we rewrite operators. If this flag is true, then the main + * traversal algorithm of this proof generator traverses operators of + * APPLY_UF and uses HO_CONG to justify rewriting of subterms when necessary. + */ + bool d_rewriteOps; + /** Get rewrite step for (hash value of) term. */ + Node getRewriteStepInternal(Node thash, bool isPre) const; + /** + * Adds a proof of t = t' to the proof pf where t' is the result of rewriting + * t based on the rewrite steps registered to this class. This method then + * returns the proved equality t = t'. + */ + Node getProofForRewriting(Node t, LazyCDProof& pf, TermContext* tc = nullptr); + /** + * Register rewrite step, returns the equality t=s if t is distinct from s + * and a rewrite step has not already been registered for t. + */ + Node registerRewriteStep(Node t, Node s, uint32_t tctx, bool isPre); + /** cache that r is the rewritten form of cur, pf can provide a proof */ + void doCache(Node curHash, Node cur, Node r, LazyCDProof& pf); + /** get debug information on this generator */ + std::string toStringDebug() const; +}; + +} // namespace cvc5 + +#endif /* CVC5__PROOF__CONV_PROOF_GENERATOR_H */ diff --git a/src/proof/conv_seq_proof_generator.cpp b/src/proof/conv_seq_proof_generator.cpp new file mode 100644 index 000000000..65a7e462b --- /dev/null +++ b/src/proof/conv_seq_proof_generator.cpp @@ -0,0 +1,172 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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. + * **************************************************************************** + * + * Term conversion sequence proof generator utility. + */ + +#include "proof/conv_seq_proof_generator.h" + +#include <sstream> + +#include "proof/proof_node_manager.h" + +namespace cvc5 { + +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 cvc5 diff --git a/src/proof/conv_seq_proof_generator.h b/src/proof/conv_seq_proof_generator.h new file mode 100644 index 000000000..8d4417134 --- /dev/null +++ b/src/proof/conv_seq_proof_generator.h @@ -0,0 +1,121 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Term conversion sequence proof generator utility. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__CONV_SEQ_PROOF_GENERATOR_H +#define CVC5__PROOF__CONV_SEQ_PROOF_GENERATOR_H + +#include "context/cdhashmap.h" +#include "expr/node.h" +#include "proof/proof_generator.h" +#include "proof/trust_node.h" + +namespace cvc5 { + +class ProofNodeManager; + +/** + * 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, std::hash<Node>>; + 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 cvc5 + +#endif /* CVC5__PROOF__CONV_SEQ_PROOF_GENERATOR_H */ diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp index 4ba409d6d..ca85aadd3 100644 --- a/src/proof/dot/dot_printer.cpp +++ b/src/proof/dot/dot_printer.cpp @@ -17,9 +17,9 @@ #include <sstream> -#include "expr/proof_checker.h" -#include "expr/proof_node_manager.h" #include "printer/smt2/smt2_printer.h" +#include "proof/proof_checker.h" +#include "proof/proof_node_manager.h" #include "theory/builtin/proof_checker.h" namespace cvc5 { diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h index 6e6785080..0027d145a 100644 --- a/src/proof/dot/dot_printer.h +++ b/src/proof/dot/dot_printer.h @@ -20,7 +20,7 @@ #include <iostream> -#include "expr/proof_node.h" +#include "proof/proof_node.h" namespace cvc5 { namespace proof { diff --git a/src/proof/eager_proof_generator.cpp b/src/proof/eager_proof_generator.cpp new file mode 100644 index 000000000..34ff4fa75 --- /dev/null +++ b/src/proof/eager_proof_generator.cpp @@ -0,0 +1,159 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Alex Ozdemir + * + * 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 the abstract proof generator class. + */ + +#include "proof/eager_proof_generator.h" + +#include "proof/proof.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" + +namespace cvc5 { +namespace theory { + +EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm, + context::Context* c, + std::string name) + : d_pnm(pnm), d_name(name), d_proofs(c == nullptr ? &d_context : c) +{ +} + +void EagerProofGenerator::setProofFor(Node f, std::shared_ptr<ProofNode> pf) +{ + // pf should prove f + Assert(pf->getResult() == f) + << "EagerProofGenerator::setProofFor: unexpected result" << std::endl + << "Expected: " << f << std::endl + << "Actual: " << pf->getResult() << std::endl; + d_proofs[f] = pf; +} +void EagerProofGenerator::setProofForConflict(Node conf, + std::shared_ptr<ProofNode> pf) +{ + // Normalize based on key + Node ckey = TrustNode::getConflictProven(conf); + setProofFor(ckey, pf); +} + +void EagerProofGenerator::setProofForLemma(Node lem, + std::shared_ptr<ProofNode> pf) +{ + // Normalize based on key + Node lkey = TrustNode::getLemmaProven(lem); + setProofFor(lkey, pf); +} + +void EagerProofGenerator::setProofForPropExp(TNode lit, + Node exp, + std::shared_ptr<ProofNode> pf) +{ + // Normalize based on key + Node pekey = TrustNode::getPropExpProven(lit, exp); + setProofFor(pekey, pf); +} + +std::shared_ptr<ProofNode> EagerProofGenerator::getProofFor(Node f) +{ + NodeProofNodeMap::iterator it = d_proofs.find(f); + if (it == d_proofs.end()) + { + return nullptr; + } + return (*it).second; +} + +bool EagerProofGenerator::hasProofFor(Node f) +{ + return d_proofs.find(f) != d_proofs.end(); +} + +TrustNode EagerProofGenerator::mkTrustNode(Node n, + std::shared_ptr<ProofNode> pf, + bool isConflict) +{ + if (pf == nullptr) + { + return TrustNode::null(); + } + if (isConflict) + { + // this shouldnt modify the key + setProofForConflict(n, pf); + // we can now return the trust node + return TrustNode::mkTrustConflict(n, this); + } + // this shouldnt modify the key + setProofForLemma(n, pf); + // we can now return the trust node + return TrustNode::mkTrustLemma(n, this); +} + +TrustNode EagerProofGenerator::mkTrustNode(Node conc, + PfRule id, + const std::vector<Node>& exp, + const std::vector<Node>& args, + bool isConflict) +{ + // if no children, its easy + if (exp.empty()) + { + std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, conc); + return mkTrustNode(conc, pf, isConflict); + } + // otherwise, we use CDProof + SCOPE + CDProof cdp(d_pnm); + cdp.addStep(conc, id, exp, args); + std::shared_ptr<ProofNode> pf = cdp.getProofFor(conc); + // We use mkNode instead of mkScope, since there is no reason to check + // whether the free assumptions of pf are in exp, since they are by the + // construction above. + std::shared_ptr<ProofNode> pfs = d_pnm->mkNode(PfRule::SCOPE, {pf}, exp); + return mkTrustNode(pfs->getResult(), pfs, isConflict); +} + +TrustNode EagerProofGenerator::mkTrustedRewrite(Node a, + Node b, + std::shared_ptr<ProofNode> pf) +{ + if (pf == nullptr) + { + return TrustNode::null(); + } + Node eq = a.eqNode(b); + setProofFor(eq, pf); + return TrustNode::mkTrustRewrite(a, b, this); +} + +TrustNode EagerProofGenerator::mkTrustedPropagation( + Node n, Node exp, std::shared_ptr<ProofNode> pf) +{ + if (pf == nullptr) + { + return TrustNode::null(); + } + setProofForPropExp(n, exp, pf); + return TrustNode::mkTrustPropExp(n, exp, this); +} + +TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f) +{ + // make the lemma + Node lem = f.orNode(f.notNode()); + return mkTrustNode(lem, PfRule::SPLIT, {}, {f}, false); +} + +std::string EagerProofGenerator::identify() const { return d_name; } + +} // namespace theory +} // namespace cvc5 diff --git a/src/proof/eager_proof_generator.h b/src/proof/eager_proof_generator.h new file mode 100644 index 000000000..ada48d893 --- /dev/null +++ b/src/proof/eager_proof_generator.h @@ -0,0 +1,197 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Alex Ozdemir, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * The eager proof generator class. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__EAGER_PROOF_GENERATOR_H +#define CVC5__PROOF__EAGER_PROOF_GENERATOR_H + +#include "context/cdhashmap.h" +#include "expr/node.h" +#include "proof/proof_generator.h" +#include "proof/proof_rule.h" +#include "proof/trust_node.h" + +namespace cvc5 { + +class ProofNode; +class ProofNodeManager; + +namespace theory { + +/** + * An eager proof generator, with explicit proof caching. + * + * The intended use of this class is to store proofs for lemmas and conflicts + * at the time they are sent out on the ProofOutputChannel. This means that the + * getProofForConflict and getProofForLemma methods are lookups in a + * (user-context depedent) map, the field d_proofs below. + * + * In detail, the method setProofForConflict(conf, pf) should be called prior to + * calling ProofOutputChannel(TrustNode(conf,X)), where X is this generator. + * Similarly for setProofForLemma. + * + * The intended usage of this class in combination with OutputChannel is + * the following: + * //----------------------------------------------------------- + * class MyEagerProofGenerator : public EagerProofGenerator + * { + * public: + * TrustNode getProvenConflictByMethodX(...) + * { + * // construct a conflict + * Node conf = [construct conflict]; + * // construct a proof for conf + * std::shared_ptr<ProofNode> pf = [construct the proof for conf]; + * // wrap the conflict in a trust node + * return mkTrustNode(conf,pf); + * } + * }; + * // [1] Make objects given user context u and output channel out. + * + * MyEagerProofGenerator epg(u); + * OutputChannel out; + * + * // [2] Assume epg realizes there is a conflict. We have it store the proof + * // internally and return the conflict node paired with epg. + * + * TrustNode pconf = epg.getProvenConflictByMethodX(...); + * + * // [3] Send the conflict on the output channel. + * + * out.trustedConflict(pconf); + * + * // [4] The trust node has information about what is proven and who can + * // prove it, where this association is valid in the remainder of the user + * // context. + * + * Node conf = pconf.getProven(); + * ProofGenerator * pg = pconf.getGenerator(); + * std::shared_ptr<ProofNode> pf = pg->getProofForConflict(conf); + * //----------------------------------------------------------- + * In other words, the proof generator epg is responsible for creating and + * storing the proof internally, and the proof output channel is responsible for + * maintaining the map that epg is who to ask for the proof of the conflict. + */ +class EagerProofGenerator : public ProofGenerator +{ + typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap; + + public: + EagerProofGenerator(ProofNodeManager* pnm, + context::Context* c = nullptr, + std::string name = "EagerProofGenerator"); + ~EagerProofGenerator() {} + /** Get the proof for formula f. */ + std::shared_ptr<ProofNode> getProofFor(Node f) override; + /** Can we give the proof for formula f? */ + bool hasProofFor(Node f) override; + /** + * Set proof for fact f, called when pf is a proof of f. + * + * @param f The fact proven by pf, + * @param pf The proof to store in this class. + */ + void setProofFor(Node f, std::shared_ptr<ProofNode> pf); + /** + * Make trust node: wrap n in a trust node with this generator, and have it + * store the proof pf to lemma or conflict n. + * + * @param n The proven node, + * @param pf The proof of n, + * @param isConflict Whether the returned trust node is a conflict (otherwise + * it is a lemma), + * @return The trust node corresponding to the fact that this generator has + * a proof of n. + */ + TrustNode mkTrustNode(Node n, + std::shared_ptr<ProofNode> pf, + bool isConflict = false); + /** + * Make trust node from a single step proof. This is a convenience function + * that avoids the need to explictly construct ProofNode by the caller. + * + * @param conc The conclusion of the rule, + * @param id The rule of the proof concluding conc + * @param exp The explanation (premises) to the proof concluding conc, + * @param args The arguments to the proof concluding conc, + * @param isConflict Whether the returned trust node is a conflict (otherwise + * it is a lemma), + * @return The trust node corresponding to the fact that this generator has + * a proof of (exp => conc), or of conc if exp is empty. + */ + TrustNode mkTrustNode(Node conc, + PfRule id, + const std::vector<Node>& exp, + const std::vector<Node>& args, + bool isConflict = false); + /** + * Make trust node: wrap `exp => n` in a trust node with this generator, and + * have it store the proof `pf` too. + * + * @param n The implication + * @param exp A conjunction of literals that imply it + * @param pf The proof of exp => n, + * @return The trust node corresponding to the fact that this generator has + * a proof of exp => n. + */ + TrustNode mkTrustedPropagation(Node n, + Node exp, + std::shared_ptr<ProofNode> pf); + /** + * Make trust node: `a = b` as a Rewrite trust node + * + * @param a the original + * @param b what is rewrites to + * @param pf The proof of a = b, + * @return The trust node corresponding to the fact that this generator has + * a proof of a = b + */ + TrustNode mkTrustedRewrite(Node a, Node b, std::shared_ptr<ProofNode> pf); + //--------------------------------------- common proofs + /** + * This returns the trust node corresponding to the splitting lemma + * (or f (not f)) and this generator. The method registers its proof in the + * map maintained by this class. + */ + TrustNode mkTrustNodeSplit(Node f); + //--------------------------------------- end common proofs + /** identify */ + std::string identify() const override; + + protected: + /** Set that pf is the proof for conflict conf */ + void setProofForConflict(Node conf, std::shared_ptr<ProofNode> pf); + /** Set that pf is the proof for lemma lem */ + void setProofForLemma(Node lem, std::shared_ptr<ProofNode> pf); + /** Set that pf is the proof for explained propagation */ + void setProofForPropExp(TNode lit, Node exp, std::shared_ptr<ProofNode> pf); + /** The proof node manager */ + ProofNodeManager* d_pnm; + /** Name identifier */ + std::string d_name; + /** A dummy context used by this class if none is provided */ + context::Context d_context; + /** + * A user-context-dependent map from lemmas and conflicts to proofs provided + * by calls to setProofForConflict and setProofForLemma above. + */ + NodeProofNodeMap d_proofs; +}; + +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__PROOF__PROOF_GENERATOR_H */ diff --git a/src/proof/lazy_proof.cpp b/src/proof/lazy_proof.cpp new file mode 100644 index 000000000..d7b62a8dc --- /dev/null +++ b/src/proof/lazy_proof.cpp @@ -0,0 +1,231 @@ +/****************************************************************************** + * 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 lazy proof utility. + */ + +#include "proof/lazy_proof.h" + +#include "proof/proof_ensure_closed.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" + +using namespace cvc5::kind; + +namespace cvc5 { + +LazyCDProof::LazyCDProof(ProofNodeManager* pnm, + ProofGenerator* dpg, + context::Context* c, + std::string name) + : CDProof(pnm, c, name), d_gens(c ? c : &d_context), d_defaultGen(dpg) +{ +} + +LazyCDProof::~LazyCDProof() {} + +std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact) +{ + Trace("lazy-cdproof") << "LazyCDProof::mkLazyProof " << fact << std::endl; + // make the proof, which should always be non-null, since we construct an + // assumption in the worst case. + std::shared_ptr<ProofNode> opf = CDProof::getProofFor(fact); + Assert(opf != nullptr); + if (!hasGenerators()) + { + Trace("lazy-cdproof") << "...no generators, finished" << std::endl; + // optimization: no generators, we are done + return opf; + } + // otherwise, we traverse the proof opf and fill in the ASSUME leafs that + // have generators + std::unordered_set<ProofNode*> visited; + std::unordered_set<ProofNode*>::iterator it; + std::vector<ProofNode*> visit; + ProofNode* cur; + visit.push_back(opf.get()); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + + if (it == visited.end()) + { + visited.insert(cur); + Node cfact = cur->getResult(); + if (getProof(cfact).get() != cur) + { + // We don't own this proof, skip it. This is to ensure that this method + // is idempotent, since it may be the case that a previous call to + // getProofFor connected a proof from a proof generator as a child of + // a ProofNode in the range of the map in CDProof. Thus, this ensures + // we don't touch such proofs. + Trace("lazy-cdproof") << "...skip unowned proof" << std::endl; + } + else if (cur->getRule() == PfRule::ASSUME) + { + bool isSym = false; + ProofGenerator* pg = getGeneratorFor(cfact, isSym); + if (pg != nullptr) + { + Trace("lazy-cdproof") + << "LazyCDProof: Call generator " << pg->identify() + << " for assumption " << cfact << std::endl; + Node cfactGen = isSym ? CDProof::getSymmFact(cfact) : cfact; + Assert(!cfactGen.isNull()); + // Do not use the addProofTo interface, instead use the update node + // interface, since this ensures that we don't take ownership for + // the current proof. Instead, it is only linked, and ignored on + // future calls to getProofFor due to the check above. + std::shared_ptr<ProofNode> pgc = pg->getProofFor(cfactGen); + // If the proof was null, then the update is not performed. This is + // not considered an error, since this behavior is equivalent to + // if pg had provided the proof (ASSUME cfactGen). Ensuring the + // proper behavior wrt closed proofs should be done outside this + // method. + if (pgc != nullptr) + { + Trace("lazy-cdproof-gen") + << "LazyCDProof: stored proof: " << *pgc.get() << std::endl; + + if (isSym) + { + d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {}); + } + else + { + d_manager->updateNode(cur, pgc.get()); + } + Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for " + << cfactGen << std::endl; + } + } + else + { + Trace("lazy-cdproof") << "LazyCDProof: " << identify() + << " : No generator for " << cfact << std::endl; + } + // Notice that we do not traverse the proofs that have been generated + // lazily by the proof generators here. In other words, we assume that + // the proofs from provided proof generators are final and need + // no further modification by this class. + } + else + { + const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren(); + for (const std::shared_ptr<ProofNode>& cp : cc) + { + visit.push_back(cp.get()); + } + } + } + } while (!visit.empty()); + // we have now updated the ASSUME leafs of opf, return it + Trace("lazy-cdproof") << "...finished" << std::endl; + Assert(opf->getResult() == fact); + return opf; +} + +void LazyCDProof::addLazyStep(Node expected, + ProofGenerator* pg, + PfRule idNull, + bool isClosed, + const char* ctx, + bool forceOverwrite) +{ + if (pg == nullptr) + { + // null generator, should have given a proof rule + if (idNull == PfRule::ASSUME) + { + Unreachable() << "LazyCDProof::addLazyStep: " << identify() + << ": failed to provide proof generator for " << expected; + return; + } + Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected + << " set (trusted) step " << idNull << "\n"; + addStep(expected, idNull, {}, {expected}); + return; + } + Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected + << " set to generator " << pg->identify() << "\n"; + if (!forceOverwrite) + { + NodeProofGeneratorMap::const_iterator it = d_gens.find(expected); + if (it != d_gens.end()) + { + // don't overwrite something that is already there + return; + } + } + // just store now + d_gens.insert(expected, pg); + // debug checking + if (isClosed) + { + Trace("lazy-cdproof-debug") << "Checking closed..." << std::endl; + pfgEnsureClosed(expected, pg, "lazy-cdproof-debug", ctx); + } +} + +ProofGenerator* LazyCDProof::getGeneratorFor(Node fact, bool& isSym) +{ + isSym = false; + NodeProofGeneratorMap::const_iterator it = d_gens.find(fact); + if (it != d_gens.end()) + { + return (*it).second; + } + Node factSym = CDProof::getSymmFact(fact); + // could be symmetry + if (factSym.isNull()) + { + // can't be symmetry, return the default generator + return d_defaultGen; + } + it = d_gens.find(factSym); + if (it != d_gens.end()) + { + isSym = true; + return (*it).second; + } + // return the default generator + return d_defaultGen; +} + +bool LazyCDProof::hasGenerators() const +{ + return !d_gens.empty() || d_defaultGen != nullptr; +} + +bool LazyCDProof::hasGenerator(Node fact) const +{ + if (d_defaultGen != nullptr) + { + return true; + } + NodeProofGeneratorMap::const_iterator it = d_gens.find(fact); + if (it != d_gens.end()) + { + return true; + } + // maybe there is a symmetric fact? + Node factSym = CDProof::getSymmFact(fact); + if (!factSym.isNull()) + { + it = d_gens.find(factSym); + } + return it != d_gens.end(); +} + +} // namespace cvc5 diff --git a/src/proof/lazy_proof.h b/src/proof/lazy_proof.h new file mode 100644 index 000000000..b566e408e --- /dev/null +++ b/src/proof/lazy_proof.h @@ -0,0 +1,110 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Lazy proof utility. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__LAZY_PROOF_H +#define CVC5__PROOF__LAZY_PROOF_H + +#include "proof/proof.h" + +namespace cvc5 { + +class ProofGenerator; +class ProofNodeManager; + +/** + * A (context-dependent) lazy proof. This class is an extension of CDProof + * that additionally maps facts to proof generators in a context-dependent + * manner. It extends CDProof with an additional method, addLazyStep for adding + * steps to a proof via a given proof generator. + */ +class LazyCDProof : public CDProof +{ + public: + /** Constructor + * + * @param pnm The proof node manager for constructing ProofNode objects. + * @param dpg The (optional) default proof generator, which is called + * for facts that have no explicitly provided generator. + * @param c The context that this class depends on. If none is provided, + * this class is context-independent. + */ + LazyCDProof(ProofNodeManager* pnm, + ProofGenerator* dpg = nullptr, + context::Context* c = nullptr, + std::string name = "LazyCDProof"); + ~LazyCDProof(); + /** + * Get lazy proof for fact, or nullptr if it does not exist. This may + * additionally call proof generators to generate proofs for ASSUME nodes that + * don't yet have a concrete proof. + */ + std::shared_ptr<ProofNode> getProofFor(Node fact) override; + /** Add step by generator + * + * This method stores that expected can be proven by proof generator pg if + * it is required to do so. This mapping is maintained in the remainder of + * the current context (according to the context c provided to this class). + * + * It is important to note that pg is asked to provide a proof for expected + * only when no other call for the fact expected is provided via the addStep + * method of this class. In particular, pg is asked to prove expected when it + * appears as the conclusion of an ASSUME leaf within CDProof::getProofFor. + * + * @param expected The fact that can be proven. + * @param pg The generator that can proof expected. + * @param trustId If a null proof generator is provided, we add a step to + * the proof that has trustId as the rule and expected as the sole argument. + * We do this only if trustId is not PfRule::ASSUME. This is primarily used + * for identifying the kind of hole when a proof generator is not given. + * @param isClosed Whether to expect that pg can provide a closed proof for + * this fact. + * @param ctx The context we are in (for debugging). + * @param forceOverwrite If this flag is true, then this call overwrites + * an existing proof generator provided for expected, if one was provided + * via a previous call to addLazyStep in the current context. + */ + void addLazyStep(Node expected, + ProofGenerator* pg, + PfRule trustId = PfRule::ASSUME, + bool isClosed = false, + const char* ctx = "LazyCDProof::addLazyStep", + bool forceOverwrite = false); + /** + * Does this have any proof generators? This method always returns true + * if the default is non-null. + */ + bool hasGenerators() const; + /** Does the given fact have an explicitly provided generator? */ + bool hasGenerator(Node fact) const; + + protected: + typedef context::CDHashMap<Node, ProofGenerator*> NodeProofGeneratorMap; + /** Maps facts that can be proven to generators */ + NodeProofGeneratorMap d_gens; + /** The default proof generator */ + ProofGenerator* d_defaultGen; + /** + * Get generator for fact, or nullptr if it doesnt exist. This method is + * robust to symmetry of (dis)equality. It updates isSym to true if a + * proof generator for the symmetric form of fact was provided. + */ + ProofGenerator* getGeneratorFor(Node fact, bool& isSym); +}; + +} // namespace cvc5 + +#endif /* CVC5__PROOF__LAZY_PROOF_H */ diff --git a/src/proof/lazy_proof_chain.cpp b/src/proof/lazy_proof_chain.cpp new file mode 100644 index 000000000..4c1b19ffe --- /dev/null +++ b/src/proof/lazy_proof_chain.cpp @@ -0,0 +1,327 @@ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Andrew Reynolds, Gereon Kremer + * + * 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 lazy proof utility. + */ + +#include "proof/lazy_proof_chain.h" + +#include "options/proof_options.h" +#include "proof/proof.h" +#include "proof/proof_ensure_closed.h" +#include "proof/proof_node.h" +#include "proof/proof_node_algorithm.h" +#include "proof/proof_node_manager.h" + +namespace cvc5 { + +LazyCDProofChain::LazyCDProofChain(ProofNodeManager* pnm, + bool cyclic, + context::Context* c, + ProofGenerator* defGen, + bool defRec) + : d_manager(pnm), + d_cyclic(cyclic), + d_defRec(defRec), + d_context(), + d_gens(c ? c : &d_context), + d_defGen(defGen) +{ +} + +LazyCDProofChain::~LazyCDProofChain() {} + +const std::map<Node, std::shared_ptr<ProofNode>> LazyCDProofChain::getLinks() + const +{ + std::map<Node, std::shared_ptr<ProofNode>> links; + for (const std::pair<const Node, ProofGenerator* const>& link : d_gens) + { + Assert(link.second); + std::shared_ptr<ProofNode> pfn = link.second->getProofFor(link.first); + Assert(pfn); + links[link.first] = pfn; + } + return links; +} + +std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact) +{ + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor " << fact << "\n"; + // which facts have had proofs retrieved for. This is maintained to avoid + // cycles. It also saves the proof node of the fact + std::unordered_map<Node, std::shared_ptr<ProofNode>> toConnect; + // leaves of proof node links in the chain, i.e. assumptions, yet to be + // expanded + std::unordered_map<Node, std::vector<std::shared_ptr<ProofNode>>> + assumptionsToExpand; + // invariant of the loop below, the first iteration notwithstanding: + // visit = domain(assumptionsToExpand) \ domain(toConnect) + std::vector<Node> visit{fact}; + std::unordered_map<Node, bool> visited; + Node cur; + do + { + cur = visit.back(); + visit.pop_back(); + auto itVisited = visited.find(cur); + // pre-traversal + if (itVisited == visited.end()) + { + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor: check " << cur << "\n"; + Assert(toConnect.find(cur) == toConnect.end()); + bool rec = true; + ProofGenerator* pg = getGeneratorForInternal(cur, rec); + if (!pg) + { + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor: nothing to do\n"; + // nothing to do for this fact, it'll be a leaf in the final proof + // node, don't post-traverse. + visited[cur] = true; + continue; + } + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor: Call generator " << pg->identify() + << " for chain link " << cur << "\n"; + std::shared_ptr<ProofNode> curPfn = pg->getProofFor(cur); + if (curPfn == nullptr) + { + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor: No proof found, skip\n"; + visited[cur] = true; + continue; + } + // map node whose proof node must be expanded to the respective poof node + toConnect[cur] = curPfn; + if (!rec) + { + // we don't want to recursively connect this proof + visited[cur] = true; + continue; + } + Trace("lazy-cdproofchain-debug") + << "LazyCDProofChain::getProofFor: stored proof: " << *curPfn.get() + << "\n"; + // retrieve free assumptions and their respective proof nodes + std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap; + expr::getFreeAssumptionsMap(curPfn, famap); + if (Trace.isOn("lazy-cdproofchain")) + { + unsigned alreadyToVisit = 0; + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor: " << famap.size() + << " free assumptions:\n"; + for (auto fap : famap) + { + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor: - " << fap.first << "\n"; + alreadyToVisit += + std::find(visit.begin(), visit.end(), fap.first) != visit.end() + ? 1 + : 0; + } + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor: " << alreadyToVisit + << " already to visit\n"; + } + // mark for post-traversal if we are controlling cycles + if (d_cyclic) + { + Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: marking " + << cur << " for cycle check\n"; + visit.push_back(cur); + visited[cur] = false; + } + else + { + visited[cur] = true; + } + // enqueue free assumptions to process + for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& + fap : famap) + { + // check cycles + if (d_cyclic) + { + // cycles are assumptions being *currently* expanded and seen again, + // i.e. in toConnect and not yet post-visited + auto itToConnect = toConnect.find(fap.first); + if (itToConnect != toConnect.end() && !visited[fap.first]) + { + // Since we have a cycle with an assumption, this fact will be an + // assumption in the final proof node produced by this + // method. Thus we erase it as something to be connected, which + // will keep it as an assumption. + Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: " + "removing cyclic assumption " + << fap.first << " from expansion\n"; + continue; + } + } + // We always add assumptions to visit so that their last seen occurrence + // is expanded (rather than the first seen occurrence, if we were not + // adding assumptions, say, in assumptionsToExpand). This is so because + // in the case where we are checking cycles this is necessary (and + // harmless when we are not). For example the cycle + // + // a2 + // ... + // ---- + // a1 + // ... + // -------- + // a0 a1 a2 + // ... + // --------------- + // n + // + // in which a2 has a1 as an assumption, which has a2 an assumption, + // would not be captured if we did not revisit a1, which is an + // assumption of n and this already occur in assumptionsToExpand when + // it shows up again as an assumption of a2. + visit.push_back(fap.first); + // add assumption proof nodes to be updated + assumptionsToExpand[fap.first].insert( + assumptionsToExpand[fap.first].end(), + fap.second.begin(), + fap.second.end()); + } + if (d_cyclic) + { + Trace("lazy-cdproofchain") << push; + Trace("lazy-cdproofchain-debug") << push; + } + } + else if (!itVisited->second) + { + visited[cur] = true; + Trace("lazy-cdproofchain") << pop; + Trace("lazy-cdproofchain-debug") << pop; + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor: post-visited " << cur << "\n"; + } + else + { + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor: already fully processed " << cur + << "\n"; + } + } while (!visit.empty()); + // expand all assumptions marked to be connected + for (const std::pair<const Node, std::shared_ptr<ProofNode>>& npfn : + toConnect) + { + auto it = assumptionsToExpand.find(npfn.first); + if (it == assumptionsToExpand.end()) + { + Assert(npfn.first == fact); + continue; + } + Assert(npfn.second); + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor: expand assumption " << npfn.first + << "\n"; + Trace("lazy-cdproofchain-debug") + << "LazyCDProofChain::getProofFor: ...expand to " << *npfn.second.get() + << "\n"; + // update each assumption proof node + for (std::shared_ptr<ProofNode> pfn : it->second) + { + d_manager->updateNode(pfn.get(), npfn.second.get()); + } + } + // final proof of fact + auto it = toConnect.find(fact); + if (it == toConnect.end()) + { + return nullptr; + } + return it->second; +} + +void LazyCDProofChain::addLazyStep(Node expected, ProofGenerator* pg) +{ + Assert(pg != nullptr); + Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected + << " set to generator " << pg->identify() << "\n"; + // note this will replace the generator for expected, if any + d_gens.insert(expected, pg); +} + +void LazyCDProofChain::addLazyStep(Node expected, + ProofGenerator* pg, + const std::vector<Node>& assumptions, + const char* ctx) +{ + Assert(pg != nullptr); + Trace("lazy-cdproofchain") << "LazyCDProofChain::addLazyStep: " << expected + << " set to generator " << pg->identify() << "\n"; + // note this will rewrite the generator for expected, if any + d_gens.insert(expected, pg); + // check if chain is closed if options::proofEagerChecking() is on + if (options::proofEagerChecking()) + { + Trace("lazy-cdproofchain") + << "LazyCDProofChain::addLazyStep: Checking closed proof...\n"; + std::shared_ptr<ProofNode> pfn = pg->getProofFor(expected); + std::vector<Node> allowedLeaves{assumptions.begin(), assumptions.end()}; + // add all current links in the chain + for (const std::pair<const Node, ProofGenerator* const>& link : d_gens) + { + allowedLeaves.push_back(link.first); + } + if (Trace.isOn("lazy-cdproofchain")) + { + Trace("lazy-cdproofchain") << "Checking relative to leaves...\n"; + for (const Node& n : allowedLeaves) + { + Trace("lazy-cdproofchain") << " - " << n << "\n"; + } + Trace("lazy-cdproofchain") << "\n"; + } + pfnEnsureClosedWrt(pfn.get(), allowedLeaves, "lazy-cdproofchain", ctx); + } +} + +bool LazyCDProofChain::hasGenerator(Node fact) const +{ + return d_gens.find(fact) != d_gens.end(); +} + +ProofGenerator* LazyCDProofChain::getGeneratorFor(Node fact) +{ + bool rec = true; + return getGeneratorForInternal(fact, rec); +} + +ProofGenerator* LazyCDProofChain::getGeneratorForInternal(Node fact, bool& rec) +{ + auto it = d_gens.find(fact); + if (it != d_gens.end()) + { + return (*it).second; + } + // otherwise, if no explicit generators, we use the default one + if (d_defGen != nullptr) + { + rec = d_defRec; + return d_defGen; + } + return nullptr; +} + +std::string LazyCDProofChain::identify() const { return "LazyCDProofChain"; } + +} // namespace cvc5 diff --git a/src/proof/lazy_proof_chain.h b/src/proof/lazy_proof_chain.h new file mode 100644 index 000000000..4315ee87a --- /dev/null +++ b/src/proof/lazy_proof_chain.h @@ -0,0 +1,154 @@ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, Andrew Reynolds, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Lazy proof chain utility. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__LAZY_PROOF_CHAIN_H +#define CVC5__PROOF__LAZY_PROOF_CHAIN_H + +#include <vector> + +#include "context/cdhashmap.h" +#include "proof/proof_generator.h" + +namespace cvc5 { + +class ProofNodeManager; + +/** + * A (context-dependent) lazy generator for proof chains. This class is an + * extension of ProofGenerator that additionally that maps facts to proof + * generators in a context-dependent manner. The map is built with the addition + * of lazy steps mapping facts to proof generators. More importantly, its + * getProofFor method expands the proof generators registered to this class by + * connecting, for the proof generated to one fact, assumptions to the proofs + * generated for those assumptinos that are registered in the chain. + */ +class LazyCDProofChain : public ProofGenerator +{ + public: + /** Constructor + * + * @param pnm The proof node manager for constructing ProofNode objects. + * @param cyclic Whether this instance is robust to cycles in the chain. + * @param c The context that this class depends on. If none is provided, + * this class is context-independent. + * @param defGen The default generator to be used if no generator exists + * for a step. + * @param defRec Whether this instance expands proofs from defGen recursively. + */ + LazyCDProofChain(ProofNodeManager* pnm, + bool cyclic = true, + context::Context* c = nullptr, + ProofGenerator* defGen = nullptr, + bool defRec = true); + ~LazyCDProofChain(); + /** + * Get lazy proof for fact, or nullptr if it does not exist, by connecting the + * proof nodes generated for each intermediate relevant fact registered in the + * chain (i.e., in the domain of d_gens). + * + * For example, if d_gens consists of the following pairs + * + * --- (A, PG1) + * --- (B, PG2) + * --- (C, PG3) + * + * and getProofFor(A) is called, with PG1 generating a proof with assumptions + * B and D, then B is expanded, with its assumption proof node being updated + * to the expanded proof node, while D is not. Assuming PG2 provides a proof + * with assumptions C and E, then C is expanded and E is not. Suppose PG3 + * gives a closed proof, thus the call getProofFor(A) produces a proof node + * + * A : ( ... B : ( ... C : (...), ... ASSUME( E ) ), ... ASSUME( D ) ) + * + * Note that the expansions are done directly on the proof nodes produced by + * the generators. + * + * If this instance has been set to be robust to cyclic proofs (i.e., d_cyclic + * is true), then the construction of the proof chain checks that there are no + * cycles, i.e., a given fact would have itself as an assumption when + * connecting the chain links. If such a cycle were to be detected then the + * fact will be marked as an assumption and not expanded in the final proof + * node. The method does not fail. + */ + std::shared_ptr<ProofNode> getProofFor(Node fact) override; + /** Add step by generator + * + * This method stores that expected can be proven by proof generator pg if + * it is required to do so. This mapping is maintained in the remainder of + * the current context (according to the context c provided to this class). + * + * Moreover the lazy steps of this class are expected to fulfill the + * requirement that pg.getProofFor(expected) generates a proof node closed + * with relation to + * (1) a fixed set F1, ..., Fn, + * (2) formulas in the current domain of d_gens. + * + * This is so that we only add links to the chain that depend on a fixed set + * of assumptions or in other links. + * + * @param expected The fact that can be proven. + * @param pg The generator that can proof expected. + * @param assumptions The fixed set of assumptions with relation to which the + * chain, now augmented with expect, must be closed. + * @param ctx The context we are in (for debugging). + */ + void addLazyStep(Node expected, + ProofGenerator* pg, + const std::vector<Node>& assumptions, + const char* ctx = "LazyCDProofChain::addLazyStep"); + + /** As above but does not do the closedness check. */ + void addLazyStep(Node expected, ProofGenerator* pg); + + /** Does the given fact have an explicitly provided generator? */ + bool hasGenerator(Node fact) const; + + /** + * Get generator for fact, or nullptr if it doesnt exist. + */ + ProofGenerator* getGeneratorFor(Node fact); + + /** identify */ + std::string identify() const override; + + /** Retrieve, for each fact in d_gens, it mapped to the proof node generated + * by its generator in d_gens. */ + const std::map<Node, std::shared_ptr<ProofNode>> getLinks() const; + + private: + /** + * Get generator for fact, or nullptr if it doesnt exist. Updates rec to + * true if we should recurse on its proof. + */ + ProofGenerator* getGeneratorForInternal(Node fact, bool& rec); + /** The proof manager, used for allocating new ProofNode objects */ + ProofNodeManager* d_manager; + /** Whether this instance is robust to cycles in the chain. */ + bool d_cyclic; + /** Whether we expand recursively (for the default generator) */ + bool d_defRec; + /** A dummy context used by this class if none is provided */ + context::Context d_context; + /** Maps facts that can be proven to generators */ + context::CDHashMap<Node, ProofGenerator*> d_gens; + /** The default proof generator (if one exists) */ + ProofGenerator* d_defGen; +}; + +} // namespace cvc5 + +#endif /* CVC5__PROOF__LAZY_PROOF_CHAIN_H */ diff --git a/src/proof/lazy_tree_proof_generator.cpp b/src/proof/lazy_tree_proof_generator.cpp new file mode 100644 index 000000000..a50b9efd4 --- /dev/null +++ b/src/proof/lazy_tree_proof_generator.cpp @@ -0,0 +1,146 @@ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * 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 the lazy tree proof generator class. + */ + +#include "proof/lazy_tree_proof_generator.h" + +#include <iostream> + +#include "expr/node.h" +#include "proof/proof_generator.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" + +namespace cvc5 { +namespace theory { + +LazyTreeProofGenerator::LazyTreeProofGenerator(ProofNodeManager* pnm, + const std::string& name) + : d_pnm(pnm), d_name(name) +{ + d_stack.emplace_back(&d_proof); +} +void LazyTreeProofGenerator::openChild() +{ + detail::TreeProofNode& pn = getCurrent(); + pn.d_children.emplace_back(); + d_stack.emplace_back(&pn.d_children.back()); +} +void LazyTreeProofGenerator::closeChild() +{ + Assert(getCurrent().d_rule != PfRule::UNKNOWN); + d_stack.pop_back(); +} +detail::TreeProofNode& LazyTreeProofGenerator::getCurrent() +{ + Assert(!d_stack.empty()) << "Proof construction has already been finished."; + return *d_stack.back(); +} +void LazyTreeProofGenerator::setCurrent(PfRule rule, + const std::vector<Node>& premise, + std::vector<Node> args, + Node proven) +{ + detail::TreeProofNode& pn = getCurrent(); + pn.d_rule = rule; + pn.d_premise = premise; + pn.d_args = args; + pn.d_proven = proven; +} +std::shared_ptr<ProofNode> LazyTreeProofGenerator::getProof() const +{ + // Check cache + if (d_cached) return d_cached; + Assert(d_stack.empty()) << "Proof construction has not yet been finished."; + std::vector<std::shared_ptr<ProofNode>> scope; + d_cached = getProof(scope, d_proof); + return d_cached; +} + +std::shared_ptr<ProofNode> LazyTreeProofGenerator::getProofFor(Node f) +{ + Assert(hasProofFor(f)); + return getProof(); +} + +bool LazyTreeProofGenerator::hasProofFor(Node f) +{ + return f == getProof()->getResult(); +} + +std::shared_ptr<ProofNode> LazyTreeProofGenerator::getProof( + std::vector<std::shared_ptr<ProofNode>>& scope, + const detail::TreeProofNode& pn) const +{ + // Store scope size to reset scope afterwards + std::size_t before = scope.size(); + std::vector<std::shared_ptr<ProofNode>> children; + if (pn.d_rule == PfRule::SCOPE) + { + // Extend scope for all but the root node + if (&pn != &d_proof) + { + for (const auto& a : pn.d_args) + { + scope.emplace_back(d_pnm->mkAssume(a)); + } + } + } + else + { + // Initialize the children with the scope + children = scope; + } + for (auto& c : pn.d_children) + { + // Recurse into tree + children.emplace_back(getProof(scope, c)); + } + for (const auto& p : pn.d_premise) + { + // Add premises as assumptions + children.emplace_back(d_pnm->mkAssume(p)); + } + // Reset scope + scope.resize(before); + return d_pnm->mkNode(pn.d_rule, children, pn.d_args); +} + +void LazyTreeProofGenerator::print(std::ostream& os, + const std::string& prefix, + const detail::TreeProofNode& pn) const +{ + os << prefix << pn.d_rule << ": "; + container_to_stream(os, pn.d_premise); + os << " ==> " << pn.d_proven << std::endl; + if (!pn.d_args.empty()) + { + os << prefix << ":args "; + container_to_stream(os, pn.d_args); + std::cout << std::endl; + } + for (const auto& c : pn.d_children) + { + print(os, prefix + '\t', c); + } +} + +std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg) +{ + ltpg.print(os, "", ltpg.d_proof); + return os; +} + +} // namespace theory +} // namespace cvc5 diff --git a/src/proof/lazy_tree_proof_generator.h b/src/proof/lazy_tree_proof_generator.h new file mode 100644 index 000000000..8b8d344e9 --- /dev/null +++ b/src/proof/lazy_tree_proof_generator.h @@ -0,0 +1,223 @@ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer + * + * 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. + * **************************************************************************** + * + * The lazy tree proof generator class. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__LAZY_TREE_PROOF_GENERATOR_H +#define CVC5__PROOF__LAZY_TREE_PROOF_GENERATOR_H + +#include <iostream> + +#include "expr/node.h" +#include "proof/proof_generator.h" +#include "proof/proof_node_manager.h" + +namespace cvc5 { +namespace theory { +namespace detail { +/** + * A single node in the proof tree created by the LazyTreeProofGenerator. + * A node directly represents a ProofNode that is eventually constructed from + * it. The Nodes of the additional field d_premise are added to d_children as + * new assumptions via ASSUME. + */ +struct TreeProofNode +{ + /** The proof rule */ + PfRule d_rule = PfRule::UNKNOWN; + /** Assumptions used as premise for this proof step */ + std::vector<Node> d_premise; + /** Arguments for this proof step */ + std::vector<Node> d_args; + /** Conclusion of this proof step */ + Node d_proven; + /** Children of this proof step */ + std::vector<TreeProofNode> d_children; +}; +} // namespace detail + +/** + * This class supports the lazy creation of a tree-shaped proof. + * The core idea is that the lazy creation is necessary because proof rules + * depend on assumptions that are only known after the whole subtree has been + * finished. + * + * We indend to argue about proofs that roughly go as follows: + * - we assume a set of assumptions + * - we do a case split + * - for every case, we derive false, possibly by nested case splits + * + * Every case is represented by a SCOPE whose child derives false. When + * composing the final proof, we explicitly extend the premise of every proof + * step with the scope (the currently selected case) that this proof step lives + * in. When doing this, we ignore the outermost scope (which assumes the + * assertion set) to allow for having conflicts that are only a subset of the + * assertion set. + * + * Consider the example x*x<1 and x>2 and the intended proof + * (SCOPE + * (ARITH_NL_CAD_SPLIT + * (SCOPE + * (ARITH_NL_CAD_DIRECT (x<=2 and x>2) ==> false) + * :args [x<=2] + * ) + * (SCOPE + * (ARITH_NL_CAD_DIRECT (x>=1 and x*x<1) ==> false) + * :args [x>=1] + * ) + * ) + * :args [ x*x<1, x>2 ] + * ) + * We obtain this proof in a way that (in general) gives us the assumptions + * for the scopes (x<=2, x>=1) only when the scope children have been fully + * computed. Thus, we store the proof in an intermediate form and add the scope + * arguments when we learn them. Once we have completed the proof, we can easily + * transform it into proper ProofNodes. + * + * This class is stateful in the sense that the interface (in particular + * openChild() and closeChild()) navigates the proof tree (and creating it + * on-the-fly). Initially, and after reset() has been called, the proof consists + * of one empty proof node (with proof rule UNKNOWN). It stores the current + * position in the proof tree internally to make the interface easier to use. + * + * THIS MAKES THIS CLASS INHERENTLY NOT THREAD-SAFE! + * + * To construct the above proof, use this class roughly as follows: + * setCurrent(SCOPE, {}, assertions, false); + * openChild(); + * // First nested scope + * openChild(); + * setCurrent(SCOPE, {}, {}, false); + * openChild(); + * setCurrent(CAD_DIRECT, {x>2}, {}, false); + * closeChild(); + * getCurrent().args = {x<=2}; + * closeChild(); + * // Second nested scope + * openChild(); + * setCurrent(SCOPE, {}, {}, false); + * openChild(); + * setCurrent(CAD_DIRECT, {x*x<1}, {}, false); + * closeChild(); + * getCurrent().args = {x>=1}; + * closeChild(); + * // Finish split + * setCurrent(CAD_SPLIT, {}, {}, false); + * closeChild(); + * closeChild(); + * + * To explicitly finish proof construction, we need to call closeChild() one + * additional time. + */ +class LazyTreeProofGenerator : public ProofGenerator +{ + public: + friend std::ostream& operator<<(std::ostream& os, + const LazyTreeProofGenerator& ltpg); + + LazyTreeProofGenerator(ProofNodeManager* pnm, + const std::string& name = "LazyTreeProofGenerator"); + + std::string identify() const override { return d_name; } + /** Create a new child and make it the current node */ + void openChild(); + /** + * Finish the current node and return to its parent + * Checks that the current node has a proof rule different from UNKNOWN. + * When called on the root node, this finishes the proof construction: we can + * no longer call getCurrent(), setCurrent() openChild() and closeChild(), but + * instead can call getProof() now. + */ + void closeChild(); + /** + * Return a reference to the current node + */ + detail::TreeProofNode& getCurrent(); + /** Set the current node / proof step */ + void setCurrent(PfRule rule, + const std::vector<Node>& premise, + std::vector<Node> args, + Node proven); + /** Construct the proof as a ProofNode */ + std::shared_ptr<ProofNode> getProof() const; + /** Return the constructed proof. Checks that we have proven f */ + std::shared_ptr<ProofNode> getProofFor(Node f) override; + /** Checks whether we have proven f */ + bool hasProofFor(Node f) override; + + /** + * Removes children from the current node based on the given predicate. + * It can be used for cases where facts (and their proofs) are eagerly + * generated and then later pruned, for example to produce smaller conflicts. + * The predicate is given as a Callable f that is called for every child with + * the id of the child and the child itself. + * f should return true if the child should be kept, fals if the child should + * be removed. + * @param f a Callable bool(std::size_t, const detail::TreeProofNode&) + */ + template <typename F> + void pruneChildren(F&& f) + { + auto& children = getCurrent().d_children; + std::size_t cur = 0; + std::size_t pos = 0; + for (std::size_t size = children.size(); cur < size; ++cur) + { + if (f(cur, children[pos])) + { + if (cur != pos) + { + children[pos] = std::move(children[cur]); + } + ++pos; + } + } + children.resize(pos); + } + + private: + /** recursive proof construction used by getProof() */ + std::shared_ptr<ProofNode> getProof( + std::vector<std::shared_ptr<ProofNode>>& scope, + const detail::TreeProofNode& pn) const; + + /** recursive debug printing used by operator<<() */ + void print(std::ostream& os, + const std::string& prefix, + const detail::TreeProofNode& pn) const; + + /** The ProofNodeManager used for constructing ProofNodes */ + ProofNodeManager* d_pnm; + /** The trace to the current node */ + std::vector<detail::TreeProofNode*> d_stack; + /** The root node of the proof tree */ + detail::TreeProofNode d_proof; + /** Caches the result of getProof() */ + mutable std::shared_ptr<ProofNode> d_cached; + /** Name of this proof generator */ + std::string d_name; +}; + +/** + * Prints the current state of a LazyTreeProofGenerator. Can also be used on a + * partially constructed proof. It is intended for debugging only and attempts + * to pretty-print itself using indentation. + */ +std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg); + +} // namespace theory +} // namespace cvc5 + +#endif diff --git a/src/proof/proof.cpp b/src/proof/proof.cpp new file mode 100644 index 000000000..a100be990 --- /dev/null +++ b/src/proof/proof.cpp @@ -0,0 +1,459 @@ +/****************************************************************************** + * 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 proof. + */ + +#include "proof/proof.h" + +#include "proof/proof_checker.h" +#include "proof/proof_node.h" +#include "proof/proof_node_manager.h" + +using namespace cvc5::kind; + +namespace cvc5 { + +CDProof::CDProof(ProofNodeManager* pnm, + context::Context* c, + std::string name, + bool autoSymm) + : d_manager(pnm), + d_context(), + d_nodes(c ? c : &d_context), + d_name(name), + d_autoSymm(autoSymm) +{ +} + +CDProof::~CDProof() {} + +std::shared_ptr<ProofNode> CDProof::getProofFor(Node fact) +{ + std::shared_ptr<ProofNode> pf = getProofSymm(fact); + if (pf != nullptr) + { + return pf; + } + // add as assumption + std::vector<Node> pargs = {fact}; + std::vector<std::shared_ptr<ProofNode>> passume; + std::shared_ptr<ProofNode> pfa = + d_manager->mkNode(PfRule::ASSUME, passume, pargs, fact); + d_nodes.insert(fact, pfa); + return pfa; +} + +std::shared_ptr<ProofNode> CDProof::getProof(Node fact) const +{ + NodeProofNodeMap::iterator it = d_nodes.find(fact); + if (it != d_nodes.end()) + { + return (*it).second; + } + return nullptr; +} + +std::shared_ptr<ProofNode> CDProof::getProofSymm(Node fact) +{ + Trace("cdproof") << "CDProof::getProofSymm: " << fact << std::endl; + std::shared_ptr<ProofNode> pf = getProof(fact); + if (pf != nullptr && !isAssumption(pf.get())) + { + Trace("cdproof") << "...existing non-assume " << pf->getRule() << std::endl; + return pf; + } + else if (!d_autoSymm) + { + Trace("cdproof") << "...not auto considering symmetry" << std::endl; + return pf; + } + Node symFact = getSymmFact(fact); + if (symFact.isNull()) + { + Trace("cdproof") << "...no possible symm" << std::endl; + // no symmetry possible, return original proof (possibly assumption) + return pf; + } + // See if a proof exists for the opposite direction, if so, add the step. + // Notice that SYMM is also disallowed. + std::shared_ptr<ProofNode> pfs = getProof(symFact); + if (pfs != nullptr) + { + // The symmetric fact exists, and the current one either does not, or is + // an assumption. We make a new proof that applies SYMM to pfs. + std::vector<std::shared_ptr<ProofNode>> pschild; + pschild.push_back(pfs); + std::vector<Node> args; + if (pf == nullptr) + { + Trace("cdproof") << "...fresh make symm" << std::endl; + std::shared_ptr<ProofNode> psym = + d_manager->mkNode(PfRule::SYMM, pschild, args, fact); + Assert(psym != nullptr); + d_nodes.insert(fact, psym); + return psym; + } + else if (!isAssumption(pfs.get())) + { + // if its not an assumption, make the connection + Trace("cdproof") << "...update symm" << std::endl; + // update pf + bool sret = d_manager->updateNode(pf.get(), PfRule::SYMM, pschild, args); + AlwaysAssert(sret); + } + } + else + { + Trace("cdproof") << "...no symm, return " + << (pf == nullptr ? "null" : "non-null") << std::endl; + } + // return original proof (possibly assumption) + return pf; +} + +bool CDProof::addStep(Node expected, + PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args, + bool ensureChildren, + CDPOverwrite opolicy) +{ + Trace("cdproof") << "CDProof::addStep: " << identify() << " : " << id << " " + << expected << ", ensureChildren = " << ensureChildren + << ", overwrite policy = " << opolicy << std::endl; + Trace("cdproof-debug") << "CDProof::addStep: " << identify() + << " : children: " << children << "\n"; + Trace("cdproof-debug") << "CDProof::addStep: " << identify() + << " : args: " << args << "\n"; + // We must always provide expected to this method + Assert(!expected.isNull()); + + std::shared_ptr<ProofNode> pprev = getProofSymm(expected); + if (pprev != nullptr) + { + if (!shouldOverwrite(pprev.get(), id, opolicy)) + { + // we should not overwrite the current step + Trace("cdproof") << "...success, no overwrite" << std::endl; + return true; + } + Trace("cdproof") << "existing proof " << pprev->getRule() + << ", overwrite..." << std::endl; + // we will overwrite the existing proof node by updating its contents below + } + // collect the child proofs, for each premise + std::vector<std::shared_ptr<ProofNode>> pchildren; + for (const Node& c : children) + { + Trace("cdproof") << "- get child " << c << std::endl; + std::shared_ptr<ProofNode> pc = getProofSymm(c); + if (pc == nullptr) + { + if (ensureChildren) + { + // failed to get a proof for a child, fail + Trace("cdproof") << "...fail, no child" << std::endl; + return false; + } + Trace("cdproof") << "--- add assume" << std::endl; + // otherwise, we initialize it as an assumption + std::vector<Node> pcargs = {c}; + std::vector<std::shared_ptr<ProofNode>> pcassume; + pc = d_manager->mkNode(PfRule::ASSUME, pcassume, pcargs, c); + // assumptions never fail to check + Assert(pc != nullptr); + d_nodes.insert(c, pc); + } + pchildren.push_back(pc); + } + + // the user may have provided SYMM of an assumption + if (id == PfRule::SYMM) + { + Assert(pchildren.size() == 1); + if (isAssumption(pchildren[0].get())) + { + // the step we are constructing is a (symmetric fact of an) assumption, so + // there is no use adding it to the proof. + return true; + } + } + + bool ret = true; + // create or update it + std::shared_ptr<ProofNode> pthis; + if (pprev == nullptr) + { + Trace("cdproof") << " new node " << expected << "..." << std::endl; + pthis = d_manager->mkNode(id, pchildren, args, expected); + if (pthis == nullptr) + { + // failed to construct the node, perhaps due to a proof checking failure + Trace("cdproof") << "...fail, proof checking" << std::endl; + return false; + } + d_nodes.insert(expected, pthis); + } + else + { + Trace("cdproof") << " update node " << expected << "..." << std::endl; + // update its value + pthis = pprev; + // We return the value of updateNode here. This means this method may return + // false if this call failed, regardless of whether we already have a proof + // step for expected. + ret = d_manager->updateNode(pthis.get(), id, pchildren, args); + } + if (ret) + { + // the result of the proof node should be expected + Assert(pthis->getResult() == expected); + + // notify new proof + notifyNewProof(expected); + } + + Trace("cdproof") << "...return " << ret << std::endl; + return ret; +} + +void CDProof::notifyNewProof(Node expected) +{ + if (!d_autoSymm) + { + return; + } + // ensure SYMM proof is also linked to an existing proof, if it is an + // assumption. + Node symExpected = getSymmFact(expected); + if (!symExpected.isNull()) + { + Trace("cdproof") << " check connect symmetry " << symExpected << std::endl; + // if it exists, we may need to update it + std::shared_ptr<ProofNode> pfs = getProof(symExpected); + if (pfs != nullptr) + { + Trace("cdproof") << " connect via getProofSymm method..." << std::endl; + // call the get function with symmetry, which will do the update + std::shared_ptr<ProofNode> pfss = getProofSymm(symExpected); + } + else + { + Trace("cdproof") << " no connect" << std::endl; + } + } +} + +bool CDProof::addStep(Node expected, + const ProofStep& step, + bool ensureChildren, + CDPOverwrite opolicy) +{ + return addStep(expected, + step.d_rule, + step.d_children, + step.d_args, + ensureChildren, + opolicy); +} + +bool CDProof::addSteps(const ProofStepBuffer& psb, + bool ensureChildren, + CDPOverwrite opolicy) +{ + const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps(); + for (const std::pair<Node, ProofStep>& ps : steps) + { + if (!addStep(ps.first, ps.second, ensureChildren, opolicy)) + { + return false; + } + } + return true; +} + +bool CDProof::addProof(std::shared_ptr<ProofNode> pn, + CDPOverwrite opolicy, + bool doCopy) +{ + if (!doCopy) + { + // If we aren't doing a deep copy, we either store pn or link its top + // node into the existing pointer + Node curFact = pn->getResult(); + std::shared_ptr<ProofNode> cur = getProofSymm(curFact); + if (cur == nullptr) + { + // Assert that the checker of this class agrees with (the externally + // provided) pn. This ensures that if pn was checked by a different + // checker than the one of the manager in this class, then it is double + // checked here, so that this class maintains the invariant that all of + // its nodes in d_nodes have been checked by the underlying checker. + Assert(d_manager->getChecker() == nullptr + || d_manager->getChecker()->check(pn.get(), curFact) == curFact); + // just store the proof for fact + d_nodes.insert(curFact, pn); + } + else if (shouldOverwrite(cur.get(), pn->getRule(), opolicy)) + { + // We update cur to have the structure of the top node of pn. Notice that + // the interface to update this node will ensure that the proof apf is a + // proof of the assumption. If it does not, then pn was wrong. + if (!d_manager->updateNode( + cur.get(), pn->getRule(), pn->getChildren(), pn->getArguments())) + { + return false; + } + } + // also need to connect via SYMM if necessary + notifyNewProof(curFact); + return true; + } + std::unordered_map<ProofNode*, bool> visited; + std::unordered_map<ProofNode*, bool>::iterator it; + std::vector<ProofNode*> visit; + ProofNode* cur; + Node curFact; + visit.push_back(pn.get()); + bool retValue = true; + do + { + cur = visit.back(); + curFact = cur->getResult(); + visit.pop_back(); + it = visited.find(cur); + if (it == visited.end()) + { + // visit the children + visited[cur] = false; + visit.push_back(cur); + const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren(); + for (const std::shared_ptr<ProofNode>& c : cs) + { + visit.push_back(c.get()); + } + } + else if (!it->second) + { + // we always call addStep, which may or may not overwrite the + // current step + std::vector<Node> pexp; + const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren(); + for (const std::shared_ptr<ProofNode>& c : cs) + { + Assert(!c->getResult().isNull()); + pexp.push_back(c->getResult()); + } + // can ensure children at this point + bool res = addStep( + curFact, cur->getRule(), pexp, cur->getArguments(), true, opolicy); + // should always succeed + Assert(res); + retValue = retValue && res; + visited[cur] = true; + } + } while (!visit.empty()); + + return retValue; +} + +bool CDProof::hasStep(Node fact) +{ + std::shared_ptr<ProofNode> pf = getProof(fact); + if (pf != nullptr && !isAssumption(pf.get())) + { + return true; + } + else if (!d_autoSymm) + { + return false; + } + Node symFact = getSymmFact(fact); + if (symFact.isNull()) + { + return false; + } + pf = getProof(symFact); + if (pf != nullptr && !isAssumption(pf.get())) + { + return true; + } + return false; +} + +ProofNodeManager* CDProof::getManager() const { return d_manager; } + +bool CDProof::shouldOverwrite(ProofNode* pn, PfRule newId, CDPOverwrite opol) +{ + Assert(pn != nullptr); + // we overwrite only if opol is CDPOverwrite::ALWAYS, or if + // opol is CDPOverwrite::ASSUME_ONLY and the previously + // provided proof pn was an assumption and the currently provided step is not + return opol == CDPOverwrite::ALWAYS + || (opol == CDPOverwrite::ASSUME_ONLY && isAssumption(pn) + && newId != PfRule::ASSUME); +} + +bool CDProof::isAssumption(ProofNode* pn) +{ + PfRule rule = pn->getRule(); + if (rule == PfRule::ASSUME) + { + return true; + } + else if (rule == PfRule::SYMM) + { + const std::vector<std::shared_ptr<ProofNode>>& pc = pn->getChildren(); + Assert(pc.size() == 1); + return pc[0]->getRule() == PfRule::ASSUME; + } + return false; +} + +bool CDProof::isSame(TNode f, TNode g) +{ + if (f == g) + { + return true; + } + Kind fk = f.getKind(); + Kind gk = g.getKind(); + if (fk == EQUAL && gk == EQUAL && f[0] == g[1] && f[1] == g[0]) + { + // symmetric equality + return true; + } + if (fk == NOT && gk == NOT && f[0].getKind() == EQUAL + && g[0].getKind() == EQUAL && f[0][0] == g[0][1] && f[0][1] == g[0][0]) + { + // symmetric disequality + return true; + } + return false; +} + +Node CDProof::getSymmFact(TNode f) +{ + bool polarity = f.getKind() != NOT; + TNode fatom = polarity ? f : f[0]; + if (fatom.getKind() != EQUAL || fatom[0] == fatom[1]) + { + return Node::null(); + } + Node symFact = fatom[1].eqNode(fatom[0]); + return polarity ? symFact : symFact.notNode(); +} + +std::string CDProof::identify() const { return d_name; } + +} // namespace cvc5 diff --git a/src/proof/proof.h b/src/proof/proof.h new file mode 100644 index 000000000..2c57e0a2e --- /dev/null +++ b/src/proof/proof.h @@ -0,0 +1,278 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Proof utility. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_H +#define CVC5__PROOF__PROOF_H + +#include <vector> + +#include "context/cdhashmap.h" +#include "expr/node.h" +#include "proof/proof_generator.h" +#include "proof/proof_step_buffer.h" + +namespace cvc5 { + +class ProofNode; +class ProofNodeManager; + +/** + * A (context-dependent) proof. + * + * This maintains a context-dependent map from formulas to ProofNode shared + * pointers. When a step is added, it internally uses mutable ProofNode pointers + * to link the steps in the proof together. + * + * It is important to note that the premises of proof steps given to this class + * are *Node* not *ProofNode*. In other words, the user of this class does + * not have to manage ProofNode pointers while using this class. Instead, + * ProofNode is the final product of this class, via the getProof interface, + * which returns a ProofNode object that has linked together the proof steps + * added to this object. + * + * Its main interface is the function addStep, which registers a single + * step in the proof. Its interface is: + * addStep( <conclusion>, <rule>, <premises>, <args>, ...<options>... ) + * where conclusion is what to be proven, rule is an identifier, premises + * are the formulas that imply conclusion, and args are additional arguments to + * the proof rule application. The options include whether we ensure children + * proofs already exist for the premises and our policty for overwriting + * existing steps. + * + * As an example, let A, B, C, D be formulas represented by Nodes. If we + * call: + * - addStep( A, ID_A, { B, C }, {} ) + * - addStep( B, ID_B, { D }, {} ) + * - addStep( E, ID_E, {}, {} ) + * with default options, then getProof( A ) returns the ProofNode of the form: + * ID_A( ID_B( ASSUME( D ) ), ASSUME( C ) ) + * Notice that the above calls to addStep can be made in either order. The + * proof step for E was not involved in the proof of A. + * + * If the user wants to combine proofs, then a addProof interface is + * available. The method addProof can be seen as syntax sugar for making + * multiple calls to addStep. Continuing the above example, if we call: + * - addProof( F, ID_F( ASSUME( A ), ASSUME( E ) ) ) + * is the same as calling steps corresponding the steps in the provided proof + * bottom-up, starting from the leaves. + * --- addStep( A, ASSUME, {}, {}, true ) + * --- addStep( E, ASSUME, {}, {}, true ) + * --- addStep( F, ID_F, { A, E }, {}, true ) + * The fifth argument provided indicates that we want to ensure child proofs + * are already available for the step (see ensureChildren in addStep below). + * This will result in getProof( F ) returning: + * ID_F( ID_A( ID_B( ASSUME( D ) ), ASSUME( C ) ), ID_E() ) + * Notice that the proof of A by ID_A was not overwritten by ASSUME in the + * addStep call above. + * + * The default policy for overwriting proof steps (CDPOverwrite::ASSUME_ONLY) + * gives ASSUME a special status. An ASSUME step can be seen as a step whose + * justification has not yet been provided. Thus, it is always overwritten. + * Other proof rules are never overwritten, unless the argument opolicy is + * CDPOverwrite::ALWAYS. + * + * As an another example, say that we call: + * - addStep( B, ID_B1 {}, {} ) + * - addStep( A, ID_A1, {B, C}, {} ) + * At this point, getProof( A ) returns: + * ID_A1( ID_B1(), ASSUME(C) ) + * Now, assume an additional call is made to addProof, where notice + * the overwrite policy is CDPOverwrite::ASSUME_ONLY by default: + * - addProof( D, ID_D( ID_A2( ID_B2(), ID_C() ) ) ) + * where assume ID_B2() and ID_C() prove B and C respectively. This call is + * equivalent to calling: + * --- addStep( B, ID_B2, {}, {}, true ) + * --- addStep( C, ID_C, {}, {}, true ) + * --- addStep( A, ID_A2, {B, C}, {}, true ) + * --- addStep( D, ID_D, {A}, {}, true ) + * Afterwards, getProof( D ) returns: + * ID_D( ID_A1( ID_B1(), ID_C() ) ) + * Notice that the steps with ID_A1 and ID_B1 were not overwritten by this call, + * whereas the assumption of C was overwritten by the proof ID_C(). Notice that + * the proof of D was completely traversed in addProof, despite encountering + * formulas, A and B, that were already given proof steps. + * + * This class requires a ProofNodeManager object, which is a trusted way of + * allocating ProofNode pointers. This manager may have an underlying checker, + * although this is not required. It also (optionally) takes a context c. + * If no context is provided, then this proof is context-independent. This + * is implemented internally by using a dummy context that is never pushed + * or popped. The map from Nodes to ProofNodes is context-dependent and is + * backtracked when its context backtracks. + * + * An important invariant of this object is that there exists (at most) one + * proof step for each Node. Thus, the ProofNode objects returned by this + * class share proofs for common subformulas, as guaranteed by the fact that + * Node objects have perfect sharing. + * + * Notice that this class is agnostic to symmetry of equality. In other + * words, adding a step that concludes (= x y) is effectively the same as + * providing a step that concludes (= y x) from the point of view of a user + * of this class. This is accomplished by adding SYMM steps on demand when + * a formula is looked up. For example say we call: + * - addStep( (= x y), ID_1 {}, {} ) + * - addStep( P, ID_2, {(= y x)}, {} ) + * Afterwards, getProof( P ) returns: + * ID_2( SYMM( ID_1() ) ) + * where notice SYMM was added so that (= y x) is a premise of the application + * of ID_2. More generally, CDProof::isSame(F,G) returns true if F and G are + * essentially the same formula according to this class. + */ +class CDProof : public ProofGenerator +{ + public: + /** + * @param pnm The proof node manager responsible for constructor ProofNode + * @param c The context this proof depends on + * @param name The name of this proof (for debugging) + * @param autoSymm Whether this proof automatically adds symmetry steps based + * on policy documented above. + */ + CDProof(ProofNodeManager* pnm, + context::Context* c = nullptr, + std::string name = "CDProof", + bool autoSymm = true); + virtual ~CDProof(); + /** + * Make proof for fact. + * + * This method always returns a non-null ProofNode. It may generate new + * steps so that a ProofNode can be constructed for fact. In particular, + * if no step exists for fact, then we may construct and return ASSUME(fact). + * If fact is of the form (= t s), no step exists for fact, but a proof + * P for (= s t) exists, then this method returns SYMM(P). + * + * Notice that this call does *not* clone the ProofNode object. Hence, the + * returned proof may be updated by further calls to this class. The caller + * should call ProofNode::clone if they want to own it. + */ + std::shared_ptr<ProofNode> getProofFor(Node fact) override; + /** Add step + * + * @param expected The intended conclusion of this proof step. This must be + * non-null. + * @param id The identifier for the proof step. + * @param children The antecendants of the proof step. Each children[i] should + * be a fact previously added as a conclusion of an addStep call when + * ensureChildren is true. + * @param args The arguments of the proof step. + * @param ensureChildren Whether we wish to ensure steps have been added + * for all nodes in children + * @param opolicy Policy for whether to overwrite if a step for + * expected was already provided (via a previous call to addStep) + * @return The true if indeed the proof step proves expected, or + * false otherwise. The latter can happen if the proof has a different (or + * invalid) conclusion, or if one of the children does not have a proof and + * ensureChildren is true. + * + * This method may create proofs justified by ASSUME of the facts in + * children that have not already been proven when ensureChildren is false. + * Notice that ensureChildren should be true if the proof is being + * constructed is a strictly eager fashion (bottom up from its leaves), while + * ensureChildren should be false if the steps are added lazily or out + * of order. + * + * This method only overwrites proofs for facts that were added as + * steps with id ASSUME when opolicy is CDPOverwrite::ASSUME_ONLY, and always + * (resp. never) overwrites an existing step if one was provided when opolicy + * is CDPOverwrite::ALWAYS (resp. CDPOverwrite::NEVER). + */ + bool addStep(Node expected, + PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args, + bool ensureChildren = false, + CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY); + /** Version with ProofStep */ + bool addStep(Node expected, + const ProofStep& step, + bool ensureChildren = false, + CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY); + /** Version with ProofStepBuffer */ + bool addSteps(const ProofStepBuffer& psb, + bool ensureChildren = false, + CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY); + /** Add proof + * + * @param pn The proof of the given fact. + * @param opolicy Policy for whether to force overwriting if a step + * was already provided. This is used for each node in the proof if doCopy + * is true. + * @param doCopy Whether we make a deep copy of the pn. + * @return true if all steps were successfully added to this class. If it + * returns true, it registers a copy of all of the subnodes of pn to this + * proof class. + * + * If doCopy is true, this method is implemented by calling addStep above for + * all subnodes of pn, traversed as a dag. This means that fresh ProofNode + * objects may be generated by this call, and further modifications to pn do + * not impact the internal data of this class. + */ + bool addProof(std::shared_ptr<ProofNode> pn, + CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY, + bool doCopy = false); + /** Return true if fact already has a proof step */ + bool hasStep(Node fact); + /** Get the proof manager for this proof */ + ProofNodeManager* getManager() const; + /** + * Is same? Returns true if f and g are the same formula, or if they are + * symmetric equalities. If two nodes f and g are the same, then a proof for + * f suffices as a proof for g according to this class. + */ + static bool isSame(TNode f, TNode g); + /** Get proof for fact, or nullptr if it does not exist. */ + std::shared_ptr<ProofNode> getProof(Node fact) const; + /** + * Get symmetric fact (a g such that isSame returns true for isSame(f,g)), or + * null if none exist. + */ + static Node getSymmFact(TNode f); + /** identify */ + std::string identify() const override; + + protected: + typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>> NodeProofNodeMap; + /** The proof manager, used for allocating new ProofNode objects */ + ProofNodeManager* d_manager; + /** A dummy context used by this class if none is provided */ + context::Context d_context; + /** The nodes of the proof */ + NodeProofNodeMap d_nodes; + /** Name identifier */ + std::string d_name; + /** Whether we automatically add symmetry steps */ + bool d_autoSymm; + /** Ensure fact sym */ + std::shared_ptr<ProofNode> getProofSymm(Node fact); + /** + * Returns true if we should overwrite proof node pn with a step having id + * newId, based on policy opol. + */ + static bool shouldOverwrite(ProofNode* pn, PfRule newId, CDPOverwrite opol); + /** Returns true if pn is an assumption. */ + static bool isAssumption(ProofNode* pn); + /** + * Notify new proof, called when a new proof of expected is provided. This is + * used internally to connect proofs of symmetric facts, when necessary. + */ + void notifyNewProof(Node expected); +}; + +} // namespace cvc5 + +#endif /* CVC5__PROOF__PROOF_MANAGER_H */ diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp new file mode 100644 index 000000000..7a2e5293e --- /dev/null +++ b/src/proof/proof_checker.cpp @@ -0,0 +1,345 @@ +/****************************************************************************** + * 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 proof checker. + */ + +#include "proof/proof_checker.h" + +#include "expr/skolem_manager.h" +#include "options/proof_options.h" +#include "proof/proof_node.h" +#include "smt/smt_statistics_registry.h" + +using namespace cvc5::kind; + +namespace cvc5 { + +Node ProofRuleChecker::check(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args) +{ + // call instance-specific checkInternal method + return checkInternal(id, children, args); +} + +bool ProofRuleChecker::getUInt32(TNode n, uint32_t& i) +{ + // must be a non-negative integer constant that fits an unsigned int + if (n.isConst() && n.getType().isInteger() + && n.getConst<Rational>().sgn() >= 0 + && n.getConst<Rational>().getNumerator().fitsUnsignedInt()) + { + i = n.getConst<Rational>().getNumerator().toUnsignedInt(); + return true; + } + return false; +} + +bool ProofRuleChecker::getBool(TNode n, bool& b) +{ + if (n.isConst() && n.getType().isBoolean()) + { + b = n.getConst<bool>(); + return true; + } + return false; +} + +bool ProofRuleChecker::getKind(TNode n, Kind& k) +{ + uint32_t i; + if (!getUInt32(n, i)) + { + return false; + } + k = static_cast<Kind>(i); + return true; +} + +Node ProofRuleChecker::mkKindNode(Kind k) +{ + if (k == UNDEFINED_KIND) + { + // UNDEFINED_KIND is negative, hence return null to avoid cast + return Node::null(); + } + return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(k))); +} + +ProofCheckerStatistics::ProofCheckerStatistics() + : d_ruleChecks(smtStatisticsRegistry().registerHistogram<PfRule>( + "ProofCheckerStatistics::ruleChecks")), + d_totalRuleChecks(smtStatisticsRegistry().registerInt( + "ProofCheckerStatistics::totalRuleChecks")) +{ +} + +Node ProofChecker::check(ProofNode* pn, Node expected) +{ + return check(pn->getRule(), pn->getChildren(), pn->getArguments(), expected); +} + +Node ProofChecker::check( + PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args, + Node expected) +{ + // optimization: immediately return for ASSUME + if (id == PfRule::ASSUME) + { + Assert(children.empty()); + Assert(args.size() == 1 && args[0].getType().isBoolean()); + Assert(expected.isNull() || expected == args[0]); + return expected; + } + // record stat + d_stats.d_ruleChecks << id; + ++d_stats.d_totalRuleChecks; + Trace("pfcheck") << "ProofChecker::check: " << id << std::endl; + std::vector<Node> cchildren; + for (const std::shared_ptr<ProofNode>& pc : children) + { + Assert(pc != nullptr); + Node cres = pc->getResult(); + if (cres.isNull()) + { + Trace("pfcheck") << "ProofChecker::check: failed child" << std::endl; + Unreachable() + << "ProofChecker::check: child proof was invalid (null conclusion)" + << std::endl; + // should not have been able to create such a proof node + return Node::null(); + } + cchildren.push_back(cres); + if (Trace.isOn("pfcheck")) + { + std::stringstream ssc; + pc->printDebug(ssc); + Trace("pfcheck") << " child: " << ssc.str() << " : " << cres + << std::endl; + } + } + Trace("pfcheck") << " args: " << args << std::endl; + Trace("pfcheck") << " expected: " << expected << std::endl; + std::stringstream out; + // we use trusted (null) checkers here, since we want the proof generation to + // proceed without failing here. We always enable output since a failure + // implies that we will exit with the error message below. + Node res = checkInternal(id, cchildren, args, expected, out, true, true); + if (res.isNull()) + { + Trace("pfcheck") << "ProofChecker::check: failed" << std::endl; + Unreachable() << "ProofChecker::check: failed, " << out.str() << std::endl; + // it did not match the given expectation, fail + return Node::null(); + } + Trace("pfcheck") << "ProofChecker::check: success!" << std::endl; + return res; +} + +Node ProofChecker::checkDebug(PfRule id, + const std::vector<Node>& cchildren, + const std::vector<Node>& args, + Node expected, + const char* traceTag) +{ + std::stringstream out; + bool traceEnabled = Trace.isOn(traceTag); + // Since we are debugging, we want to treat trusted (null) checkers as + // a failure. We only enable output if the trace is enabled for efficiency. + Node res = + checkInternal(id, cchildren, args, expected, out, false, traceEnabled); + if (traceEnabled) + { + Trace(traceTag) << "ProofChecker::checkDebug: " << id; + if (res.isNull()) + { + Trace(traceTag) << " failed, " << out.str() << std::endl; + } + else + { + Trace(traceTag) << " success" << std::endl; + } + Trace(traceTag) << "cchildren: " << cchildren << std::endl; + Trace(traceTag) << " args: " << args << std::endl; + } + return res; +} + +Node ProofChecker::checkInternal(PfRule id, + const std::vector<Node>& cchildren, + const std::vector<Node>& args, + Node expected, + std::stringstream& out, + bool useTrustedChecker, + bool enableOutput) +{ + std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id); + if (it == d_checker.end()) + { + // no checker for the rule + if (enableOutput) + { + out << "no checker for rule " << id << std::endl; + } + return Node::null(); + } + else if (it->second == nullptr) + { + if (useTrustedChecker) + { + Notice() << "ProofChecker::check: trusting PfRule " << id << std::endl; + // trusted checker + return expected; + } + else + { + if (enableOutput) + { + out << "trusted checker for rule " << id << std::endl; + } + return Node::null(); + } + } + // check it with the corresponding checker + Node res = it->second->check(id, cchildren, args); + if (!expected.isNull()) + { + Node expectedw = expected; + if (res != expectedw) + { + if (enableOutput) + { + out << "result does not match expected value." << std::endl + << " PfRule: " << id << std::endl; + for (const Node& c : cchildren) + { + out << " child: " << c << std::endl; + } + for (const Node& a : args) + { + out << " arg: " << a << std::endl; + } + out << " result: " << res << std::endl + << " expected: " << expected << std::endl; + } + // it did not match the given expectation, fail + return Node::null(); + } + } + // fails if pedantic level is not met + if (options::proofEagerChecking()) + { + std::stringstream serr; + if (isPedanticFailure(id, serr, enableOutput)) + { + if (enableOutput) + { + out << serr.str() << std::endl; + if (Trace.isOn("proof-pedantic")) + { + Trace("proof-pedantic") + << "Failed pedantic check for " << id << std::endl; + Trace("proof-pedantic") << "Expected: " << expected << std::endl; + out << "Expected: " << expected << std::endl; + } + } + return Node::null(); + } + } + return res; +} + +void ProofChecker::registerChecker(PfRule id, ProofRuleChecker* psc) +{ + std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id); + if (it != d_checker.end()) + { + // checker is already provided + Notice() << "ProofChecker::registerChecker: checker already exists for " + << id << std::endl; + return; + } + d_checker[id] = psc; +} + +void ProofChecker::registerTrustedChecker(PfRule id, + ProofRuleChecker* psc, + uint32_t plevel) +{ + AlwaysAssert(plevel <= 10) << "ProofChecker::registerTrustedChecker: " + "pedantic level must be 0-10, got " + << plevel << " for " << id; + registerChecker(id, psc); + // overwrites if already there + if (d_plevel.find(id) != d_plevel.end()) + { + Notice() << "ProofChecker::registerTrustedRule: already provided pedantic " + "level for " + << id << std::endl; + } + d_plevel[id] = plevel; +} + +ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id) +{ + std::map<PfRule, ProofRuleChecker*>::const_iterator it = d_checker.find(id); + if (it == d_checker.end()) + { + return nullptr; + } + return it->second; +} + +uint32_t ProofChecker::getPedanticLevel(PfRule id) const +{ + std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id); + if (itp != d_plevel.end()) + { + return itp->second; + } + return 0; +} + +bool ProofChecker::isPedanticFailure(PfRule id, + std::ostream& out, + bool enableOutput) const +{ + if (d_pclevel == 0) + { + return false; + } + std::map<PfRule, uint32_t>::const_iterator itp = d_plevel.find(id); + if (itp != d_plevel.end()) + { + if (itp->second <= d_pclevel) + { + if (enableOutput) + { + out << "pedantic level for " << id << " not met (rule level is " + << itp->second << " which is at or below the pedantic level " + << d_pclevel << ")"; + bool pedanticTraceEnabled = Trace.isOn("proof-pedantic"); + if (!pedanticTraceEnabled) + { + out << ", use -t proof-pedantic for details"; + } + } + return true; + } + } + return false; +} + +} // namespace cvc5 diff --git a/src/proof/proof_checker.h b/src/proof/proof_checker.h new file mode 100644 index 000000000..ac5531bf4 --- /dev/null +++ b/src/proof/proof_checker.h @@ -0,0 +1,206 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Proof checker utility. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_CHECKER_H +#define CVC5__PROOF__PROOF_CHECKER_H + +#include <map> + +#include "expr/node.h" +#include "proof/proof_rule.h" +#include "util/statistics_stats.h" + +namespace cvc5 { + +class ProofChecker; +class ProofNode; + +/** A virtual base class for checking a proof rule */ +class ProofRuleChecker +{ + public: + ProofRuleChecker() {} + virtual ~ProofRuleChecker() {} + /** + * This checks a single step in a proof. + * + * Return the formula that is proven by a proof node with the given id, + * premises and arguments, or null if such a proof node is not well-formed. + * + * Note that the input/output of this method expects to be terms in *Skolem + * form*, which is passed to checkInternal below. Rule checkers may + * convert premises to witness form when necessary. + * + * @param id The id of the proof node to check + * @param children The premises of the proof node to check. These are nodes + * corresponding to the conclusion (ProofNode::getResult) of the children + * of the proof node we are checking in Skolem form. + * @param args The arguments of the proof node to check + * @return The conclusion of the proof node, in Skolem form, if successful or + * null if such a proof node is malformed. + */ + Node check(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args); + + /** get an index from a node, return false if we fail */ + static bool getUInt32(TNode n, uint32_t& i); + /** get a Boolean from a node, return false if we fail */ + static bool getBool(TNode n, bool& b); + /** get a Kind from a node, return false if we fail */ + static bool getKind(TNode n, Kind& k); + /** Make a Kind into a node */ + static Node mkKindNode(Kind k); + + /** Register all rules owned by this rule checker into pc. */ + virtual void registerTo(ProofChecker* pc) {} + + protected: + /** + * This checks a single step in a proof. + * + * @param id The id of the proof node to check + * @param children The premises of the proof node to check. These are nodes + * corresponding to the conclusion (ProofNode::getResult) of the children + * of the proof node we are checking. + * @param args The arguments of the proof node to check + * @return The conclusion of the proof node if successful or null if such a + * proof node is malformed. + */ + virtual Node checkInternal(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args) = 0; +}; + +/** Statistics class */ +class ProofCheckerStatistics +{ + public: + ProofCheckerStatistics(); + /** Counts the number of checks for each kind of proof rule */ + HistogramStat<PfRule> d_ruleChecks; + /** Total number of rule checks */ + IntStat d_totalRuleChecks; +}; + +/** A class for checking proofs */ +class ProofChecker +{ + public: + ProofChecker(uint32_t pclevel = 0) : d_pclevel(pclevel) {} + ~ProofChecker() {} + /** + * Return the formula that is proven by proof node pn, or null if pn is not + * well-formed. If expected is non-null, then we return null if pn does not + * prove expected. + * + * @param pn The proof node to check + * @param expected The (optional) formula that is the expected conclusion of + * the proof node. + * @return The conclusion of the proof node if successful or null if the + * proof is malformed, or if no checker is available for id. + */ + Node check(ProofNode* pn, Node expected = Node::null()); + /** Same as above, with explicit arguments + * + * @param id The id of the proof node to check + * @param children The children of the proof node to check + * @param args The arguments of the proof node to check + * @param expected The (optional) formula that is the expected conclusion of + * the proof node. + * @return The conclusion of the proof node if successful or null if the + * proof is malformed, or if no checker is available for id. + */ + Node check(PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args, + Node expected = Node::null()); + /** + * Same as above, without conclusions instead of proof node children. This + * is used for debugging. In particular, this function does not throw an + * assertion failure when a proof step is malformed and can be used without + * constructing proof nodes. + * + * @param id The id of the proof node to check + * @param children The conclusions of the children of the proof node to check + * @param args The arguments of the proof node to check + * @param expected The (optional) formula that is the expected conclusion of + * the proof node. + * @param traceTag The trace tag to print debug information to + * @return The conclusion of the proof node if successful or null if the + * proof is malformed, or if no checker is available for id. + */ + Node checkDebug(PfRule id, + const std::vector<Node>& cchildren, + const std::vector<Node>& args, + Node expected = Node::null(), + const char* traceTag = ""); + /** Indicate that psc is the checker for proof rule id */ + void registerChecker(PfRule id, ProofRuleChecker* psc); + /** + * Indicate that id is a trusted rule with the given pedantic level, e.g.: + * 0: (mandatory) always a failure to use the given id + * 1: (major) failure on all (non-zero) pedantic levels + * 10: (minor) failure only on pedantic levels >= 10. + */ + void registerTrustedChecker(PfRule id, + ProofRuleChecker* psc, + uint32_t plevel = 10); + /** get checker for */ + ProofRuleChecker* getCheckerFor(PfRule id); + + /** + * Get the pedantic level for id if it has been assigned a pedantic + * level via registerTrustedChecker above, or zero otherwise. + */ + uint32_t getPedanticLevel(PfRule id) const; + + /** + * Is pedantic failure? If so, we return true and write a debug message on the + * output stream out if enableOutput is true. + */ + bool isPedanticFailure(PfRule id, + std::ostream& out, + bool enableOutput = true) const; + + private: + /** statistics class */ + ProofCheckerStatistics d_stats; + /** Maps proof rules to their checker */ + std::map<PfRule, ProofRuleChecker*> d_checker; + /** Maps proof trusted rules to their pedantic level */ + std::map<PfRule, uint32_t> d_plevel; + /** The pedantic level of this checker */ + uint32_t d_pclevel; + /** + * Check internal. This is used by check and checkDebug above. It writes + * checking errors on out when enableOutput is true. We treat trusted checkers + * (nullptr in the range of the map d_checker) as failures if + * useTrustedChecker = false. + */ + Node checkInternal(PfRule id, + const std::vector<Node>& cchildren, + const std::vector<Node>& args, + Node expected, + std::stringstream& out, + bool useTrustedChecker, + bool enableOutput); +}; + +} // namespace cvc5 + +#endif /* CVC5__PROOF__PROOF_CHECKER_H */ diff --git a/src/proof/proof_ensure_closed.cpp b/src/proof/proof_ensure_closed.cpp new file mode 100644 index 000000000..774b25ef6 --- /dev/null +++ b/src/proof/proof_ensure_closed.cpp @@ -0,0 +1,183 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa + * + * 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 debug checks for ensuring proofs are closed. + */ + +#include "proof/proof_ensure_closed.h" + +#include <sstream> + +#include "options/proof_options.h" +#include "options/smt_options.h" +#include "proof/proof_generator.h" +#include "proof/proof_node.h" +#include "proof/proof_node_algorithm.h" + +namespace cvc5 { + +/** + * Ensure closed with respect to assumptions, internal version, which + * generalizes the check for a proof generator or a proof node. + */ +void ensureClosedWrtInternal(Node proven, + ProofGenerator* pg, + ProofNode* pnp, + const std::vector<Node>& assumps, + const char* c, + const char* ctx, + bool reqGen) +{ + if (!options::produceProofs()) + { + // proofs not enabled, do not do check + return; + } + bool isTraceDebug = Trace.isOn(c); + if (!options::proofEagerChecking() && !isTraceDebug) + { + // trace is off and proof new eager checking is off, do not do check + return; + } + std::stringstream sdiag; + bool isTraceOn = Trace.isOn(c); + if (!isTraceOn) + { + sdiag << ", use -t " << c << " for details"; + } + bool dumpProofTraceOn = Trace.isOn("dump-proof-error"); + if (!dumpProofTraceOn) + { + sdiag << ", use -t dump-proof-error for details on proof"; + } + // get the proof node in question, which is either provided or built by the + // proof generator + std::shared_ptr<ProofNode> pn; + std::stringstream ss; + if (pnp != nullptr) + { + Assert(pg == nullptr); + ss << "ProofNode in context " << ctx; + } + else + { + ss << "ProofGenerator: " << (pg == nullptr ? "null" : pg->identify()) + << " in context " << ctx; + if (pg == nullptr) + { + // only failure if flag is true + if (reqGen) + { + Unreachable() << "...ensureClosed: no generator in context " << ctx + << sdiag.str(); + } + } + else + { + Assert(!proven.isNull()); + pn = pg->getProofFor(proven); + pnp = pn.get(); + } + } + Trace(c) << "=== ensureClosed: " << ss.str() << std::endl; + Trace(c) << "Proven: " << proven << std::endl; + if (pnp == nullptr) + { + if (pg == nullptr) + { + // did not require generator + Assert(!reqGen); + Trace(c) << "...ensureClosed: no generator in context " << ctx + << std::endl; + return; + } + } + // if we don't have a proof node, a generator failed + if (pnp == nullptr) + { + Assert(pg != nullptr); + AlwaysAssert(false) << "...ensureClosed: null proof from " << ss.str() + << sdiag.str(); + } + std::vector<Node> fassumps; + expr::getFreeAssumptions(pnp, fassumps); + bool isClosed = true; + std::stringstream ssf; + for (const Node& fa : fassumps) + { + if (std::find(assumps.begin(), assumps.end(), fa) == assumps.end()) + { + isClosed = false; + ssf << "- " << fa << std::endl; + } + } + if (!isClosed) + { + Trace(c) << "Free assumptions:" << std::endl; + Trace(c) << ssf.str(); + if (!assumps.empty()) + { + Trace(c) << "Expected assumptions:" << std::endl; + for (const Node& a : assumps) + { + Trace(c) << "- " << a << std::endl; + } + } + if (dumpProofTraceOn) + { + Trace("dump-proof-error") << " Proof: " << *pnp << std::endl; + } + } + AlwaysAssert(isClosed) << "...ensureClosed: open proof from " << ss.str() + << sdiag.str(); + Trace(c) << "...ensureClosed: success" << std::endl; + Trace(c) << "====" << std::endl; +} + +void pfgEnsureClosed(Node proven, + ProofGenerator* pg, + const char* c, + const char* ctx, + bool reqGen) +{ + Assert(!proven.isNull()); + // proof generator may be null + std::vector<Node> assumps; + ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen); +} + +void pfgEnsureClosedWrt(Node proven, + ProofGenerator* pg, + const std::vector<Node>& assumps, + const char* c, + const char* ctx, + bool reqGen) +{ + Assert(!proven.isNull()); + // proof generator may be null + ensureClosedWrtInternal(proven, pg, nullptr, assumps, c, ctx, reqGen); +} + +void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx) +{ + ensureClosedWrtInternal(Node::null(), nullptr, pn, {}, c, ctx, false); +} + +void pfnEnsureClosedWrt(ProofNode* pn, + const std::vector<Node>& assumps, + const char* c, + const char* ctx) +{ + ensureClosedWrtInternal(Node::null(), nullptr, pn, assumps, c, ctx, false); +} + +} // namespace cvc5 diff --git a/src/proof/proof_ensure_closed.h b/src/proof/proof_ensure_closed.h new file mode 100644 index 000000000..cacfeeeed --- /dev/null +++ b/src/proof/proof_ensure_closed.h @@ -0,0 +1,73 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Debug checks for ensuring proofs are closed. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_ENSURE_CLOSED_H +#define CVC5__PROOF__PROOF_ENSURE_CLOSED_H + +#include "expr/node.h" + +namespace cvc5 { + +class ProofGenerator; +class ProofNode; + +/** + * Debug check closed on Trace c. Context ctx is string for debugging. + * This method throws an assertion failure if pg cannot provide a closed + * proof for fact proven. This is checked only if --proof-eager-checking + * is enabled or the Trace c is enabled. + * + * @param reqGen Whether we consider a null generator to be a failure. + */ +void pfgEnsureClosed(Node proven, + ProofGenerator* pg, + const char* c, + const char* ctx, + bool reqGen = true); + +/** + * Debug check closed with Trace c. Context ctx is string for debugging and + * assumps is the set of allowed open assertions. This method throws an + * assertion failure if pg cannot provide a proof for fact proven whose + * free assumptions are contained in assumps. + * + * @param reqGen Whether we consider a null generator to be a failure. + */ +void pfgEnsureClosedWrt(Node proven, + ProofGenerator* pg, + const std::vector<Node>& assumps, + const char* c, + const char* ctx, + bool reqGen = true); + +/** + * Debug check closed with Trace c, proof node versions. This gives an + * assertion failure if pn is not closed. Detailed information is printed + * on trace c. Context ctx is a string used for debugging. + */ +void pfnEnsureClosed(ProofNode* pn, const char* c, const char* ctx); +/** + * Same as above, but throws an assertion failure only if the free assumptions + * of pn are not contained in assumps. + */ +void pfnEnsureClosedWrt(ProofNode* pn, + const std::vector<Node>& assumps, + const char* c, + const char* ctx); +} // namespace cvc5 + +#endif /* CVC5__PROOF__PROOF_ENSURE_CLOSED_H */ diff --git a/src/proof/proof_generator.cpp b/src/proof/proof_generator.cpp new file mode 100644 index 000000000..bbfde7986 --- /dev/null +++ b/src/proof/proof_generator.cpp @@ -0,0 +1,77 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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 proof generator utility. + */ + +#include "proof/proof_generator.h" + +#include <sstream> + +#include "options/smt_options.h" +#include "proof/proof.h" +#include "proof/proof_node.h" +#include "proof/proof_node_algorithm.h" + +namespace cvc5 { + +std::ostream& operator<<(std::ostream& out, CDPOverwrite opol) +{ + switch (opol) + { + case CDPOverwrite::ALWAYS: out << "ALWAYS"; break; + case CDPOverwrite::ASSUME_ONLY: out << "ASSUME_ONLY"; break; + case CDPOverwrite::NEVER: out << "NEVER"; break; + default: out << "CDPOverwrite:unknown"; break; + } + return out; +} + +ProofGenerator::ProofGenerator() {} + +ProofGenerator::~ProofGenerator() {} + +std::shared_ptr<ProofNode> ProofGenerator::getProofFor(Node f) +{ + Unreachable() << "ProofGenerator::getProofFor: " << identify() + << " has no implementation" << std::endl; + return nullptr; +} + +bool ProofGenerator::addProofTo(Node f, + CDProof* pf, + CDPOverwrite opolicy, + bool doCopy) +{ + Trace("pfgen") << "ProofGenerator::addProofTo: " << f << "..." << std::endl; + Assert(pf != nullptr); + // plug in the proof provided by the generator, if it exists + std::shared_ptr<ProofNode> apf = getProofFor(f); + if (apf != nullptr) + { + Trace("pfgen") << "...got proof " << *apf.get() << std::endl; + if (pf->addProof(apf, opolicy, doCopy)) + { + Trace("pfgen") << "...success!" << std::endl; + return true; + } + Trace("pfgen") << "...failed to add proof" << std::endl; + } + else + { + Trace("pfgen") << "...failed, no proof" << std::endl; + Assert(false) << "Failed to get proof from generator for fact " << f; + } + return false; +} + +} // namespace cvc5 diff --git a/src/proof/proof_generator.h b/src/proof/proof_generator.h new file mode 100644 index 000000000..a8fe43909 --- /dev/null +++ b/src/proof/proof_generator.h @@ -0,0 +1,113 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * The abstract proof generator class. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_GENERATOR_H +#define CVC5__PROOF__PROOF_GENERATOR_H + +#include "expr/node.h" + +namespace cvc5 { + +class CDProof; +class ProofNode; + +/** An overwrite policy for CDProof */ +enum class CDPOverwrite : uint32_t +{ + // always overwrite an existing step. + ALWAYS, + // overwrite ASSUME with non-ASSUME steps. + ASSUME_ONLY, + // never overwrite an existing step. + NEVER, +}; +/** Writes a overwrite policy name to a stream. */ +std::ostream& operator<<(std::ostream& out, CDPOverwrite opol); + +/** + * An abstract proof generator class. + * + * A proof generator is intended to be used as a utility e.g. in theory + * solvers for constructing and storing proofs internally. A theory may have + * multiple instances of ProofGenerator objects, e.g. if it has more than one + * way of justifying lemmas or conflicts. + * + * A proof generator has two main interfaces for generating proofs: + * (1) getProofFor, and (2) addProofTo. The latter is optional. + * + * The addProofTo method can be used as an optimization for avoiding + * the construction of the ProofNode for a given fact. + * + * If no implementation of addProofTo is provided, then addProofTo(f, pf) + * calls getProofFor(f) and links the topmost ProofNode of the returned proof + * into pf. Note this top-most ProofNode can be avoided in the addProofTo + * method. + */ +class ProofGenerator +{ + public: + ProofGenerator(); + virtual ~ProofGenerator(); + /** Get the proof for formula f + * + * This forces the proof generator to construct a proof for formula f and + * return it. If this is an "eager" proof generator, this function is expected + * to be implemented as a map lookup. If this is a "lazy" proof generator, + * this function is expected to invoke a proof producing procedure of the + * generator. + * + * It should be the case that hasProofFor(f) is true. + * + * @param f The fact to get the proof for. + * @return The proof for f. + */ + virtual std::shared_ptr<ProofNode> getProofFor(Node f); + /** + * Add the proof for formula f to proof pf. The proof of f is overwritten in + * pf based on the policy opolicy. + * + * @param f The fact to get the proof for. + * @param pf The CDProof object to add the proof to. + * @param opolicy The overwrite policy for adding to pf. + * @param doCopy Whether to do a deep copy of the proof steps into pf. + * @return True if this call was sucessful. + */ + virtual bool addProofTo(Node f, + CDProof* pf, + CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY, + bool doCopy = false); + /** + * Can we give the proof for formula f? This is used for debugging. This + * returns false if the generator cannot provide a proof of formula f. + * + * Also notice that this function does not require the proof for f to be + * constructed at the time of this call. Thus, if this is a "lazy" proof + * generator, it is expected that this call is implemented as a map lookup + * into the bookkeeping maintained by the generator only. + * + * Notice the default return value is true. In other words, a proof generator + * may choose to override this function to verify the construction, although + * we do not insist this is the case. + */ + virtual bool hasProofFor(Node f) { return true; } + /** Identify this generator (for debugging, etc..) */ + virtual std::string identify() const = 0; +}; + +} // namespace cvc5 + +#endif /* CVC5__PROOF__PROOF_GENERATOR_H */ diff --git a/src/proof/proof_node.cpp b/src/proof/proof_node.cpp new file mode 100644 index 000000000..e3affb306 --- /dev/null +++ b/src/proof/proof_node.cpp @@ -0,0 +1,72 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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 proof node utility. + */ + +#include "proof/proof_node.h" + +#include "proof/proof_node_algorithm.h" +#include "proof/proof_node_to_sexpr.h" + +namespace cvc5 { + +ProofNode::ProofNode(PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args) +{ + setValue(id, children, args); +} + +PfRule ProofNode::getRule() const { return d_rule; } + +const std::vector<std::shared_ptr<ProofNode>>& ProofNode::getChildren() const +{ + return d_children; +} + +const std::vector<Node>& ProofNode::getArguments() const { return d_args; } + +Node ProofNode::getResult() const { return d_proven; } + +bool ProofNode::isClosed() +{ + std::vector<Node> assumps; + expr::getFreeAssumptions(this, assumps); + return assumps.empty(); +} + +void ProofNode::setValue( + PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args) +{ + d_rule = id; + d_children = children; + d_args = args; +} + +void ProofNode::printDebug(std::ostream& os) const +{ + // convert to sexpr and print + ProofNodeToSExpr pnts; + Node ps = pnts.convertToSExpr(this); + os << ps; +} + +std::ostream& operator<<(std::ostream& out, const ProofNode& pn) +{ + pn.printDebug(out); + return out; +} + +} // namespace cvc5 diff --git a/src/proof/proof_node.h b/src/proof/proof_node.h new file mode 100644 index 000000000..db82cc63d --- /dev/null +++ b/src/proof/proof_node.h @@ -0,0 +1,145 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, Alex Ozdemir + * + * 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. + * **************************************************************************** + * + * Proof node utility. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_NODE_H +#define CVC5__PROOF__PROOF_NODE_H + +#include <vector> + +#include "expr/node.h" +#include "proof/proof_rule.h" + +namespace cvc5 { + +class ProofNodeManager; +class ProofNode; + +// Alias for shared pointer to a proof node +using Pf = std::shared_ptr<ProofNode>; + +struct ProofNodeHashFunction +{ + inline size_t operator()(std::shared_ptr<ProofNode> pfn) const; +}; /* struct ProofNodeHashFunction */ + +/** A node in a proof + * + * A ProofNode represents a single step in a proof. It contains: + * (1) d_id, an identifier indicating the kind of inference, + * (2) d_children, the child ProofNode objects indicating its premises, + * (3) d_args, additional arguments used to determine the conclusion, + * (4) d_proven, cache of the formula that this ProofNode proves. + * + * Overall, a ProofNode and its children form a directed acyclic graph. + * + * A ProofNode is partially mutable in that (1), (2) and (3) can be + * modified. A motivating example of when this is useful is when a ProofNode + * is established to be a "hole" for something to be proven later. On the other + * hand, (4) is intended to be immutable. + * + * The method setValue is private and can be called by objects that manage + * ProofNode objects in trusted ways that ensure that the node maintains + * the invariant above. Furthermore, notice that this class is not responsible + * for setting d_proven; this is done externally by a ProofNodeManager class. + * + * Notice that all fields of ProofNode are stored in ***Skolem form***. Their + * correctness is checked in ***witness form*** (for details on this + * terminology, see expr/skolem_manager.h). As a simple example, say a + * theory solver has a term t, and wants to introduce a unit lemma (= k t) + * where k is a fresh Skolem variable. It creates this variable via: + * k = SkolemManager::mkPurifySkolem(t,"k"); + * A checked ProofNode for the fact (= k t) then may have fields: + * d_rule := MACRO_SR_PRED_INTRO, + * d_children := {}, + * d_args := {(= k t)} + * d_proven := (= k t). + * Its justification via the rule MACRO_SR_PRED_INTRO (see documentation + * in theory/builtin/proof_kinds) is in terms of the witness form of the + * argument: + * (= (witness ((z T)) (= z t)) t) + * which, by that rule's side condition, is such that: + * Rewriter::rewrite((= (witness ((z T)) (= z t)) t)) = true. + * Notice that the correctness of the rule is justified here by rewriting + * the witness form of (= k t). The conversion to/from witness form is + * managed by ProofRuleChecker::check. + * + * An external proof checker is expected to formalize the ProofNode only in + * terms of *witness* forms. + * + * However, the rest of cvc5 sees only the *Skolem* form of arguments and + * conclusions in ProofNode, since this is what is used throughout cvc5. + */ +class ProofNode +{ + friend class ProofNodeManager; + + public: + ProofNode(PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args); + ~ProofNode() {} + /** get the rule of this proof node */ + PfRule getRule() const; + /** Get children */ + const std::vector<std::shared_ptr<ProofNode>>& getChildren() const; + /** Get arguments */ + const std::vector<Node>& getArguments() const; + /** get what this node proves, or the null node if this is an invalid proof */ + Node getResult() const; + /** + * Returns true if this is a closed proof (i.e. it has no free assumptions). + */ + bool isClosed(); + /** Print debug on output strem os */ + void printDebug(std::ostream& os) const; + + private: + /** + * Set value, called to overwrite the contents of this ProofNode with the + * given arguments. + */ + void setValue(PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args); + /** The proof rule */ + PfRule d_rule; + /** The children of this proof node */ + std::vector<std::shared_ptr<ProofNode>> d_children; + /** arguments of this node */ + std::vector<Node> d_args; + /** The cache of the fact that has been proven, modifiable by ProofChecker */ + Node d_proven; +}; + +inline size_t ProofNodeHashFunction::operator()( + std::shared_ptr<ProofNode> pfn) const +{ + return pfn->getResult().getId() + static_cast<unsigned>(pfn->getRule()); +} + +/** + * Serializes a given proof node to the given stream. + * + * @param out the output stream to use + * @param pn the proof node to output to the stream + * @return the stream + */ +std::ostream& operator<<(std::ostream& out, const ProofNode& pn); + +} // namespace cvc5 + +#endif /* CVC5__PROOF__PROOF_NODE_H */ diff --git a/src/proof/proof_node_algorithm.cpp b/src/proof/proof_node_algorithm.cpp new file mode 100644 index 000000000..82ccc034f --- /dev/null +++ b/src/proof/proof_node_algorithm.cpp @@ -0,0 +1,176 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa + * + * 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 proof node algorithm utilities. + */ + +#include "proof/proof_node_algorithm.h" + +#include "proof/proof_node.h" + +namespace cvc5 { +namespace expr { + +void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump) +{ + std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amap; + std::shared_ptr<ProofNode> spn = std::make_shared<ProofNode>( + pn->getRule(), pn->getChildren(), pn->getArguments()); + getFreeAssumptionsMap(spn, amap); + for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& p : + amap) + { + assump.push_back(p.first); + } +} + +void getFreeAssumptionsMap( + std::shared_ptr<ProofNode> pn, + std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap) +{ + // proof should not be cyclic + // visited set false after preorder traversal, true after postorder traversal + std::unordered_map<ProofNode*, bool> visited; + std::unordered_map<ProofNode*, bool>::iterator it; + std::vector<std::shared_ptr<ProofNode>> visit; + std::vector<std::shared_ptr<ProofNode>> traversing; + // Maps a bound assumption to the number of bindings it is under + // e.g. in (SCOPE (SCOPE (ASSUME x) (x y)) (y)), y would be mapped to 2 at + // (ASSUME x), and x would be mapped to 1. + // + // This map is used to track which nodes are in scope while traversing the + // DAG. The in-scope assumptions are keys in the map. They're removed when + // their binding count drops to zero. Let's annotate the above example to + // serve as an illustration: + // + // (SCOPE0 (SCOPE1 (ASSUME x) (x y)) (y)) + // + // This is how the map changes during the traversal: + // after previsiting SCOPE0: { y: 1 } + // after previsiting SCOPE1: { y: 2, x: 1 } + // at ASSUME: { y: 2, x: 1 } (so x is in scope!) + // after postvisiting SCOPE1: { y: 1 } + // after postvisiting SCOPE2: {} + // + std::unordered_map<Node, uint32_t> scopeDepth; + std::shared_ptr<ProofNode> cur; + visit.push_back(pn); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur.get()); + const std::vector<Node>& cargs = cur->getArguments(); + if (it == visited.end()) + { + PfRule id = cur->getRule(); + if (id == PfRule::ASSUME) + { + visited[cur.get()] = true; + Assert(cargs.size() == 1); + Node f = cargs[0]; + if (!scopeDepth.count(f)) + { + amap[f].push_back(cur); + } + } + else + { + if (id == PfRule::SCOPE) + { + // mark that its arguments are bound in the current scope + for (const Node& a : cargs) + { + scopeDepth[a] += 1; + } + // will need to unbind the variables below + } + // The following loop cannot be merged with the loop above because the + // same subproof + visited[cur.get()] = false; + visit.push_back(cur); + traversing.push_back(cur); + const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren(); + for (const std::shared_ptr<ProofNode>& cp : cs) + { + if (std::find(traversing.begin(), traversing.end(), cp) + != traversing.end()) + { + Unhandled() << "getFreeAssumptionsMap: cyclic proof! (use " + "--proof-eager-checking)" + << std::endl; + } + visit.push_back(cp); + } + } + } + else if (!it->second) + { + Assert(!traversing.empty()); + traversing.pop_back(); + visited[cur.get()] = true; + if (cur->getRule() == PfRule::SCOPE) + { + // unbind its assumptions + for (const Node& a : cargs) + { + auto scopeCt = scopeDepth.find(a); + Assert(scopeCt != scopeDepth.end()); + scopeCt->second -= 1; + if (scopeCt->second == 0) + { + scopeDepth.erase(scopeCt); + } + } + } + } + } while (!visit.empty()); +} + +bool containsSubproof(ProofNode* pn, ProofNode* pnc) +{ + std::unordered_set<const ProofNode*> visited; + return containsSubproof(pn, pnc, visited); +} + +bool containsSubproof(ProofNode* pn, + ProofNode* pnc, + std::unordered_set<const ProofNode*>& visited) +{ + std::unordered_map<const ProofNode*, bool>::iterator it; + std::vector<const ProofNode*> visit; + visit.push_back(pn); + const ProofNode* cur; + while (!visit.empty()) + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur == pnc) + { + return true; + } + const std::vector<std::shared_ptr<ProofNode>>& children = + cur->getChildren(); + for (const std::shared_ptr<ProofNode>& cp : children) + { + visit.push_back(cp.get()); + } + } + } + return false; +} + +} // namespace expr +} // namespace cvc5 diff --git a/src/proof/proof_node_algorithm.h b/src/proof/proof_node_algorithm.h new file mode 100644 index 000000000..1ccefb0a2 --- /dev/null +++ b/src/proof/proof_node_algorithm.h @@ -0,0 +1,76 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Proof node algorithm utilities. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_NODE_ALGORITHM_H +#define CVC5__PROOF__PROOF_NODE_ALGORITHM_H + +#include <vector> + +#include "expr/node.h" + +namespace cvc5 { + +class ProofNode; + +namespace expr { + +/** + * This adds to the vector assump all formulas that are "free assumptions" of + * the proof whose root is ProofNode pn. A free assumption is a formula F + * that is an argument (in d_args) of a ProofNode whose kind is ASSUME, and + * that proof node is not beneath an application of SCOPE containing F as an + * argument. + * + * This traverses the structure of the dag represented by this ProofNode. + * Its implementation is analogous to expr::getFreeVariables. + * + * @param pn The proof node. + * @param assump The vector to add the free asumptions of pn to. + */ +void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump); +/** + * Same as above, but maps assumptions to the proof pointer(s) for that + * assumption. Notice that depending on how pn is constructed, there may be + * multiple ProofNode that are ASSUME proofs of the same assumption, which + * are each added to the range of the assumption. + * + * @param pn The proof node. + * @param amap The mapping to add the free asumptions of pn and their + * corresponding proof nodes to. + */ +void getFreeAssumptionsMap( + std::shared_ptr<ProofNode> pn, + std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap); + +/** + * @return true if pn contains pnc. + */ +bool containsSubproof(ProofNode* pn, ProofNode* pnc); + +/** + * Same as above, with a visited cache. + * + * @return true if pn contains pnc. + */ +bool containsSubproof(ProofNode* pn, + ProofNode* pnc, + std::unordered_set<const ProofNode*>& visited); + +} // namespace expr +} // namespace cvc5 + +#endif /* CVC5__PROOF__PROOF_NODE_ALGORITHM_H */ diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp new file mode 100644 index 000000000..cf19eebdf --- /dev/null +++ b/src/proof/proof_node_manager.cpp @@ -0,0 +1,407 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, 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 proof node manager. + */ + +#include "proof/proof_node_manager.h" + +#include <sstream> + +#include "options/proof_options.h" +#include "proof/proof.h" +#include "proof/proof_checker.h" +#include "proof/proof_node.h" +#include "proof/proof_node_algorithm.h" +#include "theory/rewriter.h" + +using namespace cvc5::kind; + +namespace cvc5 { + +ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc) +{ + d_true = NodeManager::currentNM()->mkConst(true); +} + +std::shared_ptr<ProofNode> ProofNodeManager::mkNode( + PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args, + Node expected) +{ + Trace("pnm") << "ProofNodeManager::mkNode " << id << " {" << expected.getId() + << "} " << expected << "\n"; + Node res = checkInternal(id, children, args, expected); + if (res.isNull()) + { + // if it was invalid, then we return the null node + return nullptr; + } + // otherwise construct the proof node and set its proven field + std::shared_ptr<ProofNode> pn = + std::make_shared<ProofNode>(id, children, args); + pn->d_proven = res; + return pn; +} + +std::shared_ptr<ProofNode> ProofNodeManager::mkAssume(Node fact) +{ + Assert(!fact.isNull()); + Assert(fact.getType().isBoolean()); + 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, + bool ensureClosed, + bool doMinimize, + Node expected) +{ + if (!ensureClosed) + { + return mkNode(PfRule::SCOPE, {pf}, assumps, expected); + } + Trace("pnm-scope") << "ProofNodeManager::mkScope " << assumps << std::endl; + // we first ensure the assumptions are flattened + std::unordered_set<Node> ac{assumps.begin(), assumps.end()}; + // map from the rewritten form of assumptions to the original. This is only + // computed in the rare case when we need rewriting to match the + // assumptions. An example of this is for Boolean constant equalities in + // scoped proofs from the proof equality engine. + std::unordered_map<Node, Node> acr; + // whether we have compute the map above + bool computedAcr = false; + + // The free assumptions of the proof + std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap; + expr::getFreeAssumptionsMap(pf, famap); + std::unordered_set<Node> acu; + for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& + fa : famap) + { + Node a = fa.first; + if (ac.find(a) != ac.end()) + { + // already covered by an assumption + acu.insert(a); + continue; + } + // trivial assumption + if (a == d_true) + { + Trace("pnm-scope") << "- justify trivial True assumption\n"; + for (std::shared_ptr<ProofNode> pfs : fa.second) + { + Assert(pfs->getResult() == a); + updateNode(pfs.get(), PfRule::MACRO_SR_PRED_INTRO, {}, {a}); + } + Trace("pnm-scope") << "...finished" << std::endl; + acu.insert(a); + continue; + } + Trace("pnm-scope") << "- try matching free assumption " << a << "\n"; + // otherwise it may be due to symmetry? + Node aeqSym = CDProof::getSymmFact(a); + Trace("pnm-scope") << " - try sym " << aeqSym << "\n"; + Node aMatch; + if (!aeqSym.isNull() && ac.count(aeqSym)) + { + Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a + << " for " << fa.second.size() << " proof nodes" + << std::endl; + aMatch = aeqSym; + } + else + { + // Otherwise, may be derivable by rewriting. Note this is used in + // ensuring that proofs from the proof equality engine that involve + // equality with Boolean constants are closed. + if (!computedAcr) + { + computedAcr = true; + for (const Node& acc : ac) + { + Node accr = theory::Rewriter::rewrite(acc); + if (accr != acc) + { + acr[accr] = acc; + } + } + } + Node ar = theory::Rewriter::rewrite(a); + std::unordered_map<Node, Node>::iterator itr = acr.find(ar); + if (itr != acr.end()) + { + aMatch = itr->second; + } + } + + // if we found a match either by symmetry or rewriting, then we connect + // the assumption here. + if (!aMatch.isNull()) + { + std::shared_ptr<ProofNode> pfaa = mkAssume(aMatch); + // must correct the orientation on this leaf + std::vector<std::shared_ptr<ProofNode>> children; + children.push_back(pfaa); + for (std::shared_ptr<ProofNode> pfs : fa.second) + { + Assert(pfs->getResult() == a); + // use SYMM if possible + if (aMatch == aeqSym) + { + updateNode(pfs.get(), PfRule::SYMM, children, {}); + } + else + { + updateNode(pfs.get(), PfRule::MACRO_SR_PRED_TRANSFORM, children, {a}); + } + } + Trace("pnm-scope") << "...finished" << std::endl; + acu.insert(aMatch); + continue; + } + // If we did not find a match, it is an error, since all free assumptions + // should be arguments to SCOPE. + std::stringstream ss; + + bool dumpProofTraceOn = Trace.isOn("dump-proof-error"); + if (dumpProofTraceOn) + { + ss << "The proof : " << *pf << std::endl; + } + ss << std::endl << "Free assumption: " << a << std::endl; + for (const Node& aprint : ac) + { + ss << "- assumption: " << aprint << std::endl; + } + if (!dumpProofTraceOn) + { + ss << "Use -t dump-proof-error for details on proof" << std::endl; + } + Unreachable() << "Generated a proof that is not closed by the scope: " + << ss.str() << std::endl; + } + if (acu.size() < ac.size()) + { + // All assumptions should match a free assumption; if one does not, then + // the explanation could have been smaller. + for (const Node& a : ac) + { + if (acu.find(a) == acu.end()) + { + Notice() << "ProofNodeManager::mkScope: assumption " << a + << " does not match a free assumption in proof" << std::endl; + } + } + } + if (doMinimize && acu.size() < ac.size()) + { + assumps.clear(); + assumps.insert(assumps.end(), acu.begin(), acu.end()); + } + else if (ac.size() < assumps.size()) + { + // remove duplicates to avoid redundant literals in clauses + assumps.clear(); + assumps.insert(assumps.end(), ac.begin(), ac.end()); + } + Node minExpected; + NodeManager* nm = NodeManager::currentNM(); + Node exp; + if (assumps.empty()) + { + // SCOPE with no arguments is a no-op, just return original + return pf; + } + Node conc = pf->getResult(); + exp = assumps.size() == 1 ? assumps[0] : nm->mkNode(AND, assumps); + if (conc.isConst() && !conc.getConst<bool>()) + { + minExpected = exp.notNode(); + } + else + { + minExpected = nm->mkNode(IMPLIES, exp, conc); + } + return mkNode(PfRule::SCOPE, {pf}, assumps, minExpected); +} + +bool ProofNodeManager::updateNode( + ProofNode* pn, + PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args) +{ + return updateNodeInternal(pn, id, children, args, true); +} + +bool ProofNodeManager::updateNode(ProofNode* pn, ProofNode* pnr) +{ + Assert(pn != nullptr); + Assert(pnr != nullptr); + if (pn->getResult() != pnr->getResult()) + { + return false; + } + // can shortcut re-check of rule + return updateNodeInternal( + pn, pnr->getRule(), pnr->getChildren(), pnr->getArguments(), false); +} + +Node ProofNodeManager::checkInternal( + PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args, + Node expected) +{ + Node res; + if (d_checker) + { + // check with the checker, which takes expected as argument + res = d_checker->check(id, children, args, expected); + Assert(!res.isNull()) + << "ProofNodeManager::checkInternal: failed to check proof"; + } + else + { + // otherwise we trust the expected value, if it exists + Assert(!expected.isNull()) << "ProofNodeManager::checkInternal: no checker " + "or expected value provided"; + res = expected; + } + return res; +} + +ProofChecker* ProofNodeManager::getChecker() const { return d_checker; } + +std::shared_ptr<ProofNode> ProofNodeManager::clone( + std::shared_ptr<ProofNode> pn) +{ + const ProofNode* orig = pn.get(); + std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>> visited; + std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>>::iterator it; + std::vector<const ProofNode*> visit; + std::shared_ptr<ProofNode> cloned; + visit.push_back(orig); + const ProofNode* cur; + while (!visit.empty()) + { + cur = visit.back(); + it = visited.find(cur); + if (it == visited.end()) + { + visited[cur] = nullptr; + const std::vector<std::shared_ptr<ProofNode>>& children = + cur->getChildren(); + for (const std::shared_ptr<ProofNode>& cp : children) + { + visit.push_back(cp.get()); + } + continue; + } + visit.pop_back(); + if (it->second.get() == nullptr) + { + std::vector<std::shared_ptr<ProofNode>> cchildren; + const std::vector<std::shared_ptr<ProofNode>>& children = + cur->getChildren(); + for (const std::shared_ptr<ProofNode>& cp : children) + { + it = visited.find(cp.get()); + Assert(it != visited.end()); + Assert(it->second != nullptr); + cchildren.push_back(it->second); + } + cloned = std::make_shared<ProofNode>( + cur->getRule(), cchildren, cur->getArguments()); + visited[cur] = cloned; + // we trust the above cloning does not change what is proven + cloned->d_proven = cur->d_proven; + } + } + Assert(visited.find(orig) != visited.end()); + return visited[orig]; +} + +bool ProofNodeManager::updateNodeInternal( + ProofNode* pn, + PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args, + bool needsCheck) +{ + Assert(pn != nullptr); + // ---------------- check for cyclic + if (options::proofEagerChecking()) + { + std::unordered_set<const ProofNode*> visited; + for (const std::shared_ptr<ProofNode>& cpc : children) + { + if (expr::containsSubproof(cpc.get(), pn, visited)) + { + std::stringstream ss; + ss << "ProofNodeManager::updateNode: attempting to make cyclic proof! " + << id << " " << pn->getResult() << ", children = " << std::endl; + for (const std::shared_ptr<ProofNode>& cp : children) + { + ss << " " << cp->getRule() << " " << cp->getResult() << std::endl; + } + ss << "Full children:" << std::endl; + for (const std::shared_ptr<ProofNode>& cp : children) + { + ss << " - "; + cp->printDebug(ss); + ss << std::endl; + } + Unreachable() << ss.str(); + } + } + } + // ---------------- end check for cyclic + + // should have already computed what is proven + Assert(!pn->d_proven.isNull()) + << "ProofNodeManager::updateProofNode: invalid proof provided"; + if (needsCheck) + { + // We expect to prove the same thing as before + Node res = checkInternal(id, children, args, pn->d_proven); + if (res.isNull()) + { + // if it was invalid, then we do not update + return false; + } + // proven field should already be the same as the result + Assert(res == pn->d_proven); + } + + // we update its value + pn->setValue(id, children, args); + return true; +} + +} // namespace cvc5 diff --git a/src/proof/proof_node_manager.h b/src/proof/proof_node_manager.h new file mode 100644 index 000000000..2fa7ed3e9 --- /dev/null +++ b/src/proof/proof_node_manager.h @@ -0,0 +1,206 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Proof node manager utility. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_NODE_MANAGER_H +#define CVC5__PROOF__PROOF_NODE_MANAGER_H + +#include <vector> + +#include "expr/node.h" +#include "proof/proof_rule.h" + +namespace cvc5 { + +class ProofChecker; +class ProofNode; + +/** + * A manager for proof node objects. This is a trusted interface for creating + * and updating ProofNode objects. + * + * In more detail, we say a ProofNode is "well-formed (with respect to checker + * X)" if its d_proven field is non-null, and corresponds to the formula that + * the ProofNode proves according to X. The ProofNodeManager class constructs + * and update nodes that are well-formed with respect to its underlying checker. + * + * If no checker is provided, then the ProofNodeManager assigns the d_proven + * field of ProofNode based on the provided "expected" argument in mkNode below, + * which must be provided in this case. + * + * The ProofNodeManager is used as a trusted way of updating ProofNode objects + * via updateNode below. In particular, this method leaves the d_proven field + * unchanged and updates (if possible) the remaining content of a given proof + * node. + * + * Notice that ProofNode objects are mutable, and hence this class does not + * cache the results of mkNode. A version of this class that caches + * immutable version of ProofNode objects could be built as an extension + * or layer on top of this class. + */ +class ProofNodeManager +{ + public: + ProofNodeManager(ProofChecker* pc = nullptr); + ~ProofNodeManager() {} + /** + * This constructs a ProofNode with the given arguments. The expected + * argument, when provided, indicates the formula that the returned node + * is expected to prove. If we find that it does not, based on the underlying + * checker, this method returns nullptr. + * + * @param id The id of the proof node. + * @param children The children of the proof node. + * @param args The arguments of the proof node. + * @param expected (Optional) the expected conclusion of the proof node. + * @return the proof node, or nullptr if the given arguments do not + * consistute a proof of the expected conclusion according to the underlying + * checker, if both are provided. It also returns nullptr if neither the + * checker nor the expected field is provided, since in this case the + * conclusion is unknown. + */ + std::shared_ptr<ProofNode> mkNode( + PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args, + Node expected = Node::null()); + /** + * Make the proof node corresponding to the assumption of fact. + * + * @param fact The fact to assume. + * @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 + * the returned proof is not closed. This is the case if a free assumption + * of pf is missing from the vector assumps. + * + * For conveinence, the proof pf may be modified to ensure that the overall + * result is closed. For instance, given input: + * pf = TRANS( ASSUME( x=y ), ASSUME( y=z ) ) + * assumps = { y=x, y=z } + * This method will modify pf to be: + * pf = TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) ) + * so that y=x matches the free assumption. The returned proof is: + * SCOPE(TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) ) :args { y=x, y=z }) + * + * When ensureClosed is true, duplicates are eliminated from assumps. The + * reason for this is due to performance, since in this method, assumps is + * converted to an unordered_set to do the above check and hence it is a + * convienient time to eliminate duplicate literals. + * + * Additionally, if both ensureClosed and doMinimize are true, assumps is + * updated to contain exactly the free asumptions of pf. This also includes + * having no duplicates. Furthermore, if assumps is empty after minimization, + * this method is a no-op. + * + * In each case, the update vector assumps is passed as arguments to SCOPE. + * + * @param pf The body of the proof, + * @param assumps The assumptions-to-close of the scope, + * @param ensureClosed Whether to ensure that the proof is closed, + * @param doMinimize Whether to minimize assumptions. + * @param expected the node that the scope should prove. + * @return The scoped proof. + */ + std::shared_ptr<ProofNode> mkScope(std::shared_ptr<ProofNode> pf, + std::vector<Node>& assumps, + bool ensureClosed = true, + bool doMinimize = false, + Node expected = Node::null()); + /** + * This method updates pn to be a proof of the form <id>( children, args ), + * while maintaining its d_proven field. This method returns false if this + * proof manager is using a checker, and we compute that the above proof + * is not a proof of the fact that pn previously proved. + * + * @param pn The proof node to update. + * @param id The updated id of the proof node. + * @param children The updated children of the proof node. + * @param args The updated arguments of the proof node. + * @return true if the update was successful. + * + * Notice that updateNode always returns true if there is no underlying + * checker. + */ + bool updateNode(ProofNode* pn, + PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args); + /** + * Update node pn to have the contents of pnr. It should be the case that + * pn and pnr prove the same fact, otherwise false is returned and pn is + * unchanged. + */ + bool updateNode(ProofNode* pn, ProofNode* pnr); + /** Get the underlying proof checker */ + ProofChecker* getChecker() const; + /** + * Clone a proof node, which creates a deep copy of pn and returns it. The + * dag structure of pn is the same as that in the returned proof node. + * + * @param pn The proof node to clone + * @return the cloned proof node. + */ + std::shared_ptr<ProofNode> clone(std::shared_ptr<ProofNode> pn); + + private: + /** The (optional) proof checker */ + ProofChecker* d_checker; + /** the true node */ + Node d_true; + /** Check internal + * + * This returns the result of proof checking a ProofNode with the provided + * arguments with an expected conclusion, which may not null if there is + * no expected conclusion. + * + * This throws an assertion error if we fail to check such a proof node, or + * if expected is provided (non-null) and is different what is proven by the + * other arguments. + */ + Node checkInternal(PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args, + Node expected); + /** + * Update node internal, return true if successful. This is called by + * the update node methods above. The argument needsCheck is whether we + * need to check the correctness of the rule application. This is false + * for the updateNode routine where pnr is an (already checked) proof node. + */ + bool updateNodeInternal( + ProofNode* pn, + PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args, + bool needsCheck); +}; + +} // namespace cvc5 + +#endif /* CVC5__PROOF__PROOF_NODE_H */ diff --git a/src/proof/proof_node_to_sexpr.cpp b/src/proof/proof_node_to_sexpr.cpp new file mode 100644 index 000000000..85fc2395e --- /dev/null +++ b/src/proof/proof_node_to_sexpr.cpp @@ -0,0 +1,148 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, 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 proof node to s-expression. + */ + +#include "proof/proof_node_to_sexpr.h" + +#include <iostream> +#include <sstream> + +#include "options/proof_options.h" +#include "proof/proof_node.h" + +using namespace cvc5::kind; + +namespace cvc5 { + +ProofNodeToSExpr::ProofNodeToSExpr() +{ + NodeManager* nm = NodeManager::currentNM(); + d_conclusionMarker = nm->mkBoundVar(":conclusion", nm->sExprType()); + d_argsMarker = nm->mkBoundVar(":args", nm->sExprType()); +} + +Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn) +{ + NodeManager* nm = NodeManager::currentNM(); + std::map<const ProofNode*, Node>::iterator it; + std::vector<const ProofNode*> visit; + std::vector<const ProofNode*> traversing; + const ProofNode* cur; + visit.push_back(pn); + do + { + cur = visit.back(); + visit.pop_back(); + it = d_pnMap.find(cur); + + if (it == d_pnMap.end()) + { + d_pnMap[cur] = Node::null(); + traversing.push_back(cur); + visit.push_back(cur); + const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren(); + for (const std::shared_ptr<ProofNode>& cp : pc) + { + if (std::find(traversing.begin(), traversing.end(), cp.get()) + != traversing.end()) + { + Unhandled() << "ProofNodeToSExpr::convertToSExpr: cyclic proof! (use " + "--proof-eager-checking)" + << std::endl; + return Node::null(); + } + visit.push_back(cp.get()); + } + } + else if (it->second.isNull()) + { + Assert(!traversing.empty()); + traversing.pop_back(); + std::vector<Node> children; + // add proof rule + children.push_back(getOrMkPfRuleVariable(cur->getRule())); + if (options::proofPrintConclusion()) + { + children.push_back(d_conclusionMarker); + children.push_back(cur->getResult()); + } + const std::vector<std::shared_ptr<ProofNode>>& pc = cur->getChildren(); + for (const std::shared_ptr<ProofNode>& cp : pc) + { + it = d_pnMap.find(cp.get()); + Assert(it != d_pnMap.end()); + Assert(!it->second.isNull()); + children.push_back(it->second); + } + // add arguments + const std::vector<Node>& args = cur->getArguments(); + if (!args.empty()) + { + children.push_back(d_argsMarker); + // needed to ensure builtin operators are not treated as operators + // this can be the case for CONG where d_args may contain a builtin + // operator + std::vector<Node> argsSafe; + for (const Node& a : args) + { + Node av = a; + if (a.getNumChildren() == 0 + && NodeManager::operatorToKind(a) != UNDEFINED_KIND) + { + av = getOrMkNodeVariable(a); + } + argsSafe.push_back(av); + } + Node argsC = nm->mkNode(SEXPR, argsSafe); + children.push_back(argsC); + } + d_pnMap[cur] = nm->mkNode(SEXPR, children); + } + } while (!visit.empty()); + Assert(d_pnMap.find(pn) != d_pnMap.end()); + Assert(!d_pnMap.find(pn)->second.isNull()); + return d_pnMap[pn]; +} + +Node ProofNodeToSExpr::getOrMkPfRuleVariable(PfRule r) +{ + std::map<PfRule, Node>::iterator it = d_pfrMap.find(r); + if (it != d_pfrMap.end()) + { + return it->second; + } + std::stringstream ss; + ss << r; + NodeManager* nm = NodeManager::currentNM(); + Node var = nm->mkBoundVar(ss.str(), nm->sExprType()); + d_pfrMap[r] = var; + return var; +} + +Node ProofNodeToSExpr::getOrMkNodeVariable(Node n) +{ + std::map<Node, Node>::iterator it = d_nodeMap.find(n); + if (it != d_nodeMap.end()) + { + return it->second; + } + std::stringstream ss; + ss << n; + NodeManager* nm = NodeManager::currentNM(); + Node var = nm->mkBoundVar(ss.str(), nm->sExprType()); + d_nodeMap[n] = var; + return var; +} + +} // namespace cvc5 diff --git a/src/proof/proof_node_to_sexpr.h b/src/proof/proof_node_to_sexpr.h new file mode 100644 index 000000000..c358f3445 --- /dev/null +++ b/src/proof/proof_node_to_sexpr.h @@ -0,0 +1,70 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Conversion from ProofNode to s-expressions. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_NODE_TO_SEXPR_H +#define CVC5__PROOF__PROOF_NODE_TO_SEXPR_H + +#include <map> + +#include "expr/node.h" +#include "proof/proof_rule.h" + +namespace cvc5 { + +class ProofNode; + +/** A class to convert ProofNode objects to s-expressions */ +class ProofNodeToSExpr +{ + public: + ProofNodeToSExpr(); + ~ProofNodeToSExpr() {} + /** Convert the given proof node to an s-expression + * + * This is useful for operations where it is useful to view a ProofNode as + * a Node. Printing is one such example, where a ProofNode can be printed + * as a dag after this conversion. + * + * The s-expression for a ProofNode has the form: + * (SEXPR (VAR "<d_rule>") S1 ... Sn (VAR ":args") (SEXPR <d_args>)) + * where S1, ..., Sn are the s-expressions for its <d_children>. + */ + Node convertToSExpr(const ProofNode* pn); + + private: + /** map proof rules to a variable */ + std::map<PfRule, Node> d_pfrMap; + /** Dummy ":args" marker */ + Node d_argsMarker; + /** Dummy ":conclusion" marker */ + Node d_conclusionMarker; + /** map proof nodes to their s-expression */ + std::map<const ProofNode*, Node> d_pnMap; + /** + * map nodes to a bound variable, used for nodes that have special AST status + * like builtin operators + */ + std::map<Node, Node> d_nodeMap; + /** get or make pf rule variable */ + Node getOrMkPfRuleVariable(PfRule r); + /** get or make node variable */ + Node getOrMkNodeVariable(Node n); +}; + +} // namespace cvc5 + +#endif /* CVC5__PROOF__PROOF_RULE_H */ diff --git a/src/proof/proof_node_updater.cpp b/src/proof/proof_node_updater.cpp new file mode 100644 index 000000000..2bdb54a45 --- /dev/null +++ b/src/proof/proof_node_updater.cpp @@ -0,0 +1,258 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa + * + * 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 a utility for updating proof nodes. + */ + +#include "proof/proof_node_updater.h" + +#include "proof/lazy_proof.h" +#include "proof/proof_ensure_closed.h" +#include "proof/proof_node_algorithm.h" +#include "proof/proof_node_manager.h" + +namespace cvc5 { + +ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {} +ProofNodeUpdaterCallback::~ProofNodeUpdaterCallback() {} + +bool ProofNodeUpdaterCallback::update(Node res, + PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args, + CDProof* cdp, + bool& continueUpdate) +{ + return false; +} + +ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm, + ProofNodeUpdaterCallback& cb, + bool mergeSubproofs, + bool autoSym) + : d_pnm(pnm), + d_cb(cb), + d_debugFreeAssumps(false), + d_mergeSubproofs(mergeSubproofs), + d_autoSym(autoSym) +{ +} + +void ProofNodeUpdater::process(std::shared_ptr<ProofNode> pf) +{ + if (d_debugFreeAssumps) + { + if (Trace.isOn("pfnu-debug")) + { + Trace("pfnu-debug2") << "Initial proof: " << *pf.get() << std::endl; + Trace("pfnu-debug") << "ProofNodeUpdater::process" << std::endl; + Trace("pfnu-debug") << "Expected free assumptions: " << std::endl; + for (const Node& fa : d_freeAssumps) + { + Trace("pfnu-debug") << "- " << fa << std::endl; + } + std::vector<Node> assump; + expr::getFreeAssumptions(pf.get(), assump); + Trace("pfnu-debug") << "Current free assumptions: " << std::endl; + for (const Node& fa : assump) + { + Trace("pfnu-debug") << "- " << fa << std::endl; + } + } + } + std::vector<std::shared_ptr<ProofNode>> traversing; + processInternal(pf, d_freeAssumps, traversing); +} + +void ProofNodeUpdater::processInternal( + std::shared_ptr<ProofNode> pf, + const std::vector<Node>& fa, + std::vector<std::shared_ptr<ProofNode>>& traversing) +{ + Trace("pf-process") << "ProofNodeUpdater::process" << std::endl; + std::unordered_map<std::shared_ptr<ProofNode>, bool> visited; + std::unordered_map<std::shared_ptr<ProofNode>, bool>::iterator it; + std::vector<std::shared_ptr<ProofNode>> visit; + std::shared_ptr<ProofNode> cur; + visit.push_back(pf); + std::map<Node, std::shared_ptr<ProofNode>>::iterator itc; + // A cache from formulas to proof nodes that are in the current scope. + // Notice that we make a fresh recursive call to process if the current + // rule is SCOPE below. + std::map<Node, std::shared_ptr<ProofNode>> resCache; + Node res; + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + res = cur->getResult(); + if (it == visited.end()) + { + if (d_mergeSubproofs) + { + itc = resCache.find(res); + if (itc != resCache.end()) + { + // already have a proof, merge it into this one + visited[cur] = true; + d_pnm->updateNode(cur.get(), itc->second.get()); + continue; + } + } + // run update to a fixed point + bool continueUpdate = true; + while (runUpdate(cur, fa, continueUpdate) && continueUpdate) + { + Trace("pf-process-debug") << "...updated proof." << std::endl; + } + visited[cur] = !continueUpdate; + if (!continueUpdate) + { + // no further changes should be made to cur according to the callback + Trace("pf-process-debug") + << "...marked to not continue update." << std::endl; + runFinalize(cur, fa, resCache); + continue; + } + traversing.push_back(cur); + visit.push_back(cur); + // If we are not the top-level proof, we were a scope, or became a scope + // after updating, we do a separate recursive call to this method. This + // allows us to properly track the assumptions in scope, which is + // important for example to merge or to determine updates based on free + // assumptions. + if (cur->getRule() == PfRule::SCOPE && cur != pf) + { + std::vector<Node> nfa; + nfa.insert(nfa.end(), fa.begin(), fa.end()); + const std::vector<Node>& args = cur->getArguments(); + nfa.insert(nfa.end(), args.begin(), args.end()); + Trace("pfnu-debug2") << "Process new scope with " << args << std::endl; + // Process in new call separately + processInternal(cur, nfa, traversing); + continue; + } + const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren(); + // now, process children + for (const std::shared_ptr<ProofNode>& cp : ccp) + { + if (std::find(traversing.begin(), traversing.end(), cp) + != traversing.end()) + { + Unhandled() + << "ProofNodeUpdater::processInternal: cyclic proof! (use " + "--proof-eager-checking)" + << std::endl; + } + visit.push_back(cp); + } + } + else if (!it->second) + { + Assert(!traversing.empty()); + traversing.pop_back(); + visited[cur] = true; + // finalize the node + runFinalize(cur, fa, resCache); + } + } while (!visit.empty()); + Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl; +} + +bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur, + const std::vector<Node>& fa, + bool& continueUpdate) +{ + // should it be updated? + if (!d_cb.shouldUpdate(cur, fa, continueUpdate)) + { + return false; + } + PfRule id = cur->getRule(); + // use CDProof to open a scope for which the callback updates + CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", d_autoSym); + const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren(); + std::vector<Node> ccn; + for (const std::shared_ptr<ProofNode>& cp : cc) + { + Node cpres = cp->getResult(); + ccn.push_back(cpres); + // store in the proof + cpf.addProof(cp); + } + Node res = cur->getResult(); + Trace("pf-process-debug") + << "Updating (" << cur->getRule() << "): " << res << std::endl; + // only if the callback updated the node + if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate)) + { + std::shared_ptr<ProofNode> npn = cpf.getProofFor(res); + std::vector<Node> fullFa; + if (d_debugFreeAssumps) + { + expr::getFreeAssumptions(cur.get(), fullFa); + Trace("pfnu-debug") << "Original proof : " << *cur << std::endl; + } + // then, update the original proof node based on this one + Trace("pf-process-debug") << "Update node..." << std::endl; + d_pnm->updateNode(cur.get(), npn.get()); + Trace("pf-process-debug") << "...update node finished." << std::endl; + if (d_debugFreeAssumps) + { + fullFa.insert(fullFa.end(), fa.begin(), fa.end()); + // We have that npn is a node we occurring the final updated version of + // the proof. We can now debug based on the expected set of free + // assumptions. + Trace("pfnu-debug") << "Ensure update closed..." << std::endl; + pfnEnsureClosedWrt( + npn.get(), fullFa, "pfnu-debug", "ProofNodeUpdater:postupdate"); + } + Trace("pf-process-debug") << "..finished" << std::endl; + return true; + } + Trace("pf-process-debug") << "..finished" << std::endl; + return false; +} + +void ProofNodeUpdater::runFinalize( + std::shared_ptr<ProofNode> cur, + const std::vector<Node>& fa, + std::map<Node, std::shared_ptr<ProofNode>>& resCache) +{ + if (d_mergeSubproofs) + { + Node res = cur->getResult(); + // cache result if we are merging subproofs + resCache[res] = cur; + } + if (d_debugFreeAssumps) + { + // We have that npn is a node we occurring the final updated version of + // the proof. We can now debug based on the expected set of free + // assumptions. + Trace("pfnu-debug") << "Ensure update closed..." << std::endl; + pfnEnsureClosedWrt( + cur.get(), fa, "pfnu-debug", "ProofNodeUpdater:finalize"); + } +} + +void ProofNodeUpdater::setDebugFreeAssumptions( + const std::vector<Node>& freeAssumps) +{ + d_freeAssumps.clear(); + d_freeAssumps.insert( + d_freeAssumps.end(), freeAssumps.begin(), freeAssumps.end()); + d_debugFreeAssumps = true; +} + +} // namespace cvc5 diff --git a/src/proof/proof_node_updater.h b/src/proof/proof_node_updater.h new file mode 100644 index 000000000..6b8841e67 --- /dev/null +++ b/src/proof/proof_node_updater.h @@ -0,0 +1,164 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * A utility for updating proof nodes. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_NODE_UPDATER_H +#define CVC5__PROOF__PROOF_NODE_UPDATER_H + +#include <map> +#include <memory> + +#include "expr/node.h" +#include "proof/proof_node.h" + +namespace cvc5 { + +class CDProof; +class ProofNode; +class ProofNodeManager; + +/** + * A virtual callback class for updating ProofNode. An example use case of this + * class is to eliminate a proof rule by expansion. + */ +class ProofNodeUpdaterCallback +{ + public: + ProofNodeUpdaterCallback(); + virtual ~ProofNodeUpdaterCallback(); + /** Should proof pn be updated? + * + * @param pn the proof node that maybe should be updated + * @param fa the assumptions in scope + * @param continueUpdate whether we should continue recursively updating pn + * @return whether we should run the update method on pn + */ + virtual bool shouldUpdate(std::shared_ptr<ProofNode> pn, + const std::vector<Node>& fa, + bool& continueUpdate) = 0; + /** + * Update the proof rule application, store steps in cdp. Return true if + * the proof changed. It can be assumed that cdp contains proofs of each + * fact in children. + * + * If continueUpdate is set to false in this method, then the resulting + * proof (the proof of res in cdp) is *not* called back to update by the + * proof node updater, nor are its children recursed. Otherwise, by default, + * the proof node updater will continue updating the resulting proof and will + * recursively update its children. This is analogous to marking REWRITE_DONE + * in a rewrite response. + */ + virtual bool update(Node res, + PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args, + CDProof* cdp, + bool& continueUpdate); +}; + +/** + * A generic class for updating ProofNode. It is parameterized by a callback + * class. Its process method runs this callback on all subproofs of a provided + * ProofNode application that meet some criteria + * (ProofNodeUpdaterCallback::shouldUpdate) + * and overwrites them based on the update procedure of the callback + * (ProofNodeUpdaterCallback::update), which uses local CDProof objects that + * should be filled in the callback for each ProofNode to update. This update + * process is applied in a *pre-order* traversal. + */ +class ProofNodeUpdater +{ + public: + /** + * @param pnm The proof node manager we are using + * @param cb The callback to apply to each node + * @param mergeSubproofs Whether to automatically merge subproofs within + * the same SCOPE that prove the same fact. + * @param autoSym Whether intermediate CDProof objects passed to updater + * callbacks automatically introduce SYMM steps. + */ + ProofNodeUpdater(ProofNodeManager* pnm, + ProofNodeUpdaterCallback& cb, + bool mergeSubproofs = false, + bool autoSym = true); + /** + * Post-process, which performs the main post-processing technique described + * above. + */ + void process(std::shared_ptr<ProofNode> pf); + + /** + * Set free assumptions to freeAssumps. This indicates that we expect + * the proof we are processing to have free assumptions that are in + * freeAssumps. This enables checking when this is violated, which is + * expensive in general. It is not recommended that this method is called + * by default. + */ + void setDebugFreeAssumptions(const std::vector<Node>& freeAssumps); + + private: + /** The proof node manager */ + ProofNodeManager* d_pnm; + /** The callback */ + ProofNodeUpdaterCallback& d_cb; + /** + * Post-process, which performs the main post-processing technique described + * above. + * + * @param pf The proof to process + * @param fa The assumptions of the scope that fa is a subproof of with + * respect to the original proof. For example, if (SCOPE P :args (A B)), we + * may call this method on P with fa = { A, B }. + * @param traversing The list of proof nodes we are currently traversing + * beneath. This is used for checking for cycles in the overall proof. + */ + void processInternal(std::shared_ptr<ProofNode> pf, + const std::vector<Node>& fa, + std::vector<std::shared_ptr<ProofNode>>& traversing); + /** + * Update proof node cur based on the callback. This modifies curr using + * ProofNodeManager::updateNode based on the proof node constructed to + * replace it by the callback. Return true if cur was updated. If + * continueUpdate is updated to false, then cur is not updated further + * and its children are not traversed. + */ + bool runUpdate(std::shared_ptr<ProofNode> cur, + const std::vector<Node>& fa, + bool& continueUpdate); + /** + * Finalize the node cur. This is called at the moment that it is established + * that cur will appear in the final proof. We do any final debug checking + * and add it to the results cache resCache if we are merging subproofs. + */ + void runFinalize(std::shared_ptr<ProofNode> cur, + const std::vector<Node>& fa, + std::map<Node, std::shared_ptr<ProofNode>>& resCache); + /** Are we debugging free assumptions? */ + bool d_debugFreeAssumps; + /** The initial free assumptions */ + std::vector<Node> d_freeAssumps; + /** Whether we are merging subproofs */ + bool d_mergeSubproofs; + /** + * Whether intermediate CDProof objects passed to updater callbacks + * automatically introduce SYMM steps. + */ + bool d_autoSym; +}; + +} // namespace cvc5 + +#endif diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp new file mode 100644 index 000000000..0cefe1209 --- /dev/null +++ b/src/proof/proof_rule.cpp @@ -0,0 +1,258 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, Gereon Kremer + * + * 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 proof rule. + */ + +#include "proof/proof_rule.h" + +#include <iostream> + +namespace cvc5 { + +const char* toString(PfRule id) +{ + switch (id) + { + //================================================= Core rules + case PfRule::ASSUME: return "ASSUME"; + case PfRule::SCOPE: return "SCOPE"; + case PfRule::SUBS: return "SUBS"; + case PfRule::REWRITE: return "REWRITE"; + case PfRule::EVALUATE: return "EVALUATE"; + case PfRule::MACRO_SR_EQ_INTRO: return "MACRO_SR_EQ_INTRO"; + case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO"; + case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM"; + case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM"; + case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM"; + //================================================= Trusted rules + case PfRule::THEORY_LEMMA: return "THEORY_LEMMA"; + case PfRule::THEORY_REWRITE: return "THEORY_REWRITE"; + case PfRule::PREPROCESS: return "PREPROCESS"; + case PfRule::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA"; + case PfRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS"; + case PfRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA"; + case PfRule::THEORY_EXPAND_DEF: return "THEORY_EXPAND_DEF"; + case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM"; + case PfRule::TRUST_REWRITE: return "TRUST_REWRITE"; + case PfRule::TRUST_SUBS: return "TRUST_SUBS"; + case PfRule::TRUST_SUBS_MAP: return "TRUST_SUBS_MAP"; + //================================================= Boolean rules + case PfRule::RESOLUTION: return "RESOLUTION"; + case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION"; + case PfRule::FACTORING: return "FACTORING"; + case PfRule::REORDERING: return "REORDERING"; + case PfRule::MACRO_RESOLUTION: return "MACRO_RESOLUTION"; + case PfRule::MACRO_RESOLUTION_TRUST: return "MACRO_RESOLUTION_TRUST"; + case PfRule::SPLIT: return "SPLIT"; + case PfRule::EQ_RESOLVE: return "EQ_RESOLVE"; + case PfRule::MODUS_PONENS: return "MODUS_PONENS"; + case PfRule::NOT_NOT_ELIM: return "NOT_NOT_ELIM"; + case PfRule::CONTRA: return "CONTRA"; + case PfRule::AND_ELIM: return "AND_ELIM"; + case PfRule::AND_INTRO: return "AND_INTRO"; + case PfRule::NOT_OR_ELIM: return "NOT_OR_ELIM"; + case PfRule::IMPLIES_ELIM: return "IMPLIES_ELIM"; + case PfRule::NOT_IMPLIES_ELIM1: return "NOT_IMPLIES_ELIM1"; + case PfRule::NOT_IMPLIES_ELIM2: return "NOT_IMPLIES_ELIM2"; + case PfRule::EQUIV_ELIM1: return "EQUIV_ELIM1"; + case PfRule::EQUIV_ELIM2: return "EQUIV_ELIM2"; + case PfRule::NOT_EQUIV_ELIM1: return "NOT_EQUIV_ELIM1"; + case PfRule::NOT_EQUIV_ELIM2: return "NOT_EQUIV_ELIM2"; + case PfRule::XOR_ELIM1: return "XOR_ELIM1"; + case PfRule::XOR_ELIM2: return "XOR_ELIM2"; + case PfRule::NOT_XOR_ELIM1: return "NOT_XOR_ELIM1"; + case PfRule::NOT_XOR_ELIM2: return "NOT_XOR_ELIM2"; + case PfRule::ITE_ELIM1: return "ITE_ELIM1"; + case PfRule::ITE_ELIM2: return "ITE_ELIM2"; + case PfRule::NOT_ITE_ELIM1: return "NOT_ITE_ELIM1"; + case PfRule::NOT_ITE_ELIM2: return "NOT_ITE_ELIM2"; + //================================================= De Morgan rules + case PfRule::NOT_AND: return "NOT_AND"; + //================================================= CNF rules + case PfRule::CNF_AND_POS: return "CNF_AND_POS"; + case PfRule::CNF_AND_NEG: return "CNF_AND_NEG"; + case PfRule::CNF_OR_POS: return "CNF_OR_POS"; + case PfRule::CNF_OR_NEG: return "CNF_OR_NEG"; + case PfRule::CNF_IMPLIES_POS: return "CNF_IMPLIES_POS"; + case PfRule::CNF_IMPLIES_NEG1: return "CNF_IMPLIES_NEG1"; + case PfRule::CNF_IMPLIES_NEG2: return "CNF_IMPLIES_NEG2"; + case PfRule::CNF_EQUIV_POS1: return "CNF_EQUIV_POS1"; + case PfRule::CNF_EQUIV_POS2: return "CNF_EQUIV_POS2"; + case PfRule::CNF_EQUIV_NEG1: return "CNF_EQUIV_NEG1"; + case PfRule::CNF_EQUIV_NEG2: return "CNF_EQUIV_NEG2"; + case PfRule::CNF_XOR_POS1: return "CNF_XOR_POS1"; + case PfRule::CNF_XOR_POS2: return "CNF_XOR_POS2"; + case PfRule::CNF_XOR_NEG1: return "CNF_XOR_NEG1"; + case PfRule::CNF_XOR_NEG2: return "CNF_XOR_NEG2"; + case PfRule::CNF_ITE_POS1: return "CNF_ITE_POS1"; + case PfRule::CNF_ITE_POS2: return "CNF_ITE_POS2"; + case PfRule::CNF_ITE_POS3: return "CNF_ITE_POS3"; + case PfRule::CNF_ITE_NEG1: return "CNF_ITE_NEG1"; + case PfRule::CNF_ITE_NEG2: return "CNF_ITE_NEG2"; + case PfRule::CNF_ITE_NEG3: return "CNF_ITE_NEG3"; + //================================================= Equality rules + case PfRule::REFL: return "REFL"; + case PfRule::SYMM: return "SYMM"; + case PfRule::TRANS: return "TRANS"; + case PfRule::CONG: return "CONG"; + case PfRule::TRUE_INTRO: return "TRUE_INTRO"; + case PfRule::TRUE_ELIM: return "TRUE_ELIM"; + case PfRule::FALSE_INTRO: return "FALSE_INTRO"; + case PfRule::FALSE_ELIM: return "FALSE_ELIM"; + case PfRule::HO_APP_ENCODE: return "HO_APP_ENCODE"; + case PfRule::HO_CONG: return "HO_CONG"; + //================================================= Array rules + case PfRule::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE"; + case PfRule::ARRAYS_READ_OVER_WRITE_CONTRA: + return "ARRAYS_READ_OVER_WRITE_CONTRA"; + case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1"; + case PfRule::ARRAYS_EXT: return "ARRAYS_EXT"; + case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST"; + //================================================= Bit-Vector rules + case PfRule::BV_BITBLAST: return "BV_BITBLAST"; + case PfRule::BV_BITBLAST_CONST: return "BV_BITBLAST_CONST"; + case PfRule::BV_BITBLAST_VAR: return "BV_BITBLAST_VAR"; + case PfRule::BV_BITBLAST_EQUAL: return "BV_BITBLAST_EQUAL"; + case PfRule::BV_BITBLAST_ULT: return "BV_BITBLAST_ULT"; + case PfRule::BV_BITBLAST_ULE: return "BV_BITBLAST_ULE"; + case PfRule::BV_BITBLAST_UGT: return "BV_BITBLAST_UGT"; + case PfRule::BV_BITBLAST_UGE: return "BV_BITBLAST_UGE"; + case PfRule::BV_BITBLAST_SLT: return "BV_BITBLAST_SLT"; + case PfRule::BV_BITBLAST_SLE: return "BV_BITBLAST_SLE"; + case PfRule::BV_BITBLAST_SGT: return "BV_BITBLAST_SGT"; + case PfRule::BV_BITBLAST_SGE: return "BV_BITBLAST_SGE"; + case PfRule::BV_BITBLAST_NOT: return "BV_BITBLAST_NOT"; + case PfRule::BV_BITBLAST_CONCAT: return "BV_BITBLAST_CONCAT"; + case PfRule::BV_BITBLAST_AND: return "BV_BITBLAST_AND"; + case PfRule::BV_BITBLAST_OR: return "BV_BITBLAST_OR"; + case PfRule::BV_BITBLAST_XOR: return "BV_BITBLAST_XOR"; + case PfRule::BV_BITBLAST_XNOR: return "BV_BITBLAST_XNOR"; + case PfRule::BV_BITBLAST_NAND: return "BV_BITBLAST_NAND"; + case PfRule::BV_BITBLAST_NOR: return "BV_BITBLAST_NOR"; + case PfRule::BV_BITBLAST_COMP: return "BV_BITBLAST_COMP"; + case PfRule::BV_BITBLAST_MULT: return "BV_BITBLAST_MULT"; + case PfRule::BV_BITBLAST_ADD: return "BV_BITBLAST_ADD"; + case PfRule::BV_BITBLAST_SUB: return "BV_BITBLAST_SUB"; + case PfRule::BV_BITBLAST_NEG: return "BV_BITBLAST_NEG"; + case PfRule::BV_BITBLAST_UDIV: return "BV_BITBLAST_UDIV"; + case PfRule::BV_BITBLAST_UREM: return "BV_BITBLAST_UREM"; + case PfRule::BV_BITBLAST_SDIV: return "BV_BITBLAST_SDIV"; + case PfRule::BV_BITBLAST_SREM: return "BV_BITBLAST_SREM"; + case PfRule::BV_BITBLAST_SMOD: return "BV_BITBLAST_SMOD"; + case PfRule::BV_BITBLAST_SHL: return "BV_BITBLAST_SHL"; + case PfRule::BV_BITBLAST_LSHR: return "BV_BITBLAST_LSHR"; + case PfRule::BV_BITBLAST_ASHR: return "BV_BITBLAST_ASHR"; + case PfRule::BV_BITBLAST_ULTBV: return "BV_BITBLAST_ULTBV"; + case PfRule::BV_BITBLAST_SLTBV: return "BV_BITBLAST_SLTBV"; + case PfRule::BV_BITBLAST_ITE: return "BV_BITBLAST_ITE"; + case PfRule::BV_BITBLAST_EXTRACT: return "BV_BITBLAST_EXTRACT"; + case PfRule::BV_BITBLAST_REPEAT: return "BV_BITBLAST_REPEAT"; + case PfRule::BV_BITBLAST_ZERO_EXTEND: return "BV_BITBLAST_ZERO_EXTEND"; + case PfRule::BV_BITBLAST_SIGN_EXTEND: return "BV_BITBLAST_SIGN_EXTEND"; + case PfRule::BV_BITBLAST_ROTATE_RIGHT: return "BV_BITBLAST_ROTATE_RIGHT"; + case PfRule::BV_BITBLAST_ROTATE_LEFT: return "BV_BITBLAST_ROTATE_LEFT"; + case PfRule::BV_EAGER_ATOM: return "BV_EAGER_ATOM"; + //================================================= Datatype rules + case PfRule::DT_UNIF: return "DT_UNIF"; + case PfRule::DT_INST: return "DT_INST"; + case PfRule::DT_COLLAPSE: return "DT_COLLAPSE"; + case PfRule::DT_SPLIT: return "DT_SPLIT"; + case PfRule::DT_CLASH: return "DT_CLASH"; + case PfRule::DT_TRUST: return "DT_TRUST"; + //================================================= Quantifiers rules + case PfRule::SKOLEM_INTRO: return "SKOLEM_INTRO"; + case PfRule::EXISTS_INTRO: return "EXISTS_INTRO"; + case PfRule::SKOLEMIZE: return "SKOLEMIZE"; + case PfRule::INSTANTIATE: return "INSTANTIATE"; + //================================================= String rules + case PfRule::CONCAT_EQ: return "CONCAT_EQ"; + case PfRule::CONCAT_UNIFY: return "CONCAT_UNIFY"; + case PfRule::CONCAT_CONFLICT: return "CONCAT_CONFLICT"; + case PfRule::CONCAT_SPLIT: return "CONCAT_SPLIT"; + case PfRule::CONCAT_CSPLIT: return "CONCAT_CSPLIT"; + case PfRule::CONCAT_LPROP: return "CONCAT_LPROP"; + case PfRule::CONCAT_CPROP: return "CONCAT_CPROP"; + case PfRule::STRING_DECOMPOSE: return "STRING_DECOMPOSE"; + case PfRule::STRING_LENGTH_POS: return "STRING_LENGTH_POS"; + case PfRule::STRING_LENGTH_NON_EMPTY: return "STRING_LENGTH_NON_EMPTY"; + case PfRule::STRING_REDUCTION: return "STRING_REDUCTION"; + case PfRule::STRING_EAGER_REDUCTION: return "STRING_EAGER_REDUCTION"; + case PfRule::RE_INTER: return "RE_INTER"; + case PfRule::RE_UNFOLD_POS: return "RE_UNFOLD_POS"; + case PfRule::RE_UNFOLD_NEG: return "RE_UNFOLD_NEG"; + case PfRule::RE_UNFOLD_NEG_CONCAT_FIXED: + return "RE_UNFOLD_NEG_CONCAT_FIXED"; + case PfRule::RE_ELIM: return "RE_ELIM"; + case PfRule::STRING_CODE_INJ: return "STRING_CODE_INJ"; + case PfRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ"; + case PfRule::STRING_TRUST: return "STRING_TRUST"; + //================================================= Arith rules + case PfRule::MACRO_ARITH_SCALE_SUM_UB: + return "ARITH_SCALE_SUM_UPPER_BOUNDS"; + case PfRule::ARITH_SUM_UB: return "ARITH_SUM_UB"; + case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY"; + case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB"; + case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB"; + case PfRule::INT_TRUST: return "INT_TRUST"; + case PfRule::ARITH_MULT_SIGN: return "ARITH_MULT_SIGN"; + case PfRule::ARITH_MULT_POS: return "ARITH_MULT_POS"; + case PfRule::ARITH_MULT_NEG: return "ARITH_MULT_NEG"; + case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT"; + case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM"; + case PfRule::ARITH_TRANS_PI: return "ARITH_TRANS_PI"; + case PfRule::ARITH_TRANS_EXP_NEG: return "ARITH_TRANS_EXP_NEG"; + case PfRule::ARITH_TRANS_EXP_POSITIVITY: + return "ARITH_TRANS_EXP_POSITIVITY"; + case PfRule::ARITH_TRANS_EXP_SUPER_LIN: return "ARITH_TRANS_EXP_SUPER_LIN"; + case PfRule::ARITH_TRANS_EXP_ZERO: return "ARITH_TRANS_EXP_ZERO"; + case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG: + return "ARITH_TRANS_EXP_APPROX_ABOVE_NEG"; + case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS: + return "ARITH_TRANS_EXP_APPROX_ABOVE_POS"; + case PfRule::ARITH_TRANS_EXP_APPROX_BELOW: + return "ARITH_TRANS_EXP_APPROX_BELOW"; + case PfRule::ARITH_TRANS_SINE_BOUNDS: return "ARITH_TRANS_SINE_BOUNDS"; + case PfRule::ARITH_TRANS_SINE_SHIFT: return "ARITH_TRANS_SINE_SHIFT"; + case PfRule::ARITH_TRANS_SINE_SYMMETRY: return "ARITH_TRANS_SINE_SYMMETRY"; + case PfRule::ARITH_TRANS_SINE_TANGENT_ZERO: + return "ARITH_TRANS_SINE_TANGENT_ZERO"; + case PfRule::ARITH_TRANS_SINE_TANGENT_PI: + return "ARITH_TRANS_SINE_TANGENT_PI"; + case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG: + return "ARITH_TRANS_SINE_APPROX_ABOVE_NEG"; + case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS: + return "ARITH_TRANS_SINE_APPROX_ABOVE_POS"; + case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG: + return "ARITH_TRANS_SINE_APPROX_BELOW_NEG"; + case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS: + return "ARITH_TRANS_SINE_APPROX_BELOW_POS"; + case PfRule::ARITH_NL_CAD_DIRECT: return "ARITH_NL_CAD_DIRECT"; + case PfRule::ARITH_NL_CAD_RECURSIVE: return "ARITH_NL_CAD_RECURSIVE"; + //================================================= Unknown rule + case PfRule::UNKNOWN: return "UNKNOWN"; + default: return "?"; + } +} + +std::ostream& operator<<(std::ostream& out, PfRule id) +{ + out << toString(id); + return out; +} + +size_t PfRuleHashFunction::operator()(PfRule id) const +{ + return static_cast<size_t>(id); +} + +} // namespace cvc5 diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h new file mode 100644 index 000000000..107285cc3 --- /dev/null +++ b/src/proof/proof_rule.h @@ -0,0 +1,1453 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Proof rule enumeration. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_RULE_H +#define CVC5__PROOF__PROOF_RULE_H + +#include <iosfwd> + +namespace cvc5 { + +/** + * An enumeration for proof rules. This enumeration is analogous to Kind for + * Node objects. In the documentation below, P:F denotes a ProofNode that + * proves formula F. + * + * Conceptually, the following proof rules form a calculus whose target + * user is the Node-level theory solvers. This means that the rules below + * are designed to reason about, among other things, common operations on Node + * objects like Rewriter::rewrite or Node::substitute. It is intended to be + * translated or printed in other formats. + * + * The following PfRule values include core rules and those categorized by + * theory, including the theory of equality. + * + * The "core rules" include two distinguished rules which have special status: + * (1) ASSUME, which represents an open leaf in a proof. + * (2) SCOPE, which closes the scope of assumptions. + * The core rules additionally correspond to generic operations that are done + * internally on nodes, e.g. calling Rewriter::rewrite. + * + * Rules with prefix MACRO_ are those that can be defined in terms of other + * rules. These exist for convienience. We provide their definition in the line + * "Macro:". + */ +enum class PfRule : uint32_t +{ + //================================================= Core rules + //======================== Assume and Scope + // ======== Assumption (a leaf) + // Children: none + // Arguments: (F) + // -------------- + // Conclusion: F + // + // This rule has special status, in that an application of assume is an + // open leaf in a proof that is not (yet) justified. An assume leaf is + // analogous to a free variable in a term, where we say "F is a free + // assumption in proof P" if it contains an application of F that is not + // bound by SCOPE (see below). + ASSUME, + // ======== Scope (a binder for assumptions) + // Children: (P:F) + // Arguments: (F1, ..., Fn) + // -------------- + // Conclusion: (=> (and F1 ... Fn) F) or (not (and F1 ... Fn)) if F is false + // + // This rule has a dual purpose with ASSUME. It is a way to close + // assumptions in a proof. We require that F1 ... Fn are free assumptions in + // P and say that F1, ..., Fn are not free in (SCOPE P). In other words, they + // are bound by this application. For example, the proof node: + // (SCOPE (ASSUME F) :args F) + // has the conclusion (=> F F) and has no free assumptions. More generally, a + // proof with no free assumptions always concludes a valid formula. + SCOPE, + + //======================== Builtin theory (common node operations) + // ======== Substitution + // Children: (P1:F1, ..., Pn:Fn) + // Arguments: (t, (ids)?) + // --------------------------------------------------------------- + // Conclusion: (= t t*sigma{ids}(Fn)*...*sigma{ids}(F1)) + // where sigma{ids}(Fi) are substitutions, which notice are applied in + // reverse order. + // Notice that ids is a MethodId identifier, which determines how to convert + // the formulas F1, ..., Fn into substitutions. + SUBS, + // ======== Rewrite + // Children: none + // Arguments: (t, (idr)?) + // ---------------------------------------- + // Conclusion: (= t Rewriter{idr}(t)) + // where idr is a MethodId identifier, which determines the kind of rewriter + // to apply, e.g. Rewriter::rewrite. + REWRITE, + // ======== Evaluate + // Children: none + // Arguments: (t) + // ---------------------------------------- + // Conclusion: (= t Evaluator::evaluate(t)) + // Note this is equivalent to: + // (REWRITE t MethodId::RW_EVALUATE) + EVALUATE, + // ======== Substitution + Rewriting equality introduction + // + // In this rule, we provide a term t and conclude that it is equal to its + // rewritten form under a (proven) substitution. + // + // Children: (P1:F1, ..., Pn:Fn) + // Arguments: (t, (ids (ida (idr)?)?)?) + // --------------------------------------------------------------- + // Conclusion: (= t t') + // where + // t' is + // Rewriter{idr}(t*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)) + // + // In other words, from the point of view of Skolem forms, this rule + // transforms t to t' by standard substitution + rewriting. + // + // The arguments ids, ida and idr are optional and specify the identifier of + // the substitution, the substitution application and rewriter respectively to + // be used. For details, see theory/builtin/proof_checker.h. + MACRO_SR_EQ_INTRO, + // ======== Substitution + Rewriting predicate introduction + // + // In this rule, we provide a formula F and conclude it, under the condition + // that it rewrites to true under a proven substitution. + // + // Children: (P1:F1, ..., Pn:Fn) + // Arguments: (F, (ids (ida (idr)?)?)?) + // --------------------------------------------------------------- + // Conclusion: F + // where + // Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)) == true + // where ids and idr are method identifiers. + // + // More generally, this rule also holds when: + // Rewriter::rewrite(toOriginal(F')) == true + // where F' is the result of the left hand side of the equality above. Here, + // notice that we apply rewriting on the original form of F', meaning that + // this rule may conclude an F whose Skolem form is justified by the + // definition of its (fresh) Skolem variables. For example, this rule may + // justify the conclusion (= k t) where k is the purification Skolem for t, + // e.g. where the original form of k is t. + // + // Furthermore, notice that the rewriting and substitution is applied only + // within the side condition, meaning the rewritten form of the original form + // of F does not escape this rule. + MACRO_SR_PRED_INTRO, + // ======== Substitution + Rewriting predicate elimination + // + // In this rule, if we have proven a formula F, then we may conclude its + // rewritten form under a proven substitution. + // + // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn) + // Arguments: ((ids (ida (idr)?)?)?) + // ---------------------------------------- + // Conclusion: F' + // where + // F' is + // Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)). + // where ids and idr are method identifiers. + // + // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO. + MACRO_SR_PRED_ELIM, + // ======== Substitution + Rewriting predicate transform + // + // In this rule, if we have proven a formula F, then we may provide a formula + // G and conclude it if F and G are equivalent after rewriting under a proven + // substitution. + // + // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn) + // Arguments: (G, (ids (ida (idr)?)?)?) + // ---------------------------------------- + // Conclusion: G + // where + // Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)) == + // Rewriter{idr}(G*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)) + // + // More generally, this rule also holds when: + // Rewriter::rewrite(toOriginal(F')) == Rewriter::rewrite(toOriginal(G')) + // where F' and G' are the result of each side of the equation above. Here, + // original forms are used in a similar manner to MACRO_SR_PRED_INTRO above. + MACRO_SR_PRED_TRANSFORM, + //================================================= Processing rules + // ======== Remove Term Formulas Axiom + // Children: none + // Arguments: (t) + // --------------------------------------------------------------- + // Conclusion: RemoveTermFormulas::getAxiomFor(t). + REMOVE_TERM_FORMULA_AXIOM, + + //================================================= Trusted rules + // ======== Theory lemma + // Children: none + // Arguments: (F, tid) + // --------------------------------------------------------------- + // Conclusion: F + // where F is a (T-valid) theory lemma generated by theory with TheoryId tid. + // This is a "coarse-grained" rule that is used as a placeholder if a theory + // did not provide a proof for a lemma or conflict. + THEORY_LEMMA, + // ======== Theory Rewrite + // Children: none + // Arguments: (F, tid, rid) + // ---------------------------------------- + // Conclusion: F + // where F is an equality of the form (= t t') where t' is obtained by + // applying the kind of rewriting given by the method identifier rid, which + // is one of: + // { RW_REWRITE_THEORY_PRE, RW_REWRITE_THEORY_POST, RW_REWRITE_EQ_EXT } + // Notice that the checker for this rule does not replay the rewrite to ensure + // correctness, since theory rewriter methods are not static. For example, + // the quantifiers rewriter involves constructing new bound variables that are + // not guaranteed to be consistent on each call. + THEORY_REWRITE, + // The remaining rules in this section have the signature of a "trusted rule": + // + // Children: none + // Arguments: (F) + // --------------------------------------------------------------- + // Conclusion: F + // + // where F is an equality of the form t = t' where t was replaced by t' + // based on some preprocessing pass, or otherwise F was added as a new + // assertion by some preprocessing pass. + PREPROCESS, + // where F was added as a new assertion by some preprocessing pass. + PREPROCESS_LEMMA, + // where F is an equality of the form t = Theory::ppRewrite(t) for some + // theory. Notice this is a "trusted" rule. + THEORY_PREPROCESS, + // where F was added as a new assertion by theory preprocessing. + THEORY_PREPROCESS_LEMMA, + // where F is an equality of the form t = t' where t was replaced by t' + // based on theory expand definitions. + THEORY_EXPAND_DEF, + // where F is an existential (exists ((x T)) (P x)) used for introducing + // a witness term (witness ((x T)) (P x)). + WITNESS_AXIOM, + // where F is an equality (= t t') that holds by a form of rewriting that + // could not be replayed during proof postprocessing. + TRUST_REWRITE, + // where F is an equality (= t t') that holds by a form of substitution that + // could not be replayed during proof postprocessing. + TRUST_SUBS, + // where F is an equality (= t t') that holds by a form of substitution that + // could not be determined by the TrustSubstitutionMap. + TRUST_SUBS_MAP, + // ========= SAT Refutation for assumption-based unsat cores + // Children: (P1, ..., Pn) + // Arguments: none + // --------------------- + // Conclusion: false + // Note: P1, ..., Pn correspond to the unsat core determined by the SAT + // solver. + SAT_REFUTATION, + + //================================================= Boolean rules + // ======== Resolution + // Children: + // (P1:C1, P2:C2) + // Arguments: (pol, L) + // --------------------- + // Conclusion: C + // where + // - C1 and C2 are nodes viewed as clauses, i.e., either an OR node with + // each children viewed as a literal or a node viewed as a literal. Note + // that an OR node could also be a literal. + // - pol is either true or false, representing the polarity of the pivot on + // the first clause + // - L is the pivot of the resolution, which occurs as is (resp. under a + // NOT) in C1 and negatively (as is) in C2 if pol = true (pol = false). + // C is a clause resulting from collecting all the literals in C1, minus the + // first occurrence of the pivot or its negation, and C2, minus the first + // occurrence of the pivot or its negation, according to the policy above. + // If the resulting clause has a single literal, that literal itself is the + // result; if it has no literals, then the result is false; otherwise it's + // an OR node of the resulting literals. + // + // Note that it may be the case that the pivot does not occur in the + // clauses. In this case the rule is not unsound, but it does not correspond + // to resolution but rather to a weakening of the clause that did not have a + // literal eliminated. + RESOLUTION, + // ======== N-ary Resolution + // Children: (P1:C_1, ..., Pm:C_n) + // Arguments: (pol_1, L_1, ..., pol_{n-1}, L_{n-1}) + // --------------------- + // Conclusion: C + // where + // - let C_1 ... C_n be nodes viewed as clauses, as defined above + // - let "C_1 <>_{L,pol} C_2" represent the resolution of C_1 with C_2 with + // pivot L and polarity pol, as defined above + // - let C_1' = C_1 (from P1), + // - for each i > 1, let C_i' = C_{i-1} <>_{L_{i-1}, pol_{i-1}} C_i' + // The result of the chain resolution is C = C_n' + CHAIN_RESOLUTION, + // ======== Factoring + // Children: (P:C1) + // Arguments: () + // --------------------- + // Conclusion: C2 + // where + // Set representations of C1 and C2 is the same and the number of literals in + // C2 is smaller than that of C1 + FACTORING, + // ======== Reordering + // Children: (P:C1) + // Arguments: (C2) + // --------------------- + // Conclusion: C2 + // where + // Set representations of C1 and C2 are the same and the number of literals + // in C2 is the same of that of C1 + REORDERING, + // ======== N-ary Resolution + Factoring + Reordering + // Children: (P1:C_1, ..., Pm:C_n) + // Arguments: (C, pol_1, L_1, ..., pol_{n-1}, L_{n-1}) + // --------------------- + // Conclusion: C + // where + // - let C_1 ... C_n be nodes viewed as clauses, as defined in RESOLUTION + // - let "C_1 <>_{L,pol} C_2" represent the resolution of C_1 with C_2 with + // pivot L and polarity pol, as defined in RESOLUTION + // - let C_1' be equal, in its set representation, to C_1 (from P1), + // - for each i > 1, let C_i' be equal, it its set representation, to + // C_{i-1} <>_{L_{i-1}, pol_{i-1}} C_i' + // The result of the chain resolution is C, which is equal, in its set + // representation, to C_n' + MACRO_RESOLUTION, + // As above but not checked + MACRO_RESOLUTION_TRUST, + + // ======== Split + // Children: none + // Arguments: (F) + // --------------------- + // Conclusion: (or F (not F)) + SPLIT, + // ======== Equality resolution + // Children: (P1:F1, P2:(= F1 F2)) + // Arguments: none + // --------------------- + // Conclusion: (F2) + // Note this can optionally be seen as a macro for EQUIV_ELIM1+RESOLUTION. + EQ_RESOLVE, + // ======== Modus ponens + // Children: (P1:F1, P2:(=> F1 F2)) + // Arguments: none + // --------------------- + // Conclusion: (F2) + // Note this can optionally be seen as a macro for IMPLIES_ELIM+RESOLUTION. + MODUS_PONENS, + // ======== Double negation elimination + // Children: (P:(not (not F))) + // Arguments: none + // --------------------- + // Conclusion: (F) + NOT_NOT_ELIM, + // ======== Contradiction + // Children: (P1:F P2:(not F)) + // Arguments: () + // --------------------- + // Conclusion: false + CONTRA, + // ======== And elimination + // Children: (P:(and F1 ... Fn)) + // Arguments: (i) + // --------------------- + // Conclusion: (Fi) + AND_ELIM, + // ======== And introduction + // Children: (P1:F1 ... Pn:Fn)) + // Arguments: () + // --------------------- + // Conclusion: (and P1 ... Pn) + AND_INTRO, + // ======== Not Or elimination + // Children: (P:(not (or F1 ... Fn))) + // Arguments: (i) + // --------------------- + // Conclusion: (not Fi) + NOT_OR_ELIM, + // ======== Implication elimination + // Children: (P:(=> F1 F2)) + // Arguments: () + // --------------------- + // Conclusion: (or (not F1) F2) + IMPLIES_ELIM, + // ======== Not Implication elimination version 1 + // Children: (P:(not (=> F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (F1) + NOT_IMPLIES_ELIM1, + // ======== Not Implication elimination version 2 + // Children: (P:(not (=> F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (not F2) + NOT_IMPLIES_ELIM2, + // ======== Equivalence elimination version 1 + // Children: (P:(= F1 F2)) + // Arguments: () + // --------------------- + // Conclusion: (or (not F1) F2) + EQUIV_ELIM1, + // ======== Equivalence elimination version 2 + // Children: (P:(= F1 F2)) + // Arguments: () + // --------------------- + // Conclusion: (or F1 (not F2)) + EQUIV_ELIM2, + // ======== Not Equivalence elimination version 1 + // Children: (P:(not (= F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (or F1 F2) + NOT_EQUIV_ELIM1, + // ======== Not Equivalence elimination version 2 + // Children: (P:(not (= F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (or (not F1) (not F2)) + NOT_EQUIV_ELIM2, + // ======== XOR elimination version 1 + // Children: (P:(xor F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (or F1 F2) + XOR_ELIM1, + // ======== XOR elimination version 2 + // Children: (P:(xor F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (or (not F1) (not F2)) + XOR_ELIM2, + // ======== Not XOR elimination version 1 + // Children: (P:(not (xor F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (or F1 (not F2)) + NOT_XOR_ELIM1, + // ======== Not XOR elimination version 2 + // Children: (P:(not (xor F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (or (not F1) F2) + NOT_XOR_ELIM2, + // ======== ITE elimination version 1 + // Children: (P:(ite C F1 F2)) + // Arguments: () + // --------------------- + // Conclusion: (or (not C) F1) + ITE_ELIM1, + // ======== ITE elimination version 2 + // Children: (P:(ite C F1 F2)) + // Arguments: () + // --------------------- + // Conclusion: (or C F2) + ITE_ELIM2, + // ======== Not ITE elimination version 1 + // Children: (P:(not (ite C F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (or (not C) (not F1)) + NOT_ITE_ELIM1, + // ======== Not ITE elimination version 1 + // Children: (P:(not (ite C F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (or C (not F2)) + NOT_ITE_ELIM2, + + //================================================= De Morgan rules + // ======== Not And + // Children: (P:(not (and F1 ... Fn)) + // Arguments: () + // --------------------- + // Conclusion: (or (not F1) ... (not Fn)) + NOT_AND, + //================================================= CNF rules + // ======== CNF And Pos + // Children: () + // Arguments: ((and F1 ... Fn), i) + // --------------------- + // Conclusion: (or (not (and F1 ... Fn)) Fi) + CNF_AND_POS, + // ======== CNF And Neg + // Children: () + // Arguments: ((and F1 ... Fn)) + // --------------------- + // Conclusion: (or (and F1 ... Fn) (not F1) ... (not Fn)) + CNF_AND_NEG, + // ======== CNF Or Pos + // Children: () + // Arguments: ((or F1 ... Fn)) + // --------------------- + // Conclusion: (or (not (or F1 ... Fn)) F1 ... Fn) + CNF_OR_POS, + // ======== CNF Or Neg + // Children: () + // Arguments: ((or F1 ... Fn), i) + // --------------------- + // Conclusion: (or (or F1 ... Fn) (not Fi)) + CNF_OR_NEG, + // ======== CNF Implies Pos + // Children: () + // Arguments: ((implies F1 F2)) + // --------------------- + // Conclusion: (or (not (implies F1 F2)) (not F1) F2) + CNF_IMPLIES_POS, + // ======== CNF Implies Neg version 1 + // Children: () + // Arguments: ((implies F1 F2)) + // --------------------- + // Conclusion: (or (implies F1 F2) F1) + CNF_IMPLIES_NEG1, + // ======== CNF Implies Neg version 2 + // Children: () + // Arguments: ((implies F1 F2)) + // --------------------- + // Conclusion: (or (implies F1 F2) (not F2)) + CNF_IMPLIES_NEG2, + // ======== CNF Equiv Pos version 1 + // Children: () + // Arguments: ((= F1 F2)) + // --------------------- + // Conclusion: (or (not (= F1 F2)) (not F1) F2) + CNF_EQUIV_POS1, + // ======== CNF Equiv Pos version 2 + // Children: () + // Arguments: ((= F1 F2)) + // --------------------- + // Conclusion: (or (not (= F1 F2)) F1 (not F2)) + CNF_EQUIV_POS2, + // ======== CNF Equiv Neg version 1 + // Children: () + // Arguments: ((= F1 F2)) + // --------------------- + // Conclusion: (or (= F1 F2) F1 F2) + CNF_EQUIV_NEG1, + // ======== CNF Equiv Neg version 2 + // Children: () + // Arguments: ((= F1 F2)) + // --------------------- + // Conclusion: (or (= F1 F2) (not F1) (not F2)) + CNF_EQUIV_NEG2, + // ======== CNF Xor Pos version 1 + // Children: () + // Arguments: ((xor F1 F2)) + // --------------------- + // Conclusion: (or (not (xor F1 F2)) F1 F2) + CNF_XOR_POS1, + // ======== CNF Xor Pos version 2 + // Children: () + // Arguments: ((xor F1 F2)) + // --------------------- + // Conclusion: (or (not (xor F1 F2)) (not F1) (not F2)) + CNF_XOR_POS2, + // ======== CNF Xor Neg version 1 + // Children: () + // Arguments: ((xor F1 F2)) + // --------------------- + // Conclusion: (or (xor F1 F2) (not F1) F2) + CNF_XOR_NEG1, + // ======== CNF Xor Neg version 2 + // Children: () + // Arguments: ((xor F1 F2)) + // --------------------- + // Conclusion: (or (xor F1 F2) F1 (not F2)) + CNF_XOR_NEG2, + // ======== CNF ITE Pos version 1 + // Children: () + // Arguments: ((ite C F1 F2)) + // --------------------- + // Conclusion: (or (not (ite C F1 F2)) (not C) F1) + CNF_ITE_POS1, + // ======== CNF ITE Pos version 2 + // Children: () + // Arguments: ((ite C F1 F2)) + // --------------------- + // Conclusion: (or (not (ite C F1 F2)) C F2) + CNF_ITE_POS2, + // ======== CNF ITE Pos version 3 + // Children: () + // Arguments: ((ite C F1 F2)) + // --------------------- + // Conclusion: (or (not (ite C F1 F2)) F1 F2) + CNF_ITE_POS3, + // ======== CNF ITE Neg version 1 + // Children: () + // Arguments: ((ite C F1 F2)) + // --------------------- + // Conclusion: (or (ite C F1 F2) (not C) (not F1)) + CNF_ITE_NEG1, + // ======== CNF ITE Neg version 2 + // Children: () + // Arguments: ((ite C F1 F2)) + // --------------------- + // Conclusion: (or (ite C F1 F2) C (not F2)) + CNF_ITE_NEG2, + // ======== CNF ITE Neg version 3 + // Children: () + // Arguments: ((ite C F1 F2)) + // --------------------- + // Conclusion: (or (ite C F1 F2) (not F1) (not F2)) + CNF_ITE_NEG3, + + //================================================= Equality rules + // ======== Reflexive + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (= t t) + REFL, + // ======== Symmetric + // Children: (P:(= t1 t2)) or (P:(not (= t1 t2))) + // Arguments: none + // ----------------------- + // Conclusion: (= t2 t1) or (not (= t2 t1)) + SYMM, + // ======== Transitivity + // Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn)) + // Arguments: none + // ----------------------- + // Conclusion: (= t1 tn) + TRANS, + // ======== Congruence + // Children: (P1:(= t1 s1), ..., Pn:(= tn sn)) + // Arguments: (<kind> f?) + // --------------------------------------------- + // Conclusion: (= (<kind> f? t1 ... tn) (<kind> f? s1 ... sn)) + // Notice that f must be provided iff <kind> is a parameterized kind, e.g. + // APPLY_UF. The actual node for <kind> is constructible via + // ProofRuleChecker::mkKindNode. + CONG, + // ======== True intro + // Children: (P:F) + // Arguments: none + // ---------------------------------------- + // Conclusion: (= F true) + TRUE_INTRO, + // ======== True elim + // Children: (P:(= F true)) + // Arguments: none + // ---------------------------------------- + // Conclusion: F + TRUE_ELIM, + // ======== False intro + // Children: (P:(not F)) + // Arguments: none + // ---------------------------------------- + // Conclusion: (= F false) + FALSE_INTRO, + // ======== False elim + // Children: (P:(= F false)) + // Arguments: none + // ---------------------------------------- + // Conclusion: (not F) + FALSE_ELIM, + // ======== HO trust + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (= t TheoryUfRewriter::getHoApplyForApplyUf(t)) + // For example, this rule concludes (f x y) = (HO_APPLY (HO_APPLY f x) y) + HO_APP_ENCODE, + // ======== Congruence + // Children: (P1:(= f g), P2:(= t1 s1), ..., Pn+1:(= tn sn)) + // Arguments: () + // --------------------------------------------- + // Conclusion: (= (f t1 ... tn) (g s1 ... sn)) + // Notice that this rule is only used when the application kinds are APPLY_UF. + HO_CONG, + + //================================================= Array rules + // ======== Read over write + // Children: (P:(not (= i1 i2))) + // Arguments: ((select (store a i2 e) i1)) + // ---------------------------------------- + // Conclusion: (= (select (store a i2 e) i1) (select a i1)) + ARRAYS_READ_OVER_WRITE, + // ======== Read over write, contrapositive + // Children: (P:(not (= (select (store a i2 e) i1) (select a i1))) + // Arguments: none + // ---------------------------------------- + // Conclusion: (= i1 i2) + ARRAYS_READ_OVER_WRITE_CONTRA, + // ======== Read over write 1 + // Children: none + // Arguments: ((select (store a i e) i)) + // ---------------------------------------- + // Conclusion: (= (select (store a i e) i) e) + ARRAYS_READ_OVER_WRITE_1, + // ======== Extensionality + // Children: (P:(not (= a b))) + // Arguments: none + // ---------------------------------------- + // Conclusion: (not (= (select a k) (select b k))) + // where k is arrays::SkolemCache::getExtIndexSkolem((not (= a b))). + ARRAYS_EXT, + // ======== Array Trust + // Children: (P1 ... Pn) + // Arguments: (F) + // --------------------- + // Conclusion: F + ARRAYS_TRUST, + + //================================================= Bit-Vector rules + // Note: bitblast() represents the result of the bit-blasted term as a + // bit-vector consisting of the output bits of the bit-blasted circuit + // representation of the term. Terms are bit-blasted according to the + // strategies defined in + // theory/bv/bitblast/bitblast_strategies_template.h. + // ======== Bitblast + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (= t bitblast(t)) + BV_BITBLAST, + // ======== Bitblast Bit-Vector Constant + // Children: none + // Arguments: (= t bitblast(t)) + // --------------------- + // Conclusion: (= t bitblast(t)) + BV_BITBLAST_CONST, + // ======== Bitblast Bit-Vector Variable + // Children: none + // Arguments: (= t bitblast(t)) + // --------------------- + // Conclusion: (= t bitblast(t)) + BV_BITBLAST_VAR, + // ======== Bitblast Bit-Vector Terms + // TODO cvc4-projects issue #275 + // Children: none + // Arguments: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t)) + // --------------------- + // Conclusion: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t)) + BV_BITBLAST_EQUAL, + BV_BITBLAST_ULT, + BV_BITBLAST_ULE, + BV_BITBLAST_UGT, + BV_BITBLAST_UGE, + BV_BITBLAST_SLT, + BV_BITBLAST_SLE, + BV_BITBLAST_SGT, + BV_BITBLAST_SGE, + BV_BITBLAST_NOT, + BV_BITBLAST_CONCAT, + BV_BITBLAST_AND, + BV_BITBLAST_OR, + BV_BITBLAST_XOR, + BV_BITBLAST_XNOR, + BV_BITBLAST_NAND, + BV_BITBLAST_NOR, + BV_BITBLAST_COMP, + BV_BITBLAST_MULT, + BV_BITBLAST_ADD, + BV_BITBLAST_SUB, + BV_BITBLAST_NEG, + BV_BITBLAST_UDIV, + BV_BITBLAST_UREM, + BV_BITBLAST_SDIV, + BV_BITBLAST_SREM, + BV_BITBLAST_SMOD, + BV_BITBLAST_SHL, + BV_BITBLAST_LSHR, + BV_BITBLAST_ASHR, + BV_BITBLAST_ULTBV, + BV_BITBLAST_SLTBV, + BV_BITBLAST_ITE, + BV_BITBLAST_EXTRACT, + BV_BITBLAST_REPEAT, + BV_BITBLAST_ZERO_EXTEND, + BV_BITBLAST_SIGN_EXTEND, + BV_BITBLAST_ROTATE_RIGHT, + BV_BITBLAST_ROTATE_LEFT, + // ======== Eager Atom + // Children: none + // Arguments: (F) + // --------------------- + // Conclusion: (= F F[0]) + // where F is of kind BITVECTOR_EAGER_ATOM + BV_EAGER_ATOM, + + //================================================= Datatype rules + // ======== Unification + // Children: (P:(= (C t1 ... tn) (C s1 ... sn))) + // Arguments: (i) + // ---------------------------------------- + // Conclusion: (= ti si) + // where C is a constructor. + DT_UNIF, + // ======== Instantiate + // Children: none + // Arguments: (t, n) + // ---------------------------------------- + // Conclusion: (= ((_ is C) t) (= t (C (sel_1 t) ... (sel_n t)))) + // where C is the n^th constructor of the type of T, and (_ is C) is the + // discriminator (tester) for C. + DT_INST, + // ======== Collapse + // Children: none + // Arguments: ((sel_i (C_j t_1 ... t_n))) + // ---------------------------------------- + // Conclusion: (= (sel_i (C_j t_1 ... t_n)) r) + // where C_j is a constructor, r is t_i if sel_i is a correctly applied + // selector, or TypeNode::mkGroundTerm() of the proper type otherwise. Notice + // that the use of mkGroundTerm differs from the rewriter which uses + // mkGroundValue in this case. + DT_COLLAPSE, + // ======== Split + // Children: none + // Arguments: (t) + // ---------------------------------------- + // Conclusion: (or ((_ is C1) t) ... ((_ is Cn) t)) + DT_SPLIT, + // ======== Clash + // Children: (P1:((_ is Ci) t), P2: ((_ is Cj) t)) + // Arguments: none + // ---------------------------------------- + // Conclusion: false + // for i != j. + DT_CLASH, + // ======== Datatype Trust + // Children: (P1 ... Pn) + // Arguments: (F) + // --------------------- + // Conclusion: F + DT_TRUST, + + //================================================= Quantifiers rules + // ======== Skolem intro + // Children: none + // Arguments: (k) + // ---------------------------------------- + // Conclusion: (= k t) + // where t is the original form of skolem k. + SKOLEM_INTRO, + // ======== Exists intro + // Children: (P:F[t]) + // Arguments: ((exists ((x T)) F[x])) + // ---------------------------------------- + // Conclusion: (exists ((x T)) F[x]) + // This rule verifies that F[x] indeed matches F[t] with a substitution + // over x. + EXISTS_INTRO, + // ======== Skolemize + // Children: (P:(exists ((x1 T1) ... (xn Tn)) F)) + // Arguments: none + // ---------------------------------------- + // Conclusion: F*sigma + // sigma maps x1 ... xn to their representative skolems obtained by + // SkolemManager::mkSkolemize, returned in the skolems argument of that + // method. Alternatively, can use negated forall as a premise. The witness + // terms for the returned skolems can be obtained by + // SkolemManager::getWitnessForm. + SKOLEMIZE, + // ======== Instantiate + // Children: (P:(forall ((x1 T1) ... (xn Tn)) F)) + // Arguments: (t1 ... tn) + // ---------------------------------------- + // Conclusion: F*sigma + // sigma maps x1 ... xn to t1 ... tn. + INSTANTIATE, + + //================================================= String rules + //======================== Core solver + // ======== Concat eq + // Children: (P1:(= (str.++ t1 ... tn t) (str.++ t1 ... tn s))) + // Arguments: (b), indicating if reverse direction + // --------------------- + // Conclusion: (= t s) + // + // Notice that t or s may be empty, in which case they are implicit in the + // concatenation above. For example, if + // P1 concludes (= x (str.++ x z)), then + // (CONCAT_EQ P1 :args false) concludes (= "" z) + // + // Also note that constants are split, such that if + // P1 concludes (= (str.++ "abc" x) (str.++ "a" y)), then + // (CONCAT_EQ P1 :args false) concludes (= (str.++ "bc" x) y) + // This splitting is done only for constants such that Word::splitConstant + // returns non-null. + CONCAT_EQ, + // ======== Concat unify + // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)), + // P2:(= (str.len t1) (str.len s1))) + // Arguments: (b), indicating if reverse direction + // --------------------- + // Conclusion: (= t1 s1) + CONCAT_UNIFY, + // ======== Concat conflict + // Children: (P1:(= (str.++ c1 t) (str.++ c2 s))) + // Arguments: (b), indicating if reverse direction + // --------------------- + // Conclusion: false + // Where c1, c2 are constants such that Word::splitConstant(c1,c2,index,b) + // is null, in other words, neither is a prefix of the other. + CONCAT_CONFLICT, + // ======== Concat split + // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)), + // P2:(not (= (str.len t1) (str.len s1)))) + // Arguments: (false) + // --------------------- + // Conclusion: (or (= t1 (str.++ s1 r_t)) (= s1 (str.++ t1 r_s))) + // where + // r_t = (skolem (suf t1 (str.len s1)))), + // r_s = (skolem (suf s1 (str.len t1)))). + // + // or the reverse form of the above: + // + // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)), + // P2:(not (= (str.len t2) (str.len s2)))) + // Arguments: (true) + // --------------------- + // Conclusion: (or (= t2 (str.++ r_t s2)) (= s2 (str.++ r_s t2))) + // where + // r_t = (skolem (pre t2 (- (str.len t2) (str.len s2))))), + // r_s = (skolem (pre s2 (- (str.len s2) (str.len t2))))). + // + // Above, (suf x n) is shorthand for (str.substr x n (- (str.len x) n)) and + // (pre x n) is shorthand for (str.substr x 0 n). + CONCAT_SPLIT, + // ======== Concat constant split + // Children: (P1:(= (str.++ t1 t2) (str.++ c s2)), + // P2:(not (= (str.len t1) 0))) + // Arguments: (false) + // --------------------- + // Conclusion: (= t1 (str.++ c r)) + // where + // r = (skolem (suf t1 1)). + // + // or the reverse form of the above: + // + // Children: (P1:(= (str.++ t1 t2) (str.++ s1 c)), + // P2:(not (= (str.len t2) 0))) + // Arguments: (true) + // --------------------- + // Conclusion: (= t2 (str.++ r c)) + // where + // r = (skolem (pre t2 (- (str.len t2) 1))). + CONCAT_CSPLIT, + // ======== Concat length propagate + // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)), + // P2:(> (str.len t1) (str.len s1))) + // Arguments: (false) + // --------------------- + // Conclusion: (= t1 (str.++ s1 r_t)) + // where + // r_t = (skolem (suf t1 (str.len s1))) + // + // or the reverse form of the above: + // + // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)), + // P2:(> (str.len t2) (str.len s2))) + // Arguments: (false) + // --------------------- + // Conclusion: (= t2 (str.++ r_t s2)) + // where + // r_t = (skolem (pre t2 (- (str.len t2) (str.len s2)))). + CONCAT_LPROP, + // ======== Concat constant propagate + // Children: (P1:(= (str.++ t1 w1 t2) (str.++ w2 s)), + // P2:(not (= (str.len t1) 0))) + // Arguments: (false) + // --------------------- + // Conclusion: (= t1 (str.++ w3 r)) + // where + // w1, w2, w3, w4 are words, + // w3 is (pre w2 p), + // w4 is (suf w2 p), + // p = Word::overlap((suf w2 1), w1), + // r = (skolem (suf t1 (str.len w3))). + // In other words, w4 is the largest suffix of (suf w2 1) that can contain a + // prefix of w1; since t1 is non-empty, w3 must therefore be contained in t1. + // + // or the reverse form of the above: + // + // Children: (P1:(= (str.++ t1 w1 t2) (str.++ s w2)), + // P2:(not (= (str.len t2) 0))) + // Arguments: (true) + // --------------------- + // Conclusion: (= t2 (str.++ r w3)) + // where + // w1, w2, w3, w4 are words, + // w3 is (suf w2 (- (str.len w2) p)), + // w4 is (pre w2 (- (str.len w2) p)), + // p = Word::roverlap((pre w2 (- (str.len w2) 1)), w1), + // r = (skolem (pre t2 (- (str.len t2) (str.len w3)))). + // In other words, w4 is the largest prefix of (pre w2 (- (str.len w2) 1)) + // that can contain a suffix of w1; since t2 is non-empty, w3 must therefore + // be contained in t2. + CONCAT_CPROP, + // ======== String decompose + // Children: (P1: (>= (str.len t) n) + // Arguments: (false) + // --------------------- + // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w1) n)) + // or + // Children: (P1: (>= (str.len t) n) + // Arguments: (true) + // --------------------- + // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w2) n)) + // where + // w1 is (skolem (pre t n)) + // w2 is (skolem (suf t n)) + STRING_DECOMPOSE, + // ======== Length positive + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0)) + STRING_LENGTH_POS, + // ======== Length non-empty + // Children: (P1:(not (= t ""))) + // Arguments: none + // --------------------- + // Conclusion: (not (= (str.len t) 0)) + STRING_LENGTH_NON_EMPTY, + //======================== Extended functions + // ======== Reduction + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (and R (= t w)) + // where w = strings::StringsPreprocess::reduce(t, R, ...). + // In other words, R is the reduction predicate for extended term t, and w is + // (skolem t) + // Notice that the free variables of R are w and the free variables of t. + STRING_REDUCTION, + // ======== Eager Reduction + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: R + // where R = strings::TermRegistry::eagerReduce(t). + STRING_EAGER_REDUCTION, + //======================== Regular expressions + // ======== Regular expression intersection + // Children: (P:(str.in.re t R1), P:(str.in.re t R2)) + // Arguments: none + // --------------------- + // Conclusion: (str.in.re t (re.inter R1 R2)). + RE_INTER, + // ======== Regular expression unfold positive + // Children: (P:(str.in.re t R)) + // Arguments: none + // --------------------- + // Conclusion:(RegExpOpr::reduceRegExpPos((str.in.re t R))), + // corresponding to the one-step unfolding of the premise. + RE_UNFOLD_POS, + // ======== Regular expression unfold negative + // Children: (P:(not (str.in.re t R))) + // Arguments: none + // --------------------- + // Conclusion:(RegExpOpr::reduceRegExpNeg((not (str.in.re t R)))), + // corresponding to the one-step unfolding of the premise. + RE_UNFOLD_NEG, + // ======== Regular expression unfold negative concat fixed + // Children: (P:(not (str.in.re t R))) + // Arguments: none + // --------------------- + // Conclusion:(RegExpOpr::reduceRegExpNegConcatFixed((not (str.in.re t + // R)),L,i)) where RegExpOpr::getRegExpConcatFixed((not (str.in.re t R)), i) = + // L. corresponding to the one-step unfolding of the premise, optimized for + // fixed length of component i of the regular expression concatenation R. + RE_UNFOLD_NEG_CONCAT_FIXED, + // ======== Regular expression elimination + // Children: none + // Arguments: (F, b) + // --------------------- + // Conclusion: (= F strings::RegExpElimination::eliminate(F, b)) + // where b is a Boolean indicating whether we are using aggressive + // eliminations. Notice this rule concludes (= F F) if no eliminations + // are performed for F. + RE_ELIM, + //======================== Code points + // Children: none + // Arguments: (t, s) + // --------------------- + // Conclusion:(or (= (str.code t) (- 1)) + // (not (= (str.code t) (str.code s))) + // (not (= t s))) + STRING_CODE_INJ, + //======================== Sequence unit + // Children: (P:(= (seq.unit x) (seq.unit y))) + // Arguments: none + // --------------------- + // Conclusion:(= x y) + // Also applies to the case where (seq.unit y) is a constant sequence + // of length one. + STRING_SEQ_UNIT_INJ, + // ======== String Trust + // Children: none + // Arguments: (Q) + // --------------------- + // Conclusion: (Q) + STRING_TRUST, + + //================================================= Arithmetic rules + // ======== Adding Inequalities + // Note: an ArithLiteral is a term of the form (>< poly const) + // where + // >< is >=, >, ==, <, <=, or not(== ...). + // poly is a polynomial + // const is a rational constant + + // Children: (P1:l1, ..., Pn:ln) + // where each li is an ArithLiteral + // not(= ...) is dis-allowed! + // + // Arguments: (k1, ..., kn), non-zero reals + // --------------------- + // Conclusion: (>< t1 t2) + // where >< is the fusion of the combination of the ><i, (flipping each it + // its ki is negative). >< is always one of <, <= + // NB: this implies that lower bounds must have negative ki, + // and upper bounds must have positive ki. + // t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n * + // poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n + // * const_n) + MACRO_ARITH_SCALE_SUM_UB, + // ======== Sum Upper Bounds + // Children: (P1, ... , Pn) + // where each Pi has form (><i, Li, Ri) + // for ><i in {<, <=, ==} + // Conclusion: (>< L R) + // where >< is < if any ><i is <, and <= otherwise. + // L is (+ L1 ... Ln) + // R is (+ R1 ... Rn) + ARITH_SUM_UB, + // ======== Tightening Strict Integer Upper Bounds + // Children: (P:(< i c)) + // where i has integer type. + // Arguments: none + // --------------------- + // Conclusion: (<= i greatestIntLessThan(c)}) + INT_TIGHT_UB, + // ======== Tightening Strict Integer Lower Bounds + // Children: (P:(> i c)) + // where i has integer type. + // Arguments: none + // --------------------- + // Conclusion: (>= i leastIntGreaterThan(c)}) + INT_TIGHT_LB, + // ======== Trichotomy of the reals + // Children: (A B) + // Arguments: (C) + // --------------------- + // Conclusion: (C), + // where (not A) (not B) and C + // are (> x c) (< x c) and (= x c) + // in some order + // note that "not" here denotes arithmetic negation, flipping + // >= to <, etc. + ARITH_TRICHOTOMY, + // ======== Arithmetic operator elimination + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: arith::OperatorElim::getAxiomFor(t) + ARITH_OP_ELIM_AXIOM, + // ======== Int Trust + // Children: (P1 ... Pn) + // Arguments: (Q) + // --------------------- + // Conclusion: (Q) + INT_TRUST, + + //======== Multiplication sign inference + // Children: none + // Arguments: (f1, ..., fk, m) + // --------------------- + // Conclusion: (=> (and f1 ... fk) (~ m 0)) + // Where f1, ..., fk are variables compared to zero (less, greater or not + // equal), m is a monomial from these variables, and ~ is the comparison (less + // or greater) that results from the signs of the variables. All variables + // with even exponent in m should be given as not equal to zero while all + // variables with odd exponent in m should be given as less or greater than + // zero. + ARITH_MULT_SIGN, + //======== Multiplication with positive factor + // Children: none + // Arguments: (m, (rel lhs rhs)) + // --------------------- + // Conclusion: (=> (and (> m 0) (rel lhs rhs)) (rel (* m lhs) (* m rhs))) + // Where rel is a relation symbol. + ARITH_MULT_POS, + //======== Multiplication with negative factor + // Children: none + // Arguments: (m, (rel lhs rhs)) + // --------------------- + // Conclusion: (=> (and (< m 0) (rel lhs rhs)) (rel_inv (* m lhs) (* m rhs))) + // Where rel is a relation symbol and rel_inv the inverted relation symbol. + ARITH_MULT_NEG, + //======== Multiplication tangent plane + // Children: none + // Arguments: (t, x, y, a, b, sgn) + // --------------------- + // Conclusion: + // sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y + // b))) sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a) + // (>= y b))) + // Where x,y are real terms (variables or extended terms), t = (* x y) + // (possibly under rewriting), a,b are real constants, and sgn is either -1 + // or 1. tplane is the tangent plane of x*y at (a,b): b*x + a*y - a*b + ARITH_MULT_TANGENT, + + // ================ Lemmas for transcendentals + //======== Assert bounds on PI + // Children: none + // Arguments: (l, u) + // --------------------- + // Conclusion: (and (>= real.pi l) (<= real.pi u)) + // Where l (u) is a valid lower (upper) bound on pi. + ARITH_TRANS_PI, + //======== Exp at negative values + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (= (< t 0) (< (exp t) 1)) + ARITH_TRANS_EXP_NEG, + //======== Exp is always positive + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (> (exp t) 0) + ARITH_TRANS_EXP_POSITIVITY, + //======== Exp grows super-linearly for positive values + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (or (<= t 0) (> exp(t) (+ t 1))) + ARITH_TRANS_EXP_SUPER_LIN, + //======== Exp at zero + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (= (= t 0) (= (exp t) 1)) + ARITH_TRANS_EXP_ZERO, + //======== Exp is approximated from above for negative values + // Children: none + // Arguments: (d, t, l, u) + // --------------------- + // Conclusion: (=> (and (>= t l) (<= t u)) (<= (exp t) (secant exp l u t)) + // Where d is an even positive number, t an arithmetic term and l (u) a lower + // (upper) bound on t. Let p be the d'th taylor polynomial at zero (also + // called the Maclaurin series) of the exponential function. (secant exp l u + // t) denotes the secant of p from (l, exp(l)) to (u, exp(u)) evaluated at t, + // calculated as follows: + // (p(l) - p(u)) / (l - u) * (t - l) + p(l) + // The lemma states that if t is between l and u, then (exp t) is below the + // secant of p from l to u. + ARITH_TRANS_EXP_APPROX_ABOVE_NEG, + //======== Exp is approximated from above for positive values + // Children: none + // Arguments: (d, t, l, u) + // --------------------- + // Conclusion: (=> (and (>= t l) (<= t u)) (<= (exp t) (secant-pos exp l u t)) + // Where d is an even positive number, t an arithmetic term and l (u) a lower + // (upper) bound on t. Let p* be a modification of the d'th taylor polynomial + // at zero (also called the Maclaurin series) of the exponential function as + // follows where p(d-1) is the regular Maclaurin series of degree d-1: + // p* = p(d-1) * (1 + t^n / n!) + // (secant-pos exp l u t) denotes the secant of p from (l, exp(l)) to (u, + // exp(u)) evaluated at t, calculated as follows: + // (p(l) - p(u)) / (l - u) * (t - l) + p(l) + // The lemma states that if t is between l and u, then (exp t) is below the + // secant of p from l to u. + ARITH_TRANS_EXP_APPROX_ABOVE_POS, + //======== Exp is approximated from below + // Children: none + // Arguments: (d, t) + // --------------------- + // Conclusion: (>= (exp t) (maclaurin exp d t)) + // Where d is an odd positive number and (maclaurin exp d t) is the d'th + // taylor polynomial at zero (also called the Maclaurin series) of the + // exponential function evaluated at t. The Maclaurin series for the + // exponential function is the following: + // e^x = \sum_{n=0}^{\infty} x^n / n! + ARITH_TRANS_EXP_APPROX_BELOW, + //======== Sine is always between -1 and 1 + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (and (<= (sin t) 1) (>= (sin t) (- 1))) + ARITH_TRANS_SINE_BOUNDS, + //======== Sine arg shifted to -pi..pi + // Children: none + // Arguments: (x, y, s) + // --------------------- + // Conclusion: (and + // (<= -pi y pi) + // (= (sin y) (sin x)) + // (ite (<= -pi x pi) (= x y) (= x (+ y (* 2 pi s)))) + // ) + // Where x is the argument to sine, y is a new real skolem that is x shifted + // into -pi..pi and s is a new integer skolem that is the number of phases y + // is shifted. + ARITH_TRANS_SINE_SHIFT, + //======== Sine is symmetric with respect to negation of the argument + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (= (- (sin t) (sin (- t))) 0) + ARITH_TRANS_SINE_SYMMETRY, + //======== Sine is bounded by the tangent at zero + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (and + // (=> (> t 0) (< (sin t) t)) + // (=> (< t 0) (> (sin t) t)) + // ) + ARITH_TRANS_SINE_TANGENT_ZERO, + //======== Sine is bounded by the tangents at -pi and pi + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (and + // (=> (> t -pi) (> (sin t) (- -pi t))) + // (=> (< t pi) (< (sin t) (- pi t))) + // ) + ARITH_TRANS_SINE_TANGENT_PI, + //======== Sine is approximated from above for negative values + // Children: none + // Arguments: (d, t, lb, ub, l, u) + // --------------------- + // Conclusion: (=> (and (>= t lb) (<= t ub)) (<= (sin t) (secant sin l u t)) + // Where d is an even positive number, t an arithmetic term, lb (ub) a + // symbolic lower (upper) bound on t (possibly containing pi) and l (u) the + // evaluated lower (upper) bound on t. Let p be the d'th taylor polynomial at + // zero (also called the Maclaurin series) of the sine function. (secant sin l + // u t) denotes the secant of p from (l, sin(l)) to (u, sin(u)) evaluated at + // t, calculated as follows: + // (p(l) - p(u)) / (l - u) * (t - l) + p(l) + // The lemma states that if t is between l and u, then (sin t) is below the + // secant of p from l to u. + ARITH_TRANS_SINE_APPROX_ABOVE_NEG, + //======== Sine is approximated from above for positive values + // Children: none + // Arguments: (d, t, c, lb, ub) + // --------------------- + // Conclusion: (=> (and (>= t lb) (<= t ub)) (<= (sin t) (upper sin c)) + // Where d is an even positive number, t an arithmetic term, c an arithmetic + // constant, and lb (ub) a symbolic lower (upper) bound on t (possibly + // containing pi). Let p be the d'th taylor polynomial at zero (also called + // the Maclaurin series) of the sine function. (upper sin c) denotes the upper + // bound on sin(c) given by p and lb,ub are such that sin(t) is the maximum of + // the sine function on (lb,ub). + ARITH_TRANS_SINE_APPROX_ABOVE_POS, + //======== Sine is approximated from below for negative values + // Children: none + // Arguments: (d, t, c, lb, ub) + // --------------------- + // Conclusion: (=> (and (>= t lb) (<= t ub)) (>= (sin t) (lower sin c)) + // Where d is an even positive number, t an arithmetic term, c an arithmetic + // constant, and lb (ub) a symbolic lower (upper) bound on t (possibly + // containing pi). Let p be the d'th taylor polynomial at zero (also called + // the Maclaurin series) of the sine function. (lower sin c) denotes the lower + // bound on sin(c) given by p and lb,ub are such that sin(t) is the minimum of + // the sine function on (lb,ub). + ARITH_TRANS_SINE_APPROX_BELOW_NEG, + //======== Sine is approximated from below for positive values + // Children: none + // Arguments: (d, t, lb, ub, l, u) + // --------------------- + // Conclusion: (=> (and (>= t lb) (<= t ub)) (>= (sin t) (secant sin l u t)) + // Where d is an even positive number, t an arithmetic term, lb (ub) a + // symbolic lower (upper) bound on t (possibly containing pi) and l (u) the + // evaluated lower (upper) bound on t. Let p be the d'th taylor polynomial at + // zero (also called the Maclaurin series) of the sine function. (secant sin l + // u t) denotes the secant of p from (l, sin(l)) to (u, sin(u)) evaluated at + // t, calculated as follows: + // (p(l) - p(u)) / (l - u) * (t - l) + p(l) + // The lemma states that if t is between l and u, then (sin t) is above the + // secant of p from l to u. + ARITH_TRANS_SINE_APPROX_BELOW_POS, + + // ================ CAD Lemmas + // We use IRP for IndexedRootPredicate. + // + // A formula "Interval" describes that a variable (xn is none is given) is + // within a particular interval whose bounds are given as IRPs. It is either + // an open interval or a point interval: + // (IRP k poly) < xn < (IRP k poly) + // xn == (IRP k poly) + // + // A formula "Cell" describes a portion + // of the real space in the following form: + // Interval(x1) and Interval(x2) and ... + // We implicitly assume a Cell to go up to n-1 (and can be empty). + // + // A formula "Covering" is a set of Intervals, implying that xn can be in + // neither of these intervals. To be a covering (of the real line), the union + // of these intervals should be the real numbers. + // ======== CAD direct conflict + // Children (Cell, A) + // --------------------- + // Conclusion: (false) + // A direct interval is generated from an assumption A (in variables x1...xn) + // over a Cell (in variables x1...xn). It derives that A evaluates to false + // over the Cell. In the actual algorithm, it means that xn can not be in the + // topmost interval of the Cell. + ARITH_NL_CAD_DIRECT, + // ======== CAD recursive interval + // Children (Cell, Covering) + // --------------------- + // Conclusion: (false) + // A recursive interval is generated from a Covering (for xn) over a Cell + // (in variables x1...xn-1). It generates the conclusion that no xn exists + // that extends the Cell and satisfies all assumptions. + ARITH_NL_CAD_RECURSIVE, + + //================================================= Unknown rule + UNKNOWN, +}; + +/** + * Converts a proof rule to a string. Note: This function is also used in + * `safe_print()`. Changing this function name or signature will result in + * `safe_print()` printing "<unsupported>" instead of the proper strings for + * the enum values. + * + * @param id The proof rule + * @return The name of the proof rule + */ +const char* toString(PfRule id); + +/** + * Writes a proof rule name to a stream. + * + * @param out The stream to write to + * @param id The proof rule to write to the stream + * @return The stream + */ +std::ostream& operator<<(std::ostream& out, PfRule id); + +/** Hash function for proof rules */ +struct PfRuleHashFunction +{ + size_t operator()(PfRule id) const; +}; /* struct PfRuleHashFunction */ + +} // namespace cvc5 + +#endif /* CVC5__PROOF__PROOF_RULE_H */ diff --git a/src/proof/proof_set.h b/src/proof/proof_set.h new file mode 100644 index 000000000..4015e0466 --- /dev/null +++ b/src/proof/proof_set.h @@ -0,0 +1,76 @@ +/****************************************************************************** + * Top contributors (to current version): + * Gereon Kremer, Andrew Reynolds + * + * 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. + * **************************************************************************** + * + * Proof set utility. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_SET_H +#define CVC5__PROOF__PROOF_SET_H + +#include <memory> + +#include "context/cdlist.h" +#include "context/context.h" +#include "proof/proof_node_manager.h" + +namespace cvc5 { + +/** + * A (context-dependent) set of proofs, which is used for memory + * management purposes. + */ +template <typename T> +class CDProofSet +{ + public: + CDProofSet(ProofNodeManager* pnm, + context::Context* c, + std::string namePrefix = "Proof") + : d_pnm(pnm), d_proofs(c), d_namePrefix(namePrefix) + { + } + /** + * Allocate a new proof. + * + * This returns a fresh proof object that remains alive in the context given + * to this class. Internally, this adds a new proof of type T to a + * context-dependent list of proofs and passes the following arguments to the + * T constructor: + * pnm, args..., name + * where pnm is the proof node manager + * provided to this proof set upon construction, args... are the arguments to + * allocateProof() and name is the namePrefix with an appended index. + */ + template <typename... Args> + T* allocateProof(Args&&... args) + { + d_proofs.push_back(std::make_shared<T>( + d_pnm, + std::forward<Args>(args)..., + d_namePrefix + "_" + std::to_string(d_proofs.size()))); + return d_proofs.back().get(); + } + + protected: + /** The proof node manager */ + ProofNodeManager* d_pnm; + /** A context-dependent list of lazy proofs. */ + context::CDList<std::shared_ptr<T>> d_proofs; + /** The name prefix of the lazy proofs */ + std::string d_namePrefix; +}; + +} // namespace cvc5 + +#endif /* CVC5__PROOF__LAZY_PROOF_SET_H */ diff --git a/src/proof/proof_step_buffer.cpp b/src/proof/proof_step_buffer.cpp new file mode 100644 index 000000000..309802505 --- /dev/null +++ b/src/proof/proof_step_buffer.cpp @@ -0,0 +1,112 @@ +/****************************************************************************** + * 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 proof step and proof step buffer utilities. + */ + +#include "proof/proof_step_buffer.h" + +#include "proof/proof_checker.h" + +using namespace cvc5::kind; + +namespace cvc5 { + +ProofStep::ProofStep() : d_rule(PfRule::UNKNOWN) {} +ProofStep::ProofStep(PfRule r, + const std::vector<Node>& children, + const std::vector<Node>& args) + : d_rule(r), d_children(children), d_args(args) +{ +} +std::ostream& operator<<(std::ostream& out, ProofStep step) +{ + out << "(step " << step.d_rule; + for (const Node& c : step.d_children) + { + out << " " << c; + } + if (!step.d_args.empty()) + { + out << " :args"; + for (const Node& a : step.d_args) + { + out << " " << a; + } + } + out << ")"; + return out; +} + +ProofStepBuffer::ProofStepBuffer(ProofChecker* pc) : d_checker(pc) {} + +Node ProofStepBuffer::tryStep(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args, + Node expected) +{ + if (d_checker == nullptr) + { + Assert(false) << "ProofStepBuffer::ProofStepBuffer: no proof checker."; + return Node::null(); + } + Node res = + d_checker->checkDebug(id, children, args, expected, "pf-step-buffer"); + if (!res.isNull()) + { + // add proof step + d_steps.push_back( + std::pair<Node, ProofStep>(res, ProofStep(id, children, args))); + } + return res; +} + +void ProofStepBuffer::addStep(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args, + Node expected) +{ + d_steps.push_back( + std::pair<Node, ProofStep>(expected, ProofStep(id, children, args))); +} + +void ProofStepBuffer::addSteps(ProofStepBuffer& psb) +{ + const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps(); + for (const std::pair<Node, ProofStep>& step : steps) + { + addStep(step.second.d_rule, + step.second.d_children, + step.second.d_args, + step.first); + } +} + +void ProofStepBuffer::popStep() +{ + Assert(!d_steps.empty()); + if (!d_steps.empty()) + { + d_steps.pop_back(); + } +} + +size_t ProofStepBuffer::getNumSteps() const { return d_steps.size(); } + +const std::vector<std::pair<Node, ProofStep>>& ProofStepBuffer::getSteps() const +{ + return d_steps; +} + +void ProofStepBuffer::clear() { d_steps.clear(); } + +} // namespace cvc5 diff --git a/src/proof/proof_step_buffer.h b/src/proof/proof_step_buffer.h new file mode 100644 index 000000000..4c1bfa8a3 --- /dev/null +++ b/src/proof/proof_step_buffer.h @@ -0,0 +1,98 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * Proof step and proof step buffer utilities. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_STEP_BUFFER_H +#define CVC5__PROOF__PROOF_STEP_BUFFER_H + +#include <vector> + +#include "expr/node.h" +#include "proof/proof_rule.h" + +namespace cvc5 { + +class ProofChecker; + +/** + * Information for constructing a step in a CDProof. Notice that the conclusion + * of the proof step is intentionally not included in this data structure. + * Instead, it is intended that conclusions may be associated with proof steps + * based on e.g. the result of proof checking. + */ +class ProofStep +{ + public: + ProofStep(); + ProofStep(PfRule r, + const std::vector<Node>& children, + const std::vector<Node>& args); + /** The proof rule */ + PfRule d_rule; + /** The proof children */ + std::vector<Node> d_children; + /** The proof arguments */ + std::vector<Node> d_args; +}; +std::ostream& operator<<(std::ostream& out, ProofStep step); + +/** + * Class used to speculatively try and buffer a set of proof steps before + * sending them to a proof object. + */ +class ProofStepBuffer +{ + public: + ProofStepBuffer(ProofChecker* pc = nullptr); + ~ProofStepBuffer() {} + /** + * Returns the conclusion of the proof step, as determined by the proof + * checker of the given proof. If this is non-null, then the given step + * is added to the buffer maintained by this class. + * + * If expected is non-null, then this method returns null if the result of + * checking is not equal to expected. + */ + Node tryStep(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args, + Node expected = Node::null()); + /** Same as above, without checking */ + void addStep(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args, + Node expected); + /** Multi-step version */ + void addSteps(ProofStepBuffer& psb); + /** pop step */ + void popStep(); + /** Get num steps */ + size_t getNumSteps() const; + /** Get steps */ + const std::vector<std::pair<Node, ProofStep>>& getSteps() const; + /** Clear */ + void clear(); + + private: + /** The proof checker*/ + ProofChecker* d_checker; + /** the queued proof steps */ + std::vector<std::pair<Node, ProofStep>> d_steps; +}; + +} // namespace cvc5 + +#endif /* CVC5__PROOF__PROOF_STEP_BUFFER_H */ diff --git a/src/proof/theory_proof_step_buffer.cpp b/src/proof/theory_proof_step_buffer.cpp new file mode 100644 index 000000000..f00c664c8 --- /dev/null +++ b/src/proof/theory_proof_step_buffer.cpp @@ -0,0 +1,240 @@ +/****************************************************************************** + * Top contributors (to current version): + * Haniel Barbosa, 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 theory proof step buffer utility. + */ + +#include "proof/theory_proof_step_buffer.h" + +#include "proof/proof.h" + +using namespace cvc5::kind; + +namespace cvc5 { +namespace theory { + +TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc) + : ProofStepBuffer(pc) +{ +} + +bool TheoryProofStepBuffer::applyEqIntro(Node src, + Node tgt, + const std::vector<Node>& exp, + MethodId ids, + MethodId ida, + MethodId idr) +{ + std::vector<Node> args; + args.push_back(src); + builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr); + Node res = tryStep(PfRule::MACRO_SR_EQ_INTRO, exp, args); + if (res.isNull()) + { + // failed to apply + return false; + } + // should have concluded the expected equality + Node expected = src.eqNode(tgt); + if (res != expected) + { + // did not provide the correct target + popStep(); + return false; + } + // successfully proved src == tgt. + return true; +} + +bool TheoryProofStepBuffer::applyPredTransform(Node src, + Node tgt, + const std::vector<Node>& exp, + MethodId ids, + MethodId ida, + MethodId idr) +{ + // symmetric equalities + if (CDProof::isSame(src, tgt)) + { + return true; + } + std::vector<Node> children; + children.push_back(src); + std::vector<Node> args; + // try to prove that tgt rewrites to src + children.insert(children.end(), exp.begin(), exp.end()); + args.push_back(tgt); + builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr); + Node res = tryStep(PfRule::MACRO_SR_PRED_TRANSFORM, children, args); + if (res.isNull()) + { + // failed to apply + return false; + } + // should definitely have concluded tgt + Assert(res == tgt); + return true; +} + +bool TheoryProofStepBuffer::applyPredIntro(Node tgt, + const std::vector<Node>& exp, + MethodId ids, + MethodId ida, + MethodId idr) +{ + std::vector<Node> args; + args.push_back(tgt); + builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr); + Node res = tryStep(PfRule::MACRO_SR_PRED_INTRO, exp, args); + if (res.isNull()) + { + return false; + } + Assert(res == tgt); + return true; +} + +Node TheoryProofStepBuffer::applyPredElim(Node src, + const std::vector<Node>& exp, + MethodId ids, + MethodId ida, + MethodId idr) +{ + std::vector<Node> children; + children.push_back(src); + children.insert(children.end(), exp.begin(), exp.end()); + std::vector<Node> args; + builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr); + Node srcRew = tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args); + if (CDProof::isSame(src, srcRew)) + { + popStep(); + } + return srcRew; +} + +Node TheoryProofStepBuffer::factorReorderElimDoubleNeg(Node n) +{ + if (n.getKind() != kind::OR) + { + return elimDoubleNegLit(n); + } + NodeManager* nm = NodeManager::currentNM(); + std::vector<Node> children{n.begin(), n.end()}; + std::vector<Node> childrenEqs; + // eliminate double neg for each lit. Do it first because it may expose + // duplicates + bool hasDoubleNeg = false; + for (unsigned i = 0; i < children.size(); ++i) + { + if (children[i].getKind() == kind::NOT + && children[i][0].getKind() == kind::NOT) + { + hasDoubleNeg = true; + childrenEqs.push_back(children[i].eqNode(children[i][0][0])); + addStep(PfRule::MACRO_SR_PRED_INTRO, + {}, + {childrenEqs.back()}, + childrenEqs.back()); + // update child + children[i] = children[i][0][0]; + } + else + { + childrenEqs.push_back(children[i].eqNode(children[i])); + addStep(PfRule::REFL, {}, {children[i]}, childrenEqs.back()); + } + } + if (hasDoubleNeg) + { + Node oldn = n; + n = nm->mkNode(kind::OR, children); + // Create a congruence step to justify replacement of each doubly negated + // literal. This is done to avoid having to use MACRO_SR_PRED_TRANSFORM + // from the old clause to the new one, which, under the standard rewriter, + // may not hold. An example is + // + // --------------------------------------------------------------------- + // (or (or (not x2) x1 x2) (not (not x2))) = (or (or (not x2) x1 x2) x2) + // + // which fails due to factoring not happening after flattening. + // + // Using congruence only the + // + // ------------------ MACRO_SR_PRED_INTRO + // (not (not t)) = t + // + // steps are added, which, since double negation is eliminated in a + // pre-rewrite in the Boolean rewriter, will always hold under the + // standard rewriter. + Node congEq = oldn.eqNode(n); + addStep(PfRule::CONG, + childrenEqs, + {ProofRuleChecker::mkKindNode(kind::OR)}, + congEq); + // add an equality resolution step to derive normalize clause + addStep(PfRule::EQ_RESOLVE, {oldn, congEq}, {}, n); + } + children.clear(); + // remove duplicates while keeping the order of children + std::unordered_set<TNode> clauseSet; + unsigned size = n.getNumChildren(); + for (unsigned i = 0; i < size; ++i) + { + if (clauseSet.count(n[i])) + { + continue; + } + children.push_back(n[i]); + clauseSet.insert(n[i]); + } + // if factoring changed + if (children.size() < size) + { + Node factored = children.empty() + ? nm->mkConst<bool>(false) + : children.size() == 1 ? children[0] + : nm->mkNode(kind::OR, children); + // don't overwrite what already has a proof step to avoid cycles + addStep(PfRule::FACTORING, {n}, {}, factored); + n = factored; + } + // nothing to order + if (children.size() < 2) + { + return n; + } + // order + std::sort(children.begin(), children.end()); + Node ordered = nm->mkNode(kind::OR, children); + // if ordering changed + if (ordered != n) + { + // don't overwrite what already has a proof step to avoid cycles + addStep(PfRule::REORDERING, {n}, {ordered}, ordered); + } + return ordered; +} + +Node TheoryProofStepBuffer::elimDoubleNegLit(Node n) +{ + // eliminate double neg + if (n.getKind() == kind::NOT && n[0].getKind() == kind::NOT) + { + addStep(PfRule::NOT_NOT_ELIM, {n}, {}, n[0][0]); + return n[0][0]; + } + return n; +} + +} // namespace theory +} // namespace cvc5 diff --git a/src/proof/theory_proof_step_buffer.h b/src/proof/theory_proof_step_buffer.h new file mode 100644 index 000000000..fc2e25e5a --- /dev/null +++ b/src/proof/theory_proof_step_buffer.h @@ -0,0 +1,120 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa + * + * 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. + * **************************************************************************** + * + * Theory proof step buffer utility. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__THEORY_PROOF_STEP_BUFFER_H +#define CVC5__PROOF__THEORY_PROOF_STEP_BUFFER_H + +#include <vector> + +#include "expr/node.h" +#include "proof/proof_step_buffer.h" +#include "theory/builtin/proof_checker.h" + +namespace cvc5 { +namespace theory { +/** + * Class used to speculatively try and buffer a set of proof steps before + * sending them to a proof object, extended with theory-specfic proof rule + * utilities. + */ +class TheoryProofStepBuffer : public ProofStepBuffer +{ + public: + TheoryProofStepBuffer(ProofChecker* pc = nullptr); + ~TheoryProofStepBuffer() {} + //---------------------------- utilities builtin proof rules + /** + * Apply equality introduction. If this method returns true, it adds proof + * step(s) to the buffer that conclude (= src tgt) from premises exp. In + * particular, it may attempt to apply the rule MACRO_SR_EQ_INTRO. This + * method should be applied when tgt is equivalent to src assuming exp. + */ + bool applyEqIntro(Node src, + Node tgt, + const std::vector<Node>& exp, + MethodId ids = MethodId::SB_DEFAULT, + MethodId ida = MethodId::SBA_SEQUENTIAL, + MethodId idr = MethodId::RW_REWRITE); + /** + * Apply predicate transform. If this method returns true, it adds (at most + * one) proof step to the buffer that conclude tgt from premises src, exp. In + * particular, it may attempt to apply MACRO_SR_PRED_TRANSFORM. This method + * should be applied when src and tgt are equivalent formulas assuming exp. + */ + bool applyPredTransform(Node src, + Node tgt, + const std::vector<Node>& exp, + MethodId ids = MethodId::SB_DEFAULT, + MethodId ida = MethodId::SBA_SEQUENTIAL, + MethodId idr = MethodId::RW_REWRITE); + /** + * Apply predicate introduction. If this method returns true, it adds proof + * step(s) to the buffer that conclude tgt from premises exp. In particular, + * it may attempt to apply the rule MACRO_SR_PRED_INTRO. This method should be + * applied when tgt is equivalent to true assuming exp. + */ + bool applyPredIntro(Node tgt, + const std::vector<Node>& exp, + MethodId ids = MethodId::SB_DEFAULT, + MethodId ida = MethodId::SBA_SEQUENTIAL, + MethodId idr = MethodId::RW_REWRITE); + /** + * Apply predicate elimination. This method returns the result of applying + * the rule MACRO_SR_PRED_ELIM on src, exp. The returned formula is equivalent + * to src assuming exp. If the return value is equivalent to src, then no + * proof step is added to this buffer, since this step is a no-op in this + * case. + * + * Notice that in contrast to the other rules above, predicate elimination + * never fails and proves a formula that is not explicitly given as an + * argument tgt. Thus, the return value of this method is Node not bool. + */ + Node applyPredElim(Node src, + const std::vector<Node>& exp, + MethodId ids = MethodId::SB_DEFAULT, + MethodId ida = MethodId::SBA_SEQUENTIAL, + MethodId idr = MethodId::RW_REWRITE); + //---------------------------- end utilities builtin proof rules + + //---------------------------- utility methods for normalizing clauses + /** + * Normalizes a non-unit clause (an OR node) according to factoring and + * reordering, i.e. removes duplicates and reorders literals (according to + * node ids). Moreover it eliminates double negations, which can be done also + * for unit clauses (a arbitrary Boolean node). All normalization steps are + * tracked via proof steps added to this proof step buffer. + * + * @param n the clause to be normalized + * @return the normalized clause node + */ + Node factorReorderElimDoubleNeg(Node n); + + /** + * Eliminates double negation of a literal if it has the form + * (not (not t)) + * If the elimination happens, a step is added to this proof step buffer. + * + * @param n the node to have the top-level double negation eliminated + * @return the normalized clause node + */ + Node elimDoubleNegLit(Node n); +}; + +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__PROOF__THEORY_PROOF_STEP_BUFFER_H */ diff --git a/src/proof/trust_node.cpp b/src/proof/trust_node.cpp new file mode 100644 index 000000000..d99e6de51 --- /dev/null +++ b/src/proof/trust_node.cpp @@ -0,0 +1,150 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * 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 the trust node utility. + */ + +#include "proof/trust_node.h" + +#include "proof/proof_ensure_closed.h" +#include "proof/proof_generator.h" + +namespace cvc5 { +namespace theory { + +const char* toString(TrustNodeKind tnk) +{ + switch (tnk) + { + case TrustNodeKind::CONFLICT: return "CONFLICT"; + case TrustNodeKind::LEMMA: return "LEMMA"; + case TrustNodeKind::PROP_EXP: return "PROP_EXP"; + case TrustNodeKind::REWRITE: return "REWRITE"; + default: return "?"; + } +} + +std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk) +{ + out << toString(tnk); + return out; +} + +TrustNode TrustNode::mkTrustConflict(Node conf, ProofGenerator* g) +{ + Node ckey = getConflictProven(conf); + // if a generator is provided, should confirm that it can prove it + Assert(g == nullptr || g->hasProofFor(ckey)); + return TrustNode(TrustNodeKind::CONFLICT, ckey, g); +} + +TrustNode TrustNode::mkTrustLemma(Node lem, ProofGenerator* g) +{ + Node lkey = getLemmaProven(lem); + // if a generator is provided, should confirm that it can prove it + Assert(g == nullptr || g->hasProofFor(lkey)); + return TrustNode(TrustNodeKind::LEMMA, lkey, g); +} + +TrustNode TrustNode::mkTrustPropExp(TNode lit, Node exp, ProofGenerator* g) +{ + Node pekey = getPropExpProven(lit, exp); + Assert(g == nullptr || g->hasProofFor(pekey)); + return TrustNode(TrustNodeKind::PROP_EXP, pekey, g); +} + +TrustNode TrustNode::mkTrustRewrite(TNode n, Node nr, ProofGenerator* g) +{ + Node rkey = getRewriteProven(n, nr); + Assert(g == nullptr || g->hasProofFor(rkey)); + return TrustNode(TrustNodeKind::REWRITE, rkey, g); +} + +TrustNode TrustNode::null() +{ + return TrustNode(TrustNodeKind::INVALID, Node::null()); +} + +TrustNode::TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g) + : d_tnk(tnk), d_proven(p), d_gen(g) +{ + // does not make sense to provide null node with generator + Assert(!d_proven.isNull() || d_gen == nullptr); +} + +TrustNodeKind TrustNode::getKind() const { return d_tnk; } + +Node TrustNode::getNode() const +{ + switch (d_tnk) + { + // the node of lemma is the node itself + case TrustNodeKind::LEMMA: return d_proven; + // the node of the rewrite is the right hand side of EQUAL + case TrustNodeKind::REWRITE: return d_proven[1]; + // the node of an explained propagation is the antecendant of an IMPLIES + // the node of a conflict is underneath a NOT + default: return d_proven[0]; + } +} + +Node TrustNode::getProven() const { return d_proven; } + +ProofGenerator* TrustNode::getGenerator() const { return d_gen; } + +bool TrustNode::isNull() const { return d_proven.isNull(); } + +std::shared_ptr<ProofNode> TrustNode::toProofNode() const +{ + if (d_gen == nullptr) + { + return nullptr; + } + return d_gen->getProofFor(d_proven); +} + +Node TrustNode::getConflictProven(Node conf) { return conf.notNode(); } + +Node TrustNode::getLemmaProven(Node lem) { return lem; } + +Node TrustNode::getPropExpProven(TNode lit, Node exp) +{ + return NodeManager::currentNM()->mkNode(kind::IMPLIES, exp, lit); +} + +Node TrustNode::getRewriteProven(TNode n, Node nr) { return n.eqNode(nr); } + +void TrustNode::debugCheckClosed(const char* c, + const char* ctx, + bool reqNullGen) +{ + pfgEnsureClosed(d_proven, d_gen, c, ctx, reqNullGen); +} + +std::string TrustNode::identifyGenerator() const +{ + if (d_gen == nullptr) + { + return "null"; + } + return d_gen->identify(); +} + +std::ostream& operator<<(std::ostream& out, TrustNode n) +{ + out << "(" << n.getKind() << " " << n.getProven() << " " + << n.identifyGenerator() << ")"; + return out; +} + +} // namespace theory +} // namespace cvc5 diff --git a/src/proof/trust_node.h b/src/proof/trust_node.h new file mode 100644 index 000000000..200dececd --- /dev/null +++ b/src/proof/trust_node.h @@ -0,0 +1,178 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Gereon Kremer + * + * 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. + * **************************************************************************** + * + * The trust node utility. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__TRUST_NODE_H +#define CVC5__PROOF__TRUST_NODE_H + +#include "expr/node.h" + +namespace cvc5 { + +class ProofGenerator; +class ProofNode; + +namespace theory { + +/** A kind for trust nodes */ +enum class TrustNodeKind : uint32_t +{ + CONFLICT, + LEMMA, + PROP_EXP, + REWRITE, + INVALID +}; +/** + * Converts a proof rule to a string. Note: This function is also used in + * `safe_print()`. Changing this function name or signature will result in + * `safe_print()` printing "<unsupported>" instead of the proper strings for + * the enum values. + * + * Returns a string with static lifetime: it should not be freed. + * + * @param tnk The trust node kind + * @return The name of the trust node kind + */ +const char* toString(TrustNodeKind tnk); + +/** + * Writes a trust node kind name to a stream. + * + * @param out The stream to write to + * @param tnk The trust node kind to write to the stream + * @return The stream + */ +std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk); + +/** + * A trust node is a pair (F, G) where F is a formula and G is a proof + * generator that can construct a proof for F if asked. + * + * More generally, a trust node is any node that can be used for a specific + * purpose that requires justification, such as being passed to + * OutputChannel::lemma. That justification is intended to be given by the + * generator that is required to construct this object. + * + * They are intended to be constructed by ProofGenerator objects themselves (a + * proof generator wraps itself in TrustNode it returns) and passed + * to ProofOutputChannel by theory solvers. + * + * The static functions for constructing them check that the generator, if + * provided, is capable of proving the given conflict or lemma, or an assertion + * failure occurs. Otherwise an assertion error is given. + * + * While this is not enforced, a `TrustNode` generally encapsulates a **closed** + * proof of the formula: one without free assumptions. + */ +class TrustNode +{ + public: + TrustNode() : d_tnk(TrustNodeKind::INVALID), d_gen(nullptr) {} + /** Make a proven node for conflict */ + static TrustNode mkTrustConflict(Node conf, ProofGenerator* g = nullptr); + /** Make a proven node for lemma */ + static TrustNode mkTrustLemma(Node lem, ProofGenerator* g = nullptr); + /** Make a proven node for explanation of propagated literal */ + static TrustNode mkTrustPropExp(TNode lit, + Node exp, + ProofGenerator* g = nullptr); + /** Make a proven node for rewrite */ + static TrustNode mkTrustRewrite(TNode n, + Node nr, + ProofGenerator* g = nullptr); + /** The null proven node */ + static TrustNode null(); + ~TrustNode() {} + /** get kind */ + TrustNodeKind getKind() const; + /** get node + * + * This is the node that is used in a common interface, either: + * (1) A T-unsat conjunction conf to pass to OutputChannel::conflict, + * (2) A valid T-formula lem to pass to OutputChannel::lemma, + * (3) A conjunction of literals exp to return in Theory::explain(lit), or + * (4) A result of rewriting a term n into an equivalent one nr. + * + * Notice that this node does not necessarily correspond to a valid formula. + * The call getProven() below retrieves a valid formula corresponding to + * the above calls. + */ + Node getNode() const; + /** get proven + * + * This is the corresponding formula that is proven by the proof generator + * for the above cases: + * (1) (not conf), for conflicts, + * (2) lem, for lemmas, + * (3) (=> exp lit), for propagations from explanations, + * (4) (= n nr), for results of rewriting. + * + * When constructing this trust node, the proof generator should be able to + * provide a proof for this fact. + */ + Node getProven() const; + /** get generator */ + ProofGenerator* getGenerator() const; + /** is null? */ + bool isNull() const; + /** + * Gets the proof node for this trust node, which is obtained by + * calling the generator's getProofFor method on the proven node. + */ + std::shared_ptr<ProofNode> toProofNode() const; + + /** Get the proven formula corresponding to a conflict call */ + static Node getConflictProven(Node conf); + /** Get the proven formula corresponding to a lemma call */ + static Node getLemmaProven(Node lem); + /** Get the proven formula corresponding to explanations for propagation */ + static Node getPropExpProven(TNode lit, Node exp); + /** Get the proven formula corresponding to a rewrite */ + static Node getRewriteProven(TNode n, Node nr); + /** For debugging */ + std::string identifyGenerator() const; + + /** + * debug check closed on Trace c, context ctx is string for debugging + * + * @param reqNullGen Whether we consider a null generator to be a failure. + */ + void debugCheckClosed(const char* c, const char* ctx, bool reqNullGen = true); + + private: + TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g = nullptr); + /** The kind */ + TrustNodeKind d_tnk; + /** The proven node */ + Node d_proven; + /** The generator */ + ProofGenerator* d_gen; +}; + +/** + * Writes a trust node to a stream. + * + * @param out The stream to write to + * @param n The trust node to write to the stream + * @return The stream + */ +std::ostream& operator<<(std::ostream& out, TrustNode n); + +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__PROOF__TRUST_NODE_H */ |