smt-lib syntax change: str.contain -> str.contains; add some prefix syntax for cvc format

3 files changed, 34 insertions, 6 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 78be92966..792c3cf9d 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -199,6 +199,15 @@ tokens {
 
   STRING_TOK = 'STRING';
   SCONCAT_TOK = 'SCONCAT';
+  SCONTAINS_TOK = 'CONTAINS';
+  SSUBSTR_TOK = 'SUBSTR';
+  SINDEXOF_TOK = 'INDEXOF';
+  SREPLACE_TOK = 'REPLACE';
+  SPREFIXOF_TOK = 'PREFIXOF';
+  SSUFFIXOF_TOK = 'SUFFIXOF';
+  STOINTEGER_TOK = 'TO_INTEGER';
+  STOSTRING_TOK = 'TO_STRING';
+  STORE_TOK = 'TO_RE';
 
   // these are parsed by special NUMBER_OR_RANGEOP rule, below
   DECIMAL_LITERAL;
@@ -1824,6 +1833,7 @@ bvTerm[CVC4::Expr& f]
 stringTerm[CVC4::Expr& f]
 @init {
   Expr f2;
+  Expr f3;
   std::string s;
   std::vector<Expr> args;
 }
@@ -1831,6 +1841,24 @@ stringTerm[CVC4::Expr& f]
   : SCONCAT_TOK LPAREN formula[f] { args.push_back(f); }
     ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN
     { f = MK_EXPR(CVC4::kind::STRING_CONCAT, args); }
+  | SCONTAINS_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::STRING_STRCTN, f, f2); }
+  | SSUBSTR_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
+    { f = MK_EXPR(CVC4::kind::STRING_SUBSTR, f, f2, f3); }
+  | SINDEXOF_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
+    { f = MK_EXPR(CVC4::kind::STRING_STRIDOF, f, f2, f3); }
+  | SREPLACE_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
+    { f = MK_EXPR(CVC4::kind::STRING_STRREPL, f, f2, f3); }
+  | SPREFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::STRING_PREFIX, f, f2); }
+  | SSUFFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+    { f = MK_EXPR(CVC4::kind::STRING_SUFFIX, f, f2); }
+  | STOINTEGER_TOK LPAREN formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::STRING_STOI, f); }
+  | STOSTRING_TOK LPAREN formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::STRING_ITOS, f); }
+  | STORE_TOK LPAREN formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::STRING_TO_REGEXP, f); }
 
     /* string literal */
   | str[s]
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f1888de39..9b598e113 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1294,8 +1294,8 @@ builtinOp[CVC4::Kind& kind]
   | STRREPL_TOK    { $kind = CVC4::kind::STRING_STRREPL; }
   | STRPREF_TOK    { $kind = CVC4::kind::STRING_PREFIX; }
   | STRSUFF_TOK    { $kind = CVC4::kind::STRING_SUFFIX; }
-  | SITOS_TOK      { $kind = CVC4::kind::STRING_ITOS; }
-  | SSTOI_TOK      { $kind = CVC4::kind::STRING_STOI; }
+  | STRITOS_TOK      { $kind = CVC4::kind::STRING_ITOS; }
+  | STRSTOI_TOK      { $kind = CVC4::kind::STRING_STOI; }
   | STRINRE_TOK    { $kind = CVC4::kind::STRING_IN_REGEXP; }
   | STRTORE_TOK    { $kind = CVC4::kind::STRING_TO_REGEXP; }
   | RECON_TOK      { $kind = CVC4::kind::REGEXP_CONCAT; }
@@ -1688,14 +1688,14 @@ INT2BV_TOK : 'int2bv';
 STRCON_TOK : 'str.++';
 STRLEN_TOK : 'str.len';
 STRSUB_TOK : 'str.substr' ;
-STRCTN_TOK : 'str.contain' ;
+STRCTN_TOK : 'str.contains' ;
 STRCAT_TOK : 'str.at' ;
 STRIDOF_TOK : 'str.indexof' ;
 STRREPL_TOK : 'str.replace' ;
 STRPREF_TOK : 'str.prefixof' ;
 STRSUFF_TOK : 'str.suffixof' ;
-SITOS_TOK : 'int.to.str' ;
-SSTOI_TOK : 'str.to.int' ;
+STRITOS_TOK : 'int.to.str' ;
+STRSTOI_TOK : 'str.to.int' ;
 STRINRE_TOK : 'str.in.re';
 STRTORE_TOK : 'str.to.re';
 RECON_TOK : 're.++';
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 80dcc8248..a2a925d13 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -331,7 +331,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::STRING_SUBSTR_TOTAL:
   case kind::STRING_SUBSTR: out << "str.substr "; break;
   case kind::STRING_CHARAT: out << "str.at "; break;
-  case kind::STRING_STRCTN: out << "str.contain "; break;
+  case kind::STRING_STRCTN: out << "str.contains "; break;
   case kind::STRING_STRIDOF: out << "str.indexof "; break;
   case kind::STRING_STRREPL: out << "str.replace "; break;
   case kind::STRING_PREFIX: out << "str.prefixof "; break;