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/cvc/cvc_printer.cpp | |
| 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/cvc/cvc_printer.cpp')
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 11 |
1 files changed, 11 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; |