diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-13 05:27:42 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-13 05:27:42 +0000 |
commit | e3e4616df5eaa4cf4c568fd15cc04a1e05f75916 (patch) | |
tree | 96ed4c5393a863e496e4d4ea9dfd22d960d0b9ec /src/parser | |
parent | ef4867a2b481be042cbf337527bf296b5ddbb5d0 (diff) |
add disequality token ("/=") and rules to CVC parser
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 3a8db1c03..0a05271e2 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -405,16 +405,22 @@ comparisonFormula[CVC4::Expr& f] @init { Expr e; Kind op; + bool negate; Debug("parser-extra") << "predicate formula: " << AntlrInput::tokenText(LT(1)) << std::endl; } : plusTerm[f] - ( ( EQUAL_TOK { op = CVC4::kind::EQUAL; } - | GT_TOK { op = CVC4::kind::GT; } - | GEQ_TOK { op = CVC4::kind::GEQ; } - | LT_TOK { op = CVC4::kind::LT; } - | LEQ_TOK { op = CVC4::kind::LEQ; }) + ( ( EQUAL_TOK { op = CVC4::kind::EQUAL; negate = false; } + | DISEQUAL_TOK { op = CVC4::kind::EQUAL; negate = true; } + | GT_TOK { op = CVC4::kind::GT; negate = false; } + | GEQ_TOK { op = CVC4::kind::GEQ; negate = false; } + | LT_TOK { op = CVC4::kind::LT; negate = false; } + | LEQ_TOK { op = CVC4::kind::LEQ; negate = false; }) plusTerm[e] - { f = MK_EXPR(op, f, e); } + { f = MK_EXPR(op, f, e); + if(negate) { + f = MK_EXPR(CVC4::kind::NOT, f); + } + } )? ; @@ -605,6 +611,7 @@ SEMICOLON : ';'; ARROW_TOK : '->'; DIV_TOK : '/'; EQUAL_TOK : '='; +DISEQUAL_TOK : '/='; EXP_TOK : '^'; GT_TOK : '>'; GEQ_TOK : '>='; |