From 5c4b9e1a6ffa97a0a1f8af41069f29764eb6c74b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 5 Jun 2020 15:52:30 -0500 Subject: [PATCH] (proof-new) Updates to CDProof (#4565) This updates CDProof with several new functionalities, including making it agnostic to symmetry of (dis)equalites. --- src/expr/proof.cpp | 325 +++++++++++++++++++++++++++++--- src/expr/proof.h | 132 ++++++++++--- src/expr/proof_node_manager.cpp | 2 + src/expr/proof_node_manager.h | 2 + 4 files changed, 410 insertions(+), 51 deletions(-) diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp index eff222b92..f9e50c0f4 100644 --- a/src/expr/proof.cpp +++ b/src/expr/proof.cpp @@ -18,6 +18,18 @@ using namespace CVC4::kind; namespace CVC4 { +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; +} + CDProof::CDProof(ProofNodeManager* pnm, context::Context* c) : d_manager(pnm), d_context(), d_nodes(c ? c : &d_context) { @@ -25,6 +37,22 @@ CDProof::CDProof(ProofNodeManager* pnm, context::Context* c) CDProof::~CDProof() {} +std::shared_ptr CDProof::mkProof(Node fact) +{ + std::shared_ptr pf = getProofSymm(fact); + if (pf != nullptr) + { + return pf; + } + // add as assumption + std::vector pargs = {fact}; + std::vector> passume; + std::shared_ptr pfa = + d_manager->mkNode(PfRule::ASSUME, passume, pargs, fact); + d_nodes.insert(fact, pfa); + return pfa; +} + std::shared_ptr CDProof::getProof(Node fact) const { NodeProofNodeMap::iterator it = d_nodes.find(fact); @@ -35,42 +63,100 @@ std::shared_ptr CDProof::getProof(Node fact) const return nullptr; } +std::shared_ptr CDProof::getProofSymm(Node fact) +{ + Trace("cdproof") << "CDProof::getProofSymm: " << fact << std::endl; + std::shared_ptr pf = getProof(fact); + if (pf != nullptr && !isAssumption(pf.get())) + { + Trace("cdproof") << "...existing non-assume " << pf->getRule() << 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 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> pschild; + pschild.push_back(pfs); + std::vector args; + if (pf == nullptr) + { + Trace("cdproof") << "...fresh make symm" << std::endl; + std::shared_ptr 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& children, const std::vector& args, bool ensureChildren, - bool forceOverwrite) + CDPOverwrite opolicy) { - // we must provide expected + Trace("cdproof") << "CDProof::addStep: " << id << " " << expected + << ", ensureChildren = " << ensureChildren + << ", overwrite policy = " << opolicy << std::endl; + // We must always provide expected to this method Assert(!expected.isNull()); - NodeProofNodeMap::iterator it = d_nodes.find(expected); - if (it != d_nodes.end()) + std::shared_ptr pprev = getProofSymm(expected); + if (pprev != nullptr) { - if (!forceOverwrite - && ((*it).second->getRule() != PfRule::ASSUME || id == PfRule::ASSUME)) + if (!shouldOverwrite(pprev.get(), id, opolicy)) { - // we do not overwrite if forceOverwrite is false and the previously - // provided step was not an assumption, or if the currently provided step - // is a (duplicate) assumption + // 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> pchildren; for (const Node& c : children) { - std::shared_ptr pc = getProof(c); + Trace("cdproof") << "- get child " << c << std::endl; + std::shared_ptr 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 pcargs = {c}; std::vector> pcassume; @@ -82,37 +168,150 @@ bool CDProof::addStep(Node expected, 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 pthis; - if (it == d_nodes.end()) + 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 = (*it).second; - d_manager->updateNode(pthis.get(), id, pchildren, args); + 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) +{ + // 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 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 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>& steps = psb.getSteps(); + for (const std::pair& ps : steps) + { + if (!addStep(ps.first, ps.second, ensureChildren, opolicy)) + { + return false; + } } - // the result of the proof node should be expected - Assert(pthis->getResult() == expected); return true; } -bool CDProof::addProof(ProofNode* pn, bool forceOverwrite) +bool CDProof::addProof(std::shared_ptr 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 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 visited; std::unordered_map::iterator it; std::vector visit; ProofNode* cur; Node curFact; - visit.push_back(pn); + visit.push_back(pn.get()); bool retValue = true; do { @@ -143,12 +342,8 @@ bool CDProof::addProof(ProofNode* pn, bool forceOverwrite) pexp.push_back(c->getResult()); } // can ensure children at this point - bool res = addStep(curFact, - cur->getRule(), - pexp, - cur->getArguments(), - true, - forceOverwrite); + bool res = addStep( + curFact, cur->getRule(), pexp, cur->getArguments(), true, opolicy); // should always succeed Assert(res); retValue = retValue && res; @@ -159,4 +354,86 @@ bool CDProof::addProof(ProofNode* pn, bool forceOverwrite) return retValue; } +bool CDProof::hasStep(Node fact) +{ + std::shared_ptr pf = getProof(fact); + if (pf != nullptr && !isAssumption(pf.get())) + { + return true; + } + 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>& 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][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(); +} + } // namespace CVC4 diff --git a/src/expr/proof.h b/src/expr/proof.h index c3b9698ca..94a3b6ab0 100644 --- a/src/expr/proof.h +++ b/src/expr/proof.h @@ -24,9 +24,23 @@ #include "expr/node.h" #include "expr/proof_node.h" #include "expr/proof_node_manager.h" +#include "expr/proof_step_buffer.h" namespace CVC4 { +/** An overwrite policy for CDProof below */ +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); + /** * A (context-dependent) proof. * @@ -76,10 +90,11 @@ namespace CVC4 { * Notice that the proof of A by ID_A was not overwritten by ASSUME in the * addStep call above. * - * The policy for overwriting proof steps 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 forceOverwrite is true. + * 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 {}, {} ) @@ -87,7 +102,7 @@ namespace CVC4 { * At this point, getProof( A ) returns: * ID_A1( ID_B1(), ASSUME(C) ) * Now, assume an additional call is made to addProof, where notice - * forceOverwrite is false by default: + * 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: @@ -114,22 +129,39 @@ namespace CVC4 { * 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 { - typedef context::CDHashMap, NodeHashFunction> - NodeProofNodeMap; - public: CDProof(ProofNodeManager* pnm, context::Context* c = nullptr); - ~CDProof(); + virtual ~CDProof(); /** - * Get proof for fact, or nullptr if it does not exist. 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. + * 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 getProof(Node fact) const; + virtual std::shared_ptr mkProof(Node fact); /** Add step * * @param expected The intended conclusion of this proof step. This must be @@ -141,8 +173,8 @@ class CDProof * @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 forceOverwrite Whether we wish to overwrite if a step for expected - * was already provided (via a previous call to addStep) + * @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 @@ -156,39 +188,85 @@ class CDProof * of order. * * This method only overwrites proofs for facts that were added as - * steps with id ASSUME when forceOverwrite is false, and otherwise always - * overwrites an existing step if one was provided when forceOverwrite is - * true. + * 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& children, const std::vector& args, bool ensureChildren = false, - bool forceOverwrite = 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 forceOverwrite Whether we wish to force overwriting if a step was - * already provided, for each node in the proof. + * @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. * - * 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 does not impact the - * internal data of this 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(ProofNode* pn, bool forceOverwrite = false); + bool addProof(std::shared_ptr 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 symmetric fact (a g such that isSame returns true for isSame(f,g)), or + * null if none exist. + */ + static Node getSymmFact(TNode f); protected: + typedef context::CDHashMap, NodeHashFunction> + 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; + /** Get proof for fact, or nullptr if it does not exist. */ + std::shared_ptr getProof(Node fact) const; + /** Ensure fact sym */ + std::shared_ptr 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 CVC4 diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index e2f5ca2dc..b4775d915 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -86,4 +86,6 @@ Node ProofNodeManager::checkInternal( return res; } +ProofChecker* ProofNodeManager::getChecker() const { return d_checker; } + } // namespace CVC4 diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h index 17c5580bf..107223692 100644 --- a/src/expr/proof_node_manager.h +++ b/src/expr/proof_node_manager.h @@ -92,6 +92,8 @@ class ProofNodeManager PfRule id, const std::vector>& children, const std::vector& args); + /** Get the underlying proof checker */ + ProofChecker* getChecker() const; private: /** The (optional) proof checker */ -- 2.30.2