simple ITE parsing

3 files changed, 45 insertions, 12 deletions

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index dbaebf5a5..01235bf88 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -63,17 +63,21 @@ Expr AntlrParser::mkExpr(Kind kind, const Expr& child) {
   return d_exprManager->mkExpr(kind, child);
 }
 
-Expr AntlrParser::mkExpr(Kind kind, const Expr& child_1,
-                                const Expr& child_2) {
+Expr AntlrParser::mkExpr(Kind kind, const Expr& child_1, const Expr& child_2) {
   return d_exprManager->mkExpr(kind, child_1, child_2);
 }
 
+Expr AntlrParser::mkExpr(Kind kind, const Expr& child_1, const Expr& child_2,
+                         const Expr& child_3) {
+  return d_exprManager->mkExpr(kind, child_1, child_2, child_3);
+}
+
 Expr AntlrParser::mkExpr(Kind kind, const std::vector<Expr>& children) {
   return d_exprManager->mkExpr(kind, children);
 }
 
-void AntlrParser::newPredicate(std::string name, 
-                               const std::vector< std::string>& sorts) {
+void AntlrParser::newPredicate(std::string name,
+                               const std::vector<std::string>& sorts) {
   if(sorts.size() == 0) {
     d_varSymbolTable.bindName(name, d_exprManager->mkVar());
   } else {
@@ -81,8 +85,8 @@ void AntlrParser::newPredicate(std::string name,
   }
 }
 
-void AntlrParser::newPredicates(const std::vector<std::string>& names, 
-                                const std::vector< std::string>& sorts) {
+void AntlrParser::newPredicates(const std::vector<std::string>& names,
+                                const std::vector<std::string>& sorts) {
   for(unsigned i = 0; i < names.size(); ++i) {
     newPredicate(names[i], sorts);
   }
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index 3025d44da..ae84318c8 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -99,7 +99,8 @@ protected:
   /**
    * Renames the antlr semantic expression to a given message.
    */
-  void rethrow(antlr::SemanticException& e, std::string msg) throw (antlr::SemanticException);
+  void rethrow(antlr::SemanticException& e, std::string msg)
+      throw (antlr::SemanticException);
 
   /**
    * Returns a variable, given a name and a type.
@@ -150,17 +151,31 @@ protected:
    * Creates a new unary CVC4 expression using the expression manager.
    * @param kind the kind of the expression
    * @param child the child
+   * @return the new unary expression
    */
   Expr mkExpr(Kind kind, const Expr& child);
 
   /**
    * Creates a new binary CVC4 expression using the expression manager.
    * @param kind the kind of the expression
-   * @param children the children of the expression
+   * @param child1 the first child
+   * @param child2 the second child
+   * @return the new binary expression
    */
   Expr mkExpr(Kind kind, const Expr& child_1, const Expr& child_2);
 
   /**
+   * Creates a new ternary CVC4 expression using the expression manager.
+   * @param kind the kind of the expression
+   * @param child_1 the first child
+   * @param child_2 the second child
+   * @param child_3
+   * @return the new ternary expression
+   */
+  Expr mkExpr(Kind kind, const Expr& child_1, const Expr& child_2,
+              const Expr& child_3);
+
+  /**
    * Creates a new CVC4 expression using the expression manager.
    * @param kind the kind of the expression
    * @param children the children of the expression
@@ -173,16 +188,15 @@ protected:
    * @param name the name of the predicate
    * @param sorts the sorts
    */
-  void newPredicate(std::string name, 
-                    const std::vector<std::string>& sorts);
+  void newPredicate(std::string name, const std::vector<std::string>& sorts);
 
   /**
    * Creates new predicates over the given sorts. Each predicate
    * will have arity sorts.size().
    * @param p_names the names of the predicates
    */
-  void newPredicates(const std::vector<std::string>& names,
-                     const std::vector<std::string>& sorts);
+  void newPredicates(const std::vector<std::string>& names, const std::vector<
+      std::string>& sorts);
 
   /**
    * Returns the precedence rank of the kind.
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.
  */