summaryrefslogtreecommitdiff
path: root/src/theory/inference_id.cpp
diff options
context:
space:
mode:
authormudathirmahgoub <mudathirmahgoub@gmail.com>2021-10-25 11:36:35 -0500
committerGitHub <noreply@github.com>2021-10-25 16:36:35 +0000
commit0e28a3a86f45e012e59751b0091760f5e2baebd6 (patch)
tree800cd7d21917b78fcef67ba7b19b14666083a27f /src/theory/inference_id.cpp
parentec0b33514ffe0b8be065da424348cc1b1d06ecb6 (diff)
Add inference for count map (#7264)
Diffstat (limited to 'src/theory/inference_id.cpp')
-rw-r--r--src/theory/inference_id.cpp25
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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback