diff options
Diffstat (limited to 'src/expr/proof.h')
| -rw-r--r-- | src/expr/proof.h | 132 |
1 files changed, 105 insertions, 27 deletions
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<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 @@ -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<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 |