Add missing InferenceIds to toString (#6320)

This PR adds InferenceIds that were previously missing from the corresponding toString() method.

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 8b35f5645ab9b45ec0d5da5acc39f7d6fb18d728..f8eadde4b5d62c1a9b0c2048b815f678a1472481 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -97,6 +97,14 @@ const char* toString(InferenceId i)
     case InferenceId::BAG_DIFFERENCE_REMOVE: return "BAG_DIFFERENCE_REMOVE";
     case InferenceId::BAG_DUPLICATE_REMOVAL: return "BAG_DUPLICATE_REMOVAL";
 
+    case InferenceId::BV_BITBLAST_CONFLICT: return "BV_BITBLAST_CONFLICT";
+    case InferenceId::BV_LAZY_CONFLICT: return "BV_LAZY_CONFLICT";
+    case InferenceId::BV_LAZY_LEMMA: return "BV_LAZY_LEMMA";
+    case InferenceId::BV_SIMPLE_LEMMA: return "BV_SIMPLE_LEMMA";
+    case InferenceId::BV_SIMPLE_BITBLAST_LEMMA: return "BV_SIMPLE_BITBLAST_LEMMA";
+    case InferenceId::BV_EXTF_LEMMA: return "BV_EXTF_LEMMA";
+    case InferenceId::BV_EXTF_COLLAPSE: return "BV_EXTF_COLLAPSE";
+
     case InferenceId::DATATYPES_PURIFY: return "DATATYPES_PURIFY";
     case InferenceId::DATATYPES_UNIF: return "DATATYPES_UNIF";
     case InferenceId::DATATYPES_INST: return "DATATYPES_INST";
@@ -339,6 +347,15 @@ const char* toString(InferenceId i)
     case InferenceId::STRINGS_REGISTER_TERM: return "STRINGS_REGISTER_TERM";
     case InferenceId::STRINGS_CMI_SPLIT: return "STRINGS_CMI_SPLIT";
 
+    case InferenceId::UF_BREAK_SYMMETRY: return "UF_BREAK_SYMMETRY";
+    case InferenceId::UF_CARD_CLIQUE: return "UF_CARD_CLIQUE";
+    case InferenceId::UF_CARD_COMBINED: return "UF_CARD_COMBINED";
+    case InferenceId::UF_CARD_ENFORCE_NEGATIVE: return "UF_CARD_ENFORCE_NEGATIVE";
+    case InferenceId::UF_CARD_EQUIV: return "UF_CARD_EQUIV";
+    case InferenceId::UF_CARD_MONOTONE_COMBINED: return "UF_CARD_MONOTONE_COMBINED";
+    case InferenceId::UF_CARD_SIMPLE_CONFLICT: return "UF_CARD_SIMPLE_CONFLICT";
+    case InferenceId::UF_CARD_SPLIT: return "UF_CARD_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";
     case InferenceId::UF_HO_EXTENSIONALITY: return "UF_HO_EXTENSIONALITY";