diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-16 14:14:33 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-16 19:14:33 +0000 |
| commit | 8c11c5b2683aa13160447aef302d82115a08081a (patch) | |
| tree | c3f878b7d0e4e221be7fb710dd92df5990adc37a /src/theory/inference_id.cpp | |
| parent | d6890791897ddebf1212d3e3147bf7aeb2415b27 (diff) | |
Further standardization of strings statistics (#6128)
Also eliminates use of raw output channel in strings.
Diffstat (limited to 'src/theory/inference_id.cpp')
| -rw-r--r-- | src/theory/inference_id.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 7eeba8497..e53ba35f8 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -292,6 +292,10 @@ const char* toString(InferenceId i) case InferenceId::STRINGS_CTN_POS: return "STRINGS_CTN_POS"; case InferenceId::STRINGS_REDUCTION: return "STRINGS_REDUCTION"; case InferenceId::STRINGS_PREFIX_CONFLICT: return "STRINGS_PREFIX_CONFLICT"; + case InferenceId::STRINGS_REGISTER_TERM_ATOMIC: + return "STRINGS_REGISTER_TERM_ATOMIC"; + case InferenceId::STRINGS_REGISTER_TERM: return "STRINGS_REGISTER_TERM"; + case InferenceId::STRINGS_CMI_SPLIT: return "STRINGS_CMI_SPLIT"; case InferenceId::UF_HO_APP_ENCODE: return "UF_HO_APP_ENCODE"; case InferenceId::UF_HO_APP_CONV_SKOLEM: return "UF_HO_APP_CONV_SKOLEM"; |