From 842fd54de1da122f4c7274796550c2fe21c11db2 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Wed, 3 Feb 2010 22:10:21 +0000 Subject: [PATCH] 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 ++++++++++++++----- src/util/command.cpp | 11 ++++++++++- src/util/command.h | 1 + 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& 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& 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: -- 2.30.2