From: Andrew Reynolds Date: Tue, 23 Jun 2020 21:41:59 +0000 (-0500) Subject: (proof-new) Updates to proof node manager (#4617) X-Git-Tag: cvc5-1.0.0~3178 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=feea2d248ebe0c024c9c5ed14a9f0bf34b06c146;p=cvc5.git (proof-new) Updates to proof node manager (#4617) Main feature added is the mkScope interface, which is agnostic to symmetry of (dis)equalities. It also adds a check for cyclic proofs when using the interface ProofNodeManager::updateNode. Note that an earlier version of this method was agnostics to predicates vs Boolean equality with constants. This is no longer required. --- diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index 2795ff836..078e918b8 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -14,6 +14,9 @@ #include "expr/proof_node_manager.h" +#include "expr/proof.h" +#include "expr/proof_node_algorithm.h" + using namespace CVC4::kind; namespace CVC4 { @@ -39,27 +42,145 @@ std::shared_ptr ProofNodeManager::mkNode( return pn; } +std::shared_ptr ProofNodeManager::mkAssume(Node fact) +{ + Assert(!fact.isNull()); + Assert(fact.getType().isBoolean()); + return mkNode(PfRule::ASSUME, {}, {fact}, fact); +} + +std::shared_ptr ProofNodeManager::mkScope( + std::shared_ptr pf, + std::vector& 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 ac{assumps.begin(), assumps.end()}; + + // The free assumptions of the proof + std::map> famap; + expr::getFreeAssumptionsMap(pf.get(), famap); + std::unordered_set acu; + for (const std::pair>& fa : famap) + { + Node a = fa.first; + if (ac.find(a) != ac.end()) + { + // already covered by an assumption + 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"; + if (!aeqSym.isNull()) + { + if (ac.count(aeqSym)) + { + Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a + << " for " << fa.second.size() << " proof nodes" + << std::endl; + std::shared_ptr pfaa = mkAssume(aeqSym); + for (ProofNode* pfs : fa.second) + { + Assert(pfs->getResult() == a); + // must correct the orientation on this leaf + std::vector> children; + children.push_back(pfaa); + std::vector args; + args.push_back(a); + updateNode(pfs, PfRule::MACRO_SR_PRED_TRANSFORM, children, args); + } + Trace("pnm-scope") << "...finished" << std::endl; + acu.insert(aeqSym); + continue; + } + } + // All free assumptions should be arguments to SCOPE. + std::stringstream ss; + pf->printDebug(ss); + ss << std::endl << "Free assumption: " << a << std::endl; + for (const Node& aprint : ac) + { + ss << "- assumption: " << aprint << 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; + Node conc = pf->getResult(); + if (assumps.empty()) + { + Assert(!conc.isConst()); + minExpected = conc; + } + else + { + exp = assumps.size() == 1 ? assumps[0] : nm->mkNode(AND, assumps); + if (conc.isConst() && !conc.getConst()) + { + 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>& children, const std::vector& args) { - // should have already computed what is proven - Assert(!pn->d_proven.isNull()) - << "ProofNodeManager::updateProofNode: invalid proof provided"; - // We expect to prove the same thing as before - Node res = checkInternal(id, children, args, pn->d_proven); - if (res.isNull()) + return updateNodeInternal(pn, id, children, args, true); +} + +bool ProofNodeManager::updateNode(ProofNode* pn, ProofNode* pnr) +{ + if (pn->getResult() != pnr->getResult()) { - // if it was invalid, then we do not update return false; } - // we update its value - pn->setValue(id, children, args); - // proven field should already be the same as the result - Assert(res == pn->d_proven); - return true; + // can shortcut re-check of rule + return updateNodeInternal( + pn, pnr->getRule(), pnr->getChildren(), pnr->getArguments(), false); } Node ProofNodeManager::checkInternal( @@ -88,4 +209,75 @@ Node ProofNodeManager::checkInternal( ProofChecker* ProofNodeManager::getChecker() const { return d_checker; } +bool ProofNodeManager::updateNodeInternal( + ProofNode* pn, + PfRule id, + const std::vector>& children, + const std::vector& args, + bool needsCheck) +{ + // ---------------- check for cyclic + std::unordered_map visited; + std::unordered_map::iterator it; + std::vector visit; + for (const std::shared_ptr& cp : children) + { + visit.push_back(cp.get()); + } + const ProofNode* cur; + while (!visit.empty()) + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + if (it == visited.end()) + { + visited[cur] = true; + if (cur == pn) + { + std::stringstream ss; + ss << "ProofNodeManager::updateNode: attempting to make cyclic proof! " + << id << " " << pn->getResult() << ", children = " << std::endl; + for (const std::shared_ptr& cp : children) + { + ss << " " << cp->getRule() << " " << cp->getResult() << std::endl; + } + ss << "Full children:" << std::endl; + for (const std::shared_ptr& cp : children) + { + ss << " - "; + cp->printDebug(ss); + ss << std::endl; + } + Unreachable() << ss.str(); + } + for (const std::shared_ptr& cp : cur->d_children) + { + visit.push_back(cp.get()); + } + } + } + // ---------------- 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 CVC4 diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h index d4f433daf..774177d66 100644 --- a/src/expr/proof_node_manager.h +++ b/src/expr/proof_node_manager.h @@ -73,6 +73,52 @@ class ProofNodeManager const std::vector>& children, const std::vector& 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 mkAssume(Node fact); + /** + * 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. + * + * 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 mkScope(std::shared_ptr pf, + std::vector& assumps, + bool ensureClosed = true, + bool doMinimize = false, + Node expected = Node::null()); + /** * This method updates pn to be a proof of the form ( children, args ), * while maintaining its d_proven field. This method returns false if this @@ -92,6 +138,12 @@ class ProofNodeManager PfRule id, const std::vector>& children, const std::vector& 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; @@ -112,6 +164,18 @@ class ProofNodeManager const std::vector>& children, const std::vector& 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>& children, + const std::vector& args, + bool needsCheck); }; } // namespace CVC4