src/prop/proof_post_processor.h

   1 /*********************                                                        */
   2 /*! \file proof_post_processor.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Haniel Barbosa
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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.\endverbatim
  11  **
  12  ** \brief The module for processing proof nodes in the prop engine
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__PROP__PROOF_POST_PROCESSOR_H
  18 #define CVC4__PROP__PROOF_POST_PROCESSOR_H
  19
  20 #include <map>
  21 #include <unordered_set>
  22
  23 #include "expr/proof_node_updater.h"
  24 #include "prop/proof_cnf_stream.h"
  25
  26 namespace CVC4 {
  27
  28 namespace prop {
  29
  30 /**
  31  * A callback class used by PropEngine for post-processing proof nodes by
  32  * connecting proofs of resolution, whose leaves are clausified preprocessed
  33  * assertions and lemmas, with the CNF transformation of these formulas, while
  34  * expanding the generators of lemmas.
  35  */
  36 class ProofPostprocessCallback : public ProofNodeUpdaterCallback
  37 {
  38  public:
  39   ProofPostprocessCallback(ProofNodeManager* pnm,
  40                            ProofCnfStream* proofCnfStream);
  41   ~ProofPostprocessCallback() {}
  42   /**
  43    * Initialize, called once for each new ProofNode to process. This initializes
  44    * static information to be used by successive calls to update. For this
  45    * callback it resets d_assumpToProof.
  46    */
  47   void initializeUpdate();
  48   /** Should proof pn be updated?
  49    *
  50    * For this callback a proof node is updatable if it's an assumption for which
  51    * the proof cnf straem has a proof. However if the proof node is blocked
  52    * (which is the case for proof nodes introduced into the proof cnf stream's
  53    * proof via expansion of its generators) then traversal is the proof node is
  54    * cancelled, i.e., continueUpdate is set to false.
  55    */
  56   bool shouldUpdate(std::shared_ptr<ProofNode> pn,
  57                     bool& continueUpdate) override;
  58   /** Update the proof rule application.
  59    *
  60    * Replaces assumptions by their proof in proof cnf stream. Note that in doing
  61    * this the proof node is blocked, so that future post-processing does not
  62    * traverse it.
  63    *
  64    * This method uses the cache in d_assumpToProof to avoid recomputing proofs
  65    * for the same assumption (in the same scope).
  66    */
  67   bool update(Node res,
  68               PfRule id,
  69               const std::vector<Node>& children,
  70               const std::vector<Node>& args,
  71               CDProof* cdp,
  72               bool& continueUpdate) override;
  73
  74  private:
  75   /** The proof node manager */
  76   ProofNodeManager* d_pnm;
  77   /** The cnf stream proof generator */
  78   ProofCnfStream* d_proofCnfStream;
  79   //---------------------------------reset at the begining of each update
  80   /** Mapping assumptions to their proof from cnf transformation */
  81   std::map<Node, std::shared_ptr<ProofNode> > d_assumpToProof;
  82   //---------------------------------end reset at the begining of each update
  83 };
  84
  85 /**
  86  * The proof postprocessor module. This postprocesses the refutation proof
  87  * produced by the SAT solver. Its main task is to connect the refutation's
  88  * assumptions to the CNF transformation proof in ProofCnfStream.
  89  */
  90 class ProofPostproccess
  91 {
  92  public:
  93   ProofPostproccess(ProofNodeManager* pnm, ProofCnfStream* proofCnfStream);
  94   ~ProofPostproccess();
  95   /** post-process
  96    *
  97    * The post-processing is done via a proof node updater run on pf with this
  98    * class's callback d_cb.
  99    */
 100   void process(std::shared_ptr<ProofNode> pf);
 101
 102  private:
 103   /** The post process callback */
 104   ProofPostprocessCallback d_cb;
 105   /** The proof node manager */
 106   ProofNodeManager* d_pnm;
 107 };
 108
 109 }  // namespace prop
 110 }  // namespace CVC4
 111
 112 #endif