src/proof/alethe/alethe_post_processor.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Hanna Lachnitt, Haniel Barbosa
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * The module for processing proof nodes into Alethe proof nodes
  14  */
  15
  16 #ifndef CVC4__PROOF__ALETHE_PROOF_PROCESSOR_H
  17 #define CVC4__PROOF__ALETHE_PROOF_PROCESSOR_H
  18
  19 #include "proof/proof_node_updater.h"
  20 #include "proof/alethe/alethe_node_converter.h"
  21 #include "proof/alethe/alethe_proof_rule.h"
  22
  23 namespace cvc5 {
  24
  25 namespace proof {
  26
  27 /**
  28  * A callback class used by the Alethe converter for post-processing proof nodes
  29  * by replacing internal rules by the rules in the Alethe calculus.
  30  */
  31 class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback
  32 {
  33  public:
  34   AletheProofPostprocessCallback(ProofNodeManager* pnm,
  35                                  AletheNodeConverter& anc);
  36   ~AletheProofPostprocessCallback() {}
  37   /** Should proof pn be updated? Only if its top-level proof rule is not an
  38    *  Alethe proof rule.
  39    */
  40   bool shouldUpdate(std::shared_ptr<ProofNode> pn,
  41                     const std::vector<Node>& fa,
  42                     bool& continueUpdate) override;
  43   /**
  44    * This method updates the proof rule application depending on the given
  45    * rule and translating it into a proof node in terms of the Alethe rules.
  46    */
  47   bool update(Node res,
  48               PfRule id,
  49               const std::vector<Node>& children,
  50               const std::vector<Node>& args,
  51               CDProof* cdp,
  52               bool& continueUpdate) override;
  53
  54  private:
  55   /** The proof node manager */
  56   ProofNodeManager* d_pnm;
  57   /** The Alethe node converter */
  58   AletheNodeConverter& d_anc;
  59   /** The cl operator
  60    * For every step the conclusion is a clause. But since the or operator
  61    *requires at least two arguments it is extended by the cl operator. In case
  62    *of more than one argument it corresponds to or otherwise it is the identity.
  63    **/
  64   Node d_cl;
  65   /**
  66    * This method adds a new ALETHE_RULE step to the proof, with `rule` as the
  67    * first argument, the original conclusion `res` as the second and
  68    * `conclusion`, the result to be printed (which may or may not differ from
  69    * `res`), as the third.
  70    *
  71    * @param rule The id of the Alethe rule,
  72    * @param res The expected result of the application,
  73    * @param conclusion The conclusion to be printed for the step
  74    * @param children The children of the application,
  75    * @param args The arguments of the application
  76    * @param cdp The proof to add to
  77    * @return True if the step could be added, or false if not.
  78    */
  79   bool addAletheStep(AletheRule rule,
  80                      Node res,
  81                      Node conclusion,
  82                      const std::vector<Node>& children,
  83                      const std::vector<Node>& args,
  84                      CDProof& cdp);
  85   /**
  86    * As above, but for proof nodes with original conclusions of the form `(or F1
  87    * ... Fn)` whose conclusion-to-be-printed must be `(cl F1 ... Fn)`.
  88    *
  89    * This method internally calls addAletheStep. The kind of the given Node has
  90    * to be OR.
  91    *
  92    * @param res The expected result of the application in form (or F1 ... Fn),
  93    * @param rule The id of the Alethe rule,
  94    * @param children The children of the application,
  95    * @param args The arguments of the application
  96    * @param cdp The proof to add to
  97    * @return True if the step could be added, or false if not.
  98    */
  99   bool addAletheStepFromOr(Node res,
 100                            AletheRule rule,
 101                            const std::vector<Node>& children,
 102                            const std::vector<Node>& args,
 103                            CDProof& cdp);
 104 };
 105
 106 /**
 107  * Final callback class used by the Alethe converter to add the last step to a
 108  * proof in the following two cases. The last step should always be printed as
 109  * (cl).
 110  *
 111  * 1. If the last step of a proof which is false is reached it is printed as (cl
 112  *    false).
 113  * 2. If one of the assumptions is false it is printed as false.
 114  *
 115  * Thus, an additional resolution step with (cl (not true)) has to be added to
 116  * transfer (cl false) into (cl).
 117  */
 118 class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
 119 {
 120  public:
 121    AletheProofPostprocessFinalCallback(ProofNodeManager* pnm,
 122                                        AletheNodeConverter& anc);
 123   ~AletheProofPostprocessFinalCallback() {}
 124   /** Should proof pn be updated? It should, if the last step is printed as (cl
 125    * false) or if it is an assumption (in that case it is printed as false).
 126    * Since the proof node should not be traversed, this method will always set
 127    * continueUpdate to false.
 128    */
 129   bool shouldUpdate(std::shared_ptr<ProofNode> pn,
 130                     const std::vector<Node>& fa,
 131                     bool& continueUpdate) override;
 132   /**
 133    * This method gets a proof node pn. If the last step of the proof is false
 134    * which is printed as (cl false) it updates the proof for false such that
 135    * (cl) is printed instead.
 136    */
 137   bool update(Node res,
 138               PfRule id,
 139               const std::vector<Node>& children,
 140               const std::vector<Node>& args,
 141               CDProof* cdp,
 142               bool& continueUpdate) override;
 143
 144  private:
 145   /** The proof node manager */
 146   ProofNodeManager* d_pnm;
 147   /** The Alethe node converter */
 148   AletheNodeConverter& d_anc;
 149   /** The cl operator is defined as described in the
 150    * AletheProofPostprocessCallback class above
 151    **/
 152   Node d_cl;
 153 };
 154
 155 /**
 156  * The proof postprocessor module. This postprocesses a proof node into one
 157  * using the rules from the Alethe calculus.
 158  */
 159 class AletheProofPostprocess
 160 {
 161  public:
 162    AletheProofPostprocess(ProofNodeManager* pnm, AletheNodeConverter& anc);
 163   ~AletheProofPostprocess();
 164   /** post-process */
 165   void process(std::shared_ptr<ProofNode> pf);
 166
 167  private:
 168   /** The proof node manager */
 169   ProofNodeManager* d_pnm;
 170   /** The post process callback */
 171   AletheProofPostprocessCallback d_cb;
 172   /** The final post process callback */
 173   AletheProofPostprocessFinalCallback d_fcb;
 174 };
 175
 176 }  // namespace proof
 177
 178 }  // namespace cvc5
 179
 180 #endif