From de06ddbed29109ce83b6a2fc0b042fcf64fa6ad4 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 9 Apr 2021 14:41:14 +0200 Subject: [PATCH] Add missing InferenceIds to toString (#6320) This PR adds InferenceIds that were previously missing from the corresponding toString() method. --- src/theory/inference_id.cpp | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) 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"; -- 2.30.2