diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-31 04:21:12 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-31 09:21:12 +0000 |
| commit | c28829ce6fc9861b8f0e902952c9983bba10820a (patch) | |
| tree | fa65880901593d7e4673aad596cf790a51943891 /src/theory/inference_id.cpp | |
| parent | 4e1c3c1c12103ef5d3f2cb3d873247bb66716287 (diff) | |
Add missing inference ids (#6242)
Towards having complete stats on inference ids for each lemma, fact, and conflict.
Diffstat (limited to 'src/theory/inference_id.cpp')
| -rw-r--r-- | src/theory/inference_id.cpp | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index c786117f3..50ede2726 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -23,6 +23,23 @@ const char* toString(InferenceId i) { switch (i) { + case InferenceId::EQ_CONSTANT_MERGE: return "EQ_CONSTANT_MERGE"; + case InferenceId::ARITH_BLACK_BOX: return "ARITH_BLACK_BOX"; + case InferenceId::ARITH_CONF_EQ: return "ARITH_CONF_EQ"; + case InferenceId::ARITH_CONF_LOWER: return "ARITH_CONF_LOWER"; + case InferenceId::ARITH_CONF_TRICHOTOMY: return "ARITH_CONF_TRICHOTOMY"; + case InferenceId::ARITH_CONF_UPPER: return "ARITH_CONF_UPPER"; + case InferenceId::ARITH_CONF_SIMPLEX: return "ARITH_CONF_SIMPLEX"; + case InferenceId::ARITH_CONF_SOI_SIMPLEX: return "ARITH_CONF_SOI_SIMPLEX"; + case InferenceId::ARITH_SPLIT_DEQ: return "ARITH_SPLIT_DEQ"; + case InferenceId::ARITH_TIGHTEN_CEIL: return "ARITH_TIGHTEN_CEIL"; + case InferenceId::ARITH_TIGHTEN_FLOOR: return "ARITH_TIGHTEN_FLOOR"; + case InferenceId::ARITH_APPROX_CUT: return "ARITH_APPROX_CUT"; + case InferenceId::ARITH_BB_LEMMA: return "ARITH_BB_LEMMA"; + case InferenceId::ARITH_DIO_CUT: return "ARITH_DIO_CUT"; + case InferenceId::ARITH_DIO_DECOMPOSITION: return "ARITH_DIO_DECOMPOSITION"; + case InferenceId::ARITH_SPLIT_FOR_NL_MODEL: + return "ARITH_SPLIT_FOR_NL_MODEL"; case InferenceId::ARITH_PP_ELIM_OPERATORS: return "ARITH_PP_ELIM_OPERATORS"; case InferenceId::ARITH_PP_ELIM_OPERATORS_LEMMA: return "ARITH_PP_ELIM_OPERATORS_LEMMA"; @@ -148,6 +165,13 @@ const char* toString(InferenceId i) case InferenceId::QUANTIFIERS_INST_CEGQI: return "QUANTIFIERS_INST_CEGQI"; case InferenceId::QUANTIFIERS_INST_SYQI: return "QUANTIFIERS_INST_SYQI"; case InferenceId::QUANTIFIERS_INST_ENUM: return "QUANTIFIERS_INST_ENUM"; + case InferenceId::QUANTIFIERS_BINT_PROXY: return "QUANTIFIERS_BINT_PROXY"; + case InferenceId::QUANTIFIERS_BINT_MIN_NG: return "QUANTIFIERS_BINT_MIN_NG"; + case InferenceId::QUANTIFIERS_CEGQI_CEX: return "QUANTIFIERS_CEGQI_CEX"; + case InferenceId::QUANTIFIERS_CEGQI_CEX_AUX: + return "QUANTIFIERS_CEGQI_CEX_AUX"; + case InferenceId::QUANTIFIERS_CEGQI_NESTED_QE: + return "QUANTIFIERS_CEGQI_NESTED_QE"; case InferenceId::QUANTIFIERS_CEGQI_CEX_DEP: return "QUANTIFIERS_CEGQI_CEX_DEP"; case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA: @@ -156,6 +180,7 @@ const char* toString(InferenceId i) return "QUANTIFIERS_CEGQI_VTS_UB_DELTA"; case InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF: return "QUANTIFIERS_CEGQI_VTS_LB_INF"; + case InferenceId::QUANTIFIERS_SYQI_CEX: return "QUANTIFIERS_SYQI_CEX"; case InferenceId::QUANTIFIERS_SYQI_EVAL_UNFOLD: return "QUANTIFIERS_SYQI_EVAL_UNFOLD"; case InferenceId::QUANTIFIERS_SYGUS_QE_PREPROC: @@ -168,9 +193,14 @@ const char* toString(InferenceId i) return "QUANTIFIERS_SYGUS_STREAM_EXCLUDE_CURRENT"; case InferenceId::QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA: return "QUANTIFIERS_SYGUS_EXAMPLE_INFER_CONTRA"; + case InferenceId::QUANTIFIERS_DSPLIT: return "QUANTIFIERS_DSPLIT"; case InferenceId::QUANTIFIERS_SKOLEMIZE: return "QUANTIFIERS_SKOLEMIZE"; case InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ: return "QUANTIFIERS_REDUCE_ALPHA_EQ"; + case InferenceId::QUANTIFIERS_HO_MATCH_PRED: + return "QUANTIFIERS_HO_MATCH_PRED"; + case InferenceId::QUANTIFIERS_PARTIAL_TRIGGER_REDUCE: + return "QUANTIFIERS_PARTIAL_TRIGGER_REDUCE"; case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP"; case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP"; @@ -200,6 +230,7 @@ const char* toString(InferenceId i) case InferenceId::SETS_UP_CLOSURE_2: return "SETS_UP_CLOSURE_2"; case InferenceId::SETS_UP_UNIV: return "SETS_UP_UNIV"; case InferenceId::SETS_UNIV_TYPE: return "SETS_UNIV_TYPE"; + case InferenceId::SETS_CARD_SPLIT_EMPTY: return "SETS_CARD_SPLIT_EMPTY"; case InferenceId::SETS_CARD_CYCLE: return "SETS_CARD_CYCLE"; case InferenceId::SETS_CARD_EQUAL: return "SETS_CARD_EQUAL"; case InferenceId::SETS_CARD_GRAPH_EMP: return "SETS_CARD_GRAPH_EMP"; |