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)
{
CDProof::~CDProof() {}
+std::shared_ptr<ProofNode> CDProof::mkProof(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);
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;
+ }
+ 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,
- 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<ProofNode> 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<std::shared_ptr<ProofNode>> pchildren;
for (const Node& c : children)
{
- std::shared_ptr<ProofNode> pc = getProof(c);
+ 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;
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 (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<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;
+ }
}
- // 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<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);
+ visit.push_back(pn.get());
bool retValue = true;
do
{
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;
return retValue;
}
+bool CDProof::hasStep(Node fact)
+{
+ std::shared_ptr<ProofNode> 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<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][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
#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.
*
* 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 {}, {} )
* 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:
* 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<Node, std::shared_ptr<ProofNode>, 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<ProofNode> getProof(Node fact) const;
+ virtual std::shared_ptr<ProofNode> mkProof(Node fact);
/** Add step
*
* @param expected The intended conclusion of this proof step. This must be
* @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
* 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<Node>& children,
const std::vector<Node>& 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<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 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<Node, std::shared_ptr<ProofNode>, 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<ProofNode> getProof(Node fact) const;
+ /** 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 CVC4
projects / cvc5.git / commitdiff