diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 73 | ||||
-rw-r--r-- | src/proof/proof_node_manager.cpp | 7 | ||||
-rw-r--r-- | src/proof/proof_node_manager.h | 8 |
3 files changed, 84 insertions, 4 deletions
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 6312f3140..ef7735b44 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -55,6 +55,79 @@ bool AletheProofPostprocessCallback::update(Node res, switch (id) { + // To keep the original shape of the proof node it is necessary to rederive + // the original conclusion. However, the term that should be printed might + // be different from that conclusion. Thus, it is stored as an additional + // argument in the proof node. Usually, the only difference is an additional + // cl operator or the outmost or operator being replaced by a cl operator. + // + // When steps are added to the proof that have not been there previously, + // it is unwise to add them in the same manner. To illustrate this the + // following counterexample shows the pitfalls of this approach: + // + // (or a (or b c)) (not a) + // --------------------------- RESOLUTION + // (or b c) + // + // is converted into an Alethe proof that should be printed as + // + // (cl a (or b c)) (cl (not a)) + // -------------------------------- RESOLUTION + // (cl (or b c)) + // --------------- OR + // (cl b c) + // + // Here, (cl (or b c)) and (cl b c) cannot correspond to the same proof node + // (or b c). Thus, we build a new proof node using the kind SEXPR + // that is then printed as (cl (or b c)). We denote this wrapping of a proof + // node by using an extra pair of parenthesis, i.e. ((or b c)) is the proof + // node printed as (cl (or b c)). + // + // + // Some proof rules have a close correspondence in Alethe. There are two + // very frequent patterns that, to avoid repetition, are described here and + // referred to in the comments on the specific proof rules below. + // + // The first pattern, which will be called singleton pattern in the + // following, adds the original proof node F with the corresponding rule R' + // of the Alethe calculus and uses the same premises as the original proof + // node (P1:F1) ... (Pn:Fn). However, the conclusion is printed as (cl F). + // + // This means a cvc5 rule R that looks as follows: + // + // (P1:F1) ... (Pn:Fn) + // --------------------- R + // F + // + // is transformed into: + // + // (P1:F1) ... (Pn:Fn) + // --------------------- R' + // (cl F)* + // + // * the corresponding proof node is F + // + // The second pattern, which will be called clause pattern in the following, + // has a disjunction (or G1 ... Gn) as conclusion. It also adds the orignal + // proof node (or G1 ... Gn) with the corresponding rule R' of the Alethe + // calculus and uses the same premises as the original proof node (P1:F1) + // ... (Pn:Fn). However, the conclusion is printed as (cl G1 ... Gn), i.e. + // the or is replaced by the cl operator. + // + // This means a cvc5 rule R that looks as follows: + // + // (P1:F1) ... (Pn:Fn) + // --------------------- R + // (or G1 ... Gn) + // + // Is transformed into: + // + // (P1:F1) ... (Pn:Fn) + // --------------------- R' + // (cl G1 ... Gn)* + // + // * the corresponding proof node is (or G1 ... Gn) + // //================================================= Core rules //======================== Assume and Scope case PfRule::ASSUME: diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp index a3ef944e0..8b4b332a1 100644 --- a/src/proof/proof_node_manager.cpp +++ b/src/proof/proof_node_manager.cpp @@ -28,7 +28,8 @@ using namespace cvc5::kind; namespace cvc5 { -ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc) +ProofNodeManager::ProofNodeManager(theory::Rewriter* rr, ProofChecker* pc) + : d_rewriter(rr), d_checker(pc) { d_true = NodeManager::currentNM()->mkConst(true); // we always allocate a proof checker, regardless of the proof checking mode @@ -160,14 +161,14 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope( computedAcr = true; for (const Node& acc : ac) { - Node accr = theory::Rewriter::rewrite(acc); + Node accr = d_rewriter->rewrite(acc); if (accr != acc) { acr[accr] = acc; } } } - Node ar = theory::Rewriter::rewrite(a); + Node ar = d_rewriter->rewrite(a); std::unordered_map<Node, Node>::iterator itr = acr.find(ar); if (itr != acr.end()) { diff --git a/src/proof/proof_node_manager.h b/src/proof/proof_node_manager.h index 928aabb76..533f6d173 100644 --- a/src/proof/proof_node_manager.h +++ b/src/proof/proof_node_manager.h @@ -28,6 +28,10 @@ namespace cvc5 { class ProofChecker; class ProofNode; +namespace theory { +class Rewriter; +} + /** * A manager for proof node objects. This is a trusted interface for creating * and updating ProofNode objects. @@ -54,7 +58,7 @@ class ProofNode; class ProofNodeManager { public: - ProofNodeManager(ProofChecker* pc = nullptr); + ProofNodeManager(theory::Rewriter* rr, ProofChecker* pc = nullptr); ~ProofNodeManager() {} /** * This constructs a ProofNode with the given arguments. The expected @@ -184,6 +188,8 @@ class ProofNodeManager static ProofNode* cancelDoubleSymm(ProofNode* pn); private: + /** The rewriter */ + theory::Rewriter* d_rewriter; /** The (optional) proof checker */ ProofChecker* d_checker; /** the true node */ |