Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Proof logger utility.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__SMT__PROOF_LOGGER_H
      16                 :            : #define CVC5__SMT__PROOF_LOGGER_H
      17                 :            : 
      18                 :            : #include "proof/eo/eo_node_converter.h"
      19                 :            : #include "proof/eo/eo_printer.h"
      20                 :            : #include "proof/proof_node.h"
      21                 :            : #include "smt/env_obj.h"
      22                 :            : 
      23                 :            : namespace cvc5::internal {
      24                 :            : 
      25                 :            : namespace smt {
      26                 :            : class Assertions;
      27                 :            : class PfManager;
      28                 :            : class ProofPostprocess;
      29                 :            : }  // namespace smt
      30                 :            : 
      31                 :            : /**
      32                 :            :  * The purpose of this class is to output proofs for all reasoning the solver
      33                 :            :  * does on-the-fly. It is enabled when proof logging is enabled.
      34                 :            :  *
      35                 :            :  * This class receives notifications for three things:
      36                 :            :  * (1) When preprocessing has completed, determining the set of input clauses.
      37                 :            :  * (2) When theory lemmas are learned
      38                 :            :  * (3) When a SAT refutation is derived.
      39                 :            :  * 
      40                 :            :  * Dependending on the proof mode, the notifications for the above three things
      41                 :            :  * may be in the form of ProofNode (if proofs are enabled for that component),
      42                 :            :  * or Node (if proofs are disabled for that component).
      43                 :            :  * 
      44                 :            :  * As with dumped proofs, the granularity of the proofs is subject to the
      45                 :            :  * option `proof-granularity`.
      46                 :            :  */
      47                 :            : class ProofLogger : protected EnvObj
      48                 :            : {
      49                 :            :  public:
      50                 :            :   /** */
      51                 :          0 :   ProofLogger(Env& env) : EnvObj(env){}
      52                 :          0 :   ~ProofLogger(){}
      53                 :            :   /**
      54                 :            :    * Called when preprocessing is complete with the list of input clauses,
      55                 :            :    * after preprocessing and conversion to CNF.
      56                 :            :    * @param input The list of input clauses.
      57                 :            :    */
      58                 :          0 :   virtual void logCnfPreprocessInputs(
      59                 :            :       CVC5_UNUSED const std::vector<Node>& inputs)
      60                 :            :   {
      61                 :          0 :   }
      62                 :            :   /**
      63                 :            :    * Called when preprocessing is complete with the proofs of the preprocessed
      64                 :            :    * inputs. The free assumptions of proofs in pfns are the preprocessed input
      65                 :            :    * formulas. If preprocess proofs are avialable, this method connects pfn to
      66                 :            :    * the original input formulas.
      67                 :            :    * @param pfns Proofs of the preprocessed inputs.
      68                 :            :    */
      69                 :          0 :   virtual void logCnfPreprocessInputProofs(
      70                 :            :       CVC5_UNUSED std::vector<std::shared_ptr<ProofNode>>& pfns)
      71                 :            :   {
      72                 :          0 :   }
      73                 :            :   /**
      74                 :            :    * Called when clause `n` is added to the SAT solver, where `n` is
      75                 :            :    * (the CNF conversion of) a theory lemma.
      76                 :            :    * @param n The theory lemma.
      77                 :            :    */
      78                 :          0 :   virtual void logTheoryLemma(CVC5_UNUSED const Node& n) {}
      79                 :            :   /**
      80                 :            :    * Called when clause `pfn` is added to the SAT solver, where `pfn`
      81                 :            :    * is a closed proof of (the CNF conversion of) a theory lemma.
      82                 :            :    * @param pfn The closed proof of a theory lemma.
      83                 :            :    */
      84                 :          0 :   virtual void logTheoryLemmaProof(CVC5_UNUSED std::shared_ptr<ProofNode>& pfn)
      85                 :            :   {
      86                 :          0 :   }
      87                 :            :   /**
      88                 :            :    * Called when the SAT solver derives false. The SAT refutation should be
      89                 :            :    * derivable by propositional reasoning via the notified preprocessed input
      90                 :            :    * and theory lemmas as given above.
      91                 :            :    */
      92                 :          0 :   virtual void logSatRefutation() {}
      93                 :            : 
      94                 :            :   /**
      95                 :            :    * Called when the SAT solver generates a proof of false. The free assumptions
      96                 :            :    * of this proof is the union of the CNF conversion of input and theory lemmas
      97                 :            :    * as notified above.
      98                 :            :    * @param pfn The refutation proof.
      99                 :            :    */
     100                 :          0 :   virtual void logSatRefutationProof(
     101                 :            :       CVC5_UNUSED std::shared_ptr<ProofNode>& pfn)
     102                 :            :   {
     103                 :          0 :   }
     104                 :            : };
     105                 :            : 
     106                 :            : /**
     107                 :            :  * The default implementation of a proof logger, which prints proofs in the
     108                 :            :  * CPC format.
     109                 :            :  */
     110                 :            : class ProofLoggerCpc : public ProofLogger
     111                 :            : {
     112                 :            :  public:
     113                 :            :   /** */
     114                 :            :   ProofLoggerCpc(Env& env,
     115                 :            :                  std::ostream& out,
     116                 :            :                  smt::PfManager* pm,
     117                 :            :                  smt::Assertions& as);
     118                 :            :   ~ProofLoggerCpc();
     119                 :            :   /** Log preprocessing input */
     120                 :            :   void logCnfPreprocessInputs(const std::vector<Node>& inputs) override;
     121                 :            :   /** Log preprocessing input proof */
     122                 :            :   void logCnfPreprocessInputProofs(
     123                 :            :       std::vector<std::shared_ptr<ProofNode>>& pfns) override;
     124                 :            :   /** Log theory lemma */
     125                 :            :   void logTheoryLemma(const Node& n) override;
     126                 :            :   /** Log theory lemma proof */
     127                 :            :   void logTheoryLemmaProof(std::shared_ptr<ProofNode>& pfn) override;
     128                 :            :   /** Log SAT refutation */
     129                 :            :   void logSatRefutation() override;
     130                 :            :   /** Log SAT refutation proof */
     131                 :            :   void logSatRefutationProof(std::shared_ptr<ProofNode>& pfn) override;
     132                 :            : 
     133                 :            :  private:
     134                 :            :   /** Pointer to the proof manager, for connecting proofs to inputsw */
     135                 :            :   smt::PfManager* d_pm;
     136                 :            :   /** Pointer to the proof node manager */
     137                 :            :   ProofNodeManager* d_pnm;
     138                 :            :   /** Reference to the assertions of SMT solver */
     139                 :            :   smt::Assertions& d_as;
     140                 :            :   /** The node converter, used for printing */
     141                 :            :   proof::EoNodeConverter d_atp;
     142                 :            :   /** The proof printer */
     143                 :            :   proof::EoPrinter d_eop;
     144                 :            :   /** The output channel we are using */
     145                 :            :   proof::EoPrintChannelOut d_eout;
     146                 :            :   /** The preprocessing proof we were notified of, which we may have created */
     147                 :            :   std::shared_ptr<ProofNode> d_ppProof;
     148                 :            :   /**
     149                 :            :    * The list of theory lemma proofs we were notified of, which we may have
     150                 :            :    * created.
     151                 :            :    */
     152                 :            :   std::vector<std::shared_ptr<ProofNode>> d_lemmaPfs;
     153                 :            : };
     154                 :            : 
     155                 :            : }  // namespace cvc5::internal
     156                 :            : 
     157                 :            : #endif /* CVC5__PROOF__PROOF_LOGGER_H */