src/smt/proof_manager.h

   1 /*********************                                                        */
   2 /*! \file proof_manager.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   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 proof manager of SmtEngine
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__SMT__PROOF_MANAGER_H
  18 #define CVC4__SMT__PROOF_MANAGER_H
  19
  20 #include "context/cdhashmap.h"
  21 #include "context/cdlist.h"
  22 #include "expr/node.h"
  23 #include "expr/proof_checker.h"
  24 #include "expr/proof_node.h"
  25 #include "expr/proof_node_manager.h"
  26 #include "smt/preprocess_proof_generator.h"
  27 #include "smt/proof_post_processor.h"
  28
  29 namespace CVC4 {
  30
  31 class SmtEngine;
  32
  33 namespace smt {
  34
  35 class Assertions;
  36 class DefinedFunction;
  37
  38 /**
  39  * This class is responsible for managing the proof output of SmtEngine, as
  40  * well as setting up the global proof checker and proof node manager.
  41  */
  42 class PfManager
  43 {
  44   /** The type of our internal map of defined functions */
  45   using DefinedFunctionMap =
  46       context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>;
  47
  48  public:
  49   PfManager(context::UserContext* u, SmtEngine* smte);
  50   ~PfManager();
  51   /**
  52    * Print the proof on the output channel of the current options in scope.
  53    *
  54    * The argument pfn is the proof for false in the current context.
  55    *
  56    * Throws an assertion failure if pg cannot provide a closed proof with
  57    * respect to assertions in as and df. For the latter, entries in the defined
  58    * function map correspond to equalities of the form (= f (lambda (...) t)),
  59    * which are considered assertions in the final proof.
  60    */
  61   void printProof(std::shared_ptr<ProofNode> pfn,
  62                   Assertions& as,
  63                   DefinedFunctionMap& df);
  64   /**
  65    * Check proof, same as above, without printing.
  66    */
  67   void checkProof(std::shared_ptr<ProofNode> pfn,
  68                   Assertions& as,
  69                   DefinedFunctionMap& df);
  70
  71   /**
  72    * Get final proof.
  73    *
  74    * The argument pfn is the proof for false in the current context.
  75    */
  76   std::shared_ptr<ProofNode> getFinalProof(std::shared_ptr<ProofNode> pfn,
  77                                            Assertions& as,
  78                                            DefinedFunctionMap& df);
  79   //--------------------------- access to utilities
  80   /** Get a pointer to the ProofChecker owned by this. */
  81   ProofChecker* getProofChecker() const;
  82   /** Get a pointer to the ProofNodeManager owned by this. */
  83   ProofNodeManager* getProofNodeManager() const;
  84   /** Get the proof generator for proofs of preprocessing. */
  85   smt::PreprocessProofGenerator* getPreprocessProofGenerator() const;
  86   //--------------------------- end access to utilities
  87  private:
  88   /**
  89    * Set final proof, which initializes d_finalProof to the given proof node of
  90    * false, postprocesses it, and stores it in d_finalProof.
  91    */
  92   void setFinalProof(std::shared_ptr<ProofNode> pfn,
  93                      Assertions& as,
  94                      DefinedFunctionMap& df);
  95   /**
  96    * Get assertions from the assertions
  97    */
  98   void getAssertions(Assertions& as,
  99                      DefinedFunctionMap& df,
 100                      std::vector<Node>& assertions);
 101   /** The false node */
 102   Node d_false;
 103   /** For the new proofs module */
 104   std::unique_ptr<ProofChecker> d_pchecker;
 105   /** A proof node manager based on the above checker */
 106   std::unique_ptr<ProofNodeManager> d_pnm;
 107   /** The preprocess proof generator. */
 108   std::unique_ptr<smt::PreprocessProofGenerator> d_pppg;
 109   /** The proof post-processor */
 110   std::unique_ptr<smt::ProofPostproccess> d_pfpp;
 111   /**
 112    * The final proof produced by the SMT engine.
 113    * Combines the proofs of preprocessing, prop engine and theory engine, to be
 114    * connected by setFinalProof().
 115    */
 116   std::shared_ptr<ProofNode> d_finalProof;
 117 }; /* class SmtEngine */
 118
 119 }  // namespace smt
 120 }  // namespace CVC4
 121
 122 #endif /* CVC4__SMT__PROOF_MANAGER_H */