Branch data     Line data    Source code

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