diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-21 08:12:11 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-21 13:12:11 +0000 |
| commit | 09097cd3b9cd3233b938ace34f3513a16ac17f80 (patch) | |
| tree | b889e15b487582e810db61b64dade7e6a14d225b /src/theory/inference_id.cpp | |
| parent | 02dd48563db0c5effd608eda70d4c262309322a6 (diff) | |
Clean up remaining raw uses of output channel (#6161)
After this PR, with only a few exceptions, all calls to output channel for lemmas, conflicts are made through inference manager.
This is work towards standardizing the statistics for theories.
Diffstat (limited to 'src/theory/inference_id.cpp')
| -rw-r--r-- | src/theory/inference_id.cpp | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index e53ba35f8..c786117f3 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -174,6 +174,17 @@ const char* toString(InferenceId i) case InferenceId::SEP_PTO_NEG_PROP: return "SEP_PTO_NEG_PROP"; case InferenceId::SEP_PTO_PROP: return "SEP_PTO_PROP"; + case InferenceId::SEP_LABEL_INTRO: return "SEP_LABEL_INTRO"; + case InferenceId::SEP_LABEL_DEF: return "SEP_LABEL_DEF"; + case InferenceId::SEP_EMP: return "SEP_EMP"; + case InferenceId::SEP_POS_REDUCTION: return "SEP_POS_REDUCTION"; + case InferenceId::SEP_NEG_REDUCTION: return "SEP_NEG_REDUCTION"; + case InferenceId::SEP_REFINEMENT: return "SEP_REFINEMENT"; + case InferenceId::SEP_NIL_NOT_IN_HEAP: return "SEP_NIL_NOT_IN_HEAP"; + case InferenceId::SEP_SYM_BREAK: return "SEP_SYM_BREAK"; + case InferenceId::SEP_WITNESS_FINITE_DATA: return "SEP_WITNESS_FINITE_DATA"; + case InferenceId::SEP_DISTINCT_REF: return "SEP_DISTINCT_REF"; + case InferenceId::SEP_REF_BOUND: return "SEP_REF_BOUND"; case InferenceId::SETS_COMPREHENSION: return "SETS_COMPREHENSION"; case InferenceId::SETS_DEQ: return "SETS_DEQ"; |