diff options
author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2021-10-25 11:36:35 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-25 16:36:35 +0000 |
commit | 0e28a3a86f45e012e59751b0091760f5e2baebd6 (patch) | |
tree | 800cd7d21917b78fcef67ba7b19b14666083a27f /src/theory/inference_id.cpp | |
parent | ec0b33514ffe0b8be065da424348cc1b1d06ecb6 (diff) |
Add inference for count map (#7264)
Diffstat (limited to 'src/theory/inference_id.cpp')
-rw-r--r-- | src/theory/inference_id.cpp | 25 |
1 files changed, 13 insertions, 12 deletions
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index af753dd26..5439e7549 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -103,18 +103,19 @@ const char* toString(InferenceId i) return "ARRAYS_CONST_ARRAY_DEFAULT"; case InferenceId::ARRAYS_EQ_TAUTOLOGY: return "ARRAYS_EQ_TAUTOLOGY"; - 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"; - case InferenceId::BAG_EQUALITY: return "BAG_EQUALITY"; - case InferenceId::BAG_DISEQUALITY: return "BAG_DISEQUALITY"; - case InferenceId::BAG_EMPTY: return "BAG_EMPTY"; - case InferenceId::BAG_UNION_DISJOINT: return "BAG_UNION_DISJOINT"; - case InferenceId::BAG_UNION_MAX: return "BAG_UNION_MAX"; - case InferenceId::BAG_INTERSECTION_MIN: return "BAG_INTERSECTION_MIN"; - case InferenceId::BAG_DIFFERENCE_SUBTRACT: return "BAG_DIFFERENCE_SUBTRACT"; - case InferenceId::BAG_DIFFERENCE_REMOVE: return "BAG_DIFFERENCE_REMOVE"; - case InferenceId::BAG_DUPLICATE_REMOVAL: return "BAG_DUPLICATE_REMOVAL"; + case InferenceId::BAGS_NON_NEGATIVE_COUNT: return "BAGS_NON_NEGATIVE_COUNT"; + case InferenceId::BAGS_MK_BAG_SAME_ELEMENT: return "BAGS_MK_BAG_SAME_ELEMENT"; + case InferenceId::BAGS_MK_BAG: return "BAGS_MK_BAG"; + case InferenceId::BAGS_EQUALITY: return "BAGS_EQUALITY"; + case InferenceId::BAGS_DISEQUALITY: return "BAGS_DISEQUALITY"; + case InferenceId::BAGS_EMPTY: return "BAGS_EMPTY"; + case InferenceId::BAGS_UNION_DISJOINT: return "BAGS_UNION_DISJOINT"; + case InferenceId::BAGS_UNION_MAX: return "BAGS_UNION_MAX"; + case InferenceId::BAGS_INTERSECTION_MIN: return "BAGS_INTERSECTION_MIN"; + case InferenceId::BAGS_DIFFERENCE_SUBTRACT: return "BAGS_DIFFERENCE_SUBTRACT"; + case InferenceId::BAGS_DIFFERENCE_REMOVE: return "BAGS_DIFFERENCE_REMOVE"; + case InferenceId::BAGS_DUPLICATE_REMOVAL: return "BAGS_DUPLICATE_REMOVAL"; + case InferenceId::BAGS_MAP: return "BAGS_MAP"; case InferenceId::BV_BITBLAST_CONFLICT: return "BV_BITBLAST_CONFLICT"; case InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA: |