diff options
Diffstat (limited to 'src/theory/strings/infer_info.cpp')
-rw-r--r-- | src/theory/strings/infer_info.cpp | 35 |
1 files changed, 19 insertions, 16 deletions
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index aa7fe8974..cdf764aa8 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -14,30 +14,33 @@ #include "theory/strings/infer_info.h" -using namespace CVC4::kind; - namespace CVC4 { namespace theory { namespace strings { -std::ostream& operator<<(std::ostream& out, Inference i) +const char* toString(Inference i) { switch (i) { - case Inference::N_ENDPOINT_EMP: out << "N_EndpointEmp"; break; - case Inference::N_UNIFY: out << "N_Unify"; break; - case Inference::N_ENDPOINT_EQ: out << "N_EndpointEq"; break; - case Inference::N_CONST: out << "N_Const"; break; - case Inference::INFER_EMP: out << "Infer-Emp"; break; - case Inference::SSPLIT_CST_PROP: out << "S-Split(CST-P)-prop"; break; - case Inference::SSPLIT_VAR_PROP: out << "S-Split(VAR)-prop"; break; - case Inference::LEN_SPLIT: out << "Len-Split(Len)"; break; - case Inference::LEN_SPLIT_EMP: out << "Len-Split(Emp)"; break; - case Inference::SSPLIT_CST: out << "S-Split(CST-P)"; break; - case Inference::SSPLIT_VAR: out << "S-Split(VAR)"; break; - case Inference::FLOOP: out << "F-Loop"; break; - default: out << "?"; break; + case Inference::N_ENDPOINT_EMP: return "N_EndpointEmp"; + case Inference::N_UNIFY: return "N_Unify"; + case Inference::N_ENDPOINT_EQ: return "N_EndpointEq"; + case Inference::N_CONST: return "N_Const"; + case Inference::INFER_EMP: return "Infer-Emp"; + case Inference::SSPLIT_CST_PROP: return "S-Split(CST-P)-prop"; + case Inference::SSPLIT_VAR_PROP: return "S-Split(VAR)-prop"; + case Inference::LEN_SPLIT: return "Len-Split(Len)"; + case Inference::LEN_SPLIT_EMP: return "Len-Split(Emp)"; + case Inference::SSPLIT_CST: return "S-Split(CST-P)"; + case Inference::SSPLIT_VAR: return "S-Split(VAR)"; + case Inference::FLOOP: return "F-Loop"; + default: return "?"; } +} + +std::ostream& operator<<(std::ostream& out, Inference i) +{ + out << toString(i); return out; } |