diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-03 19:50:44 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-03 19:50:44 +0000 |
| commit | e0fc2cbe091097d95dbe6dd2eb9b6416b75be279 (patch) | |
| tree | 8259c8bac6274d16e1d78a9c96ab41fa2fbdfdac /src/parser/cvc | |
| parent | 03ca7cdb382216ef995665cc59a07b4125241965 (diff) | |
simple ITE parsing
Diffstat (limited to 'src/parser/cvc')
| -rw-r--r-- | src/parser/cvc/cvc_parser.g | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 1cbdbd067..474c38c96 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -211,11 +211,26 @@ boolIffFormula returns [CVC4::Expr iffFormula] */ primaryBoolFormula returns [CVC4::Expr formula] : formula = boolAtom + | formula = iteFormula | NOT formula = primaryBoolFormula { formula = mkExpr(CVC4::NOT, formula); } | LPAREN formula = boolFormula RPAREN ; /** + * Parses an ITE boolean formula. + */ +iteFormula returns [CVC4::Expr formula] +{ + Expr iteCondition, iteThen, iteElse; +} + : IF iteCondition = boolFormula + THEN iteThen = boolFormula + ELSE iteElse = boolFormula + ENDIF + { formula = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); } + ; + +/** * Parses the Boolean atoms (variables and predicates). * @return the expression representing the atom. */ |