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 inference enumeration.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/inference_id.h"
      14                 :            : 
      15                 :            : #include <iostream>
      16                 :            : 
      17                 :            : #include "proof/proof_checker.h"
      18                 :            : #include "util/rational.h"
      19                 :            : 
      20                 :            : using namespace cvc5::internal::kind;
      21                 :            : 
      22                 :            : namespace cvc5::internal {
      23                 :            : namespace theory {
      24                 :            : 
      25                 :        402 : const char* toString(InferenceId i)
      26                 :            : {
      27 [ +  + ][ +  + ]:        402 :   switch (i)
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  + ]
         [ +  + ][ +  - ]
                    [ - ]
      28                 :            :   {
      29                 :          1 :     case InferenceId::NONE: return "NONE";
      30                 :          1 :     case InferenceId::INPUT: return "INPUT";
      31                 :          1 :     case InferenceId::EQ_CONSTANT_MERGE: return "EQ_CONSTANT_MERGE";
      32                 :          1 :     case InferenceId::COMBINATION_SPLIT: return "COMBINATION_SPLIT";
      33                 :          1 :     case InferenceId::CONFLICT_REWRITE_LIT: return "CONFLICT_REWRITE_LIT";
      34                 :          1 :     case InferenceId::EXPLAINED_PROPAGATION: return "EXPLAINED_PROPAGATION";
      35                 :          1 :     case InferenceId::THEORY_PP_SKOLEM_LEM: return "THEORY_PP_SKOLEM_LEM";
      36                 :          1 :     case InferenceId::EXTT_SIMPLIFY: return "EXTT_SIMPLIFY";
      37                 :          1 :     case InferenceId::ARITH_BLACK_BOX: return "ARITH_BLACK_BOX";
      38                 :          1 :     case InferenceId::ARITH_CONF_EQ: return "ARITH_CONF_EQ";
      39                 :          1 :     case InferenceId::ARITH_CONF_LOWER: return "ARITH_CONF_LOWER";
      40                 :          1 :     case InferenceId::ARITH_CONF_TRICHOTOMY: return "ARITH_CONF_TRICHOTOMY";
      41                 :          1 :     case InferenceId::ARITH_CONF_UPPER: return "ARITH_CONF_UPPER";
      42                 :          1 :     case InferenceId::ARITH_CONF_SIMPLEX: return "ARITH_CONF_SIMPLEX";
      43                 :          1 :     case InferenceId::ARITH_CONF_SOI_SIMPLEX: return "ARITH_CONF_SOI_SIMPLEX";
      44                 :          1 :     case InferenceId::ARITH_CONF_FACT_QUEUE: return "ARITH_CONF_FACT_QUEUE";
      45                 :          1 :     case InferenceId::ARITH_CONF_BRANCH_CUT: return "ARITH_CONF_BRANCH_CUT";
      46                 :          1 :     case InferenceId::ARITH_CONF_REPLAY_ASSERT:
      47                 :          1 :       return "ARITH_CONF_REPLAY_ASSERT";
      48                 :          1 :     case InferenceId::ARITH_CONF_REPLAY_LOG: return "ARITH_CONF_REPLAY_LOG";
      49                 :          1 :     case InferenceId::ARITH_CONF_REPLAY_LOG_REC:
      50                 :          1 :       return "ARITH_CONF_REPLAY_LOG_REC";
      51                 :          1 :     case InferenceId::ARITH_CONF_UNATE_PROP: return "ARITH_CONF_UNATE_PROP";
      52                 :          3 :     case InferenceId::ARITH_SPLIT_DEQ: return "ARITH_SPLIT_DEQ";
      53                 :          1 :     case InferenceId::ARITH_EQUIV_ATOM: return "ARITH_EQUIV_ATOM";
      54                 :          1 :     case InferenceId::ARITH_TIGHTEN_CEIL: return "ARITH_TIGHTEN_CEIL";
      55                 :          1 :     case InferenceId::ARITH_TIGHTEN_FLOOR: return "ARITH_TIGHTEN_FLOOR";
      56                 :          1 :     case InferenceId::ARITH_APPROX_CUT: return "ARITH_APPROX_CUT";
      57                 :          1 :     case InferenceId::ARITH_BB_LEMMA: return "ARITH_BB_LEMMA";
      58                 :          1 :     case InferenceId::ARITH_DIO_CUT: return "ARITH_DIO_CUT";
      59                 :          1 :     case InferenceId::ARITH_DIO_DECOMPOSITION: return "ARITH_DIO_DECOMPOSITION";
      60                 :          1 :     case InferenceId::ARITH_UNATE: return "ARITH_UNATE";
      61                 :          1 :     case InferenceId::ARITH_ROW_IMPL: return "ARITH_ROW_IMPL";
      62                 :          1 :     case InferenceId::ARITH_SPLIT_FOR_NL_MODEL:
      63                 :          1 :       return "ARITH_SPLIT_FOR_NL_MODEL";
      64                 :          1 :     case InferenceId::ARITH_DEMAND_RESTART: return "ARITH_DEMAND_RESTART";
      65                 :          1 :     case InferenceId::ARITH_PP_ELIM_OPERATORS: return "ARITH_PP_ELIM_OPERATORS";
      66                 :          1 :     case InferenceId::ARITH_PP_ELIM_OPERATORS_LEMMA:
      67                 :          1 :       return "ARITH_PP_ELIM_OPERATORS_LEMMA";
      68                 :          1 :     case InferenceId::ARITH_NL_CONGRUENCE: return "ARITH_NL_CONGRUENCE";
      69                 :          1 :     case InferenceId::ARITH_NL_SHARED_TERM_SPLIT:
      70                 :          1 :       return "ARITH_NL_SHARED_TERM_SPLIT";
      71                 :          1 :     case InferenceId::ARITH_NL_SHARED_TERM_FACTOR_SPLIT:
      72                 :          1 :       return "ARITH_NL_SHARED_TERM_FACTOR_SPLIT";
      73                 :          1 :     case InferenceId::ARITH_NL_SPLIT_ZERO: return "ARITH_NL_SPLIT_ZERO";
      74                 :          1 :     case InferenceId::ARITH_NL_SIGN: return "ARITH_NL_SIGN";
      75                 :          1 :     case InferenceId::ARITH_NL_COMPARISON: return "ARITH_NL_COMPARISON";
      76                 :          1 :     case InferenceId::ARITH_NL_INFER_BOUNDS_NT:
      77                 :          1 :       return "ARITH_NL_INFER_BOUNDS_NT";
      78                 :          1 :     case InferenceId::ARITH_NL_FACTOR: return "ARITH_NL_FACTOR";
      79                 :          1 :     case InferenceId::ARITH_NL_RES_INFER_BOUNDS:
      80                 :          1 :       return "ARITH_NL_RES_INFER_BOUNDS";
      81                 :          1 :     case InferenceId::ARITH_NL_TANGENT_PLANE: return "ARITH_NL_TANGENT_PLANE";
      82                 :          1 :     case InferenceId::ARITH_NL_FLATTEN_MON: return "ARITH_NL_FLATTEN_MON";
      83                 :          1 :     case InferenceId::ARITH_NL_T_SINE_SYMM: return "ARITH_NL_T_SINE_SYMM";
      84                 :          1 :     case InferenceId::ARITH_NL_T_SINE_BOUNDARY_REDUCE:
      85                 :          1 :       return "ARITH_NL_T_SINE_BOUNDARY_REDUCE";
      86                 :          1 :     case InferenceId::ARITH_NL_T_PURIFY_ARG: return "ARITH_NL_T_PURIFY_ARG";
      87                 :          1 :     case InferenceId::ARITH_NL_T_PURIFY_ARG_PHASE_SHIFT:
      88                 :          1 :       return "ARITH_NL_T_PURIFY_ARG_PHASE_SHIFT";
      89                 :          1 :     case InferenceId::ARITH_NL_T_INIT_REFINE: return "ARITH_NL_T_INIT_REFINE";
      90                 :          1 :     case InferenceId::ARITH_NL_T_PI_BOUND: return "ARITH_NL_T_PI_BOUND";
      91                 :          1 :     case InferenceId::ARITH_NL_T_MONOTONICITY: return "ARITH_NL_T_MONOTONICITY";
      92                 :          1 :     case InferenceId::ARITH_NL_T_SECANT: return "ARITH_NL_T_SECANT";
      93                 :          1 :     case InferenceId::ARITH_NL_T_TANGENT: return "ARITH_NL_T_TANGENT";
      94                 :          1 :     case InferenceId::ARITH_NL_IAND_INIT_REFINE:
      95                 :          1 :       return "ARITH_NL_IAND_INIT_REFINE";
      96                 :          1 :     case InferenceId::ARITH_NL_IAND_VALUE_REFINE:
      97                 :          1 :       return "ARITH_NL_IAND_VALUE_REFINE";
      98                 :          1 :     case InferenceId::ARITH_NL_IAND_SUM_REFINE:
      99                 :          1 :       return "ARITH_NL_IAND_SUM_REFINE";
     100                 :          1 :     case InferenceId::ARITH_NL_IAND_BITWISE_REFINE:
     101                 :          1 :       return "ARITH_NL_IAND_BITWISE_REFINE";
     102                 :          1 :     case InferenceId::ARITH_NL_PIAND_INIT_REFINE:
     103                 :          1 :       return "ARITH_NL_PIAND_INIT_REFINE";
     104                 :          1 :     case InferenceId::ARITH_NL_PIAND_SUM_REFINE:
     105                 :          1 :       return "ARITH_NL_PIAND_SUM_REFINE";
     106                 :          1 :     case InferenceId::ARITH_NL_PIAND_BASE_CASE_REFINE:
     107                 :          1 :       return "ARITH_NL_PIAND_BASE_CASE_REFINE";
     108                 :          1 :     case InferenceId::ARITH_NL_PIAND_DIFFERENCE_REFINE:
     109                 :          1 :       return "ARITH_NL_PIAND_DIFFERENCE_REFINE";
     110                 :          1 :     case InferenceId::ARITH_NL_PIAND_SYMETRY_REFINE:
     111                 :          1 :       return "ARITH_NL_PIAND_SYMETRY_REFINE";
     112                 :          1 :     case InferenceId::ARITH_NL_PIAND_CONTRADITION_REFINE:
     113                 :          1 :       return "ARITH_NL_PIAND_CONTRADITION_REFINE";
     114                 :          1 :     case InferenceId::ARITH_NL_PIAND_ONE_REFINE:
     115                 :          1 :       return "ARITH_NL_PIAND_ONE_REFINE";
     116                 :          1 :     case InferenceId::ARITH_NL_POW2_INIT_REFINE:
     117                 :          1 :       return "ARITH_NL_POW2_INIT_REFINE";
     118                 :          1 :     case InferenceId::ARITH_NL_POW2_VALUE_REFINE:
     119                 :          1 :       return "ARITH_NL_POW2_VALUE_REFINE";
     120                 :          1 :     case InferenceId::ARITH_NL_POW2_MONOTONE_REFINE:
     121                 :          1 :       return "ARITH_NL_POW2_MONOTONE_REFINE";
     122                 :          1 :     case InferenceId::ARITH_NL_POW2_DIV0_CASE_REFINE:
     123                 :          1 :       return "ARITH_NL_POW2_DIV0_CASE_REFINE";
     124                 :          1 :     case InferenceId::ARITH_NL_POW2_LOWER_BOUND_CASE_REFINE:
     125                 :          1 :       return "ARITH_NL_POW2_LOWER_BOUND_CASE_REFINE";
     126                 :          1 :     case InferenceId::ARITH_NL_COVERING_CONFLICT:
     127                 :          1 :       return "ARITH_NL_COVERING_CONFLICT";
     128                 :          1 :     case InferenceId::ARITH_NL_COVERING_EXCLUDED_INTERVAL:
     129                 :          1 :       return "ARITH_NL_COVERING_EXCLUDED_INTERVAL";
     130                 :          1 :     case InferenceId::ARITH_NL_ICP_CONFLICT: return "ARITH_NL_ICP_CONFLICT";
     131                 :          1 :     case InferenceId::ARITH_NL_ICP_PROPAGATION:
     132                 :          1 :       return "ARITH_NL_ICP_PROPAGATION";
     133                 :          1 :     case InferenceId::FF_LEMMA: return "FF_LEMMA";
     134                 :            : 
     135                 :          1 :     case InferenceId::ARRAYS_EXT: return "ARRAYS_EXT";
     136                 :          1 :     case InferenceId::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE";
     137                 :          1 :     case InferenceId::ARRAYS_READ_OVER_WRITE_1:
     138                 :          1 :       return "ARRAYS_READ_OVER_WRITE_1";
     139                 :          1 :     case InferenceId::ARRAYS_READ_OVER_WRITE_CONTRA:
     140                 :          1 :       return "ARRAYS_READ_OVER_WRITE_CONTRA";
     141                 :          1 :     case InferenceId::ARRAYS_CONST_ARRAY_DEFAULT:
     142                 :          1 :       return "ARRAYS_CONST_ARRAY_DEFAULT";
     143                 :          1 :     case InferenceId::ARRAYS_EQ_TAUTOLOGY: return "ARRAYS_EQ_TAUTOLOGY";
     144                 :            : 
     145                 :          1 :     case InferenceId::BAGS_NON_NEGATIVE_COUNT: return "BAGS_NON_NEGATIVE_COUNT";
     146                 :          1 :     case InferenceId::BAGS_BAG_MAKE: return "BAGS_BAG_MAKE";
     147                 :          1 :     case InferenceId::BAGS_BAG_MAKE_SPLIT: return "BAGS_BAG_MAKE_SPLIT";
     148                 :          1 :     case InferenceId::BAGS_SKOLEM: return "BAGS_SKOLEM";
     149                 :          1 :     case InferenceId::BAGS_CG_SPLIT: return "BAGS_CG_SPLIT";
     150                 :          1 :     case InferenceId::BAGS_DISEQUALITY: return "BAGS_DISEQUALITY";
     151                 :          1 :     case InferenceId::BAGS_EMPTY: return "BAGS_EMPTY";
     152                 :          1 :     case InferenceId::BAGS_UNION_DISJOINT: return "BAGS_UNION_DISJOINT";
     153                 :          1 :     case InferenceId::BAGS_UNION_MAX: return "BAGS_UNION_MAX";
     154                 :          1 :     case InferenceId::BAGS_INTERSECTION_MIN: return "BAGS_INTERSECTION_MIN";
     155                 :          1 :     case InferenceId::BAGS_DIFFERENCE_SUBTRACT:
     156                 :          1 :       return "BAGS_DIFFERENCE_SUBTRACT";
     157                 :          1 :     case InferenceId::BAGS_DIFFERENCE_REMOVE: return "BAGS_DIFFERENCE_REMOVE";
     158                 :          1 :     case InferenceId::BAGS_SETOF: return "BAGS_SETOF";
     159                 :          1 :     case InferenceId::BAGS_MAP_DOWN: return "BAGS_MAP_DOWN";
     160                 :          1 :     case InferenceId::BAGS_MAP_DOWN_INJECTIVE: return "BAGS_MAP_DOWN_INJECTIVE";
     161                 :          1 :     case InferenceId::BAGS_MAP_UP_INJECTIVE: return "BAGS_MAP_UP_INJECTIVE";
     162                 :          1 :     case InferenceId::BAGS_MAP_UP1: return "BAGS_MAP_UP1";
     163                 :          1 :     case InferenceId::BAGS_MAP_UP2: return "BAGS_MAP_UP2";
     164                 :          1 :     case InferenceId::BAGS_FILTER_DOWN: return "BAGS_FILTER_DOWN";
     165                 :          1 :     case InferenceId::BAGS_FILTER_UP: return "BAGS_FILTER_UP";
     166                 :          1 :     case InferenceId::BAGS_FOLD: return "BAGS_FOLD";
     167                 :          1 :     case InferenceId::BAGS_CARD: return "BAGS_CARD";
     168                 :          1 :     case InferenceId::BAGS_CARD_EMPTY: return "BAGS_CARD_EMPTY";
     169                 :          1 :     case InferenceId::TABLES_PRODUCT_UP: return "TABLES_PRODUCT_UP";
     170                 :          1 :     case InferenceId::TABLES_PRODUCT_DOWN: return "TABLES_PRODUCT_DOWN";
     171                 :          1 :     case InferenceId::TABLES_JOIN_DOWN: return "TABLES_JOIN_DOWN";
     172                 :          1 :     case InferenceId::TABLES_GROUP_NOT_EMPTY: return "TABLES_GROUP_NOT_EMPTY";
     173                 :          1 :     case InferenceId::TABLES_GROUP_UP1: return "TABLES_GROUP_UP1";
     174                 :          1 :     case InferenceId::TABLES_GROUP_UP2: return "TABLES_GROUP_UP2";
     175                 :          1 :     case InferenceId::TABLES_GROUP_DOWN: return "TABLES_GROUP_DOWN";
     176                 :          1 :     case InferenceId::TABLES_GROUP_PART_COUNT: return "TABLES_GROUP_PART_COUNT";
     177                 :          1 :     case InferenceId::TABLES_GROUP_SAME_PROJECTION:
     178                 :          1 :       return "TABLES_GROUP_SAME_PROJECTION";
     179                 :          1 :     case InferenceId::TABLES_GROUP_SAME_PART: return "TABLES_GROUP_SAME_PART";
     180                 :            : 
     181                 :          1 :     case InferenceId::BV_BITBLAST_CONFLICT: return "BV_BITBLAST_CONFLICT";
     182                 :          1 :     case InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA:
     183                 :          1 :       return "BV_BITBLAST_EAGER_LEMMA";
     184                 :          1 :     case InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA:
     185                 :          1 :       return "BV_BITBLAST_INTERNAL_BITBLAST_LEMMA";
     186                 :            : 
     187                 :          1 :     case InferenceId::DATATYPES_PURIFY: return "DATATYPES_PURIFY";
     188                 :          1 :     case InferenceId::DATATYPES_UNIF: return "DATATYPES_UNIF";
     189                 :          1 :     case InferenceId::DATATYPES_INST: return "DATATYPES_INST";
     190                 :          1 :     case InferenceId::DATATYPES_SPLIT: return "DATATYPES_SPLIT";
     191                 :          1 :     case InferenceId::DATATYPES_BINARY_SPLIT: return "DATATYPES_BINARY_SPLIT";
     192                 :          1 :     case InferenceId::DATATYPES_LABEL_EXH: return "DATATYPES_LABEL_EXH";
     193                 :          1 :     case InferenceId::DATATYPES_COLLAPSE_SEL: return "DATATYPES_COLLAPSE_SEL";
     194                 :          1 :     case InferenceId::DATATYPES_CLASH_CONFLICT:
     195                 :          1 :       return "DATATYPES_CLASH_CONFLICT";
     196                 :          1 :     case InferenceId::DATATYPES_TESTER_CONFLICT:
     197                 :          1 :       return "DATATYPES_TESTER_CONFLICT";
     198                 :          1 :     case InferenceId::DATATYPES_TESTER_MERGE_CONFLICT:
     199                 :          1 :       return "DATATYPES_TESTER_MERGE_CONFLICT";
     200                 :          1 :     case InferenceId::DATATYPES_BISIMILAR: return "DATATYPES_BISIMILAR";
     201                 :          1 :     case InferenceId::DATATYPES_REC_SINGLETON_EQ:
     202                 :          1 :       return "DATATYPES_REC_SINGLETON_EQ";
     203                 :          1 :     case InferenceId::DATATYPES_REC_SINGLETON_FORCE_DEQ:
     204                 :          1 :       return "DATATYPES_REC_SINGLETON_FORCE_DEQ";
     205                 :          1 :     case InferenceId::DATATYPES_CYCLE: return "DATATYPES_CYCLE";
     206                 :          1 :     case InferenceId::DATATYPES_HEIGHT_ZERO: return "DATATYPES_HEIGHT_ZERO";
     207                 :          1 :     case InferenceId::DATATYPES_SYGUS_SYM_BREAK:
     208                 :          1 :       return "DATATYPES_SYGUS_SYM_BREAK";
     209                 :          1 :     case InferenceId::DATATYPES_SYGUS_CDEP_SYM_BREAK:
     210                 :          1 :       return "DATATYPES_SYGUS_CDEP_SYM_BREAK";
     211                 :          1 :     case InferenceId::DATATYPES_SYGUS_ENUM_SYM_BREAK:
     212                 :          1 :       return "DATATYPES_SYGUS_ENUM_SYM_BREAK";
     213                 :          1 :     case InferenceId::DATATYPES_SYGUS_SIMPLE_SYM_BREAK:
     214                 :          1 :       return "DATATYPES_SYGUS_SIMPLE_SYM_BREAK";
     215                 :          1 :     case InferenceId::DATATYPES_SYGUS_FAIR_SIZE:
     216                 :          1 :       return "DATATYPES_SYGUS_FAIR_SIZE";
     217                 :          1 :     case InferenceId::DATATYPES_SYGUS_FAIR_SIZE_CONFLICT:
     218                 :          1 :       return "DATATYPES_SYGUS_FAIR_SIZE_CONFLICT";
     219                 :          1 :     case InferenceId::DATATYPES_SYGUS_VAR_AGNOSTIC:
     220                 :          1 :       return "DATATYPES_SYGUS_VAR_AGNOSTIC";
     221                 :          1 :     case InferenceId::DATATYPES_SYGUS_VALUE_CORRECTION:
     222                 :          1 :       return "DATATYPES_SYGUS_VALUE_CORRECTION";
     223                 :          1 :     case InferenceId::DATATYPES_SYGUS_MT_BOUND:
     224                 :          1 :       return "DATATYPES_SYGUS_MT_BOUND";
     225                 :          1 :     case InferenceId::DATATYPES_SYGUS_MT_POS: return "DATATYPES_SYGUS_MT_POS";
     226                 :            : 
     227                 :          1 :     case InferenceId::FP_PREPROCESS: return "FP_PREPROCESS";
     228                 :          1 :     case InferenceId::FP_EQUATE_TERM: return "FP_EQUATE_TERM";
     229                 :          1 :     case InferenceId::FP_REGISTER_TERM: return "FP_REGISTER_TERM";
     230                 :            : 
     231                 :          1 :     case InferenceId::QUANTIFIERS_INST_E_MATCHING:
     232                 :          1 :       return "QUANTIFIERS_INST_E_MATCHING";
     233                 :          1 :     case InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE:
     234                 :          1 :       return "QUANTIFIERS_INST_E_MATCHING_SIMPLE";
     235                 :          1 :     case InferenceId::QUANTIFIERS_INST_E_MATCHING_MT:
     236                 :          1 :       return "QUANTIFIERS_INST_E_MATCHING_MT";
     237                 :          1 :     case InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL:
     238                 :          1 :       return "QUANTIFIERS_INST_E_MATCHING_MTL";
     239                 :          1 :     case InferenceId::QUANTIFIERS_INST_E_MATCHING_HO:
     240                 :          1 :       return "QUANTIFIERS_INST_E_MATCHING_HO";
     241                 :          1 :     case InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN:
     242                 :          1 :       return "QUANTIFIERS_INST_E_MATCHING_VAR_GEN";
     243                 :          1 :     case InferenceId::QUANTIFIERS_INST_E_MATCHING_RELATIONAL:
     244                 :          1 :       return "QUANTIFIERS_INST_E_MATCHING_RELATIONAL";
     245                 :          2 :     case InferenceId::QUANTIFIERS_INST_CBQI_CONFLICT:
     246                 :          2 :       return "QUANTIFIERS_INST_CBQI_CONFLICT";
     247                 :          1 :     case InferenceId::QUANTIFIERS_INST_CBQI_PROP:
     248                 :          1 :       return "QUANTIFIERS_INST_CBQI_PROP";
     249                 :          1 :     case InferenceId::QUANTIFIERS_INST_SUB_CONFLICT:
     250                 :          1 :       return "QUANTIFIERS_INST_SUB_CONFLICT";
     251                 :          1 :     case InferenceId::QUANTIFIERS_SUB_UC: return "QUANTIFIERS_SUB_UC";
     252                 :          1 :     case InferenceId::QUANTIFIERS_INST_FMF_EXH:
     253                 :          1 :       return "QUANTIFIERS_INST_FMF_EXH";
     254                 :          1 :     case InferenceId::QUANTIFIERS_INST_FMF_FMC:
     255                 :          1 :       return "QUANTIFIERS_INST_FMF_FMC";
     256                 :          1 :     case InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH:
     257                 :          1 :       return "QUANTIFIERS_INST_FMF_FMC_EXH";
     258                 :          1 :     case InferenceId::QUANTIFIERS_INST_CEGQI: return "QUANTIFIERS_INST_CEGQI";
     259                 :          1 :     case InferenceId::QUANTIFIERS_INST_SYQI: return "QUANTIFIERS_INST_SYQI";
     260                 :          1 :     case InferenceId::QUANTIFIERS_INST_MBQI: return "QUANTIFIERS_INST_MBQI";
     261                 :          1 :     case InferenceId::QUANTIFIERS_INST_MBQI_ENUM:
     262                 :          1 :       return "QUANTIFIERS_INST_MBQI_ENUM";
     263                 :          1 :     case InferenceId::QUANTIFIERS_INST_ENUM: return "QUANTIFIERS_INST_ENUM";
     264                 :          1 :     case InferenceId::QUANTIFIERS_INST_POOL: return "QUANTIFIERS_INST_POOL";
     265                 :          1 :     case InferenceId::QUANTIFIERS_INST_POOL_TUPLE:
     266                 :          1 :       return "QUANTIFIERS_INST_POOL_TUPLE";
     267                 :          1 :     case InferenceId::QUANTIFIERS_BINT_PROXY: return "QUANTIFIERS_BINT_PROXY";
     268                 :          1 :     case InferenceId::QUANTIFIERS_BINT_MIN_NG: return "QUANTIFIERS_BINT_MIN_NG";
     269                 :          1 :     case InferenceId::QUANTIFIERS_CEGQI_CEX: return "QUANTIFIERS_CEGQI_CEX";
     270                 :          1 :     case InferenceId::QUANTIFIERS_CEGQI_CEX_AUX:
     271                 :          1 :       return "QUANTIFIERS_CEGQI_CEX_AUX";
     272                 :          1 :     case InferenceId::QUANTIFIERS_CEGQI_NESTED_QE:
     273                 :          1 :       return "QUANTIFIERS_CEGQI_NESTED_QE";
     274                 :          1 :     case InferenceId::QUANTIFIERS_CEGQI_CEX_DEP:
     275                 :          1 :       return "QUANTIFIERS_CEGQI_CEX_DEP";
     276                 :          1 :     case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA:
     277                 :          1 :       return "QUANTIFIERS_CEGQI_VTS_LB_DELTA";
     278                 :          1 :     case InferenceId::QUANTIFIERS_CEGQI_VTS_UB_DELTA:
     279                 :          1 :       return "QUANTIFIERS_CEGQI_VTS_UB_DELTA";
     280                 :          1 :     case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF:
     281                 :          1 :       return "QUANTIFIERS_CEGQI_VTS_LB_INF";
     282                 :          1 :     case InferenceId::QUANTIFIERS_MBQI_ENUM_CHOICE:
     283                 :          1 :       return "QUANTIFIERS_MBQI_ENUM_CHOICE";
     284                 :          1 :     case InferenceId::QUANTIFIERS_ORACLE_INTERFACE:
     285                 :          1 :       return "QUANTIFIERS_ORACLE_INTERFACE";
     286                 :          1 :     case InferenceId::QUANTIFIERS_ORACLE_PURIFY_SUBS:
     287                 :          1 :       return "QUANTIFIERS_ORACLE_PURIFY_SUBS";
     288                 :          1 :     case InferenceId::QUANTIFIERS_SYQI_CEX: return "QUANTIFIERS_SYQI_CEX";
     289                 :          1 :     case InferenceId::QUANTIFIERS_SYQI_EVAL_UNFOLD:
     290                 :          1 :       return "QUANTIFIERS_SYQI_EVAL_UNFOLD";
     291                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT:
     292                 :          1 :       return "QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT";
     293                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_ACTIVE_GEN_EXCLUDE_CURRENT:
     294                 :          1 :       return "QUANTIFIERS_SYGUS_ACTIVE_GEN_EXCLUDE_CURRENT";
     295                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT:
     296                 :          1 :       return "QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT";
     297                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_INC_EXCLUDE_CURRENT:
     298                 :          1 :       return "QUANTIFIERS_SYGUS_INC_EXCLUDE_CURRENT";
     299                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_SC_EXCLUDE_CURRENT:
     300                 :          1 :       return "QUANTIFIERS_SYGUS_SC_EXCLUDE_CURRENT";
     301                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_NO_VERIFY_EXCLUDE_CURRENT:
     302                 :          1 :       return "QUANTIFIERS_SYGUS_NO_VERIFY_EXCLUDE_CURRENT";
     303                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_REPEAT_CEX_EXCLUDE_CURRENT:
     304                 :          1 :       return "QUANTIFIERS_SYGUS_REPEAT_CEX_EXCLUDE_CURRENT";
     305                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA:
     306                 :          1 :       return "QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA";
     307                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_SI_INFEASIBLE:
     308                 :          1 :       return "QUANTIFIERS_SYGUS_SI_INFEASIBLE";
     309                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB:
     310                 :          1 :       return "QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB";
     311                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_SEPARATION:
     312                 :          1 :       return "QUANTIFIERS_SYGUS_UNIF_PI_SEPARATION";
     313                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_FAIR_SIZE:
     314                 :          1 :       return "QUANTIFIERS_SYGUS_UNIF_PI_FAIR_SIZE";
     315                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_REM_OPS:
     316                 :          1 :       return "QUANTIFIERS_SYGUS_UNIF_PI_REM_OPS";
     317                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB:
     318                 :          1 :       return "QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB";
     319                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN:
     320                 :          1 :       return "QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN";
     321                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_COND_EXCLUDE:
     322                 :          1 :       return "QUANTIFIERS_SYGUS_UNIF_PI_COND_EXCLUDE";
     323                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_REFINEMENT:
     324                 :          1 :       return "QUANTIFIERS_SYGUS_UNIF_PI_REFINEMENT";
     325                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_CEGIS_UCL_SYM_BREAK:
     326                 :          1 :       return "QUANTIFIERS_SYGUS_CEGIS_UCL_SYM_BREAK";
     327                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_CEGIS_UCL_EXCLUDE:
     328                 :          1 :       return "QUANTIFIERS_SYGUS_CEGIS_UCL_EXCLUDE";
     329                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_REPAIR_CONST_EXCLUDE:
     330                 :          1 :       return "QUANTIFIERS_SYGUS_REPAIR_CONST_EXCLUDE";
     331                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE:
     332                 :          1 :       return "QUANTIFIERS_SYGUS_CEGIS_REFINE";
     333                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE_SAMPLE:
     334                 :          1 :       return "QUANTIFIERS_SYGUS_CEGIS_REFINE_SAMPLE";
     335                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_REFINE_EVAL:
     336                 :          1 :       return "QUANTIFIERS_SYGUS_REFINE_EVAL";
     337                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_EVAL_UNFOLD:
     338                 :          1 :       return "QUANTIFIERS_SYGUS_EVAL_UNFOLD";
     339                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_PBE_EXCLUDE:
     340                 :          1 :       return "QUANTIFIERS_SYGUS_PBE_EXCLUDE";
     341                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_PBE_CONSTRUCT_SOL:
     342                 :          1 :       return "QUANTIFIERS_SYGUS_PBE_CONSTRUCT_SOL";
     343                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_COMPLETE_ENUM:
     344                 :          1 :       return "QUANTIFIERS_SYGUS_COMPLETE_ENUM";
     345                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_SC_INFEASIBLE:
     346                 :          1 :       return "QUANTIFIERS_SYGUS_SC_INFEASIBLE";
     347                 :          1 :     case InferenceId::QUANTIFIERS_SYGUS_NO_WF_GRAMMAR:
     348                 :          1 :       return "QUANTIFIERS_SYGUS_NO_WF_GRAMMAR";
     349                 :          1 :     case InferenceId::QUANTIFIERS_DSPLIT: return "QUANTIFIERS_DSPLIT";
     350                 :          1 :     case InferenceId::QUANTIFIERS_CONJ_GEN_SPLIT:
     351                 :          1 :       return "QUANTIFIERS_CONJ_GEN_SPLIT";
     352                 :          1 :     case InferenceId::QUANTIFIERS_CONJ_GEN_GT_ENUM:
     353                 :          1 :       return "QUANTIFIERS_CONJ_GEN_GT_ENUM";
     354                 :          1 :     case InferenceId::QUANTIFIERS_SKOLEMIZE: return "QUANTIFIERS_SKOLEMIZE";
     355                 :          1 :     case InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ:
     356                 :          1 :       return "QUANTIFIERS_REDUCE_ALPHA_EQ";
     357                 :          1 :     case InferenceId::QUANTIFIERS_HO_MATCH_PRED:
     358                 :          1 :       return "QUANTIFIERS_HO_MATCH_PRED";
     359                 :          1 :     case InferenceId::QUANTIFIERS_HO_PURIFY: return "QUANTIFIERS_HO_PURIFY";
     360                 :          1 :     case InferenceId::QUANTIFIERS_PARTIAL_TRIGGER_REDUCE:
     361                 :          1 :       return "QUANTIFIERS_PARTIAL_TRIGGER_REDUCE";
     362                 :          1 :     case InferenceId::QUANTIFIERS_GT_PURIFY: return "QUANTIFIERS_GT_PURIFY";
     363                 :          1 :     case InferenceId::QUANTIFIERS_TDB_DEQ_CONG:
     364                 :          1 :       return "QUANTIFIERS_TDB_DEQ_CONG";
     365                 :          1 :     case InferenceId::QUANTIFIERS_CEGQI_WITNESS:
     366                 :          1 :       return "QUANTIFIERS_CEGQI_WITNESS";
     367                 :            : 
     368                 :          1 :     case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP";
     369                 :          1 :     case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP";
     370                 :          1 :     case InferenceId::SEP_LABEL_INTRO: return "SEP_LABEL_INTRO";
     371                 :          1 :     case InferenceId::SEP_LABEL_DEF: return "SEP_LABEL_DEF";
     372                 :          1 :     case InferenceId::SEP_EMP: return "SEP_EMP";
     373                 :          1 :     case InferenceId::SEP_POS_REDUCTION: return "SEP_POS_REDUCTION";
     374                 :          1 :     case InferenceId::SEP_NEG_REDUCTION: return "SEP_NEG_REDUCTION";
     375                 :          1 :     case InferenceId::SEP_REFINEMENT: return "SEP_REFINEMENT";
     376                 :          1 :     case InferenceId::SEP_NIL_NOT_IN_HEAP: return "SEP_NIL_NOT_IN_HEAP";
     377                 :          1 :     case InferenceId::SEP_SYM_BREAK: return "SEP_SYM_BREAK";
     378                 :          1 :     case InferenceId::SEP_WITNESS_FINITE_DATA: return "SEP_WITNESS_FINITE_DATA";
     379                 :          1 :     case InferenceId::SEP_DISTINCT_REF: return "SEP_DISTINCT_REF";
     380                 :          1 :     case InferenceId::SEP_REF_BOUND: return "SEP_REF_BOUND";
     381                 :            : 
     382                 :          1 :     case InferenceId::SETS_SKOLEM: return "SETS_SKOLEM";
     383                 :          1 :     case InferenceId::SETS_CG_SPLIT: return "SETS_CG_SPLIT";
     384                 :          1 :     case InferenceId::SETS_COMPREHENSION: return "SETS_COMPREHENSION";
     385                 :          1 :     case InferenceId::SETS_DEQ: return "SETS_DEQ";
     386                 :          1 :     case InferenceId::SETS_DOWN_CLOSURE: return "SETS_DOWN_CLOSURE";
     387                 :          1 :     case InferenceId::SETS_EQ_CONFLICT: return "SETS_EQ_CONFLICT";
     388                 :          1 :     case InferenceId::SETS_EQ_MEM: return "SETS_EQ_MEM";
     389                 :          1 :     case InferenceId::SETS_EQ_MEM_CONFLICT: return "SETS_EQ_MEM_CONFLICT";
     390                 :          1 :     case InferenceId::SETS_FILTER_DOWN: return "SETS_FILTER_DOWN";
     391                 :          1 :     case InferenceId::SETS_FILTER_UP: return "SETS_FILTER_UP";
     392                 :          1 :     case InferenceId::SETS_FOLD: return "SETS_FOLD";
     393                 :          1 :     case InferenceId::SETS_MAP_DOWN_POSITIVE: return "SETS_MAP_DOWN_POSITIVE";
     394                 :          1 :     case InferenceId::SETS_MAP_UP: return "SETS_MAP_UP";
     395                 :          1 :     case InferenceId::SETS_MEM_EQ: return "SETS_MEM_EQ";
     396                 :          1 :     case InferenceId::SETS_MEM_EQ_CONFLICT: return "SETS_MEM_EQ_CONFLICT";
     397                 :          1 :     case InferenceId::SETS_PROXY: return "SETS_PROXY";
     398                 :          1 :     case InferenceId::SETS_PROXY_SINGLETON: return "SETS_PROXY_SINGLETON";
     399                 :          1 :     case InferenceId::SETS_SINGLETON_EQ: return "SETS_SINGLETON_EQ";
     400                 :          1 :     case InferenceId::SETS_UP_CLOSURE: return "SETS_UP_CLOSURE";
     401                 :          1 :     case InferenceId::SETS_UP_CLOSURE_2: return "SETS_UP_CLOSURE_2";
     402                 :          1 :     case InferenceId::SETS_UP_UNIV: return "SETS_UP_UNIV";
     403                 :          1 :     case InferenceId::SETS_CARD_SPLIT_EMPTY: return "SETS_CARD_SPLIT_EMPTY";
     404                 :          1 :     case InferenceId::SETS_CARD_SPLIT_EQ: return "SETS_CARD_SPLIT_EQ";
     405                 :          1 :     case InferenceId::SETS_CARD_CYCLE: return "SETS_CARD_CYCLE";
     406                 :          1 :     case InferenceId::SETS_CARD_EQUAL: return "SETS_CARD_EQUAL";
     407                 :          1 :     case InferenceId::SETS_CARD_GRAPH_EMP: return "SETS_CARD_GRAPH_EMP";
     408                 :          1 :     case InferenceId::SETS_CARD_GRAPH_EMP_PARENT:
     409                 :          1 :       return "SETS_CARD_GRAPH_EMP_PARENT";
     410                 :          1 :     case InferenceId::SETS_CARD_GRAPH_EQ_PARENT:
     411                 :          1 :       return "SETS_CARD_GRAPH_EQ_PARENT";
     412                 :          1 :     case InferenceId::SETS_CARD_GRAPH_EQ_PARENT_2:
     413                 :          1 :       return "SETS_CARD_GRAPH_EQ_PARENT_2";
     414                 :          1 :     case InferenceId::SETS_CARD_GRAPH_PARENT_SINGLETON:
     415                 :          1 :       return "SETS_CARD_GRAPH_PARENT_SINGLETON";
     416                 :          1 :     case InferenceId::SETS_CARD_MINIMAL: return "SETS_CARD_MINIMAL";
     417                 :          1 :     case InferenceId::SETS_CARD_NEGATIVE_MEMBER:
     418                 :          1 :       return "SETS_CARD_NEGATIVE_MEMBER";
     419                 :          1 :     case InferenceId::SETS_CARD_POSITIVE: return "SETS_CARD_POSITIVE";
     420                 :          1 :     case InferenceId::SETS_CARD_UNIV_SUPERSET: return "SETS_CARD_UNIV_SUPERSET";
     421                 :          1 :     case InferenceId::SETS_CARD_UNIV_TYPE: return "SETS_CARD_UNIV_TYPE";
     422                 :          1 :     case InferenceId::SETS_RELS_IDENTITY_DOWN: return "SETS_RELS_IDENTITY_DOWN";
     423                 :          1 :     case InferenceId::SETS_RELS_IDENTITY_UP: return "SETS_RELS_IDENTITY_UP";
     424                 :          1 :     case InferenceId::SETS_RELS_JOIN_COMPOSE: return "SETS_RELS_JOIN_COMPOSE";
     425                 :          1 :     case InferenceId::SETS_RELS_JOIN_IMAGE_DOWN:
     426                 :          1 :       return "SETS_RELS_JOIN_IMAGE_DOWN";
     427                 :          1 :     case InferenceId::SETS_RELS_JOIN_IMAGE_UP: return "SETS_RELS_JOIN_IMAGE_UP";
     428                 :          1 :     case InferenceId::SETS_RELS_JOIN_SPLIT_1: return "SETS_RELS_JOIN_SPLIT_1";
     429                 :          1 :     case InferenceId::SETS_RELS_JOIN_SPLIT_2: return "SETS_RELS_JOIN_SPLIT_2";
     430                 :          1 :     case InferenceId::SETS_RELS_TABLE_JOIN_UP: return "SETS_RELS_TABLE_JOIN_UP";
     431                 :          1 :     case InferenceId::SETS_RELS_TABLE_JOIN_DOWN:
     432                 :          1 :       return "SETS_RELS_TABLE_JOIN_DOWN";
     433                 :          1 :     case InferenceId::SETS_RELS_PRODUCE_COMPOSE:
     434                 :          1 :       return "SETS_RELS_PRODUCE_COMPOSE";
     435                 :          1 :     case InferenceId::SETS_RELS_PRODUCT_SPLIT: return "SETS_RELS_PRODUCT_SPLIT";
     436                 :          1 :     case InferenceId::SETS_RELS_TCLOSURE_UP: return "SETS_RELS_TCLOSURE_UP";
     437                 :          1 :     case InferenceId::SETS_RELS_TCLOSURE_DOWN: return "SETS_RELS_TCLOSURE_DOWN";
     438                 :          1 :     case InferenceId::SETS_RELS_TRANSPOSE_EQ: return "SETS_RELS_TRANSPOSE_EQ";
     439                 :          1 :     case InferenceId::SETS_RELS_TRANSPOSE_REV: return "SETS_RELS_TRANSPOSE_REV";
     440                 :          1 :     case InferenceId::SETS_RELS_TUPLE_REDUCTION:
     441                 :          1 :       return "SETS_RELS_TUPLE_REDUCTION";
     442                 :          1 :     case InferenceId::SETS_RELS_GROUP_NOT_EMPTY:
     443                 :          1 :       return "SETS_RELS_GROUP_NOT_EMPTY";
     444                 :          1 :     case InferenceId::SETS_RELS_GROUP_UP1: return "SETS_RELS_GROUP_UP1";
     445                 :          1 :     case InferenceId::SETS_RELS_GROUP_UP2: return "SETS_RELS_GROUP_UP2";
     446                 :          1 :     case InferenceId::SETS_RELS_GROUP_DOWN: return "SETS_RELS_GROUP_DOWN";
     447                 :          1 :     case InferenceId::SETS_RELS_GROUP_PART_MEMBER:
     448                 :          1 :       return "SETS_RELS_GROUP_PART_MEMBER";
     449                 :          1 :     case InferenceId::SETS_RELS_GROUP_SAME_PROJECTION:
     450                 :          1 :       return "SETS_RELS_GROUP_SAME_PROJECTION";
     451                 :          1 :     case InferenceId::SETS_RELS_GROUP_SAME_PART:
     452                 :          1 :       return "SETS_RELS_GROUP_SAME_PART";
     453                 :            : 
     454                 :          1 :     case InferenceId::STRINGS_I_NORM_S: return "STRINGS_I_NORM_S";
     455                 :          1 :     case InferenceId::STRINGS_I_CONST_MERGE: return "STRINGS_I_CONST_MERGE";
     456                 :          1 :     case InferenceId::STRINGS_I_CONST_CONFLICT:
     457                 :          1 :       return "STRINGS_I_CONST_CONFLICT";
     458                 :          1 :     case InferenceId::STRINGS_I_CYCLE_CONFLICT:
     459                 :          1 :       return "STRINGS_I_CYCLE_CONFLICT";
     460                 :          1 :     case InferenceId::STRINGS_I_NORM: return "STRINGS_I_NORM";
     461                 :          1 :     case InferenceId::STRINGS_UNIT_SPLIT: return "STRINGS_UNIT_SPLIT";
     462                 :          1 :     case InferenceId::STRINGS_UNIT_INJ_OOB: return "STRINGS_UNIT_INJ_OOB";
     463                 :          1 :     case InferenceId::STRINGS_UNIT_INJ: return "STRINGS_UNIT_INJ";
     464                 :          1 :     case InferenceId::STRINGS_UNIT_CONST_CONFLICT:
     465                 :          1 :       return "STRINGS_UNIT_CONST_CONFLICT";
     466                 :          1 :     case InferenceId::STRINGS_UNIT_INJ_DEQ: return "STRINGS_UNIT_INJ_DEQ";
     467                 :          1 :     case InferenceId::STRINGS_CARD_SP: return "STRINGS_CARD_SP";
     468                 :          1 :     case InferenceId::STRINGS_CARDINALITY: return "STRINGS_CARDINALITY";
     469                 :          1 :     case InferenceId::STRINGS_I_CYCLE_E: return "STRINGS_I_CYCLE_E";
     470                 :          1 :     case InferenceId::STRINGS_I_CYCLE: return "STRINGS_I_CYCLE";
     471                 :          1 :     case InferenceId::STRINGS_F_CONST: return "STRINGS_F_CONST";
     472                 :          1 :     case InferenceId::STRINGS_F_UNIFY: return "STRINGS_F_UNIFY";
     473                 :          1 :     case InferenceId::STRINGS_F_ENDPOINT_EMP: return "STRINGS_F_ENDPOINT_EMP";
     474                 :          1 :     case InferenceId::STRINGS_F_ENDPOINT_EQ: return "STRINGS_F_ENDPOINT_EQ";
     475                 :          1 :     case InferenceId::STRINGS_F_NCTN: return "STRINGS_F_NCTN";
     476                 :          1 :     case InferenceId::STRINGS_N_EQ_CONF: return "STRINGS_N_EQ_CONF";
     477                 :          1 :     case InferenceId::STRINGS_N_ENDPOINT_EMP: return "STRINGS_N_ENDPOINT_EMP";
     478                 :          1 :     case InferenceId::STRINGS_N_UNIFY: return "STRINGS_N_UNIFY";
     479                 :          1 :     case InferenceId::STRINGS_N_ENDPOINT_EQ: return "STRINGS_N_ENDPOINT_EQ";
     480                 :          1 :     case InferenceId::STRINGS_N_CONST: return "STRINGS_N_CONST";
     481                 :          1 :     case InferenceId::STRINGS_INFER_EMP: return "STRINGS_INFER_EMP";
     482                 :          1 :     case InferenceId::STRINGS_SSPLIT_CST_PROP: return "STRINGS_SSPLIT_CST_PROP";
     483                 :          1 :     case InferenceId::STRINGS_SSPLIT_VAR_PROP: return "STRINGS_SSPLIT_VAR_PROP";
     484                 :          1 :     case InferenceId::STRINGS_LEN_SPLIT: return "STRINGS_LEN_SPLIT";
     485                 :          1 :     case InferenceId::STRINGS_LEN_SPLIT_EMP: return "STRINGS_LEN_SPLIT_EMP";
     486                 :          1 :     case InferenceId::STRINGS_SSPLIT_CST: return "STRINGS_SSPLIT_CST";
     487                 :          1 :     case InferenceId::STRINGS_SSPLIT_VAR: return "STRINGS_SSPLIT_VAR";
     488                 :          1 :     case InferenceId::STRINGS_FLOOP: return "STRINGS_FLOOP";
     489                 :          1 :     case InferenceId::STRINGS_FLOOP_CONFLICT: return "STRINGS_FLOOP_CONFLICT";
     490                 :          1 :     case InferenceId::STRINGS_NORMAL_FORM: return "STRINGS_NORMAL_FORM";
     491                 :          1 :     case InferenceId::STRINGS_N_NCTN: return "STRINGS_N_NCTN";
     492                 :          1 :     case InferenceId::STRINGS_LEN_NORM: return "STRINGS_LEN_NORM";
     493                 :          1 :     case InferenceId::STRINGS_DEQ_DISL_EMP_SPLIT:
     494                 :          1 :       return "STRINGS_DEQ_DISL_EMP_SPLIT";
     495                 :          1 :     case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT:
     496                 :          1 :       return "STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT";
     497                 :          1 :     case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT:
     498                 :          1 :       return "STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT";
     499                 :          1 :     case InferenceId::STRINGS_DEQ_STRINGS_EQ: return "STRINGS_DEQ_STRINGS_EQ";
     500                 :          1 :     case InferenceId::STRINGS_DEQ_DISL_STRINGS_SPLIT:
     501                 :          1 :       return "STRINGS_DEQ_DISL_STRINGS_SPLIT";
     502                 :          1 :     case InferenceId::STRINGS_DEQ_LENS_EQ: return "STRINGS_DEQ_LENS_EQ";
     503                 :          1 :     case InferenceId::STRINGS_DEQ_NORM_EMP: return "STRINGS_DEQ_NORM_EMP";
     504                 :          1 :     case InferenceId::STRINGS_DEQ_LENGTH_SP: return "STRINGS_DEQ_LENGTH_SP";
     505                 :          1 :     case InferenceId::STRINGS_DEQ_EXTENSIONALITY:
     506                 :          1 :       return "STRINGS_DEQ_EXTENSIONALITY";
     507                 :          1 :     case InferenceId::STRINGS_CODE_INJ: return "STRINGS_CODE_INJ";
     508                 :          1 :     case InferenceId::STRINGS_ARRAY_UPDATE_UNIT:
     509                 :          1 :       return "STRINGS_ARRAY_UPDATE_UNIT";
     510                 :          1 :     case InferenceId::STRINGS_ARRAY_UPDATE_CONCAT:
     511                 :          1 :       return "STRINGS_ARRAY_UPDATE_CONCAT";
     512                 :          1 :     case InferenceId::STRINGS_ARRAY_UPDATE_CONCAT_INVERSE:
     513                 :          1 :       return "STRINGS_ARRAY_UPDATE_CONCAT_INVERSE";
     514                 :          1 :     case InferenceId::STRINGS_ARRAY_NTH_UNIT: return "STRINGS_ARRAY_NTH_UNIT";
     515                 :          1 :     case InferenceId::STRINGS_ARRAY_NTH_CONCAT:
     516                 :          1 :       return "STRINGS_ARRAY_NTH_CONCAT";
     517                 :          1 :     case InferenceId::STRINGS_ARRAY_NTH_EXTRACT:
     518                 :          1 :       return "STRINGS_ARRAY_NTH_EXTRACT";
     519                 :          1 :     case InferenceId::STRINGS_ARRAY_NTH_UPDATE:
     520                 :          1 :       return "STRINGS_ARRAY_NTH_UPDATE";
     521                 :          1 :     case InferenceId::STRINGS_ARRAY_NTH_TERM_FROM_UPDATE:
     522                 :          1 :       return "STRINGS_ARRAY_NTH_TERM_FROM_UPDATE";
     523                 :          1 :     case InferenceId::STRINGS_ARRAY_UPDATE_BOUND:
     524                 :          1 :       return "STRINGS_ARRAY_UPDATE_BOUND";
     525                 :          1 :     case InferenceId::STRINGS_ARRAY_EQ_SPLIT: return "STRINGS_ARRAY_EQ_SPLIT";
     526                 :          1 :     case InferenceId::STRINGS_ARRAY_NTH_REV: return "STRINGS_ARRAY_NTH_REV";
     527                 :          1 :     case InferenceId::STRINGS_RE_NF_CONFLICT: return "STRINGS_RE_NF_CONFLICT";
     528                 :          1 :     case InferenceId::STRINGS_RE_UNFOLD_POS: return "STRINGS_RE_UNFOLD_POS";
     529                 :          1 :     case InferenceId::STRINGS_RE_UNFOLD_NEG: return "STRINGS_RE_UNFOLD_NEG";
     530                 :          1 :     case InferenceId::STRINGS_RE_INTER_INCLUDE:
     531                 :          1 :       return "STRINGS_RE_INTER_INCLUDE";
     532                 :          1 :     case InferenceId::STRINGS_RE_INTER_CONF: return "STRINGS_RE_INTER_CONF";
     533                 :          1 :     case InferenceId::STRINGS_RE_INTER_INFER: return "STRINGS_RE_INTER_INFER";
     534                 :          1 :     case InferenceId::STRINGS_RE_DELTA: return "STRINGS_RE_DELTA";
     535                 :          1 :     case InferenceId::STRINGS_RE_DELTA_CONF: return "STRINGS_RE_DELTA_CONF";
     536                 :          1 :     case InferenceId::STRINGS_RE_DERIVE: return "STRINGS_RE_DERIVE";
     537                 :          1 :     case InferenceId::STRINGS_EXTF: return "STRINGS_EXTF";
     538                 :          1 :     case InferenceId::STRINGS_EXTF_N: return "STRINGS_EXTF_N";
     539                 :          1 :     case InferenceId::STRINGS_EXTF_D: return "STRINGS_EXTF_D";
     540                 :          1 :     case InferenceId::STRINGS_EXTF_D_N: return "STRINGS_EXTF_D_N";
     541                 :          1 :     case InferenceId::STRINGS_EXTF_EQ_REW: return "STRINGS_EXTF_EQ_REW";
     542                 :          1 :     case InferenceId::STRINGS_EXTF_REW_SAME: return "STRINGS_EXTF_REW_SAME";
     543                 :          1 :     case InferenceId::STRINGS_CTN_TRANS: return "STRINGS_CTN_TRANS";
     544                 :          1 :     case InferenceId::STRINGS_CTN_DECOMPOSE: return "STRINGS_CTN_DECOMPOSE";
     545                 :          1 :     case InferenceId::STRINGS_CTN_NEG_EQUAL: return "STRINGS_CTN_NEG_EQUAL";
     546                 :          1 :     case InferenceId::STRINGS_CTN_POS: return "STRINGS_CTN_POS";
     547                 :          1 :     case InferenceId::STRINGS_REDUCTION: return "STRINGS_REDUCTION";
     548                 :          1 :     case InferenceId::STRINGS_PREFIX_CONFLICT: return "STRINGS_PREFIX_CONFLICT";
     549                 :          1 :     case InferenceId::STRINGS_PREFIX_CONFLICT_MIN:
     550                 :          1 :       return "STRINGS_PREFIX_CONFLICT_MIN";
     551                 :          1 :     case InferenceId::STRINGS_ARITH_BOUND_CONFLICT:
     552                 :          1 :       return "STRINGS_ARITH_BOUND_CONFLICT";
     553                 :          1 :     case InferenceId::STRINGS_REGISTER_TERM_ATOMIC:
     554                 :          1 :       return "STRINGS_REGISTER_TERM_ATOMIC";
     555                 :          1 :     case InferenceId::STRINGS_REGISTER_TERM: return "STRINGS_REGISTER_TERM";
     556                 :          1 :     case InferenceId::STRINGS_CMI_SPLIT: return "STRINGS_CMI_SPLIT";
     557                 :          1 :     case InferenceId::STRINGS_CONST_SEQ_PURIFY:
     558                 :          1 :       return "STRINGS_CONST_SEQ_PURIFY";
     559                 :          1 :     case InferenceId::STRINGS_RE_EQ_ELIM_EQUIV:
     560                 :          1 :       return "STRINGS_RE_EQ_ELIM_EQUIV";
     561                 :            : 
     562                 :          1 :     case InferenceId::UF_BREAK_SYMMETRY: return "UF_BREAK_SYMMETRY";
     563                 :          1 :     case InferenceId::UF_NOT_DISTINCT_ELIM: return "UF_NOT_DISTINCT_ELIM";
     564                 :          1 :     case InferenceId::UF_DISTINCT_DEQ: return "UF_DISTINCT_DEQ";
     565                 :          1 :     case InferenceId::UF_DISTINCT_DEQ_MODEL: return "UF_DISTINCT_DEQ_MODEL";
     566                 :          1 :     case InferenceId::UF_CARD_CLIQUE: return "UF_CARD_CLIQUE";
     567                 :          1 :     case InferenceId::UF_CARD_COMBINED: return "UF_CARD_COMBINED";
     568                 :          1 :     case InferenceId::UF_CARD_ENFORCE_NEGATIVE:
     569                 :          1 :       return "UF_CARD_ENFORCE_NEGATIVE";
     570                 :          1 :     case InferenceId::UF_CARD_SIMPLE_CONFLICT: return "UF_CARD_SIMPLE_CONFLICT";
     571                 :          1 :     case InferenceId::UF_CARD_SPLIT: return "UF_CARD_SPLIT";
     572                 :            : 
     573                 :          1 :     case InferenceId::UF_HO_CG_SPLIT: return "UF_HO_CG_SPLIT";
     574                 :          1 :     case InferenceId::UF_HO_APP_ENCODE: return "UF_HO_APP_ENCODE";
     575                 :          1 :     case InferenceId::UF_HO_APP_CONV_SKOLEM: return "UF_HO_APP_CONV_SKOLEM";
     576                 :          1 :     case InferenceId::UF_HO_EXTENSIONALITY: return "UF_HO_EXTENSIONALITY";
     577                 :          1 :     case InferenceId::UF_HO_MODEL_APP_ENCODE: return "UF_HO_MODEL_APP_ENCODE";
     578                 :          1 :     case InferenceId::UF_HO_MODEL_EXTENSIONALITY:
     579                 :          1 :       return "UF_HO_MODEL_EXTENSIONALITY";
     580                 :          1 :     case InferenceId::UF_HO_LAMBDA_UNIV_EQ: return "HO_LAMBDA_UNIV_EQ";
     581                 :          1 :     case InferenceId::UF_HO_LAMBDA_APP_REDUCE: return "HO_LAMBDA_APP_REDUCE";
     582                 :          1 :     case InferenceId::UF_HO_LAMBDA_LAZY_LIFT: return "UF_HO_LAMBDA_LAZY_LIFT";
     583                 :          1 :     case InferenceId::UF_ARITH_BV_CONV_REDUCTION:
     584                 :          1 :       return "UF_ARITH_BV_CONV_REDUCTION";
     585                 :          1 :     case InferenceId::UF_ARITH_BV_CONV_VALUE_REFINE:
     586                 :          1 :       return "UF_ARITH_BV_CONV_VALUE_REFINE";
     587                 :          1 :     case InferenceId::PARTITION_GENERATOR_PARTITION:
     588                 :          1 :       return "PARTITION_GENERATOR_PARTITION";
     589                 :          1 :     case InferenceId::PLUGIN_LEMMA: return "PLUGIN_LEMMA";
     590                 :          0 :     case InferenceId::UNKNOWN: return "?";
     591                 :            : 
     592                 :          0 :     default:
     593                 :          0 :       DebugUnhandled() << "No print for inference id "
     594                 :          0 :                        << static_cast<size_t>(i);
     595                 :            :       return "?Unhandled";
     596                 :            :   }
     597                 :            : }
     598                 :            : 
     599                 :        402 : std::ostream& operator<<(std::ostream& out, InferenceId i)
     600                 :            : {
     601                 :        402 :   out << toString(i);
     602                 :        402 :   return out;
     603                 :            : }
     604                 :            : 
     605                 :      73988 : Node mkInferenceIdNode(NodeManager* nm, InferenceId i)
     606                 :            : {
     607                 :     147976 :   return nm->mkConstInt(Rational(static_cast<uint32_t>(i)));
     608                 :            : }
     609                 :            : 
     610                 :       6468 : bool getInferenceId(TNode n, InferenceId& i)
     611                 :            : {
     612                 :            :   uint32_t index;
     613         [ -  + ]:       6468 :   if (!ProofRuleChecker::getUInt32(n, index))
     614                 :            :   {
     615                 :          0 :     return false;
     616                 :            :   }
     617                 :       6468 :   i = static_cast<InferenceId>(index);
     618                 :       6468 :   return true;
     619                 :            : }
     620                 :            : 
     621                 :            : }  // namespace theory
     622                 :            : }  // namespace cvc5::internal