diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-06 19:00:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-06 19:00:13 -0500 |
| commit | fab7010523fd2e635c2c9dfd382acdefdb96d6b4 (patch) | |
| tree | d69370211e672c9d32534a39d01d6108c24e2261 /src/theory/strings/infer_info.cpp | |
| parent | 45e489e2d48e3edde15be2187e32893fc35d859b (diff) | |
Enum for all remaining string inferences (#4220)
Merges the Flat Form inferences enum into Inferences. Adds documentation for (most of) these inferences. Removes the old infrastructure for inferences based on a debug string in InferenceManager.
Diffstat (limited to 'src/theory/strings/infer_info.cpp')
| -rw-r--r-- | src/theory/strings/infer_info.cpp | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index 07c67e167..6881970ef 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -26,7 +26,15 @@ const char* toString(Inference i) case Inference::I_CONST_MERGE: return "I_CONST_MERGE"; case Inference::I_CONST_CONFLICT: return "I_CONST_CONFLICT"; case Inference::I_NORM: return "I_NORM"; + case Inference::CARD_SP: return "CARD_SP"; case Inference::CARDINALITY: return "CARDINALITY"; + case Inference::I_CYCLE_E: return "I_CYCLE_E"; + case Inference::I_CYCLE: return "I_CYCLE"; + case Inference::F_CONST: return "F_CONST"; + case Inference::F_UNIFY: return "F_UNIFY"; + case Inference::F_ENDPOINT_EMP: return "F_ENDPOINT_EMP"; + case Inference::F_ENDPOINT_EQ: return "F_ENDPOINT_EQ"; + case Inference::F_NCTN: return "F_NCTN"; case Inference::N_ENDPOINT_EMP: return "N_ENDPOINT_EMP"; case Inference::N_UNIFY: return "N_UNIFY"; case Inference::N_ENDPOINT_EQ: return "N_ENDPOINT_EQ"; @@ -39,6 +47,10 @@ const char* toString(Inference i) case Inference::SSPLIT_CST: return "SSPLIT_CST"; case Inference::SSPLIT_VAR: return "SSPLIT_VAR"; case Inference::FLOOP: return "FLOOP"; + case Inference::FLOOP_CONFLICT: return "FLOOP_CONFLICT"; + case Inference::NORMAL_FORM: return "NORMAL_FORM"; + case Inference::N_NCTN: return "N_NCTN"; + case Inference::LEN_NORM: return "LEN_NORM"; case Inference::DEQ_DISL_EMP_SPLIT: return "DEQ_DISL_EMP_SPLIT"; case Inference::DEQ_DISL_FIRST_CHAR_EQ_SPLIT: return "DEQ_DISL_FIRST_CHAR_EQ_SPLIT"; @@ -48,6 +60,9 @@ const char* toString(Inference i) case Inference::DEQ_DISL_STRINGS_SPLIT: return "DEQ_DISL_STRINGS_SPLIT"; case Inference::DEQ_LENS_EQ: return "DEQ_LENS_EQ"; case Inference::DEQ_NORM_EMP: return "DEQ_NORM_EMP"; + case Inference::DEQ_LENGTH_SP: return "DEQ_LENGTH_SP"; + case Inference::CODE_PROXY: return "CODE_PROXY"; + case Inference::CODE_INJ: return "CODE_INJ"; case Inference::RE_NF_CONFLICT: return "RE_NF_CONFLICT"; case Inference::RE_UNFOLD_POS: return "RE_UNFOLD_POS"; case Inference::RE_UNFOLD_NEG: return "RE_UNFOLD_NEG"; @@ -59,6 +74,9 @@ const char* toString(Inference i) case Inference::RE_DERIVE: return "RE_DERIVE"; case Inference::EXTF: return "EXTF"; case Inference::EXTF_N: return "EXTF_N"; + case Inference::EXTF_D: return "EXTF_D"; + case Inference::EXTF_D_N: return "EXTF_D_N"; + case Inference::EXTF_EQ_REW: return "EXTF_EQ_REW"; case Inference::CTN_TRANS: return "CTN_TRANS"; case Inference::CTN_DECOMPOSE: return "CTN_DECOMPOSE"; case Inference::CTN_NEG_EQUAL: return "CTN_NEG_EQUAL"; |