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 checker utility.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__PROOF__PROOF_CHECKER_H
      16                 :            : #define CVC5__PROOF__PROOF_CHECKER_H
      17                 :            : 
      18                 :            : #include <map>
      19                 :            : 
      20                 :            : #include "expr/node.h"
      21                 :            : #include "options/proof_options.h"
      22                 :            : #include "proof/proof_rule_checker.h"
      23                 :            : #include "util/statistics_stats.h"
      24                 :            : 
      25                 :            : namespace cvc5::internal {
      26                 :            : 
      27                 :            : namespace rewriter {
      28                 :            : class RewriteDb;
      29                 :            : }
      30                 :            : /** Statistics class */
      31                 :            : class ProofCheckerStatistics
      32                 :            : {
      33                 :            :  public:
      34                 :            :   ProofCheckerStatistics(StatisticsRegistry& sr);
      35                 :            :   /** Counts the number of checks for each kind of proof rule */
      36                 :            :   HistogramStat<ProofRule> d_ruleChecks;
      37                 :            :   /** Total number of rule checks */
      38                 :            :   IntStat d_totalRuleChecks;
      39                 :            : };
      40                 :            : 
      41                 :            : /** A class for checking proofs */
      42                 :            : class ProofChecker
      43                 :            : {
      44                 :            :  public:
      45                 :            :   ProofChecker(StatisticsRegistry& sr,
      46                 :            :                options::ProofCheckMode pcMode,
      47                 :            :                uint32_t pclevel = 0,
      48                 :            :                rewriter::RewriteDb* rdb = nullptr);
      49                 :      15191 :   ~ProofChecker() {}
      50                 :            :   /** Reset, which clears the rule checkers */
      51                 :            :   void reset();
      52                 :            :   /**
      53                 :            :    * Return the formula that is proven by proof node pn, or null if pn is not
      54                 :            :    * well-formed. If expected is non-null, then we return null if pn does not
      55                 :            :    * prove expected.
      56                 :            :    *
      57                 :            :    * @param pn The proof node to check
      58                 :            :    * @param expected The (optional) formula that is the expected conclusion of
      59                 :            :    * the proof node.
      60                 :            :    * @return The conclusion of the proof node if successful or null if the
      61                 :            :    * proof is malformed, or if no checker is available for id.
      62                 :            :    */
      63                 :            :   Node check(ProofNode* pn, Node expected = Node::null());
      64                 :            :   /** Same as above, with explicit arguments
      65                 :            :    *
      66                 :            :    * @param id The id of the proof node to check
      67                 :            :    * @param children The children of the proof node to check
      68                 :            :    * @param args The arguments of the proof node to check
      69                 :            :    * @param expected The (optional) formula that is the expected conclusion of
      70                 :            :    * the proof node.
      71                 :            :    * @return The conclusion of the proof node if successful or null if the
      72                 :            :    * proof is malformed, or if no checker is available for id.
      73                 :            :    */
      74                 :            :   Node check(ProofRule id,
      75                 :            :              const std::vector<std::shared_ptr<ProofNode>>& children,
      76                 :            :              const std::vector<Node>& args,
      77                 :            :              Node expected = Node::null());
      78                 :            :   /**
      79                 :            :    * Same as above, without conclusions instead of proof node children. This
      80                 :            :    * is used for debugging. In particular, this function does not throw an
      81                 :            :    * assertion failure when a proof step is malformed and can be used without
      82                 :            :    * constructing proof nodes.
      83                 :            :    *
      84                 :            :    * @param id The id of the proof node to check
      85                 :            :    * @param children The conclusions of the children of the proof node to check
      86                 :            :    * @param args The arguments of the proof node to check
      87                 :            :    * @param expected The (optional) formula that is the expected conclusion of
      88                 :            :    * the proof node.
      89                 :            :    * @param traceTag The trace tag to print debug information to
      90                 :            :    * @return The conclusion of the proof node if successful or null if the
      91                 :            :    * proof is malformed, or if no checker is available for id.
      92                 :            :    */
      93                 :            :   Node checkDebug(ProofRule id,
      94                 :            :                   const std::vector<Node>& cchildren,
      95                 :            :                   const std::vector<Node>& args,
      96                 :            :                   Node expected = Node::null(),
      97                 :            :                   const char* traceTag = "");
      98                 :            :   /** Indicate that psc is the checker for proof rule id */
      99                 :            :   void registerChecker(ProofRule id, ProofRuleChecker* psc);
     100                 :            :   /**
     101                 :            :    * Indicate that id is a trusted rule with the given pedantic level, e.g.:
     102                 :            :    *  0: (mandatory) always a failure to use the given id
     103                 :            :    *  1: (major) failure on all (non-zero) pedantic levels
     104                 :            :    * 10: (minor) failure only on pedantic levels >= 10.
     105                 :            :    */
     106                 :            :   void registerTrustedChecker(ProofRule id,
     107                 :            :                               ProofRuleChecker* psc,
     108                 :            :                               uint32_t plevel = 10);
     109                 :            :   /** get checker for */
     110                 :            :   ProofRuleChecker* getCheckerFor(ProofRule id);
     111                 :            :   /** get the rewrite database */
     112                 :            :   rewriter::RewriteDb* getRewriteDatabase();
     113                 :            :   /**
     114                 :            :    * Get the pedantic level for id if it has been assigned a pedantic
     115                 :            :    * level via registerTrustedChecker above, or zero otherwise.
     116                 :            :    */
     117                 :            :   uint32_t getPedanticLevel(ProofRule id) const;
     118                 :            : 
     119                 :            :   /**
     120                 :            :    * Is pedantic failure? If so, we return true and write a debug message on the
     121                 :            :    * output stream out if enableOutput is true.
     122                 :            :    */
     123                 :            :   bool isPedanticFailure(ProofRule id, std::ostream* out) const;
     124                 :            : 
     125                 :            :   /** Assigns argument pcMode to d_pcMode. */
     126                 :            :   void setProofCheckMode(options::ProofCheckMode pcMode);
     127                 :            : 
     128                 :            :  private:
     129                 :            :   /** statistics class */
     130                 :            :   ProofCheckerStatistics d_stats;
     131                 :            :   /** Maps proof rules to their checker */
     132                 :            :   std::map<ProofRule, ProofRuleChecker*> d_checker;
     133                 :            :   /** Maps proof trusted rules to their pedantic level */
     134                 :            :   std::map<ProofRule, uint32_t> d_plevel;
     135                 :            :   /** The proof checking mode */
     136                 :            :   options::ProofCheckMode d_pcMode;
     137                 :            :   /** The pedantic level of this checker */
     138                 :            :   uint32_t d_pclevel;
     139                 :            :   /** Pointer to the rewrite database */
     140                 :            :   rewriter::RewriteDb* d_rdb;
     141                 :            :   /**
     142                 :            :    * Check internal. This is used by check and checkDebug above. It writes
     143                 :            :    * checking errors on out when enableOutput is true. We treat trusted checkers
     144                 :            :    * (nullptr in the range of the map d_checker) as failures if
     145                 :            :    * useTrustedChecker = false.
     146                 :            :    */
     147                 :            :   Node checkInternal(ProofRule id,
     148                 :            :                      const std::vector<Node>& cchildren,
     149                 :            :                      const std::vector<Node>& args,
     150                 :            :                      Node expected,
     151                 :            :                      std::stringstream* out,
     152                 :            :                      bool useTrustedChecker);
     153                 :            : };
     154                 :            : 
     155                 :            : }  // namespace cvc5::internal
     156                 :            : 
     157                 :            : #endif /* CVC5__PROOF__PROOF_CHECKER_H */