Branch data     Line data    Source code

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