diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2021-02-17 15:39:42 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-17 15:39:42 +0100 |
| commit | fb5e3113312322c21a00062b22c358c30fa27101 (patch) | |
| tree | e3809bd67d9f897f5d99b90a8c514acad6ff1976 /src/theory/inference_id.cpp | |
| parent | 2d6de44a51fed47a625ae73181efbcc3dac0c751 (diff) | |
Add InferenceIds for theory of arrays (#5910)
This PR introduces new InferenceIds for the theory of arrays and uses them instead of InferenceId::UNKNOWN.
Diffstat (limited to 'src/theory/inference_id.cpp')
| -rw-r--r-- | src/theory/inference_id.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index c037a035a..5a2158d00 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -46,6 +46,11 @@ const char* toString(InferenceId i) case InferenceId::ARITH_NL_ICP_CONFLICT: return "ICP_CONFLICT"; case InferenceId::ARITH_NL_ICP_PROPAGATION: return "ICP_PROPAGATION"; + case InferenceId::ARRAYS_EXT: return "ARRAYS_EXT"; + case InferenceId::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE"; + case InferenceId::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1"; + case InferenceId::ARRAYS_READ_OVER_WRITE_CONTRA: return "ARRAYS_READ_OVER_WRITE_CONTRA"; + case InferenceId::BAG_NON_NEGATIVE_COUNT: return "BAG_NON_NEGATIVE_COUNT"; case InferenceId::BAG_MK_BAG_SAME_ELEMENT: return "BAG_MK_BAG_SAME_ELEMENT"; case InferenceId::BAG_MK_BAG: return "BAG_MK_BAG"; |