diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-03 22:10:21 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-03 22:10:21 +0000 |
commit | 842fd54de1da122f4c7274796550c2fe21c11db2 (patch) | |
tree | fec6236bc8c3e3b92cd3759ed13f4acc7bc6c6d2 /src/parser/cvc/cvc_parser.g | |
parent | e0fc2cbe091097d95dbe6dd2eb9b6416b75be279 (diff) |
ELSEIF support and parser debugging with '-d parser'
Diffstat (limited to 'src/parser/cvc/cvc_parser.g')
-rw-r--r-- | src/parser/cvc/cvc_parser.g | 22 |
1 files changed, 18 insertions, 4 deletions
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 474c38c96..eb21283a3 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -223,10 +223,24 @@ iteFormula returns [CVC4::Expr formula] { Expr iteCondition, iteThen, iteElse; } - : IF iteCondition = boolFormula - THEN iteThen = boolFormula - ELSE iteElse = boolFormula - ENDIF + : IF iteCondition = boolFormula + THEN iteThen = boolFormula + iteElse = iteElseFormula + ENDIF + { formula = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); } + ; + +/** + * Parses the else part of the ITE, i.e. ELSE f, or ELSIF b THEN f1 ... + */ +iteElseFormula returns [CVC4::Expr formula] +{ + Expr iteCondition, iteThen, iteElse; +} + : ELSE formula = boolFormula + | ELSEIF iteCondition = boolFormula + THEN iteThen = boolFormula + iteElse = iteElseFormula { formula = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); } ; |