src/smt/proof_manager.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Gereon Kremer, 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 proof manager of SmtEngine.
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__SMT__PROOF_MANAGER_H
  19 #define CVC5__SMT__PROOF_MANAGER_H
  20
  21 #include "context/cdhashmap.h"
  22 #include "expr/node.h"
  23 #include "smt/env_obj.h"
  24
  25 namespace cvc5 {
  26
  27 class ProofChecker;
  28 class ProofNode;
  29 class ProofNodeManager;
  30 class SmtEngine;
  31
  32 namespace rewriter {
  33 class RewriteDb;
  34 }
  35
  36 namespace smt {
  37
  38 class Assertions;
  39 class PreprocessProofGenerator;
  40 class ProofPostproccess;
  41
  42 /**
  43  * This class is responsible for managing the proof output of SmtEngine, as
  44  * well as setting up the global proof checker and proof node manager.
  45  *
  46  * The proof production of an SmtEngine is directly impacted by whether, and
  47  * how, we are producing unsat cores:
  48  *
  49  * - If we are producing unsat cores using the old proof infrastructure, then
  50  *   SmtEngine will not have proofs in the sense of this proof manager.
  51  *
  52  * - If we are producing unsat cores using this proof infrastructure, then the
  53  *   SmtEngine will have proofs using this proof manager, according to the unsat
  54  *   core mode:
  55  *
  56  *   - assumption mode: proofs only for preprocessing, not in sat solver or
  57  *   theory engine, and level of granularity set to off (unless otherwise
  58  *   specified by the user)
  59  *
  60  *   - sat-proof mode: proofs for preprocessing + sat solver, not in theory
  61  *   engine and level of granularity set to off (unless otherwise specified by
  62  *   the user)
  63  *
  64  *   - full-proof mode: proofs for the whole solver as normal
  65  *
  66  *   Note that if --produce-proofs is set then full-proof mode of unsat cores is
  67  *   forced.
  68  *
  69  * - If we are not producing unsat cores then the SmtEngine will have proofs as
  70  *   long as --produce-proofs is on.
  71  *
  72  * - If SmtEngine has been configured in a way that is incompatible with proofs
  73  *   then unsat core production will be disabled.
  74  */
  75 class PfManager : protected EnvObj
  76 {
  77  public:
  78   PfManager(Env& env);
  79   ~PfManager();
  80   /**
  81    * Print the proof on the given output stream.
  82    *
  83    * The argument pfn is the proof for false in the current context.
  84    *
  85    * Throws an assertion failure if pg cannot provide a closed proof with
  86    * respect to assertions in as. Note this includes equalities of the form
  87    * (= f (lambda (...) t)) which originate from define-fun commands for f.
  88    * These are considered assertions in the final proof.
  89    */
  90   void printProof(std::ostream& out,
  91                   std::shared_ptr<ProofNode> pfn,
  92                   Assertions& as);
  93   /**
  94    * Check proof, same as above, without printing.
  95    */
  96   void checkProof(std::shared_ptr<ProofNode> pfn, Assertions& as);
  97
  98   /**
  99    * Get final proof.
 100    *
 101    * The argument pfn is the proof for false in the current context.
 102    */
 103   std::shared_ptr<ProofNode> getFinalProof(std::shared_ptr<ProofNode> pfn,
 104                                            Assertions& as);
 105   //--------------------------- access to utilities
 106   /** Get a pointer to the ProofChecker owned by this. */
 107   ProofChecker* getProofChecker() const;
 108   /** Get a pointer to the ProofNodeManager owned by this. */
 109   ProofNodeManager* getProofNodeManager() const;
 110   /** Get the rewrite database, containing definitions of rewrites from DSL. */
 111   rewriter::RewriteDb* getRewriteDatabase() const;
 112   /** Get the proof generator for proofs of preprocessing. */
 113   smt::PreprocessProofGenerator* getPreprocessProofGenerator() const;
 114   //--------------------------- end access to utilities
 115  private:
 116   /**
 117    * Set final proof, which initializes d_finalProof to the given proof node of
 118    * false, postprocesses it, and stores it in d_finalProof.
 119    */
 120   void setFinalProof(std::shared_ptr<ProofNode> pfn, Assertions& as);
 121   /**
 122    * Get assertions from the assertions
 123    */
 124   void getAssertions(Assertions& as,
 125                      std::vector<Node>& assertions);
 126   /** The false node */
 127   Node d_false;
 128   /** For the new proofs module */
 129   std::unique_ptr<ProofChecker> d_pchecker;
 130   /** A proof node manager based on the above checker */
 131   std::unique_ptr<ProofNodeManager> d_pnm;
 132   /** The preprocess proof generator. */
 133   std::unique_ptr<smt::PreprocessProofGenerator> d_pppg;
 134   /** The proof post-processor */
 135   std::unique_ptr<smt::ProofPostproccess> d_pfpp;
 136
 137   /**
 138    * The final proof produced by the SMT engine.
 139    * Combines the proofs of preprocessing, prop engine and theory engine, to be
 140    * connected by setFinalProof().
 141    */
 142   std::shared_ptr<ProofNode> d_finalProof;
 143 }; /* class SmtEngine */
 144
 145 }  // namespace smt
 146 }  // namespace cvc5
 147
 148 #endif /* CVC5__SMT__PROOF_MANAGER_H */