Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Daniel Larraz, Mathias Preiner
       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                 :            :  * Implementation of trust identifier
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "proof/trust_id.h"
      17                 :            : 
      18                 :            : #include "proof/proof_checker.h"
      19                 :            : #include "util/rational.h"
      20                 :            : 
      21                 :            : using namespace cvc5::internal::kind;
      22                 :            : 
      23                 :            : namespace cvc5::internal {
      24                 :            : 
      25                 :       7091 : const char* toString(TrustId id)
      26                 :            : {
      27 [ -  - ][ +  - ]:       7091 :   switch (id)
         [ +  - ][ +  + ]
         [ +  + ][ +  + ]
         [ +  - ][ -  - ]
         [ +  - ][ -  - ]
         [ +  + ][ +  + ]
         [ +  - ][ +  - ]
         [ +  - ][ -  - ]
         [ -  - ][ -  - ]
         [ +  + ][ +  + ]
         [ -  - ][ -  + ]
         [ -  + ][ +  + ]
         [ -  + ][ -  - ]
         [ +  + ][ +  + ]
         [ -  + ][ -  - ]
         [ +  + ][ +  - ]
         [ +  + ][ +  + ]
         [ +  + ][ -  + ]
         [ +  - ][ -  - ]
      28                 :            :   {
      29                 :          0 :     case TrustId::NONE: return "NONE";
      30                 :          0 :     case TrustId::PREPROCESSED_INPUT: return "PREPROCESSED_INPUT";
      31                 :        796 :     case TrustId::THEORY_LEMMA: return "THEORY_LEMMA";
      32                 :          0 :     case TrustId::SMT_REFUTATION: return "SMT_REFUTATION";
      33                 :            :     // core
      34                 :       3007 :     case TrustId::THEORY_INFERENCE_ARITH: return "THEORY_INFERENCE_ARITH";
      35                 :          0 :     case TrustId::THEORY_INFERENCE_ARRAYS: return "THEORY_INFERENCE_ARRAYS";
      36                 :          3 :     case TrustId::THEORY_INFERENCE_DATATYPES:
      37                 :          3 :       return "THEORY_INFERENCE_DATATYPES";
      38                 :         33 :     case TrustId::THEORY_INFERENCE_SEP: return "THEORY_INFERENCE_SEP";
      39                 :        146 :     case TrustId::THEORY_INFERENCE_SETS: return "THEORY_INFERENCE_SETS";
      40                 :         53 :     case TrustId::THEORY_INFERENCE_STRINGS: return "THEORY_INFERENCE_STRINGS";
      41                 :         25 :     case TrustId::PP_STATIC_REWRITE: return "PP_STATIC_REWRITE";
      42                 :          6 :     case TrustId::THEORY_PREPROCESS: return "THEORY_PREPROCESS";
      43                 :         12 :     case TrustId::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA";
      44                 :          0 :     case TrustId::THEORY_EXPAND_DEF: return "THEORY_EXPAND_DEF";
      45                 :            :     // preprocess passes
      46                 :          0 :     case TrustId::PREPROCESS_BV_GUASS: return "PREPROCESS_BV_GUASS";
      47                 :          0 :     case TrustId::PREPROCESS_BV_GUASS_LEMMA: return "PREPROCESS_BV_GUASS_LEMMA";
      48                 :         20 :     case TrustId::PREPROCESS_BV_TO_BOOL: return "PREPROCESS_BV_TO_BOOL";
      49                 :          0 :     case TrustId::PREPROCESS_BV_TO_INT: return "PREPROCESS_BV_TO_INT";
      50                 :          0 :     case TrustId::PREPROCESS_BV_TO_INT_LEMMA:
      51                 :          0 :       return "PREPROCESS_BV_TO_INT_LEMMA";
      52                 :          0 :     case TrustId::PREPROCESS_BOOL_TO_BV: return "PREPROCESS_BOOL_TO_BV";
      53                 :          8 :     case TrustId::PREPROCESS_ACKERMANN: return "PREPROCESS_ACKERMANN";
      54                 :         60 :     case TrustId::PREPROCESS_ACKERMANN_LEMMA:
      55                 :         60 :       return "PREPROCESS_ACKERMANN_LEMMA";
      56                 :          1 :     case TrustId::PREPROCESS_STATIC_LEARNING_LEMMA:
      57                 :          1 :       return "PREPROCESS_STATIC_LEARNING_LEMMA";
      58                 :         20 :     case TrustId::PREPROCESS_HO_ELIM: return "PREPROCESS_HO_ELIM";
      59                 :          3 :     case TrustId::PREPROCESS_HO_ELIM_LEMMA: return "PREPROCESS_HO_ELIM_LEMMA";
      60                 :          0 :     case TrustId::PREPROCESS_BITVECTOR_EAGER_ATOMS:
      61                 :          0 :       return "PREPROCESS_BITVECTOR_EAGER_ATOMS";
      62                 :          1 :     case TrustId::PREPROCESS_FF_BITSUM: return "PREPROCESS_FF_BITSUM";
      63                 :          0 :     case TrustId::PREPROCESS_FF_DISJUNCTIVE_BIT:
      64                 :          0 :       return "PREPROCESS_FF_DISJUNCTIVE_BIT";
      65                 :         13 :     case TrustId::PREPROCESS_FUN_DEF_FMF: return "PREPROCESS_FUN_DEF_FMF";
      66                 :          0 :     case TrustId::PREPROCESS_ITE_SIMP: return "PREPROCESS_ITE_SIMP";
      67                 :          0 :     case TrustId::PREPROCESS_LEARNED_REWRITE:
      68                 :          0 :       return "PREPROCESS_LEARNED_REWRITE";
      69                 :          0 :     case TrustId::PREPROCESS_LEARNED_REWRITE_LEMMA:
      70                 :          0 :       return "PREPROCESS_LEARNED_REWRITE_LEMMA";
      71                 :          0 :     case TrustId::PREPROCESS_MIPLIB_TRICK: return "PREPROCESS_MIPLIB_TRICK";
      72                 :          0 :     case TrustId::PREPROCESS_MIPLIB_TRICK_LEMMA:
      73                 :          0 :       return "PREPROCESS_MIPLIB_TRICK_LEMMA";
      74                 :          0 :     case TrustId::PREPROCESS_NL_EXT_PURIFY: return "PREPROCESS_NL_EXT_PURIFY";
      75                 :          0 :     case TrustId::PREPROCESS_NL_EXT_PURIFY_LEMMA:
      76                 :          0 :       return "PREPROCESS_NL_EXT_PURIFY_LEMMA";
      77                 :          3 :     case TrustId::PREPROCESS_BV_INTRO_POW2: return "PREPROCESS_BV_INTRO_POW2";
      78                 :          1 :     case TrustId::PREPROCESS_FOREIGN_THEORY_REWRITE:
      79                 :          1 :       return "PREPROCESS_FOREIGN_THEORY_REWRITE";
      80                 :         11 :     case TrustId::PREPROCESS_UNCONSTRAINED_SIMP:
      81                 :         11 :       return "PREPROCESS_UNCONSTRAINED_SIMP";
      82                 :          2 :     case TrustId::PREPROCESS_QUANTIFIERS_PP: return "PREPROCESS_QUANTIFIERS_PP";
      83                 :          0 :     case TrustId::PREPROCESS_REAL_TO_INT: return "PREPROCESS_REAL_TO_INT";
      84                 :          0 :     case TrustId::PREPROCESS_SORT_INFER: return "PREPROCESS_SORT_INFER";
      85                 :          0 :     case TrustId::PREPROCESS_SORT_INFER_LEMMA:
      86                 :          0 :       return "PREPROCESS_SORT_INFER_LEMMA";
      87                 :          3 :     case TrustId::PREPROCESS_STRINGS_EAGER_PP:
      88                 :          3 :       return "PREPROCESS_STRINGS_EAGER_PP";
      89                 :            :     // other
      90                 :          0 :     case TrustId::UF_DISTINCT: return "UF_DISTINCT";
      91                 :         31 :     case TrustId::ARITH_NL_COVERING_DIRECT: return "ARITH_NL_COVERING_DIRECT";
      92                 :         21 :     case TrustId::ARITH_NL_COVERING_RECURSIVE:
      93                 :         21 :       return "ARITH_NL_COVERING_RECURSIVE";
      94                 :         92 :     case TrustId::ARITH_NL_COMPARE_LIT_TRANSFORM:
      95                 :         92 :       return "ARITH_NL_COMPARE_LIT_TRANSFORM";
      96                 :          0 :     case TrustId::ARITH_DIO_LEMMA: return "ARITH_DIO_LEMMA";
      97                 :         47 :     case TrustId::ARITH_STATIC_LEARN: return "ARITH_STATIC_LEARN";
      98                 :          0 :     case TrustId::ARITH_NL_COMPARE_LEMMA: return "ARITH_NL_COMPARE_LEMMA";
      99                 :          0 :     case TrustId::ARITH_NL_FLATTEN_MON_LEMMA:
     100                 :          0 :       return "ARITH_NL_FLATTEN_MON_LEMMA";
     101                 :        141 :     case TrustId::BV_BITBLAST_CONFLICT: return "BV_BITBLAST_CONFLICT";
     102                 :         12 :     case TrustId::BV_PP_ASSERT: return "BV_PP_ASSERT";
     103                 :        149 :     case TrustId::DIAMONDS: return "DIAMONDS";
     104                 :         16 :     case TrustId::EXT_THEORY_REWRITE: return "EXT_THEORY_REWRITE";
     105                 :          0 :     case TrustId::REWRITE_NO_ELABORATE: return "REWRITE_NO_ELABORATE";
     106                 :          1 :     case TrustId::FLATTENING_REWRITE: return "FLATTENING_REWRITE";
     107                 :          0 :     case TrustId::SUBS_NO_ELABORATE: return "SUBS_NO_ELABORATE";
     108                 :          0 :     case TrustId::SUBS_MAP: return "SUBS_MAP";
     109                 :          6 :     case TrustId::SUBS_EQ: return "SUBS_EQ";
     110                 :       2057 :     case TrustId::ARITH_PRED_CAST_TYPE: return "ARITH_PRED_CAST_TYPE";
     111                 :         21 :     case TrustId::RE_ELIM: return "RE_ELIM";
     112                 :          0 :     case TrustId::QUANTIFIERS_PREPROCESS: return "QUANTIFIERS_PREPROCESS";
     113                 :          7 :     case TrustId::QUANTIFIERS_INST_REWRITE: return "QUANTIFIERS_INST_REWRITE";
     114                 :          2 :     case TrustId::QUANTIFIERS_SUB_CBQI_LEMMA:
     115                 :          2 :       return "QUANTIFIERS_SUB_CBQI_LEMMA";
     116                 :          6 :     case TrustId::QUANTIFIERS_NESTED_QE_LEMMA:
     117                 :          6 :       return "QUANTIFIERS_NESTED_QE_LEMMA";
     118                 :         40 :     case TrustId::STRINGS_PP_STATIC_REWRITE: return "STRINGS_PP_STATIC_REWRITE";
     119                 :         26 :     case TrustId::VALID_WITNESS: return "VALID_WITNESS";
     120                 :          4 :     case TrustId::SUBTYPE_ELIMINATION: return "SUBTYPE_ELIMINATION";
     121                 :          0 :     case TrustId::MACRO_THEORY_REWRITE_RCONS:
     122                 :          0 :       return "MACRO_THEORY_REWRITE_RCONS";
     123                 :         15 :     case TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE:
     124                 :         15 :       return "MACRO_THEORY_REWRITE_RCONS_SIMPLE";
     125                 :        170 :     case TrustId::INT_BLASTER: return "INT_BLASTER";
     126                 :            :     // unknown sources
     127                 :          0 :     case TrustId::UNKNOWN_PREPROCESS: return "UNKNOWN_PREPROCESS";
     128                 :          0 :     case TrustId::UNKNOWN_PREPROCESS_LEMMA: return "UNKNOWN_PREPROCESS_LEMMA";
     129                 :          0 :     default: return "TrustId::Unknown";
     130                 :            :   };
     131                 :            : }
     132                 :            : 
     133                 :       7091 : std::ostream& operator<<(std::ostream& out, TrustId id)
     134                 :            : {
     135                 :       7091 :   out << toString(id);
     136                 :       7091 :   return out;
     137                 :            : }
     138                 :            : 
     139                 :     293776 : Node mkTrustId(NodeManager* nm, TrustId id)
     140                 :            : {
     141                 :     587552 :   return nm->mkConstInt(Rational(static_cast<uint32_t>(id)));
     142                 :            : }
     143                 :            : 
     144                 :      75233 : bool getTrustId(TNode n, TrustId& i)
     145                 :            : {
     146                 :            :   uint32_t index;
     147         [ -  + ]:      75233 :   if (!ProofRuleChecker::getUInt32(n, index))
     148                 :            :   {
     149                 :          0 :     return false;
     150                 :            :   }
     151                 :      75233 :   i = static_cast<TrustId>(index);
     152                 :      75233 :   return true;
     153                 :            : }
     154                 :            : 
     155                 :            : }  // namespace cvc5::internal