From 48cccffd5fac5cb5ed436ba1457b444185f267fb Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 25 Jun 2018 19:12:23 -0700 Subject: Minor improvements in SMT2 and CVC printers (#2089) This commit adds support for string concatenation, charat, and length operators in the CVC printer and support for re.nostr, re.allchar, and insert into a set in the SMT2 printer. --- src/printer/smt2/smt2_printer.cpp | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/printer/smt2') 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"; -- cgit v1.2.3