From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 19 Feb 2014 04:10:44 +0000 (-0500)
Subject: String parsing example in CVC parser
X-Git-Tag: cvc5-1.0.0~7083
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=718d76cb16a0f9dd8db10996d9f61646d4fa2419;p=cvc5.git

String parsing example in CVC parser
---

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