diff options
Diffstat (limited to 'src/theory/inference_id.cpp')
| -rw-r--r-- | src/theory/inference_id.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index a26147f09..c0700c06e 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -16,6 +16,7 @@ #include "theory/inference_id.h" #include <iostream> +#include "util/rational.h" namespace cvc5 { namespace theory { @@ -243,9 +244,11 @@ const char* toString(InferenceId i) case InferenceId::SEP_DISTINCT_REF: return "SEP_DISTINCT_REF"; case InferenceId::SEP_REF_BOUND: return "SEP_REF_BOUND"; + case InferenceId::SETS_CG_SPLIT: return "SETS_CG_SPLIT"; case InferenceId::SETS_COMPREHENSION: return "SETS_COMPREHENSION"; case InferenceId::SETS_DEQ: return "SETS_DEQ"; case InferenceId::SETS_DOWN_CLOSURE: return "SETS_DOWN_CLOSURE"; + case InferenceId::SETS_EQ_CONFLICT: return "SETS_EQ_CONFLICT"; case InferenceId::SETS_EQ_MEM: return "SETS_EQ_MEM"; case InferenceId::SETS_EQ_MEM_CONFLICT: return "SETS_EQ_MEM_CONFLICT"; case InferenceId::SETS_MEM_EQ: return "SETS_MEM_EQ"; @@ -393,5 +396,10 @@ std::ostream& operator<<(std::ostream& out, InferenceId i) return out; } +Node mkInferenceIdNode(InferenceId i) +{ + return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(i))); +} + } // namespace theory } // namespace cvc5 |