From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Fri, 9 Apr 2021 12:41:14 +0000 (+0200)
Subject: Add missing InferenceIds to toString (#6320)
X-Git-Tag: cvc5-1.0.0~1937
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=de06ddbed29109ce83b6a2fc0b042fcf64fa6ad4;p=cvc5.git

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 8b35f5645..f8eadde4b 100644
--- 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";