diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-25 19:12:23 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-06-25 19:12:23 -0700 |
| commit | 48cccffd5fac5cb5ed436ba1457b444185f267fb (patch) | |
| tree | 578e405261fac0be9d1871df325585834dddddeb /src/printer/smt2 | |
| parent | d73be51484c4628354cbd29a794fc11a1f3b8682 (diff) | |
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.
Diffstat (limited to 'src/printer/smt2')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
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"; |