ELSEIF support and parser debugging with '-d parser'

5 files changed, 53 insertions, 14 deletions

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 01235bf88..3522bfd75 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -47,7 +47,6 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) :
 
 Expr AntlrParser::getVariable(std::string var_name) {
   Expr e = d_varSymbolTable.getObject(var_name);
-  Debug("parser") << "getvar " << var_name << " gives " << e << endl;
   return e;
 }
 
@@ -64,20 +63,27 @@ Expr AntlrParser::mkExpr(Kind kind, const Expr& child) {
 }
 
 Expr AntlrParser::mkExpr(Kind kind, const Expr& child_1, const Expr& child_2) {
-  return d_exprManager->mkExpr(kind, child_1, child_2);
+  Expr result = d_exprManager->mkExpr(kind, child_1, child_2);
+  Debug("parser") << "mkExpr() => " << result << std::endl;
+  return result;
 }
 
 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 result = d_exprManager->mkExpr(kind, child_1, child_2, child_3);
+  Debug("parser") << "mkExpr() => " << result << std::endl;
+  return result;
 }
 
 Expr AntlrParser::mkExpr(Kind kind, const std::vector<Expr>& children) {
-  return d_exprManager->mkExpr(kind, children);
+  Expr result = d_exprManager->mkExpr(kind, children);
+  Debug("parser") << "mkExpr() => " << result << std::endl;
+  return result;
 }
 
 void AntlrParser::newPredicate(std::string name,
                                const std::vector<std::string>& sorts) {
+  Debug("parser") << "newPredicate(" << name << ")" << std::endl;
   if(sorts.size() == 0) {
     d_varSymbolTable.bindName(name, d_exprManager->mkVar());
   } else {
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); }
   ;
 
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index a38868d3b..2f9ac6724 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -19,6 +19,7 @@
 
 #include "parser.h"
 #include "util/command.h"
+#include "util/output.h"
 #include "util/Assert.h"
 #include "parser_exception.h"
 #include "parser/antlr_parser.h"
@@ -41,21 +42,26 @@ bool Parser::done() const {
   return d_done;
 }
 
-Command* Parser::parseNextCommand() throw(ParserException, AssertionException) {
+Command* Parser::parseNextCommand() throw (ParserException, AssertionException) {
+  Debug("parser") << "parseNextCommand()" << std::endl;
   Command* cmd = NULL;
   if(!done()) {
     try {
       cmd = d_antlrParser->parseCommand();
-      if (cmd == NULL) setDone();
+      if(cmd == NULL) {
+        setDone();
+      }
     } catch(antlr::ANTLRException& e) {
       setDone();
       throw ParserException(e.toString());
     }
   }
+  Debug("parser") << "parseNextCommand() => " << cmd << std::endl;
   return cmd;
 }
 
-Expr Parser::parseNextExpression() throw(ParserException, AssertionException) {
+Expr Parser::parseNextExpression() throw (ParserException, AssertionException) {
+  Debug("parser") << "parseNextExpression()" << std::endl;
   Expr result;
   if(!done()) {
     try {
@@ -67,6 +73,7 @@ Expr Parser::parseNextExpression() throw(ParserException, AssertionException) {
       throw ParserException(e.toString());
     }
   }
+  Debug("parser") << "parseNextExpression() => " << result << std::endl;
   return result;
 }
 
@@ -78,8 +85,10 @@ Parser::~Parser() {
   }
 }
 
-Parser::Parser(istream* input, AntlrParser* antlrParser, CharScanner* antlrLexer, bool deleteInput) :
-  d_done(false), d_antlrParser(antlrParser), d_antlrLexer(antlrLexer), d_input(input), d_deleteInput(deleteInput) {
+Parser::Parser(istream* input, AntlrParser* antlrParser,
+               CharScanner* antlrLexer, bool deleteInput) :
+  d_done(false), d_antlrParser(antlrParser), d_antlrLexer(antlrLexer),
+      d_input(input), d_deleteInput(deleteInput) {
 }
 
 Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
diff --git a/src/util/command.cpp b/src/util/command.cpp
index 06545a0a0..90204a63f 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -34,6 +34,15 @@ ostream& operator<<(ostream& out, const Command& c) {
   return out;
 }
 
+ostream& operator<<(ostream& out, const Command* c) {
+  if (c == NULL) {
+    out << "null";
+  } else {
+    c->toStream(out);
+  }
+  return out;
+}
+
 std::string Command::toString() const {
   stringstream ss;
   toStream(ss);
@@ -111,7 +120,7 @@ void CheckSatCommand::toStream(ostream& out) const {
 
 void QueryCommand::toStream(ostream& out) const {
   out << "Query(";
-  d_expr.printAst(out, 2);
+  d_expr.printAst(out, 0);
   out << ")";
 }
 
diff --git a/src/util/command.h b/src/util/command.h
index b41be4592..57edfea01 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -30,6 +30,7 @@ namespace CVC4 {
 namespace CVC4 {
 
 std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
 
 class CVC4_PUBLIC Command {
 public: