diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-08 19:12:41 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-08 19:12:41 +0000 |
| commit | 8b84abb2a69ef595b4ccae8bde56414dd3fa295c (patch) | |
| tree | 508255034dff7dec5d181a8929c8ac41b34ac758 /src/parser | |
| parent | d81e163d8d8351fce8a26f3f9e8a6303fbf1358a (diff) | |
Adding missing operators in SMT2 parser: UMINUS, DIVISION, GEQ, LEQ
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 13 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 1 |
2 files changed, 10 insertions, 4 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index c23ccca6b..89c37883a 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -212,10 +212,12 @@ term[CVC4::Expr& expr] /* Unary AND/OR can be replaced with the argument. It just so happens expr should already by the only argument. */ Assert( expr == args[0] ); - } else if( CVC4::kind::isAssociative(kind) && + } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { /* Special treatment for associative operators with lots of children */ expr = EXPR_MANAGER->mkAssociative(kind,args); + } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) { + expr = MK_EXPR(CVC4::kind::UMINUS, args[0]); } else { PARSER_STATE->checkOperator(kind, args.size()); expr = MK_EXPR(kind, args); @@ -304,15 +306,16 @@ builtinOp[CVC4::Kind& kind] | ITE_TOK { $kind = CVC4::kind::ITE; } | GREATER_THAN_TOK { $kind = CVC4::kind::GT; } - | GREATER_THAN_TOK EQUAL_TOK + | GREATER_THAN_EQUAL_TOK { $kind = CVC4::kind::GEQ; } - | LESS_THAN_TOK EQUAL_TOK + | LESS_THAN_EQUAL_TOK { $kind = CVC4::kind::LEQ; } | LESS_THAN_TOK { $kind = CVC4::kind::LT; } | PLUS_TOK { $kind = CVC4::kind::PLUS; } - | STAR_TOK { $kind = CVC4::kind::MULT; } | MINUS_TOK { $kind = CVC4::kind::MINUS; } + | STAR_TOK { $kind = CVC4::kind::MULT; } + | DIV_TOK { $kind = CVC4::kind::DIVISION; } | SELECT_TOK { $kind = CVC4::kind::SELECT; } | STORE_TOK { $kind = CVC4::kind::STORE; } // NOTE: Theory operators go here @@ -427,8 +430,10 @@ EQUAL_TOK : '='; EXISTS_TOK : 'exists'; FORALL_TOK : 'forall'; GREATER_THAN_TOK : '>'; +GREATER_THAN_EQUAL_TOK : '>='; IMPLIES_TOK : '=>'; LESS_THAN_TOK : '<'; +LESS_THAN_EQUAL_TOK : '<='; MINUS_TOK : '-'; NOT_TOK : 'not'; OR_TOK : 'or'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e25b8217b..23879fda8 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -36,6 +36,7 @@ void Smt2::addArithmeticOperators() { addOperator(kind::MINUS); addOperator(kind::UMINUS); addOperator(kind::MULT); + addOperator(kind::DIVISION); addOperator(kind::LT); addOperator(kind::LEQ); addOperator(kind::GT); |