diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-09-25 13:00:13 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-09-27 09:25:52 -0500 |
| commit | fd085ea019e11e8ac3080431d1a46979ee40af4d (patch) | |
| tree | 095f37c266dc43285aba3eae132ea685466724d4 /src/parser | |
| parent | 89a4d42b358de2d610c64ecbae357efbbcd26ec4 (diff) | |
for morgan to see the regression problems
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 638c64a69..8af543039 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -870,6 +870,10 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] expr = MK_EXPR(kind, args); } } + //| /* substring */ + //LPAREN_TOK STRSUB_TOK n1=INTEGER_LITERAL n2=INTEGER_LITERAL RPAREN_TOK + //{ + //} | /* A non-built-in function application */ LPAREN_TOK functionName[name, CHECK_DECLARED] @@ -1620,6 +1624,7 @@ STRCON_TOK : 'str.++'; STRLEN_TOK : 'str.len'; STRINRE_TOK : 'str.in.re'; STRTORE_TOK : 'str.to.re'; +//STRSUB_TOK : 'str.sub' ; RECON_TOK : 're.++'; REOR_TOK : 're.or'; REINTER_TOK : 're.inter'; |