From e439cc095fdef2991fd41c5350de18dc96eb16b7 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 15 Apr 2015 23:59:11 -0400
Subject: [PATCH] string parser builtinop changes

---
 src/parser/smt2/Smt2.g   | 51 ----------------------------------------
 src/parser/smt2/smt2.cpp | 27 +++++++++++++++++++--
 2 files changed, 25 insertions(+), 53 deletions(-)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 2c91f3e47..0fa048763 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2043,32 +2043,6 @@ builtinOp[CVC4::Kind& kind]
                        PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode");
                      } }
 
-  | STRCON_TOK     { $kind = CVC4::kind::STRING_CONCAT; }
-  | STRLEN_TOK     { $kind = CVC4::kind::STRING_LENGTH; }
-  | STRSUB_TOK     { $kind = CVC4::kind::STRING_SUBSTR; }
-  | STRCTN_TOK     { $kind = CVC4::kind::STRING_STRCTN; }
-  | STRCAT_TOK     { $kind = CVC4::kind::STRING_CHARAT; }
-  | STRIDOF_TOK    { $kind = CVC4::kind::STRING_STRIDOF; }
-  | STRREPL_TOK    { $kind = CVC4::kind::STRING_STRREPL; }
-  | STRPREF_TOK    { $kind = CVC4::kind::STRING_PREFIX; }
-  | STRSUFF_TOK    { $kind = CVC4::kind::STRING_SUFFIX; }
-  | STRITOS_TOK    { $kind = CVC4::kind::STRING_ITOS; }
-  | STRSTOI_TOK    { $kind = CVC4::kind::STRING_STOI; }
-  | STRU16TOS_TOK    { $kind = CVC4::kind::STRING_U16TOS; }
-  | STRSTOU16_TOK    { $kind = CVC4::kind::STRING_STOU16; }
-  | STRU32TOS_TOK    { $kind = CVC4::kind::STRING_U32TOS; }
-  | STRSTOU32_TOK    { $kind = CVC4::kind::STRING_STOU32; }
-  | STRINRE_TOK    { $kind = CVC4::kind::STRING_IN_REGEXP; }
-  | STRTORE_TOK    { $kind = CVC4::kind::STRING_TO_REGEXP; }
-  | RECON_TOK      { $kind = CVC4::kind::REGEXP_CONCAT; }
-  | REUNION_TOK    { $kind = CVC4::kind::REGEXP_UNION; }
-  | REINTER_TOK    { $kind = CVC4::kind::REGEXP_INTER; }
-  | RESTAR_TOK     { $kind = CVC4::kind::REGEXP_STAR; }
-  | REPLUS_TOK     { $kind = CVC4::kind::REGEXP_PLUS; }
-  | REOPT_TOK      { $kind = CVC4::kind::REGEXP_OPT; }
-  | RERANGE_TOK    { $kind = CVC4::kind::REGEXP_RANGE; }
-  | RELOOP_TOK    { $kind = CVC4::kind::REGEXP_LOOP; }
-  
   | DTSIZE_TOK     { $kind = CVC4::kind::DT_SIZE; }
   
   | FMFCARD_TOK    { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; }
@@ -2449,31 +2423,6 @@ DIVISIBLE_TOK : 'divisible';
 BV2NAT_TOK : 'bv2nat';
 INT2BV_TOK : 'int2bv';
 
-STRCON_TOK : 'str.++';
-STRLEN_TOK : 'str.len';
-STRSUB_TOK : 'str.substr' ;
-STRCTN_TOK : 'str.contains' ;
-STRCAT_TOK : 'str.at' ;
-STRIDOF_TOK : 'str.indexof' ;
-STRREPL_TOK : 'str.replace' ;
-STRPREF_TOK : 'str.prefixof' ;
-STRSUFF_TOK : 'str.suffixof' ;
-STRITOS_TOK : 'int.to.str' ;
-STRSTOI_TOK : 'str.to.int' ;
-STRU16TOS_TOK : 'u16.to.str' ;
-STRSTOU16_TOK : 'str.to.u16' ;
-STRU32TOS_TOK : 'u32.to.str' ;
-STRSTOU32_TOK : 'str.to.u32' ;
-STRINRE_TOK : 'str.in.re';
-STRTORE_TOK : 'str.to.re';
-RECON_TOK : 're.++';
-REUNION_TOK : 're.union';
-REINTER_TOK : 're.inter';
-RESTAR_TOK : 're.*';
-REPLUS_TOK : 're.+';
-REOPT_TOK : 're.opt';
-RERANGE_TOK : 're.range';
-RELOOP_TOK : 're.loop';
 RENOSTR_TOK : 're.nostr';
 REALLCHAR_TOK : 're.allchar';
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 8f0b14328..fbf017e93 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -93,8 +93,31 @@ void Smt2::addBitvectorOperators() {
 }
 
 void Smt2::addStringOperators() {
-  Parser::addOperator(kind::STRING_CONCAT);
-  Parser::addOperator(kind::STRING_LENGTH);
+  addOperator(kind::STRING_CONCAT, "str.++");
+  addOperator(kind::STRING_LENGTH, "str.len");
+  addOperator(kind::STRING_SUBSTR, "str.substr" );
+  addOperator(kind::STRING_STRCTN, "str.contains" );
+  addOperator(kind::STRING_CHARAT, "str.at" );
+  addOperator(kind::STRING_STRIDOF, "str.indexof" );
+  addOperator(kind::STRING_STRREPL, "str.replace" );
+  addOperator(kind::STRING_PREFIX, "str.prefixof" );
+  addOperator(kind::STRING_SUFFIX, "str.suffixof" );
+  addOperator(kind::STRING_ITOS, "int.to.str" );
+  addOperator(kind::STRING_STOI, "str.to.int" );
+  addOperator(kind::STRING_U16TOS, "u16.to.str" );
+  addOperator(kind::STRING_STOU16, "str.to.u16" );
+  addOperator(kind::STRING_U32TOS, "u32.to.str" );
+  addOperator(kind::STRING_STOU32, "str.to.u32" );
+  addOperator(kind::STRING_IN_REGEXP, "str.in.re");
+  addOperator(kind::STRING_TO_REGEXP, "str.to.re");
+  addOperator(kind::REGEXP_CONCAT, "re.++");
+  addOperator(kind::REGEXP_UNION, "re.union");
+  addOperator(kind::REGEXP_INTER, "re.inter");
+  addOperator(kind::REGEXP_STAR, "re.*");
+  addOperator(kind::REGEXP_PLUS, "re.+");
+  addOperator(kind::REGEXP_OPT, "re.opt");
+  addOperator(kind::REGEXP_RANGE, "re.range");
+  addOperator(kind::REGEXP_LOOP, "re.loop");
 }
 
 void Smt2::addFloatingPointOperators() {
-- 
2.30.2