From e0fc2cbe091097d95dbe6dd2eb9b6416b75be279 Mon Sep 17 00:00:00 2001
From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Wed, 3 Feb 2010 19:50:44 +0000
Subject: simple ITE parsing

---
 src/parser/cvc/cvc_parser.g | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'src/parser/cvc')

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,10 +211,25 @@ 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.
-- 
cgit v1.2.3