From 48cccffd5fac5cb5ed436ba1457b444185f267fb Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 25 Jun 2018 19:12:23 -0700 Subject: [PATCH] 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/cvc/cvc_printer.cpp | 11 +++++++++++ src/printer/smt2/smt2_printer.cpp | 3 +++ 2 files changed, 14 insertions(+) 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"; -- 2.30.2