add negative int2str

3 files changed, 50 insertions, 10 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 75607b9d8..78be92966 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -195,6 +195,11 @@ tokens {
   BVSLE_TOK = 'BVSLE';
   BVSGE_TOK = 'BVSGE';
 
+  // Strings
+
+  STRING_TOK = 'STRING';
+  SCONCAT_TOK = 'SCONCAT';
+
   // these are parsed by special NUMBER_OR_RANGEOP rule, below
   DECIMAL_LITERAL;
   INTEGER_LITERAL;
@@ -1187,6 +1192,9 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
       t = EXPR_MANAGER->mkBitVectorType(k);
     }
 
+    /* string type */
+  | STRING_TOK { t = EXPR_MANAGER->stringType(); }
+
     /* basic types */
   | BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); }
   | REAL_TOK { t = EXPR_MANAGER->realType(); }
@@ -1810,6 +1818,24 @@ bvTerm[CVC4::Expr& f]
     { f = MK_EXPR(CVC4::kind::BITVECTOR_IS_INTEGER, f); }
   */
 
+  | stringTerm[f]
+  ;
+
+stringTerm[CVC4::Expr& f]
+@init {
+  Expr f2;
+  std::string s;
+  std::vector<Expr> args;
+}
+    /* String prefix operators */
+  : 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); }
+
+    /* string literal */
+  | str[s]
+    { f = MK_CONST(CVC4::String(s)); }
+
   | simpleTerm[f]
   ;
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 6e8e9ea00..f97f4a8ae 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1270,7 +1270,14 @@ builtinOp[CVC4::Kind& kind]
                      if(PARSER_STATE->strictModeEnabled()) {
                        PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode");
                      } }
-
+  //NEW string
+  //STRCONS_TOK    { $kind = CVC4::kind::STRING_CONCAT; }
+  //STRREVCONS_TOK { $kind = CVC4::kind::STRING_CONCAT; }
+  //STRHEAD_TOK    { $kind = CVC4::kind::STRING_CONCAT; }
+  //STRTAIL_TOK    { $kind = CVC4::kind::STRING_CONCAT; }
+  //STRLAST_TOK    { $kind = CVC4::kind::STRING_CONCAT; }
+  //STRFIRST_TOK   { $kind = CVC4::kind::STRING_CONCAT; }
+  //OLD string
   | STRCON_TOK     { $kind = CVC4::kind::STRING_CONCAT; }
   | STRLEN_TOK     { $kind = CVC4::kind::STRING_LENGTH; }
   | STRSUB_TOK     { $kind = CVC4::kind::STRING_SUBSTR; }
@@ -1280,8 +1287,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; }
-  | STRITOS_TOK    { $kind = CVC4::kind::STRING_ITOS; }
-  | STRSTOI_TOK    { $kind = CVC4::kind::STRING_STOI; }
+  | SITOS_TOK      { $kind = CVC4::kind::STRING_ITOS; }
+  | SSTOI_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; }
@@ -1290,7 +1297,7 @@ builtinOp[CVC4::Kind& kind]
   | 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; }
+  | RERANGE_TOK    { $kind = CVC4::kind::REGEXP_RANGE; }
 
   // NOTE: Theory operators go here
   ;
@@ -1652,7 +1659,14 @@ BV2NAT_TOK : 'bv2nat';
 INT2BV_TOK : 'int2bv';
 
 //STRING
-//STRCST_TOK : 'str.cst';
+//NEW
+//STRCONS_TOK : 'str.cons';
+//STRREVCONS_TOK : 'str.revcons';
+//STRHEAD_TOK : 'str.head';
+//STRTAIL_TOK : 'str.tail';
+//STRLAST_TOK : 'str.last';
+//STRFIRST_TOK : 'str.first';
+//OLD
 STRCON_TOK : 'str.++';
 STRLEN_TOK : 'str.len';
 STRSUB_TOK : 'str.substr' ;
@@ -1662,8 +1676,8 @@ 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' ;
+SITOS_TOK : 'int.to.str' ;
+SSTOI_TOK : 'str.to.int' ;
 STRINRE_TOK : 'str.in.re';
 STRTORE_TOK : 'str.to.re';
 RECON_TOK : 're.++';
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 43e7829bb..6520f5517 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -232,7 +232,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 		}
 	} else if( t.getKind() == kind::STRING_ITOS ) {
 		if(options::stringExp()) {
-			Node num = t[0];//NodeManager::currentNM()->mkNode(kind::ABS, t[0]);
+			Node num = NodeManager::currentNM()->mkNode(kind::ABS, t[0]);
 			Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num);
 			Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret);
 
@@ -306,13 +306,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 			conc = NodeManager::currentNM()->mkNode( kind::IMPLIES, g1, conc );
 			conc = NodeManager::currentNM()->mkNode( kind::FORALL, b1v, conc );
 			new_nodes.push_back( conc );
-			/*
+			
 			Node sign = NodeManager::currentNM()->mkNode(kind::ITE, 
 							NodeManager::currentNM()->mkNode(kind::GEQ, t[0], d_zero),
 							NodeManager::currentNM()->mkConst(::CVC4::String("")),
 							NodeManager::currentNM()->mkConst(::CVC4::String("-")));
 			conc = t.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sign, pret) );
-			new_nodes.push_back( conc );*/
+			new_nodes.push_back( conc );
 
 			d_cache[t] = t;
 			retNode = t;