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