From 842fd54de1da122f4c7274796550c2fe21c11db2 Mon Sep 17 00:00:00 2001
From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Wed, 3 Feb 2010 22:10:21 +0000
Subject: ELSEIF support and parser debugging with '-d parser'

---
 src/parser/antlr_parser.cpp | 14 ++++++++++----
 src/parser/cvc/cvc_parser.g | 22 ++++++++++++++++++----
 src/parser/parser.cpp       | 19 ++++++++++++++-----
 3 files changed, 42 insertions(+), 13 deletions(-)

(limited to 'src/parser')

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,
-- 
cgit v1.2.3