diff options
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 11 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 3 |
2 files changed, 14 insertions, 0 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index f06e3e80e..6fa7eadeb 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -907,6 +907,17 @@ void CvcPrinter::toStream( out << "INST_PATTERN_LIST"; break; + // string operators + case kind::STRING_CONCAT: + out << "CONCAT"; + break; + case kind::STRING_CHARAT: + out << "CHARAT"; + break; + case kind::STRING_LENGTH: + out << "LENGTH"; + break; + default: Warning() << "Kind printing not implemented for the case of " << n.getKind() << endl; break; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 320496b91..f6d3cc743 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -605,6 +605,7 @@ void Smt2Printer::toStream(std::ostream& out, out << smtKindString(k, d_variant) << " "; break; case kind::MEMBER: typeChildren = true; + case kind::INSERT: case kind::SET_TYPE: case kind::SINGLETON: case kind::COMPLEMENT: out << smtKindString(k, d_variant) << " "; break; @@ -1068,6 +1069,8 @@ static string smtKindString(Kind k, Variant v) return v == smt2_6_1_variant ? "str.in-re" : "str.in.re"; case kind::STRING_TO_REGEXP: return v == smt2_6_1_variant ? "str.to-re" : "str.to.re"; + case kind::REGEXP_EMPTY: return "re.nostr"; + case kind::REGEXP_SIGMA: return "re.allchar"; case kind::REGEXP_CONCAT: return "re.++"; case kind::REGEXP_UNION: return "re.union"; case kind::REGEXP_INTER: return "re.inter"; |