src/theory/inference_id.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Gereon Kremer
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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 inference enumeration.
  14  */
  15
  16 #include "theory/inference_id.h"
  17
  18 #include <iostream>
  19 #include "proof/proof_checker.h"
  20 #include "util/rational.h"
  21
  22 using namespace cvc5::kind;
  23
  24 namespace cvc5 {
  25 namespace theory {
  26
  27 const char* toString(InferenceId i)
  28 {
  29   switch (i)
  30   {
  31     case InferenceId::EQ_CONSTANT_MERGE: return "EQ_CONSTANT_MERGE";
  32     case InferenceId::COMBINATION_SPLIT: return "COMBINATION_SPLIT";
  33     case InferenceId::EXTT_SIMPLIFY: return "EXTT_SIMPLIFY";
  34     case InferenceId::ARITH_BLACK_BOX: return "ARITH_BLACK_BOX";
  35     case InferenceId::ARITH_CONF_EQ: return "ARITH_CONF_EQ";
  36     case InferenceId::ARITH_CONF_LOWER: return "ARITH_CONF_LOWER";
  37     case InferenceId::ARITH_CONF_TRICHOTOMY: return "ARITH_CONF_TRICHOTOMY";
  38     case InferenceId::ARITH_CONF_UPPER: return "ARITH_CONF_UPPER";
  39     case InferenceId::ARITH_CONF_SIMPLEX: return "ARITH_CONF_SIMPLEX";
  40     case InferenceId::ARITH_CONF_SOI_SIMPLEX: return "ARITH_CONF_SOI_SIMPLEX";
  41     case InferenceId::ARITH_CONF_FACT_QUEUE: return "ARITH_CONF_FACT_QUEUE";
  42     case InferenceId::ARITH_SPLIT_DEQ: return "ARITH_SPLIT_DEQ";
  43     case InferenceId::ARITH_TIGHTEN_CEIL: return "ARITH_TIGHTEN_CEIL";
  44     case InferenceId::ARITH_TIGHTEN_FLOOR: return "ARITH_TIGHTEN_FLOOR";
  45     case InferenceId::ARITH_APPROX_CUT: return "ARITH_APPROX_CUT";
  46     case InferenceId::ARITH_BB_LEMMA: return "ARITH_BB_LEMMA";
  47     case InferenceId::ARITH_DIO_CUT: return "ARITH_DIO_CUT";
  48     case InferenceId::ARITH_DIO_DECOMPOSITION: return "ARITH_DIO_DECOMPOSITION";
  49     case InferenceId::ARITH_UNATE: return "ARITH_UNATE";
  50     case InferenceId::ARITH_ROW_IMPL: return "ARITH_ROW_IMPL";
  51     case InferenceId::ARITH_SPLIT_FOR_NL_MODEL:
  52       return "ARITH_SPLIT_FOR_NL_MODEL";
  53     case InferenceId::ARITH_PP_ELIM_OPERATORS: return "ARITH_PP_ELIM_OPERATORS";
  54     case InferenceId::ARITH_PP_ELIM_OPERATORS_LEMMA:
  55       return "ARITH_PP_ELIM_OPERATORS_LEMMA";
  56     case InferenceId::ARITH_NL_CONGRUENCE: return "ARITH_NL_CONGRUENCE";
  57     case InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT:
  58       return "ARITH_NL_SHARED_TERM_VALUE_SPLIT";
  59     case InferenceId::ARITH_NL_CM_QUADRATIC_EQ:
  60       return "ARITH_NL_CM_QUADRATIC_EQ";
  61     case InferenceId::ARITH_NL_SPLIT_ZERO: return "ARITH_NL_SPLIT_ZERO";
  62     case InferenceId::ARITH_NL_SIGN: return "ARITH_NL_SIGN";
  63     case InferenceId::ARITH_NL_COMPARISON: return "ARITH_NL_COMPARISON";
  64     case InferenceId::ARITH_NL_INFER_BOUNDS: return "ARITH_NL_INFER_BOUNDS";
  65     case InferenceId::ARITH_NL_INFER_BOUNDS_NT:
  66       return "ARITH_NL_INFER_BOUNDS_NT";
  67     case InferenceId::ARITH_NL_FACTOR: return "ARITH_NL_FACTOR";
  68     case InferenceId::ARITH_NL_RES_INFER_BOUNDS:
  69       return "ARITH_NL_RES_INFER_BOUNDS";
  70     case InferenceId::ARITH_NL_TANGENT_PLANE: return "ARITH_NL_TANGENT_PLANE";
  71     case InferenceId::ARITH_NL_T_PURIFY_ARG: return "ARITH_NL_T_PURIFY_ARG";
  72     case InferenceId::ARITH_NL_T_INIT_REFINE: return "ARITH_NL_T_INIT_REFINE";
  73     case InferenceId::ARITH_NL_T_PI_BOUND: return "ARITH_NL_T_PI_BOUND";
  74     case InferenceId::ARITH_NL_T_MONOTONICITY: return "ARITH_NL_T_MONOTONICITY";
  75     case InferenceId::ARITH_NL_T_SECANT: return "ARITH_NL_T_SECANT";
  76     case InferenceId::ARITH_NL_T_TANGENT: return "ARITH_NL_T_TANGENT";
  77     case InferenceId::ARITH_NL_IAND_INIT_REFINE:
  78       return "ARITH_NL_IAND_INIT_REFINE";
  79     case InferenceId::ARITH_NL_IAND_VALUE_REFINE:
  80       return "ARITH_NL_IAND_VALUE_REFINE";
  81     case InferenceId::ARITH_NL_IAND_SUM_REFINE:
  82       return "ARITH_NL_IAND_SUM_REFINE";
  83     case InferenceId::ARITH_NL_IAND_BITWISE_REFINE:
  84       return "ARITH_NL_IAND_BITWISE_REFINE";
  85     case InferenceId::ARITH_NL_POW2_INIT_REFINE:
  86       return "ARITH_NL_POW2_INIT_REFINE";
  87     case InferenceId::ARITH_NL_POW2_VALUE_REFINE:
  88       return "ARITH_NL_POW2_VALUE_REFINE";
  89     case InferenceId::ARITH_NL_POW2_MONOTONE_REFINE:
  90       return "ARITH_NL_POW2_MONOTONE_REFINE";
  91     case InferenceId::ARITH_NL_POW2_TRIVIAL_CASE_REFINE:
  92       return "ARITH_NL_POW2_TRIVIAL_CASE_REFINE";
  93     case InferenceId::ARITH_NL_CAD_CONFLICT: return "ARITH_NL_CAD_CONFLICT";
  94     case InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL:
  95       return "ARITH_NL_CAD_EXCLUDED_INTERVAL";
  96     case InferenceId::ARITH_NL_ICP_CONFLICT: return "ARITH_NL_ICP_CONFLICT";
  97     case InferenceId::ARITH_NL_ICP_PROPAGATION:
  98       return "ARITH_NL_ICP_PROPAGATION";
  99
 100     case InferenceId::ARRAYS_EXT: return "ARRAYS_EXT";
 101     case InferenceId::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE";
 102     case InferenceId::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1";
 103     case InferenceId::ARRAYS_READ_OVER_WRITE_CONTRA: return "ARRAYS_READ_OVER_WRITE_CONTRA";
 104     case InferenceId::ARRAYS_CONST_ARRAY_DEFAULT:
 105       return "ARRAYS_CONST_ARRAY_DEFAULT";
 106     case InferenceId::ARRAYS_EQ_TAUTOLOGY: return "ARRAYS_EQ_TAUTOLOGY";
 107
 108     case InferenceId::BAGS_NON_NEGATIVE_COUNT: return "BAGS_NON_NEGATIVE_COUNT";
 109     case InferenceId::BAGS_BAG_MAKE: return "BAGS_BAG_MAKE";
 110     case InferenceId::BAGS_BAG_MAKE_SPLIT: return "BAGS_BAG_MAKE_SPLIT";
 111     case InferenceId::BAGS_COUNT_SKOLEM: return "BAGS_COUNT_SKOLEM";
 112     case InferenceId::BAGS_EQUALITY: return "BAGS_EQUALITY";
 113     case InferenceId::BAGS_DISEQUALITY: return "BAGS_DISEQUALITY";
 114     case InferenceId::BAGS_EMPTY: return "BAGS_EMPTY";
 115     case InferenceId::BAGS_UNION_DISJOINT: return "BAGS_UNION_DISJOINT";
 116     case InferenceId::BAGS_UNION_MAX: return "BAGS_UNION_MAX";
 117     case InferenceId::BAGS_INTERSECTION_MIN: return "BAGS_INTERSECTION_MIN";
 118     case InferenceId::BAGS_DIFFERENCE_SUBTRACT:
 119       return "BAGS_DIFFERENCE_SUBTRACT";
 120     case InferenceId::BAGS_DIFFERENCE_REMOVE: return "BAGS_DIFFERENCE_REMOVE";
 121     case InferenceId::BAGS_DUPLICATE_REMOVAL: return "BAGS_DUPLICATE_REMOVAL";
 122     case InferenceId::BAGS_MAP: return "BAGS_MAP";
 123     case InferenceId::BAGS_FOLD: return "BAGS_FOLD";
 124     case InferenceId::BAGS_CARD: return "BAGS_CARD";
 125
 126     case InferenceId::BV_BITBLAST_CONFLICT: return "BV_BITBLAST_CONFLICT";
 127     case InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA:
 128       return "BV_BITBLAST_EAGER_LEMMA";
 129     case InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA:
 130       return "BV_BITBLAST_INTERNAL_BITBLAST_LEMMA";
 131     case InferenceId::BV_LAYERED_CONFLICT: return "BV_LAYERED_CONFLICT";
 132     case InferenceId::BV_LAYERED_LEMMA: return "BV_LAYERED_LEMMA";
 133     case InferenceId::BV_EXTF_LEMMA: return "BV_EXTF_LEMMA";
 134     case InferenceId::BV_EXTF_COLLAPSE: return "BV_EXTF_COLLAPSE";
 135
 136     case InferenceId::DATATYPES_PURIFY: return "DATATYPES_PURIFY";
 137     case InferenceId::DATATYPES_UNIF: return "DATATYPES_UNIF";
 138     case InferenceId::DATATYPES_INST: return "DATATYPES_INST";
 139     case InferenceId::DATATYPES_SPLIT: return "DATATYPES_SPLIT";
 140     case InferenceId::DATATYPES_BINARY_SPLIT: return "DATATYPES_BINARY_SPLIT";
 141     case InferenceId::DATATYPES_LABEL_EXH: return "DATATYPES_LABEL_EXH";
 142     case InferenceId::DATATYPES_COLLAPSE_SEL: return "DATATYPES_COLLAPSE_SEL";
 143     case InferenceId::DATATYPES_CLASH_CONFLICT:
 144       return "DATATYPES_CLASH_CONFLICT";
 145     case InferenceId::DATATYPES_TESTER_CONFLICT:
 146       return "DATATYPES_TESTER_CONFLICT";
 147     case InferenceId::DATATYPES_TESTER_MERGE_CONFLICT:
 148       return "DATATYPES_TESTER_MERGE_CONFLICT";
 149     case InferenceId::DATATYPES_BISIMILAR: return "DATATYPES_BISIMILAR";
 150     case InferenceId::DATATYPES_REC_SINGLETON_EQ:
 151       return "DATATYPES_REC_SINGLETON_EQ";
 152     case InferenceId::DATATYPES_REC_SINGLETON_FORCE_DEQ:
 153       return "DATATYPES_REC_SINGLETON_FORCE_DEQ";
 154     case InferenceId::DATATYPES_CYCLE: return "DATATYPES_CYCLE";
 155     case InferenceId::DATATYPES_SIZE_POS: return "DATATYPES_SIZE_POS";
 156     case InferenceId::DATATYPES_HEIGHT_ZERO: return "DATATYPES_HEIGHT_ZERO";
 157     case InferenceId::DATATYPES_SYGUS_SYM_BREAK:
 158       return "DATATYPES_SYGUS_SYM_BREAK";
 159     case InferenceId::DATATYPES_SYGUS_CDEP_SYM_BREAK:
 160       return "DATATYPES_SYGUS_CDEP_SYM_BREAK";
 161     case InferenceId::DATATYPES_SYGUS_ENUM_SYM_BREAK:
 162       return "DATATYPES_SYGUS_ENUM_SYM_BREAK";
 163     case InferenceId::DATATYPES_SYGUS_SIMPLE_SYM_BREAK:
 164       return "DATATYPES_SYGUS_SIMPLE_SYM_BREAK";
 165     case InferenceId::DATATYPES_SYGUS_FAIR_SIZE:
 166       return "DATATYPES_SYGUS_FAIR_SIZE";
 167     case InferenceId::DATATYPES_SYGUS_FAIR_SIZE_CONFLICT:
 168       return "DATATYPES_SYGUS_FAIR_SIZE_CONFLICT";
 169     case InferenceId::DATATYPES_SYGUS_VAR_AGNOSTIC:
 170       return "DATATYPES_SYGUS_VAR_AGNOSTIC";
 171     case InferenceId::DATATYPES_SYGUS_SIZE_CORRECTION:
 172       return "DATATYPES_SYGUS_SIZE_CORRECTION";
 173     case InferenceId::DATATYPES_SYGUS_VALUE_CORRECTION:
 174       return "DATATYPES_SYGUS_VALUE_CORRECTION";
 175     case InferenceId::DATATYPES_SYGUS_MT_BOUND:
 176       return "DATATYPES_SYGUS_MT_BOUND";
 177     case InferenceId::DATATYPES_SYGUS_MT_POS: return "DATATYPES_SYGUS_MT_POS";
 178
 179     case InferenceId::FP_PREPROCESS: return "FP_PREPROCESS";
 180     case InferenceId::FP_EQUATE_TERM: return "FP_EQUATE_TERM";
 181     case InferenceId::FP_REGISTER_TERM: return "FP_REGISTER_TERM";
 182
 183     case InferenceId::QUANTIFIERS_INST_E_MATCHING:
 184       return "QUANTIFIERS_INST_E_MATCHING";
 185     case InferenceId::QUANTIFIERS_INST_E_MATCHING_SIMPLE:
 186       return "QUANTIFIERS_INST_E_MATCHING_SIMPLE";
 187     case InferenceId::QUANTIFIERS_INST_E_MATCHING_MT:
 188       return "QUANTIFIERS_INST_E_MATCHING_MT";
 189     case InferenceId::QUANTIFIERS_INST_E_MATCHING_MTL:
 190       return "QUANTIFIERS_INST_E_MATCHING_MTL";
 191     case InferenceId::QUANTIFIERS_INST_E_MATCHING_HO:
 192       return "QUANTIFIERS_INST_E_MATCHING_HO";
 193     case InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN:
 194       return "QUANTIFIERS_INST_E_MATCHING_VAR_GEN";
 195     case InferenceId::QUANTIFIERS_INST_CBQI_CONFLICT:
 196       return "QUANTIFIERS_INST_CBQI_CONFLICT";
 197     case InferenceId::QUANTIFIERS_INST_CBQI_PROP:
 198       return "QUANTIFIERS_INST_CBQI_PROP";
 199     case InferenceId::QUANTIFIERS_INST_FMF_EXH:
 200       return "QUANTIFIERS_INST_FMF_EXH";
 201     case InferenceId::QUANTIFIERS_INST_FMF_FMC:
 202       return "QUANTIFIERS_INST_FMF_FMC";
 203     case InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH:
 204       return "QUANTIFIERS_INST_FMF_FMC_EXH";
 205     case InferenceId::QUANTIFIERS_INST_CEGQI: return "QUANTIFIERS_INST_CEGQI";
 206     case InferenceId::QUANTIFIERS_INST_SYQI: return "QUANTIFIERS_INST_SYQI";
 207     case InferenceId::QUANTIFIERS_INST_ENUM: return "QUANTIFIERS_INST_ENUM";
 208     case InferenceId::QUANTIFIERS_INST_POOL: return "QUANTIFIERS_INST_POOL";
 209     case InferenceId::QUANTIFIERS_BINT_PROXY: return "QUANTIFIERS_BINT_PROXY";
 210     case InferenceId::QUANTIFIERS_BINT_MIN_NG: return "QUANTIFIERS_BINT_MIN_NG";
 211     case InferenceId::QUANTIFIERS_CEGQI_CEX: return "QUANTIFIERS_CEGQI_CEX";
 212     case InferenceId::QUANTIFIERS_CEGQI_CEX_AUX:
 213       return "QUANTIFIERS_CEGQI_CEX_AUX";
 214     case InferenceId::QUANTIFIERS_CEGQI_NESTED_QE:
 215       return "QUANTIFIERS_CEGQI_NESTED_QE";
 216     case InferenceId::QUANTIFIERS_CEGQI_CEX_DEP:
 217       return "QUANTIFIERS_CEGQI_CEX_DEP";
 218     case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA:
 219       return "QUANTIFIERS_CEGQI_VTS_LB_DELTA";
 220     case InferenceId::QUANTIFIERS_CEGQI_VTS_UB_DELTA:
 221       return "QUANTIFIERS_CEGQI_VTS_UB_DELTA";
 222     case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF:
 223       return "QUANTIFIERS_CEGQI_VTS_LB_INF";
 224     case InferenceId::QUANTIFIERS_SYQI_CEX: return "QUANTIFIERS_SYQI_CEX";
 225     case InferenceId::QUANTIFIERS_SYQI_EVAL_UNFOLD:
 226       return "QUANTIFIERS_SYQI_EVAL_UNFOLD";
 227     case InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC:
 228       return "QUANTIFIERS_SYGUS_QE_PREPROC";
 229     case InferenceId::QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT:
 230       return "QUANTIFIERS_SYGUS_ENUM_ACTIVE_GUARD_SPLIT";
 231     case InferenceId::QUANTIFIERS_SYGUS_EXCLUDE_CURRENT:
 232       return "QUANTIFIERS_SYGUS_EXCLUDE_CURRENT";
 233     case InferenceId::QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT:
 234       return "QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT";
 235     case InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA:
 236       return "QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA";
 237     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB:
 238       return "QUANTIFIERS_SYGUS_UNIF_PI_INTER_ENUM_SB";
 239     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_SEPARATION:
 240       return "QUANTIFIERS_SYGUS_UNIF_PI_SEPARATION";
 241     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_FAIR_SIZE:
 242       return "QUANTIFIERS_SYGUS_UNIF_PI_FAIR_SIZE";
 243     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_REM_OPS:
 244       return "QUANTIFIERS_SYGUS_UNIF_PI_REM_OPS";
 245     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB:
 246       return "QUANTIFIERS_SYGUS_UNIF_PI_ENUM_SB";
 247     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN:
 248       return "QUANTIFIERS_SYGUS_UNIF_PI_DOMAIN";
 249     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_COND_EXCLUDE:
 250       return "QUANTIFIERS_SYGUS_UNIF_PI_COND_EXCLUDE";
 251     case InferenceId::QUANTIFIERS_SYGUS_UNIF_PI_REFINEMENT:
 252       return "QUANTIFIERS_SYGUS_UNIF_PI_REFINEMENT";
 253     case InferenceId::QUANTIFIERS_SYGUS_CEGIS_UCL_SYM_BREAK:
 254       return "QUANTIFIERS_SYGUS_CEGIS_UCL_SYM_BREAK";
 255     case InferenceId::QUANTIFIERS_SYGUS_CEGIS_UCL_EXCLUDE:
 256       return "QUANTIFIERS_SYGUS_CEGIS_UCL_EXCLUDE";
 257     case InferenceId::QUANTIFIERS_SYGUS_REPAIR_CONST_EXCLUDE:
 258       return "QUANTIFIERS_SYGUS_REPAIR_CONST_EXCLUDE";
 259     case InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE:
 260       return "QUANTIFIERS_SYGUS_CEGIS_REFINE";
 261     case InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE_SAMPLE:
 262       return "QUANTIFIERS_SYGUS_CEGIS_REFINE_SAMPLE";
 263     case InferenceId::QUANTIFIERS_SYGUS_REFINE_EVAL:
 264       return "QUANTIFIERS_SYGUS_REFINE_EVAL";
 265     case InferenceId::QUANTIFIERS_SYGUS_EVAL_UNFOLD:
 266       return "QUANTIFIERS_SYGUS_EVAL_UNFOLD";
 267     case InferenceId::QUANTIFIERS_SYGUS_PBE_EXCLUDE:
 268       return "QUANTIFIERS_SYGUS_PBE_EXCLUDE";
 269     case InferenceId::QUANTIFIERS_SYGUS_PBE_CONSTRUCT_SOL:
 270       return "QUANTIFIERS_SYGUS_PBE_CONSTRUCT_SOL";
 271     case InferenceId::QUANTIFIERS_DSPLIT: return "QUANTIFIERS_DSPLIT";
 272     case InferenceId::QUANTIFIERS_CONJ_GEN_SPLIT:
 273       return "QUANTIFIERS_CONJ_GEN_SPLIT";
 274     case InferenceId::QUANTIFIERS_CONJ_GEN_GT_ENUM:
 275       return "QUANTIFIERS_CONJ_GEN_GT_ENUM";
 276     case InferenceId::QUANTIFIERS_SKOLEMIZE: return "QUANTIFIERS_SKOLEMIZE";
 277     case InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ:
 278       return "QUANTIFIERS_REDUCE_ALPHA_EQ";
 279     case InferenceId::QUANTIFIERS_HO_MATCH_PRED:
 280       return "QUANTIFIERS_HO_MATCH_PRED";
 281     case InferenceId::QUANTIFIERS_HO_PURIFY: return "QUANTIFIERS_HO_PURIFY";
 282     case InferenceId::QUANTIFIERS_PARTIAL_TRIGGER_REDUCE:
 283       return "QUANTIFIERS_PARTIAL_TRIGGER_REDUCE";
 284     case InferenceId::QUANTIFIERS_GT_PURIFY: return "QUANTIFIERS_GT_PURIFY";
 285     case InferenceId::QUANTIFIERS_TDB_DEQ_CONG:
 286       return "QUANTIFIERS_TDB_DEQ_CONG";
 287
 288     case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP";
 289     case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP";
 290     case InferenceId::SEP_LABEL_INTRO: return "SEP_LABEL_INTRO";
 291     case InferenceId::SEP_LABEL_DEF: return "SEP_LABEL_DEF";
 292     case InferenceId::SEP_EMP: return "SEP_EMP";
 293     case InferenceId::SEP_POS_REDUCTION: return "SEP_POS_REDUCTION";
 294     case InferenceId::SEP_NEG_REDUCTION: return "SEP_NEG_REDUCTION";
 295     case InferenceId::SEP_REFINEMENT: return "SEP_REFINEMENT";
 296     case InferenceId::SEP_NIL_NOT_IN_HEAP: return "SEP_NIL_NOT_IN_HEAP";
 297     case InferenceId::SEP_SYM_BREAK: return "SEP_SYM_BREAK";
 298     case InferenceId::SEP_WITNESS_FINITE_DATA: return "SEP_WITNESS_FINITE_DATA";
 299     case InferenceId::SEP_DISTINCT_REF: return "SEP_DISTINCT_REF";
 300     case InferenceId::SEP_REF_BOUND: return "SEP_REF_BOUND";
 301
 302     case InferenceId::SETS_CG_SPLIT: return "SETS_CG_SPLIT";
 303     case InferenceId::SETS_COMPREHENSION: return "SETS_COMPREHENSION";
 304     case InferenceId::SETS_DEQ: return "SETS_DEQ";
 305     case InferenceId::SETS_DOWN_CLOSURE: return "SETS_DOWN_CLOSURE";
 306     case InferenceId::SETS_EQ_CONFLICT: return "SETS_EQ_CONFLICT";
 307     case InferenceId::SETS_EQ_MEM: return "SETS_EQ_MEM";
 308     case InferenceId::SETS_EQ_MEM_CONFLICT: return "SETS_EQ_MEM_CONFLICT";
 309     case InferenceId::SETS_MEM_EQ: return "SETS_MEM_EQ";
 310     case InferenceId::SETS_MEM_EQ_CONFLICT: return "SETS_MEM_EQ_CONFLICT";
 311     case InferenceId::SETS_PROXY: return "SETS_PROXY";
 312     case InferenceId::SETS_PROXY_SINGLETON: return "SETS_PROXY_SINGLETON";
 313     case InferenceId::SETS_SINGLETON_EQ: return "SETS_SINGLETON_EQ";
 314     case InferenceId::SETS_UP_CLOSURE: return "SETS_UP_CLOSURE";
 315     case InferenceId::SETS_UP_CLOSURE_2: return "SETS_UP_CLOSURE_2";
 316     case InferenceId::SETS_UP_UNIV: return "SETS_UP_UNIV";
 317     case InferenceId::SETS_UNIV_TYPE: return "SETS_UNIV_TYPE";
 318     case InferenceId::SETS_CARD_SPLIT_EMPTY: return "SETS_CARD_SPLIT_EMPTY";
 319     case InferenceId::SETS_CARD_CYCLE: return "SETS_CARD_CYCLE";
 320     case InferenceId::SETS_CARD_EQUAL: return "SETS_CARD_EQUAL";
 321     case InferenceId::SETS_CARD_GRAPH_EMP: return "SETS_CARD_GRAPH_EMP";
 322     case InferenceId::SETS_CARD_GRAPH_EMP_PARENT:
 323       return "SETS_CARD_GRAPH_EMP_PARENT";
 324     case InferenceId::SETS_CARD_GRAPH_EQ_PARENT:
 325       return "SETS_CARD_GRAPH_EQ_PARENT";
 326     case InferenceId::SETS_CARD_GRAPH_EQ_PARENT_2:
 327       return "SETS_CARD_GRAPH_EQ_PARENT_2";
 328     case InferenceId::SETS_CARD_GRAPH_PARENT_SINGLETON:
 329       return "SETS_CARD_GRAPH_PARENT_SINGLETON";
 330     case InferenceId::SETS_CARD_MINIMAL: return "SETS_CARD_MINIMAL";
 331     case InferenceId::SETS_CARD_NEGATIVE_MEMBER:
 332       return "SETS_CARD_NEGATIVE_MEMBER";
 333     case InferenceId::SETS_CARD_POSITIVE: return "SETS_CARD_POSITIVE";
 334     case InferenceId::SETS_CARD_UNIV_SUPERSET: return "SETS_CARD_UNIV_SUPERSET";
 335     case InferenceId::SETS_CARD_UNIV_TYPE: return "SETS_CARD_UNIV_TYPE";
 336     case InferenceId::SETS_RELS_IDENTITY_DOWN: return "SETS_RELS_IDENTITY_DOWN";
 337     case InferenceId::SETS_RELS_IDENTITY_UP: return "SETS_RELS_IDENTITY_UP";
 338     case InferenceId::SETS_RELS_JOIN_COMPOSE: return "SETS_RELS_JOIN_COMPOSE";
 339     case InferenceId::SETS_RELS_JOIN_IMAGE_DOWN:
 340       return "SETS_RELS_JOIN_IMAGE_DOWN";
 341     case InferenceId::SETS_RELS_JOIN_IMAGE_UP: return "SETS_RELS_JOIN_IMAGE_UP";
 342     case InferenceId::SETS_RELS_JOIN_SPLIT_1: return "SETS_RELS_JOIN_SPLIT_1";
 343     case InferenceId::SETS_RELS_JOIN_SPLIT_2: return "SETS_RELS_JOIN_SPLIT_2";
 344     case InferenceId::SETS_RELS_PRODUCE_COMPOSE:
 345       return "SETS_RELS_PRODUCE_COMPOSE";
 346     case InferenceId::SETS_RELS_PRODUCT_SPLIT: return "SETS_RELS_PRODUCT_SPLIT";
 347     case InferenceId::SETS_RELS_TCLOSURE_FWD: return "SETS_RELS_TCLOSURE_FWD";
 348     case InferenceId::SETS_RELS_TCLOSURE_UP: return "SETS_RELS_TCLOSURE_UP";
 349     case InferenceId::SETS_RELS_TRANSPOSE_EQ: return "SETS_RELS_TRANSPOSE_EQ";
 350     case InferenceId::SETS_RELS_TRANSPOSE_REV: return "SETS_RELS_TRANSPOSE_REV";
 351     case InferenceId::SETS_RELS_TUPLE_REDUCTION:
 352       return "SETS_RELS_TUPLE_REDUCTION";
 353
 354     case InferenceId::STRINGS_I_NORM_S: return "STRINGS_I_NORM_S";
 355     case InferenceId::STRINGS_I_CONST_MERGE: return "STRINGS_I_CONST_MERGE";
 356     case InferenceId::STRINGS_I_CONST_CONFLICT:
 357       return "STRINGS_I_CONST_CONFLICT";
 358     case InferenceId::STRINGS_I_NORM: return "STRINGS_I_NORM";
 359     case InferenceId::STRINGS_UNIT_INJ: return "STRINGS_UNIT_INJ";
 360     case InferenceId::STRINGS_UNIT_CONST_CONFLICT:
 361       return "STRINGS_UNIT_CONST_CONFLICT";
 362     case InferenceId::STRINGS_UNIT_INJ_DEQ: return "STRINGS_UNIT_INJ_DEQ";
 363     case InferenceId::STRINGS_CARD_SP: return "STRINGS_CARD_SP";
 364     case InferenceId::STRINGS_CARDINALITY: return "STRINGS_CARDINALITY";
 365     case InferenceId::STRINGS_I_CYCLE_E: return "STRINGS_I_CYCLE_E";
 366     case InferenceId::STRINGS_I_CYCLE: return "STRINGS_I_CYCLE";
 367     case InferenceId::STRINGS_F_CONST: return "STRINGS_F_CONST";
 368     case InferenceId::STRINGS_F_UNIFY: return "STRINGS_F_UNIFY";
 369     case InferenceId::STRINGS_F_ENDPOINT_EMP: return "STRINGS_F_ENDPOINT_EMP";
 370     case InferenceId::STRINGS_F_ENDPOINT_EQ: return "STRINGS_F_ENDPOINT_EQ";
 371     case InferenceId::STRINGS_F_NCTN: return "STRINGS_F_NCTN";
 372     case InferenceId::STRINGS_N_EQ_CONF: return "STRINGS_N_EQ_CONF";
 373     case InferenceId::STRINGS_N_ENDPOINT_EMP: return "STRINGS_N_ENDPOINT_EMP";
 374     case InferenceId::STRINGS_N_UNIFY: return "STRINGS_N_UNIFY";
 375     case InferenceId::STRINGS_N_ENDPOINT_EQ: return "STRINGS_N_ENDPOINT_EQ";
 376     case InferenceId::STRINGS_N_CONST: return "STRINGS_N_CONST";
 377     case InferenceId::STRINGS_INFER_EMP: return "STRINGS_INFER_EMP";
 378     case InferenceId::STRINGS_SSPLIT_CST_PROP: return "STRINGS_SSPLIT_CST_PROP";
 379     case InferenceId::STRINGS_SSPLIT_VAR_PROP: return "STRINGS_SSPLIT_VAR_PROP";
 380     case InferenceId::STRINGS_LEN_SPLIT: return "STRINGS_LEN_SPLIT";
 381     case InferenceId::STRINGS_LEN_SPLIT_EMP: return "STRINGS_LEN_SPLIT_EMP";
 382     case InferenceId::STRINGS_SSPLIT_CST: return "STRINGS_SSPLIT_CST";
 383     case InferenceId::STRINGS_SSPLIT_VAR: return "STRINGS_SSPLIT_VAR";
 384     case InferenceId::STRINGS_FLOOP: return "STRINGS_FLOOP";
 385     case InferenceId::STRINGS_FLOOP_CONFLICT: return "STRINGS_FLOOP_CONFLICT";
 386     case InferenceId::STRINGS_NORMAL_FORM: return "STRINGS_NORMAL_FORM";
 387     case InferenceId::STRINGS_N_NCTN: return "STRINGS_N_NCTN";
 388     case InferenceId::STRINGS_LEN_NORM: return "STRINGS_LEN_NORM";
 389     case InferenceId::STRINGS_DEQ_DISL_EMP_SPLIT:
 390       return "STRINGS_DEQ_DISL_EMP_SPLIT";
 391     case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT:
 392       return "STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT";
 393     case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT:
 394       return "STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT";
 395     case InferenceId::STRINGS_DEQ_STRINGS_EQ: return "STRINGS_DEQ_STRINGS_EQ";
 396     case InferenceId::STRINGS_DEQ_DISL_STRINGS_SPLIT:
 397       return "STRINGS_DEQ_DISL_STRINGS_SPLIT";
 398     case InferenceId::STRINGS_DEQ_LENS_EQ: return "STRINGS_DEQ_LENS_EQ";
 399     case InferenceId::STRINGS_DEQ_NORM_EMP: return "STRINGS_DEQ_NORM_EMP";
 400     case InferenceId::STRINGS_DEQ_LENGTH_SP: return "STRINGS_DEQ_LENGTH_SP";
 401     case InferenceId::STRINGS_DEQ_EXTENSIONALITY:
 402       return "STRINGS_DEQ_EXTENSIONALITY";
 403     case InferenceId::STRINGS_CODE_PROXY: return "STRINGS_CODE_PROXY";
 404     case InferenceId::STRINGS_CODE_INJ: return "STRINGS_CODE_INJ";
 405     case InferenceId::STRINGS_ARRAY_UPDATE_UNIT:
 406       return "STRINGS_ARRAY_UPDATE_UNIT";
 407     case InferenceId::STRINGS_ARRAY_UPDATE_CONCAT:
 408       return "STRINGS_ARRAY_UPDATE_CONCAT";
 409     case InferenceId::STRINGS_ARRAY_UPDATE_CONCAT_INVERSE:
 410       return "STRINGS_ARRAY_UPDATE_CONCAT_INVERSE";
 411     case InferenceId::STRINGS_ARRAY_NTH_UNIT: return "STRINGS_ARRAY_NTH_UNIT";
 412     case InferenceId::STRINGS_ARRAY_NTH_CONCAT:
 413       return "STRINGS_ARRAY_NTH_CONCAT";
 414     case InferenceId::STRINGS_ARRAY_NTH_EXTRACT:
 415       return "STRINGS_ARRAY_NTH_EXTRACT";
 416     case InferenceId::STRINGS_ARRAY_NTH_UPDATE:
 417       return "STRINGS_ARRAY_NTH_UPDATE";
 418     case InferenceId::STRINGS_ARRAY_NTH_TERM_FROM_UPDATE:
 419       return "STRINGS_ARRAY_NTH_TERM_FROM_UPDATE";
 420     case InferenceId::STRINGS_ARRAY_NTH_UPDATE_WITH_UNIT:
 421       return "STRINGS_ARRAY_NTH_UPDATE_WITH_UNIT";
 422     case InferenceId::STRINGS_ARRAY_NTH_REV: return "STRINGS_ARRAY_NTH_REV";
 423     case InferenceId::STRINGS_RE_NF_CONFLICT: return "STRINGS_RE_NF_CONFLICT";
 424     case InferenceId::STRINGS_RE_UNFOLD_POS: return "STRINGS_RE_UNFOLD_POS";
 425     case InferenceId::STRINGS_RE_UNFOLD_NEG: return "STRINGS_RE_UNFOLD_NEG";
 426     case InferenceId::STRINGS_RE_INTER_INCLUDE:
 427       return "STRINGS_RE_INTER_INCLUDE";
 428     case InferenceId::STRINGS_RE_INTER_CONF: return "STRINGS_RE_INTER_CONF";
 429     case InferenceId::STRINGS_RE_INTER_INFER: return "STRINGS_RE_INTER_INFER";
 430     case InferenceId::STRINGS_RE_DELTA: return "STRINGS_RE_DELTA";
 431     case InferenceId::STRINGS_RE_DELTA_CONF: return "STRINGS_RE_DELTA_CONF";
 432     case InferenceId::STRINGS_RE_DERIVE: return "STRINGS_RE_DERIVE";
 433     case InferenceId::STRINGS_EXTF: return "STRINGS_EXTF";
 434     case InferenceId::STRINGS_EXTF_N: return "STRINGS_EXTF_N";
 435     case InferenceId::STRINGS_EXTF_D: return "STRINGS_EXTF_D";
 436     case InferenceId::STRINGS_EXTF_D_N: return "STRINGS_EXTF_D_N";
 437     case InferenceId::STRINGS_EXTF_EQ_REW: return "STRINGS_EXTF_EQ_REW";
 438     case InferenceId::STRINGS_CTN_TRANS: return "STRINGS_CTN_TRANS";
 439     case InferenceId::STRINGS_CTN_DECOMPOSE: return "STRINGS_CTN_DECOMPOSE";
 440     case InferenceId::STRINGS_CTN_NEG_EQUAL: return "STRINGS_CTN_NEG_EQUAL";
 441     case InferenceId::STRINGS_CTN_POS: return "STRINGS_CTN_POS";
 442     case InferenceId::STRINGS_REDUCTION: return "STRINGS_REDUCTION";
 443     case InferenceId::STRINGS_PREFIX_CONFLICT: return "STRINGS_PREFIX_CONFLICT";
 444     case InferenceId::STRINGS_ARITH_BOUND_CONFLICT:
 445       return "STRINGS_ARITH_BOUND_CONFLICT";
 446     case InferenceId::STRINGS_REGISTER_TERM_ATOMIC:
 447       return "STRINGS_REGISTER_TERM_ATOMIC";
 448     case InferenceId::STRINGS_REGISTER_TERM: return "STRINGS_REGISTER_TERM";
 449     case InferenceId::STRINGS_CMI_SPLIT: return "STRINGS_CMI_SPLIT";
 450
 451     case InferenceId::UF_BREAK_SYMMETRY: return "UF_BREAK_SYMMETRY";
 452     case InferenceId::UF_CARD_CLIQUE: return "UF_CARD_CLIQUE";
 453     case InferenceId::UF_CARD_COMBINED: return "UF_CARD_COMBINED";
 454     case InferenceId::UF_CARD_ENFORCE_NEGATIVE: return "UF_CARD_ENFORCE_NEGATIVE";
 455     case InferenceId::UF_CARD_EQUIV: return "UF_CARD_EQUIV";
 456     case InferenceId::UF_CARD_MONOTONE_COMBINED: return "UF_CARD_MONOTONE_COMBINED";
 457     case InferenceId::UF_CARD_SIMPLE_CONFLICT: return "UF_CARD_SIMPLE_CONFLICT";
 458     case InferenceId::UF_CARD_SPLIT: return "UF_CARD_SPLIT";
 459
 460     case InferenceId::UF_HO_APP_ENCODE: return "UF_HO_APP_ENCODE";
 461     case InferenceId::UF_HO_APP_CONV_SKOLEM: return "UF_HO_APP_CONV_SKOLEM";
 462     case InferenceId::UF_HO_EXTENSIONALITY: return "UF_HO_EXTENSIONALITY";
 463     case InferenceId::UF_HO_MODEL_APP_ENCODE: return "UF_HO_MODEL_APP_ENCODE";
 464     case InferenceId::UF_HO_MODEL_EXTENSIONALITY:
 465       return "UF_HO_MODEL_EXTENSIONALITY";
 466     case InferenceId::UF_HO_LAMBDA_UNIV_EQ: return "HO_LAMBDA_UNIV_EQ";
 467     case InferenceId::UF_HO_LAMBDA_APP_REDUCE: return "HO_LAMBDA_APP_REDUCE";
 468
 469     default: return "?";
 470   }
 471 }
 472
 473 std::ostream& operator<<(std::ostream& out, InferenceId i)
 474 {
 475   out << toString(i);
 476   return out;
 477 }
 478
 479 Node mkInferenceIdNode(InferenceId i)
 480 {
 481   return NodeManager::currentNM()->mkConstInt(
 482       Rational(static_cast<uint32_t>(i)));
 483 }
 484
 485 bool getInferenceId(TNode n, InferenceId& i)
 486 {
 487   uint32_t index;
 488   if (!ProofRuleChecker::getUInt32(n, index))
 489   {
 490     return false;
 491   }
 492   i = static_cast<InferenceId>(index);
 493   return true;
 494 }
 495
 496 }  // namespace theory
 497 }  // namespace cvc5