src/theory/inference_id.cpp

   1 /*********************                                                        */
   2 /*! \file inference_id.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Gereon Kremer, Yoni Zohar
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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.\endverbatim
  11  **
  12  ** \brief Implementation of inference enumeration.
  13  **/
  14
  15 #include "theory/inference_id.h"
  16
  17 namespace CVC4 {
  18 namespace theory {
  19
  20 const char* toString(InferenceId i)
  21 {
  22   switch (i)
  23   {
  24     case InferenceId::ARITH_PP_ELIM_OPERATORS: return "ARITH_PP_ELIM_OPERATORS";
  25     case InferenceId::ARITH_NL_CONGRUENCE: return "ARITH_NL_CONGRUENCE";
  26     case InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT:
  27       return "ARITH_NL_SHARED_TERM_VALUE_SPLIT";
  28     case InferenceId::ARITH_NL_CM_QUADRATIC_EQ:
  29       return "ARITH_NL_CM_QUADRATIC_EQ";
  30     case InferenceId::ARITH_NL_SPLIT_ZERO: return "ARITH_NL_SPLIT_ZERO";
  31     case InferenceId::ARITH_NL_SIGN: return "ARITH_NL_SIGN";
  32     case InferenceId::ARITH_NL_COMPARISON: return "ARITH_NL_COMPARISON";
  33     case InferenceId::ARITH_NL_INFER_BOUNDS: return "ARITH_NL_INFER_BOUNDS";
  34     case InferenceId::ARITH_NL_INFER_BOUNDS_NT:
  35       return "ARITH_NL_INFER_BOUNDS_NT";
  36     case InferenceId::ARITH_NL_FACTOR: return "ARITH_NL_FACTOR";
  37     case InferenceId::ARITH_NL_RES_INFER_BOUNDS:
  38       return "ARITH_NL_RES_INFER_BOUNDS";
  39     case InferenceId::ARITH_NL_TANGENT_PLANE: return "ARITH_NL_TANGENT_PLANE";
  40     case InferenceId::ARITH_NL_T_PURIFY_ARG: return "ARITH_NL_T_PURIFY_ARG";
  41     case InferenceId::ARITH_NL_T_INIT_REFINE: return "ARITH_NL_T_INIT_REFINE";
  42     case InferenceId::ARITH_NL_T_PI_BOUND: return "ARITH_NL_T_PI_BOUND";
  43     case InferenceId::ARITH_NL_T_MONOTONICITY: return "ARITH_NL_T_MONOTONICITY";
  44     case InferenceId::ARITH_NL_T_SECANT: return "ARITH_NL_T_SECANT";
  45     case InferenceId::ARITH_NL_T_TANGENT: return "ARITH_NL_T_TANGENT";
  46     case InferenceId::ARITH_NL_IAND_INIT_REFINE:
  47       return "ARITH_NL_IAND_INIT_REFINE";
  48     case InferenceId::ARITH_NL_IAND_VALUE_REFINE:
  49       return "ARITH_NL_IAND_VALUE_REFINE";
  50     case InferenceId::ARITH_NL_IAND_SUM_REFINE:
  51       return "ARITH_NL_IAND_SUM_REFINE";
  52     case InferenceId::ARITH_NL_IAND_BITWISE_REFINE:
  53       return "ARITH_NL_IAND_BITWISE_REFINE";
  54     case InferenceId::ARITH_NL_CAD_CONFLICT: return "ARITH_NL_CAD_CONFLICT";
  55     case InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL:
  56       return "ARITH_NL_CAD_EXCLUDED_INTERVAL";
  57     case InferenceId::ARITH_NL_ICP_CONFLICT: return "ARITH_NL_ICP_CONFLICT";
  58     case InferenceId::ARITH_NL_ICP_PROPAGATION:
  59       return "ARITH_NL_ICP_PROPAGATION";
  60
  61     case InferenceId::ARRAYS_EXT: return "ARRAYS_EXT";
  62     case InferenceId::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE";
  63     case InferenceId::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1";
  64     case InferenceId::ARRAYS_READ_OVER_WRITE_CONTRA: return "ARRAYS_READ_OVER_WRITE_CONTRA";
  65
  66     case InferenceId::BAG_NON_NEGATIVE_COUNT: return "BAG_NON_NEGATIVE_COUNT";
  67     case InferenceId::BAG_MK_BAG_SAME_ELEMENT: return "BAG_MK_BAG_SAME_ELEMENT";
  68     case InferenceId::BAG_MK_BAG: return "BAG_MK_BAG";
  69     case InferenceId::BAG_EQUALITY: return "BAG_EQUALITY";
  70     case InferenceId::BAG_DISEQUALITY: return "BAG_DISEQUALITY";
  71     case InferenceId::BAG_EMPTY: return "BAG_EMPTY";
  72     case InferenceId::BAG_UNION_DISJOINT: return "BAG_UNION_DISJOINT";
  73     case InferenceId::BAG_UNION_MAX: return "BAG_UNION_MAX";
  74     case InferenceId::BAG_INTERSECTION_MIN: return "BAG_INTERSECTION_MIN";
  75     case InferenceId::BAG_DIFFERENCE_SUBTRACT: return "BAG_DIFFERENCE_SUBTRACT";
  76     case InferenceId::BAG_DIFFERENCE_REMOVE: return "BAG_DIFFERENCE_REMOVE";
  77     case InferenceId::BAG_DUPLICATE_REMOVAL: return "BAG_DUPLICATE_REMOVAL";
  78
  79     case InferenceId::DATATYPES_PURIFY: return "DATATYPES_PURIFY";
  80     case InferenceId::DATATYPES_UNIF: return "DATATYPES_UNIF";
  81     case InferenceId::DATATYPES_INST: return "DATATYPES_INST";
  82     case InferenceId::DATATYPES_SPLIT: return "DATATYPES_SPLIT";
  83     case InferenceId::DATATYPES_BINARY_SPLIT: return "DATATYPES_BINARY_SPLIT";
  84     case InferenceId::DATATYPES_LABEL_EXH: return "DATATYPES_LABEL_EXH";
  85     case InferenceId::DATATYPES_COLLAPSE_SEL: return "DATATYPES_COLLAPSE_SEL";
  86     case InferenceId::DATATYPES_CLASH_CONFLICT:
  87       return "DATATYPES_CLASH_CONFLICT";
  88     case InferenceId::DATATYPES_TESTER_CONFLICT:
  89       return "DATATYPES_TESTER_CONFLICT";
  90     case InferenceId::DATATYPES_TESTER_MERGE_CONFLICT:
  91       return "DATATYPES_TESTER_MERGE_CONFLICT";
  92     case InferenceId::DATATYPES_BISIMILAR: return "DATATYPES_BISIMILAR";
  93     case InferenceId::DATATYPES_REC_SINGLETON_EQ:
  94       return "DATATYPES_REC_SINGLETON_EQ";
  95     case InferenceId::DATATYPES_REC_SINGLETON_FORCE_DEQ:
  96       return "DATATYPES_REC_SINGLETON_FORCE_DEQ";
  97     case InferenceId::DATATYPES_CYCLE: return "DATATYPES_CYCLE";
  98     case InferenceId::DATATYPES_SIZE_POS: return "DATATYPES_SIZE_POS";
  99     case InferenceId::DATATYPES_HEIGHT_ZERO: return "DATATYPES_HEIGHT_ZERO";
 100
 101     case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP";
 102     case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP";
 103
 104     case InferenceId::SETS_COMPREHENSION: return "SETS_COMPREHENSION";
 105     case InferenceId::SETS_DEQ: return "SETS_DEQ";
 106     case InferenceId::SETS_DOWN_CLOSURE: return "SETS_DOWN_CLOSURE";
 107     case InferenceId::SETS_EQ_MEM: return "SETS_EQ_MEM";
 108     case InferenceId::SETS_EQ_MEM_CONFLICT: return "SETS_EQ_MEM_CONFLICT";
 109     case InferenceId::SETS_MEM_EQ: return "SETS_MEM_EQ";
 110     case InferenceId::SETS_MEM_EQ_CONFLICT: return "SETS_MEM_EQ_CONFLICT";
 111     case InferenceId::SETS_PROXY: return "SETS_PROXY";
 112     case InferenceId::SETS_PROXY_SINGLETON: return "SETS_PROXY_SINGLETON";
 113     case InferenceId::SETS_SINGLETON_EQ: return "SETS_SINGLETON_EQ";
 114     case InferenceId::SETS_UP_CLOSURE: return "SETS_UP_CLOSURE";
 115     case InferenceId::SETS_UP_CLOSURE_2: return "SETS_UP_CLOSURE_2";
 116     case InferenceId::SETS_UP_UNIV: return "SETS_UP_UNIV";
 117     case InferenceId::SETS_UNIV_TYPE: return "SETS_UNIV_TYPE";
 118     case InferenceId::SETS_CARD_CYCLE: return "SETS_CARD_CYCLE";
 119     case InferenceId::SETS_CARD_EQUAL: return "SETS_CARD_EQUAL";
 120     case InferenceId::SETS_CARD_GRAPH_EMP: return "SETS_CARD_GRAPH_EMP";
 121     case InferenceId::SETS_CARD_GRAPH_EMP_PARENT:
 122       return "SETS_CARD_GRAPH_EMP_PARENT";
 123     case InferenceId::SETS_CARD_GRAPH_EQ_PARENT:
 124       return "SETS_CARD_GRAPH_EQ_PARENT";
 125     case InferenceId::SETS_CARD_GRAPH_EQ_PARENT_2:
 126       return "SETS_CARD_GRAPH_EQ_PARENT_2";
 127     case InferenceId::SETS_CARD_GRAPH_PARENT_SINGLETON:
 128       return "SETS_CARD_GRAPH_PARENT_SINGLETON";
 129     case InferenceId::SETS_CARD_MINIMAL: return "SETS_CARD_MINIMAL";
 130     case InferenceId::SETS_CARD_NEGATIVE_MEMBER:
 131       return "SETS_CARD_NEGATIVE_MEMBER";
 132     case InferenceId::SETS_CARD_POSITIVE: return "SETS_CARD_POSITIVE";
 133     case InferenceId::SETS_CARD_UNIV_SUPERSET: return "SETS_CARD_UNIV_SUPERSET";
 134     case InferenceId::SETS_CARD_UNIV_TYPE: return "SETS_CARD_UNIV_TYPE";
 135     case InferenceId::SETS_RELS_IDENTITY_DOWN: return "SETS_RELS_IDENTITY_DOWN";
 136     case InferenceId::SETS_RELS_IDENTITY_UP: return "SETS_RELS_IDENTITY_UP";
 137     case InferenceId::SETS_RELS_JOIN_COMPOSE: return "SETS_RELS_JOIN_COMPOSE";
 138     case InferenceId::SETS_RELS_JOIN_IMAGE_DOWN:
 139       return "SETS_RELS_JOIN_IMAGE_DOWN";
 140     case InferenceId::SETS_RELS_JOIN_SPLIT_1: return "SETS_RELS_JOIN_SPLIT_1";
 141     case InferenceId::SETS_RELS_JOIN_SPLIT_2: return "SETS_RELS_JOIN_SPLIT_2";
 142     case InferenceId::SETS_RELS_PRODUCE_COMPOSE:
 143       return "SETS_RELS_PRODUCE_COMPOSE";
 144     case InferenceId::SETS_RELS_PRODUCT_SPLIT: return "SETS_RELS_PRODUCT_SPLIT";
 145     case InferenceId::SETS_RELS_TCLOSURE_FWD: return "SETS_RELS_TCLOSURE_FWD";
 146     case InferenceId::SETS_RELS_TRANSPOSE_EQ: return "SETS_RELS_TRANSPOSE_EQ";
 147     case InferenceId::SETS_RELS_TRANSPOSE_REV: return "SETS_RELS_TRANSPOSE_REV";
 148     case InferenceId::SETS_RELS_TUPLE_REDUCTION:
 149       return "SETS_RELS_TUPLE_REDUCTION";
 150
 151     case InferenceId::STRINGS_I_NORM_S: return "STRINGS_I_NORM_S";
 152     case InferenceId::STRINGS_I_CONST_MERGE: return "STRINGS_I_CONST_MERGE";
 153     case InferenceId::STRINGS_I_CONST_CONFLICT:
 154       return "STRINGS_I_CONST_CONFLICT";
 155     case InferenceId::STRINGS_I_NORM: return "STRINGS_I_NORM";
 156     case InferenceId::STRINGS_UNIT_INJ: return "STRINGS_UNIT_INJ";
 157     case InferenceId::STRINGS_UNIT_CONST_CONFLICT:
 158       return "STRINGS_UNIT_CONST_CONFLICT";
 159     case InferenceId::STRINGS_UNIT_INJ_DEQ: return "STRINGS_UNIT_INJ_DEQ";
 160     case InferenceId::STRINGS_CARD_SP: return "STRINGS_CARD_SP";
 161     case InferenceId::STRINGS_CARDINALITY: return "STRINGS_CARDINALITY";
 162     case InferenceId::STRINGS_I_CYCLE_E: return "STRINGS_I_CYCLE_E";
 163     case InferenceId::STRINGS_I_CYCLE: return "STRINGS_I_CYCLE";
 164     case InferenceId::STRINGS_F_CONST: return "STRINGS_F_CONST";
 165     case InferenceId::STRINGS_F_UNIFY: return "STRINGS_F_UNIFY";
 166     case InferenceId::STRINGS_F_ENDPOINT_EMP: return "STRINGS_F_ENDPOINT_EMP";
 167     case InferenceId::STRINGS_F_ENDPOINT_EQ: return "STRINGS_F_ENDPOINT_EQ";
 168     case InferenceId::STRINGS_F_NCTN: return "STRINGS_F_NCTN";
 169     case InferenceId::STRINGS_N_EQ_CONF: return "STRINGS_N_EQ_CONF";
 170     case InferenceId::STRINGS_N_ENDPOINT_EMP: return "STRINGS_N_ENDPOINT_EMP";
 171     case InferenceId::STRINGS_N_UNIFY: return "STRINGS_N_UNIFY";
 172     case InferenceId::STRINGS_N_ENDPOINT_EQ: return "STRINGS_N_ENDPOINT_EQ";
 173     case InferenceId::STRINGS_N_CONST: return "STRINGS_N_CONST";
 174     case InferenceId::STRINGS_INFER_EMP: return "STRINGS_INFER_EMP";
 175     case InferenceId::STRINGS_SSPLIT_CST_PROP: return "STRINGS_SSPLIT_CST_PROP";
 176     case InferenceId::STRINGS_SSPLIT_VAR_PROP: return "STRINGS_SSPLIT_VAR_PROP";
 177     case InferenceId::STRINGS_LEN_SPLIT: return "STRINGS_LEN_SPLIT";
 178     case InferenceId::STRINGS_LEN_SPLIT_EMP: return "STRINGS_LEN_SPLIT_EMP";
 179     case InferenceId::STRINGS_SSPLIT_CST: return "STRINGS_SSPLIT_CST";
 180     case InferenceId::STRINGS_SSPLIT_VAR: return "STRINGS_SSPLIT_VAR";
 181     case InferenceId::STRINGS_FLOOP: return "STRINGS_FLOOP";
 182     case InferenceId::STRINGS_FLOOP_CONFLICT: return "STRINGS_FLOOP_CONFLICT";
 183     case InferenceId::STRINGS_NORMAL_FORM: return "STRINGS_NORMAL_FORM";
 184     case InferenceId::STRINGS_N_NCTN: return "STRINGS_N_NCTN";
 185     case InferenceId::STRINGS_LEN_NORM: return "STRINGS_LEN_NORM";
 186     case InferenceId::STRINGS_DEQ_DISL_EMP_SPLIT:
 187       return "STRINGS_DEQ_DISL_EMP_SPLIT";
 188     case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT:
 189       return "STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT";
 190     case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT:
 191       return "STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT";
 192     case InferenceId::STRINGS_DEQ_STRINGS_EQ: return "STRINGS_DEQ_STRINGS_EQ";
 193     case InferenceId::STRINGS_DEQ_DISL_STRINGS_SPLIT:
 194       return "STRINGS_DEQ_DISL_STRINGS_SPLIT";
 195     case InferenceId::STRINGS_DEQ_LENS_EQ: return "STRINGS_DEQ_LENS_EQ";
 196     case InferenceId::STRINGS_DEQ_NORM_EMP: return "STRINGS_DEQ_NORM_EMP";
 197     case InferenceId::STRINGS_DEQ_LENGTH_SP: return "STRINGS_DEQ_LENGTH_SP";
 198     case InferenceId::STRINGS_CODE_PROXY: return "STRINGS_CODE_PROXY";
 199     case InferenceId::STRINGS_CODE_INJ: return "STRINGS_CODE_INJ";
 200     case InferenceId::STRINGS_RE_NF_CONFLICT: return "STRINGS_RE_NF_CONFLICT";
 201     case InferenceId::STRINGS_RE_UNFOLD_POS: return "STRINGS_RE_UNFOLD_POS";
 202     case InferenceId::STRINGS_RE_UNFOLD_NEG: return "STRINGS_RE_UNFOLD_NEG";
 203     case InferenceId::STRINGS_RE_INTER_INCLUDE:
 204       return "STRINGS_RE_INTER_INCLUDE";
 205     case InferenceId::STRINGS_RE_INTER_CONF: return "STRINGS_RE_INTER_CONF";
 206     case InferenceId::STRINGS_RE_INTER_INFER: return "STRINGS_RE_INTER_INFER";
 207     case InferenceId::STRINGS_RE_DELTA: return "STRINGS_RE_DELTA";
 208     case InferenceId::STRINGS_RE_DELTA_CONF: return "STRINGS_RE_DELTA_CONF";
 209     case InferenceId::STRINGS_RE_DERIVE: return "STRINGS_RE_DERIVE";
 210     case InferenceId::STRINGS_EXTF: return "STRINGS_EXTF";
 211     case InferenceId::STRINGS_EXTF_N: return "STRINGS_EXTF_N";
 212     case InferenceId::STRINGS_EXTF_D: return "STRINGS_EXTF_D";
 213     case InferenceId::STRINGS_EXTF_D_N: return "STRINGS_EXTF_D_N";
 214     case InferenceId::STRINGS_EXTF_EQ_REW: return "STRINGS_EXTF_EQ_REW";
 215     case InferenceId::STRINGS_CTN_TRANS: return "STRINGS_CTN_TRANS";
 216     case InferenceId::STRINGS_CTN_DECOMPOSE: return "STRINGS_CTN_DECOMPOSE";
 217     case InferenceId::STRINGS_CTN_NEG_EQUAL: return "STRINGS_CTN_NEG_EQUAL";
 218     case InferenceId::STRINGS_CTN_POS: return "STRINGS_CTN_POS";
 219     case InferenceId::STRINGS_REDUCTION: return "STRINGS_REDUCTION";
 220     case InferenceId::STRINGS_PREFIX_CONFLICT: return "STRINGS_PREFIX_CONFLICT";
 221
 222     case InferenceId::UF_HO_APP_ENCODE: return "UF_HO_APP_ENCODE";
 223     case InferenceId::UF_HO_APP_CONV_SKOLEM: return "UF_HO_APP_CONV_SKOLEM";
 224     case InferenceId::UF_HO_EXTENSIONALITY: return "UF_HO_EXTENSIONALITY";
 225     case InferenceId::UF_HO_MODEL_APP_ENCODE: return "UF_HO_MODEL_APP_ENCODE";
 226     case InferenceId::UF_HO_MODEL_EXTENSIONALITY:
 227       return "UF_HO_MODEL_EXTENSIONALITY";
 228
 229     default: return "?";
 230   }
 231 }
 232
 233 std::ostream& operator<<(std::ostream& out, InferenceId i)
 234 {
 235   out << toString(i);
 236   return out;
 237 }
 238
 239 }  // namespace theory
 240 }  // namespace CVC4