simple ITE parsing

diff --git a/src/expr/expr.h b/src/expr/expr.h
index 8d0d4f347d096a8aa8402fd081451fa117bc5a31..0bbdcd09a9013013a14832dc95b58768b17cf081 100644 (file)
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -132,10 +132,10 @@ public:
   /**
    * Very basic pretty printer for Expr.
    * This is equivalent to calling e.getNode().printAst(...)
-   * @param o output stream to print to.
+   * @param out output stream to print to.
    * @param indent number of spaces to indent the formula by.
    */
-  void printAst(std::ostream & o, int indent = 0) const;
+  void printAst(std::ostream & out, int indent = 0) const;
   
 private:
   

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 0212b4fdd98b58339c0df80e09daa176992b6bae..78c4f9186fdc2c958db607f15d1e12318c646ddc 100644 (file)
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -128,7 +128,7 @@ void Node::printAst(ostream & o, int ind) const{
   if(getKind() == VARIABLE){
     o << ' ' << getId();
 
-  }else if(getNumChildren() > 1){
+  }else if(getNumChildren() >= 1){
     for(Node::iterator child = begin(); child != end(); ++child){
       (*child).printAst(o, ind+1);
     }

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index dbaebf5a5e6de32748ff51ec7fa44b52dcaf3488..01235bf88c5beb304c8a06821f95beabbbee320b 100644 (file)
--- 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 3025d44da88d008f489a5e2287b9a94de41a4dd3..ae84318c83acf5f5f5f44e5e40aec3a57666b822 100644 (file)
--- 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,16 +151,30 @@ 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
@@ -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 1cbdbd067b3a86d1adc38a9dee063d0e83936da4..474c38c9619ec17eb52c02a924c7f493b6cf25c2 100644 (file)
--- 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.

diff --git a/src/util/command.cpp b/src/util/command.cpp
index 334180967daa12373249dabdae1fb552443c760e..06545a0a0063e603ebd8cd18ee6b03b9e9fc70c4 100644 (file)
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -110,7 +110,9 @@ void CheckSatCommand::toStream(ostream& out) const {
 }
 
 void QueryCommand::toStream(ostream& out) const {
-  out << "Query(" << d_expr << ")";
+  out << "Query(";
+  d_expr.printAst(out, 2);
+  out << ")";
 }
 
 void CommandSequence::toStream(ostream& out) const {

diff --git a/test/regress/logops.cvc b/test/regress/logops.cvc
index 663a659f371a4ee9fe2a0bbc2583d014f3ec40f2..35e0809922baac7c0cb3603d3d083631e419ac6b 100644 (file)
--- a/test/regress/logops.cvc
+++ b/test/regress/logops.cvc
@@ -2,11 +2,13 @@
 
 a, b, c: BOOLEAN;
 
-QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a);
+%% QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a);
 
-QUERY (IF c THEN a ELSE b ENDIF) <=> (c AND a) OR (NOT c AND b);
+%% QUERY NOT c AND b;
 
-QUERY (a => b) <=> (NOT a OR b);
+QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b));
 
-QUERY TRUE XOR FALSE;
+%% QUERY (a => b) <=> (NOT a OR b);
+
+%% QUERY TRUE XOR FALSE;