diff options
| author | Cristian Cadar <cristic@cs.stanford.edu> | 2009-06-25 05:42:37 +0000 |
|---|---|---|
| committer | Cristian Cadar <cristic@cs.stanford.edu> | 2009-06-25 05:42:37 +0000 |
| commit | 0da7412d643890e299cc83d8f09b8b90d0ae94bd (patch) | |
| tree | 565e8544b6fd77dd3f790cf57e015206c9cd7077 /lib/SMT/smtlib.y | |
| parent | 6b72fb47d929cebe933158e52129c0310db15906 (diff) | |
| download | klee-0da7412d643890e299cc83d8f09b8b90d0ae94bd.tar.gz | |
Added support for flets.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74167 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/SMT/smtlib.y')
| -rw-r--r-- | lib/SMT/smtlib.y | 51 |
1 files changed, 16 insertions, 35 deletions
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y index 2055d0cd..38e58170 100644 --- a/lib/SMT/smtlib.y +++ b/lib/SMT/smtlib.y @@ -100,7 +100,7 @@ int smtliberror(const char *s) %type <node> an_formula an_logical_formula an_atom prop_atom %type <node> an_term basic_term an_fun an_arithmetic_fun an_pred %type <str> logic_name status attribute user_value annotation annotations -%type <str> var +%type <str> var fvar %token <str> NUMERAL_TOK %token <str> SYM_TOK @@ -474,7 +474,6 @@ an_formula: $$ = $1; } - | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK { PARSER->PushVarEnv(); @@ -486,26 +485,16 @@ an_formula: PARSER->PopVarEnv(); } - -/* - | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula RPAREN_TOK - { - CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC3::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - } - - | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_formula RPAREN_TOK + | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK + { + PARSER->PushFVarEnv(); + PARSER->AddFVar(*$4, $5); + } + an_formula annotations { - CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC3::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; + $$ = $8; + PARSER->PopFVarEnv(); } -*/ ; @@ -563,20 +552,16 @@ prop_atom: { $$ = ConstantExpr::create(1, 1); } + | FALSE_TOK { $$ = ConstantExpr::create(0, 1);; } -/* + | fvar { - $$ = $1; + $$ = PARSER->GetFVar(*$1); } - | pred_symb - { - $$ = $1; - } -*/ ; @@ -859,16 +844,12 @@ basic_term: { $$ = ConstantExpr::create(1, 1); } + | BIT0_TOK { $$ = ConstantExpr::create(0, 1);; } -/* - | fvar - { - $$ = $1; - } -*/ + | var { $$ = PARSER->GetVar(*$1); @@ -1108,13 +1089,13 @@ var: } ; -/* + fvar: DOLLAR_TOK SYM_TOK { $$ = $2; } ; -*/ + %% |