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.

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index f06e3e80e7cfef8999e6ccacaa87df2c90b6ea67..6fa7eadeb0313da3f61dc098bd03db867b977d9b 100644 (file)
--- 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 320496b9128209c1333344bc6fc521619980c027..f6d3cc743ba99379382ec1feb53109b3113a57b1 100644 (file)
--- 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";