diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-02-18 23:10:44 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-02-20 10:45:23 -0600 |
| commit | cf73d7b9f09bda2356c62d16fab03853e48bacbc (patch) | |
| tree | b0c7edff41d4be92d7b2de331abb09093abd2fbb | |
| parent | 531ec6e52b75cd2f600a3fc781383e7539f2335a (diff) | |
String parsing example in CVC parser
| -rw-r--r-- | src/parser/cvc/Cvc.g | 26 |
1 files changed, 26 insertions, 0 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] ; |