From cf73d7b9f09bda2356c62d16fab03853e48bacbc Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 18 Feb 2014 23:10:44 -0500
Subject: [PATCH] String parsing example in CVC parser

---
 src/parser/cvc/Cvc.g | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

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]
   ;
 
-- 
2.30.2