diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-06-18 06:04:21 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-06-18 06:04:21 +0000 |
| commit | ebf837cd9401828603ccc949aa1f6ead74572a5b (patch) | |
| tree | 31fe2878a0c77d7b28b9b8d0c9ec09d8aa5f3378 /src/parser | |
| parent | 025262221c7fe1a055330ed6c9c48af77ac991c2 (diff) | |
fixed smt version 1 parser for quantifiers
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt/Smt.g | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 9f1f458c9..d44f7abcb 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -225,6 +225,7 @@ annotatedFormula[CVC4::Expr& expr] Kind kind; std::string name; std::vector<Expr> args; /* = getExprVector(); */ + std::vector<Expr> args2; Expr op; /* Operator expression FIXME: move away kill it */ } : /* a built-in operator application */ @@ -255,8 +256,9 @@ annotatedFormula[CVC4::Expr& expr] { args.push_back(PARSER_STATE->mkVar(name, t)); } )+ annotatedFormula[expr] RPAREN_TOK - { args.push_back(expr); - expr = MK_EXPR(kind, args); + { args2.push_back( MK_EXPR( kind::BOUND_VAR_LIST, args ) ); + args2.push_back(expr); + expr = MK_EXPR(kind, args2); PARSER_STATE->popScope(); } |