From 2eef69eb63f3a5637f8711944e3d056672872f20 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Fri, 18 Dec 2009 05:07:19 +0000 Subject: [PATCH] Lots of parser changes to make Chris happy. Yet more to come later. --- src/main/getopt.cpp | 10 +- src/main/main.cpp | 49 ++------- src/parser/antlr_parser.cpp | 79 +++++++-------- src/parser/antlr_parser.h | 69 ++++++------- src/parser/cvc/Makefile.am | 2 - src/parser/cvc/Makefile.in | 5 +- src/parser/cvc/cvc_parser.cpp | 82 --------------- src/parser/cvc/cvc_parser.g | 120 ++++++++++++++++++---- src/parser/cvc/cvc_parser.h | 80 --------------- src/parser/parser.cpp | 89 +++++++++++++++- src/parser/parser.h | 83 ++++++++++----- src/parser/smt/Makefile.am | 2 - src/parser/smt/Makefile.in | 5 +- src/parser/smt/smt_parser.cpp | 79 --------------- src/parser/smt/smt_parser.g | 185 +++++++++++++++++++++------------- src/parser/smt/smt_parser.h | 79 --------------- src/parser/symbol_table.h | 19 ++-- src/util/command.cpp | 75 ++++++++++++-- src/util/command.h | 50 +++++++-- src/util/options.h | 9 +- 20 files changed, 571 insertions(+), 600 deletions(-) delete mode 100644 src/parser/cvc/cvc_parser.cpp delete mode 100644 src/parser/cvc/cvc_parser.h delete mode 100644 src/parser/smt/smt_parser.cpp delete mode 100644 src/parser/smt/smt_parser.h diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index c191b2a15..81cbc2df8 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -30,9 +30,11 @@ #include "about.h" #include "util/output.h" #include "util/options.h" +#include "parser/parser.h" using namespace std; using namespace CVC4; +using namespace CVC4::parser; namespace CVC4 { namespace main { @@ -97,13 +99,13 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti case 'L': if(!strcmp(optarg, "cvc4") || !strcmp(optarg, "pl")) { - opts->lang = Options::LANG_CVC4; + opts->lang = Parser::LANG_CVC4; break; } else if(!strcmp(optarg, "smtlib") || !strcmp(optarg, "smt")) { - opts->lang = Options::LANG_SMTLIB; + opts->lang = Parser::LANG_SMTLIB; break; } else if(!strcmp(optarg, "auto")) { - opts->lang = Options::LANG_AUTO; + opts->lang = Parser::LANG_AUTO; break; } @@ -126,7 +128,7 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti // silences CVC4 (except "sat" or "unsat" or "unknown", forces smtlib input) opts->smtcomp_mode = true; opts->verbosity = -1; - opts->lang = Options::LANG_SMTLIB; + opts->lang = Parser::LANG_SMTLIB; break; case '?': diff --git a/src/main/main.cpp b/src/main/main.cpp index 6f32e474b..595915100 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -23,8 +23,6 @@ #include "main.h" #include "usage.h" #include "parser/parser.h" -#include "parser/smt/smt_parser.h" -#include "parser/cvc/cvc_parser.h" #include "expr/expr_manager.h" #include "smt/smt_engine.h" #include "util/command.h" @@ -69,13 +67,14 @@ int main(int argc, char *argv[]) { bool inputFromStdin = firstArgIndex >= argc; // Auto-detect input language by filename extension - if(!inputFromStdin && options.lang == Options::LANG_AUTO) { + if(!inputFromStdin && options.lang == Parser::LANG_AUTO) { if(!strcmp(".smt", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4)) { - options.lang = Options::LANG_SMTLIB; - } - else if(!strcmp(".cvc", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4) || - !strcmp(".cvc4", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 5)) { - options.lang = Options::LANG_CVC4; + options.lang = Parser::LANG_SMTLIB; + } else if(!strcmp(".cvc", argv[firstArgIndex] + + strlen(argv[firstArgIndex]) - 4) + || !strcmp(".cvc4", argv[firstArgIndex] + strlen(argv[firstArgIndex]) + - 5)) { + options.lang = Parser::LANG_CVC4; } } @@ -100,34 +99,12 @@ int main(int argc, char *argv[]) { } } - // Set up the input stream, either cin or a file - const char* fname; - istream* in; - ifstream* file; - if(inputFromStdin) { - fname = "stdin"; - in = &cin; - } else { - fname = argv[firstArgIndex]; - file = new ifstream(fname); - in = file; - } - // Create the parser Parser* parser; - switch(options.lang) { - case Options::LANG_SMTLIB: - parser = new SmtParser(&exprMgr, *in, fname); - break; - case Options::LANG_CVC4: - parser = new CvcParser(&exprMgr, *in, fname); - break; - case Options::LANG_AUTO: - cerr << "Auto language detection not supported yet." << endl; - abort(); - default: - cerr << "Unknown language" << endl; - abort(); + if(inputFromStdin) { + parser = Parser::getNewParser(&exprMgr, options.lang, cin); + } else { + parser = Parser::getNewParser(&exprMgr, options.lang, argv[firstArgIndex]); } // Parse and execute commands until we are done @@ -145,10 +122,6 @@ int main(int argc, char *argv[]) { // Remove the parser delete parser; - if(! inputFromStdin) { - // Delete handle to input file - delete file; - } } catch(OptionException& e) { if(options.smtcomp_mode) { cout << "unknown" << endl; diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index c42415c54..be51aee6b 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -33,23 +33,6 @@ using namespace CVC4::parser; namespace CVC4 { namespace parser { -ostream& operator<<(ostream& out, AntlrParser::BenchmarkStatus status) { - switch(status) { - case AntlrParser::SMT_SATISFIABLE: - out << "sat"; - break; - case AntlrParser::SMT_UNSATISFIABLE: - out << "unsat"; - break; - case AntlrParser::SMT_UNKNOWN: - out << "unknown"; - break; - default: - Unhandled("Unhandled ostream case for AntlrParser::BenchmarkStatus"); - } - return out; -} - unsigned AntlrParser::getPrecedence(Kind kind) { switch(kind) { // Boolean operators @@ -82,60 +65,56 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) : } Expr AntlrParser::getVariable(std::string var_name) { - Expr e = d_var_symbol_table.getObject(var_name); + Expr e = d_varSymbolTable.getObject(var_name); Debug("parser") << "getvar " << var_name << " gives " << e << endl; return e; } Expr AntlrParser::getTrueExpr() const { - return d_expr_manager->mkExpr(TRUE); + return d_exprManager->mkExpr(TRUE); } Expr AntlrParser::getFalseExpr() const { - return d_expr_manager->mkExpr(FALSE); + return d_exprManager->mkExpr(FALSE); } -Expr AntlrParser::newExpression(Kind kind, const Expr& child) { - return d_expr_manager->mkExpr(kind, child); +Expr AntlrParser::mkExpr(Kind kind, const Expr& child) { + return d_exprManager->mkExpr(kind, child); } -Expr AntlrParser::newExpression(Kind kind, const Expr& child_1, const Expr& child_2) { - return d_expr_manager->mkExpr(kind, child_1, 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::newExpression(Kind kind, const std::vector& children) { - return d_expr_manager->mkExpr(kind, children); +Expr AntlrParser::mkExpr(Kind kind, const std::vector& children) { + return d_exprManager->mkExpr(kind, children); } void AntlrParser::newPredicate(std::string p_name, const std::vector< std::string>& p_sorts) { - if(p_sorts.size() == 0) - d_var_symbol_table.bindName(p_name, d_expr_manager->mkVar()); - else + if(p_sorts.size() == 0) { + d_varSymbolTable.bindName(p_name, d_exprManager->mkVar()); + } else { Unhandled("Non unary predicate not supported yet!"); + } } void AntlrParser::newPredicates(const std::vector& p_names) { vector sorts; - for(unsigned i = 0; i < p_names.size(); ++i) + for(unsigned i = 0; i < p_names.size(); ++i) { newPredicate(p_names[i], sorts); -} - -void AntlrParser::setBenchmarkStatus(BenchmarkStatus status) { - d_benchmark_status = status; -} - -void AntlrParser::addExtraSorts(const std::vector& extra_sorts) { + } } void AntlrParser::setExpressionManager(ExprManager* em) { - d_expr_manager = em; + d_exprManager = em; } bool AntlrParser::isDeclared(string name, SymbolType type) { switch(type) { case SYM_VARIABLE: - return d_var_symbol_table.isBound(name); + return d_varSymbolTable.isBound(name); default: Unhandled("Unhandled symbol type!"); } @@ -148,8 +127,8 @@ void AntlrParser::rethrow(antlr::SemanticException& e, string new_message) LT(0).get()->getColumn()); } -Expr AntlrParser::createPrecedenceExpr(const vector& exprs, - const vector& kinds) { +Expr AntlrParser::createPrecedenceExpr(const vector& exprs, const vector< + Kind>& kinds) { Assert( exprs.size() > 0, "Expected non-empty vector expr"); Assert( kinds.size() + 1 == exprs.size(), "Expected kinds to match exprs"); return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1); @@ -184,14 +163,28 @@ Expr AntlrParser::createPrecedenceExpr(const std::vector& exprs, Assert( end_index < exprs.size(), "Expected end_index < exprs.size. "); Assert( start_index <= end_index, "Expected start_index <= end_index. "); - if(start_index == end_index) + if(start_index == end_index) { return exprs[start_index]; + } unsigned pivot = findPivot(kinds, start_index, end_index - 1); Expr child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot); Expr child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index); - return d_expr_manager->mkExpr(kinds[pivot], child_1, child_2); + return d_exprManager->mkExpr(kinds[pivot], child_1, child_2); +} + +bool AntlrParser::checkDeclation(string varName, DeclarationCheck check) { + switch(check) { + case CHECK_DECLARED: + return isDeclared(varName, SYM_VARIABLE); + case CHECK_UNDECLARED: + return !isDeclared(varName, SYM_VARIABLE); + case CHECK_NONE: + return true; + default: + Unhandled("Unknown check type!"); + } } }/* CVC4::parser namespace */ diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index 8a9dea5ad..271171281 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -42,14 +42,14 @@ class AntlrParser : public antlr::LLkParser { public: - /** The status an SMT benchmark can have */ - enum BenchmarkStatus { - /** Benchmark is satisfiable */ - SMT_SATISFIABLE, - /** Benchmark is unsatisfiable */ - SMT_UNSATISFIABLE, - /** The status of the benchmark is unknown */ - SMT_UNKNOWN + /** Types of check for the symols */ + enum DeclarationCheck { + /** Enforce that the symbol has been declared */ + CHECK_DECLARED, + /** Enforce that the symbol has not been declared */ + CHECK_UNDECLARED, + /** Don't check anything */ + CHECK_NONE }; /** @@ -58,6 +58,18 @@ public: */ void setExpressionManager(ExprManager* expr_manager); + /** + * Parse a command. + * @return a command + */ + virtual Command* parseCommand() = 0; + + /** + * Parse an expression. + * @return the expression + */ + virtual Expr parseExpr() = 0; + protected: /** @@ -96,6 +108,14 @@ protected: */ Expr getVariable(std::string var_name); + /** + * Return true if the the declaration policy we want to enforce is true. + * @param varName the symbol to check + * @oaram check the kind of check to perform + * @return true if the check holds + */ + bool checkDeclation(std::string varName, DeclarationCheck check); + /** * Types of symbols. */ @@ -131,21 +151,21 @@ protected: * @param kind the kind of the expression * @param child the child */ - Expr newExpression(Kind kind, const Expr& child); + 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 */ - Expr newExpression(Kind kind, const Expr& child_1, const Expr& child_2); + Expr mkExpr(Kind kind, const Expr& child_1, const Expr& child_2); /** * Creates a new CVC4 expression using the expression manager. * @param kind the kind of the expression * @param children the children of the expression */ - Expr newExpression(Kind kind, const std::vector& children); + Expr mkExpr(Kind kind, const std::vector& children); /** * Creates a new expression based on the given string of expressions and kinds, @@ -169,24 +189,6 @@ protected: */ void newPredicates(const std::vector& p_names); - /** - * Sets the status of the benchmark. - * @param status the status of the benchmark - */ - void setBenchmarkStatus(BenchmarkStatus status); - - /** - * Returns the status of the parsed benchmark. - * @return the status of the parsed banchmark - */ - BenchmarkStatus getBenchmarkStatus() const; - - /** - * Adds the extra sorts to the signature of the benchmark. - * @param extra_sorts the sorts to add - */ - void addExtraSorts(const std::vector& extra_sorts); - /** * Returns the precedence rank of the kind. */ @@ -206,18 +208,13 @@ private: */ Expr createPrecedenceExpr(const std::vector& exprs, const std::vector& kinds, unsigned start_index, unsigned end_index); - /** The status of the benchmark */ - BenchmarkStatus d_benchmark_status; - /** The expression manager */ - ExprManager* d_expr_manager; + ExprManager* d_exprManager; /** The symbol table lookup */ - SymbolTable d_var_symbol_table; + SymbolTable d_varSymbolTable; }; -std::ostream& operator<<(std::ostream& out, AntlrParser::BenchmarkStatus status); - }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index 666c408cf..ad0eb70d8 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -24,8 +24,6 @@ ANTLR_STUFF = \ libparsercvc_la_SOURCES = \ cvc_lexer.g \ cvc_parser.g \ - cvc_parser.h \ - cvc_parser.cpp \ $(ANTLR_STUFF) BUILT_SOURCES = $(ANTLR_STUFF) diff --git a/src/parser/cvc/Makefile.in b/src/parser/cvc/Makefile.in index 3fd1701c8..28b80800e 100644 --- a/src/parser/cvc/Makefile.in +++ b/src/parser/cvc/Makefile.in @@ -56,7 +56,7 @@ am__objects_1 = am__objects_2 = AntlrCvcLexer.lo $(am__objects_1) am__objects_3 = AntlrCvcParser.lo am__objects_4 = $(am__objects_2) $(am__objects_3) -am_libparsercvc_la_OBJECTS = cvc_parser.lo $(am__objects_4) +am_libparsercvc_la_OBJECTS = $(am__objects_4) libparsercvc_la_OBJECTS = $(am_libparsercvc_la_OBJECTS) DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) depcomp = $(SHELL) $(top_srcdir)/config/depcomp @@ -249,8 +249,6 @@ ANTLR_STUFF = \ libparsercvc_la_SOURCES = \ cvc_lexer.g \ cvc_parser.g \ - cvc_parser.h \ - cvc_parser.cpp \ $(ANTLR_STUFF) BUILT_SOURCES = $(ANTLR_STUFF) @@ -310,7 +308,6 @@ distclean-compile: @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcLexer.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrCvcParser.Plo@am__quote@ -@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/cvc_parser.Plo@am__quote@ .cpp.o: @am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< diff --git a/src/parser/cvc/cvc_parser.cpp b/src/parser/cvc/cvc_parser.cpp deleted file mode 100644 index 57d5e6c96..000000000 --- a/src/parser/cvc/cvc_parser.cpp +++ /dev/null @@ -1,82 +0,0 @@ -/********************* -*- C++ -*- */ -/** cvc_parser.cpp - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** CVC presentation language parser implementation. - **/ - -#include -#include - -#include "parser/parser.h" -#include "util/command.h" -#include "util/Assert.h" -#include "parser/parser_exception.h" -#include "parser/antlr_parser.h" -#include "parser/cvc/cvc_parser.h" -#include "parser/cvc/generated/AntlrCvcParser.hpp" -#include "parser/cvc/generated/AntlrCvcLexer.hpp" - -using namespace std; - -namespace CVC4 { -namespace parser { - -Command* CvcParser::parseNextCommand() throw(ParserException) { - Command* cmd = 0; - if(!done()) { - try { - cmd = d_antlr_parser->command(); - if(cmd == 0) { - setDone(); - cmd = new EmptyCommand("EOF"); - } - } catch(antlr::ANTLRException& e) { - setDone(); - throw ParserException(e.toString()); - } - } - return cmd; -} - -Expr CvcParser::parseNextExpression() throw(ParserException) { - Expr result; - if(!done()) { - try { - result = d_antlr_parser->formula(); - } catch(antlr::ANTLRException& e) { - setDone(); - throw ParserException(e.toString()); - } - } - return result; -} - -CvcParser::~CvcParser() { - delete d_antlr_parser; - delete d_antlr_lexer; -} - -CvcParser::CvcParser(ExprManager*em, istream& input, const char* file_name) : - Parser(em), d_input(input) { - if(!d_input) { - throw ParserException(string("Read error") + - ((file_name != NULL) ? (string(" on ") + file_name) : "")); - } - d_antlr_lexer = new AntlrCvcLexer(d_input); - d_antlr_lexer->setFilename(file_name); - d_antlr_parser = new AntlrCvcParser(*d_antlr_lexer); - d_antlr_parser->setExpressionManager(d_expr_manager); - d_antlr_parser->setFilename(file_name); -} - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 864719cfa..c7f932a0c 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -28,6 +28,23 @@ options { k = 2; } +/** + * Parses the next command. + * @return command or 0 if EOF + */ +parseCommand returns [CVC4::Command* cmd] + : cmd = command + ; + +/** + * Parses the next expression. + * @return the parsed expression (null expression if EOF) + */ +parseExpr returns [CVC4::Expr expr] + : expr = formula + | EOF + ; + /** * Matches a command of the input. If a declaration, it will return an empty * command. @@ -41,64 +58,118 @@ command returns [CVC4::Command* cmd = 0] | QUERY f = formula { cmd = new QueryCommand(f); } | CHECKSAT f = formula { cmd = new CheckSatCommand(f); } | CHECKSAT { cmd = new CheckSatCommand(); } - | identifierList[ids] COLON type { + | identifierList[ids, CHECK_UNDECLARED] COLON type { // [chris 12/15/2009] FIXME: decls may not be BOOLEAN newPredicates(ids); - cmd = new EmptyCommand("Declaration"); + cmd = new DeclarationCommand(ids); } | EOF ; -identifierList[std::vector& id_list] - : id1:IDENTIFIER { id_list.push_back(id1->getText()); } - ( - COMMA - id2:IDENTIFIER { id_list.push_back(id2->getText()); } - )* +/** + * Mathches a list of identifiers separated by a comma and puts them in the + * given list. + * @param idList the list to fill with identifiers. + * @param check what kinds of check to perform on the symbols + */ +identifierList[std::vector& idList, DeclarationCheck check = CHECK_NONE] +{ + string id; +} + : id = identifier { idList.push_back(id); } + (COMMA id = identifier { idList.push_back(id); })* ; + +/** + * Matches an identifier and returns a string. + */ +identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id] + : x:IDENTIFIER { checkDeclation(x->getText(), check) }? + { + id = x->getText(); + } + exception catch [antlr::SemanticException& ex] { + switch (check) { + case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared"); + case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared"); + default: throw ex; + } + } + ; + +/** + * Matches a type. + * TODO: parse more types + */ type : BOOLEAN ; +/** + * Matches a CVC4 formula. + * @return the expression representing the formula + */ formula returns [CVC4::Expr formula] - : formula = bool_formula + : formula = boolFormula ; -bool_formula returns [CVC4::Expr formula] +/** + * Matches a CVC4 basic Boolean formula (AND, OR, NOT...). It parses the list of + * operands (primaryBoolFormulas) and operators (Kinds) and then calls the + * createPrecedenceExpr method to build the expression using the precedence + * and associativity of the operators. + * @return the expression representing the formula + */ +boolFormula returns [CVC4::Expr formula] { vector formulas; vector kinds; Expr f1, f2; Kind k; } - : f1 = primary_bool_formula { formulas.push_back(f1); } - ( k = bool_operator { kinds.push_back(k); } f2 = primary_bool_formula { formulas.push_back(f2); } )* + : f1 = primaryBoolFormula { formulas.push_back(f1); } + ( k = boolOperator { kinds.push_back(k); } f2 = primaryBoolFormula { formulas.push_back(f2); } )* { // Create the expression based on precedences formula = createPrecedenceExpr(formulas, kinds); } ; -primary_bool_formula returns [CVC4::Expr formula] - : formula = bool_atom - | NOT formula = primary_bool_formula { formula = newExpression(CVC4::NOT, formula); } - | LPAREN formula = bool_formula RPAREN +/** + * Parses a primary Boolean formula. A primary Boolean formula is either a + * Boolean atom (variables and predicates) a negation of a primary Boolean + * formula or a formula enclosed in parenthesis. + * @return the expression representing the formula + */ +primaryBoolFormula returns [CVC4::Expr formula] + : formula = boolAtom + | NOT formula = primaryBoolFormula { formula = mkExpr(CVC4::NOT, formula); } + | LPAREN formula = boolFormula RPAREN ; -bool_operator returns [CVC4::Kind kind] +/** + * Parses the Boolean operators and returns the corresponding CVC4 expression + * kind. + * @param the kind of the Boolean operator + */ +boolOperator returns [CVC4::Kind kind] : IMPLIES { kind = CVC4::IMPLIES; } | AND { kind = CVC4::AND; } | OR { kind = CVC4::OR; } | XOR { kind = CVC4::XOR; } | IFF { kind = CVC4::IFF; } ; - -bool_atom returns [CVC4::Expr atom] + +/** + * Parses the Boolean atoms (variables and predicates). + * @return the expression representing the atom. + */ +boolAtom returns [CVC4::Expr atom] { string p; } - : p = predicate_sym {isDeclared(p, SYM_VARIABLE)}? { atom = getVariable(p); } + : p = predicateSymbol[CHECK_DECLARED] { atom = getVariable(p); } exception catch [antlr::SemanticException ex] { rethrow(ex, "Undeclared variable " + p); } @@ -106,7 +177,12 @@ bool_atom returns [CVC4::Expr atom] | FALSE { atom = getFalseExpr(); } ; -predicate_sym returns [std::string p] - : id:IDENTIFIER { p = id->getText(); } +/** + * Parses a predicate symbol (an identifier). + * @param what kind of check to perform on the id + * @return the predicate symol + */ +predicateSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string pSymbol] + : pSymbol = identifier[check] ; \ No newline at end of file diff --git a/src/parser/cvc/cvc_parser.h b/src/parser/cvc/cvc_parser.h deleted file mode 100644 index 82d659566..000000000 --- a/src/parser/cvc/cvc_parser.h +++ /dev/null @@ -1,80 +0,0 @@ -/********************* -*- C++ -*- */ -/** cvc_parser.h - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** CVC presentation language parser abstraction. - **/ - -#ifndef __CVC4__PARSER__CVC_PARSER_H -#define __CVC4__PARSER__CVC_PARSER_H - -#include -#include -#include -#include "cvc4_config.h" -#include "parser/parser_exception.h" -#include "parser/parser.h" - -namespace CVC4 { -namespace parser { - -/** - * The CVC parser. - */ -class CVC4_PUBLIC CvcParser : public Parser { - -public: - - /** - * Construct the parser that uses the given expression manager and parses - * from the given input stream. - * @param em the expression manager to use - * @param input the input stream to parse - * @param file_name the name of the file (for diagnostic output) - */ - CvcParser(ExprManager* em, std::istream& input, const char* file_name = ""); - - /** - * Destructor. - */ - ~CvcParser(); - - /** - * Parses the next command. By default, the CVC parser produces one - * CommandSequence command. If parsing is successful, we should be - * done after the first call to this command. - * @return the CommandSequence command that includes the whole - * benchmark - */ - Command* parseNextCommand() throw(ParserException); - - /** - * Parses the next complete expression of the stream. - * @return the expression parsed - */ - Expr parseNextExpression() throw(ParserException); - -protected: - - /** The ANTLR smt lexer */ - AntlrCvcLexer* d_antlr_lexer; - - /** The ANTLR smt parser */ - AntlrCvcParser* d_antlr_parser; - - /** The file stream we might be using */ - std::istream& d_input; -}; - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__PARSER__CVC_PARSER_H */ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 2ff409686..e919a53e8 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -15,6 +15,7 @@ #include #include +#include #include "parser.h" #include "util/command.h" @@ -27,14 +28,11 @@ #include "parser/cvc/generated/AntlrCvcLexer.hpp" using namespace std; +using namespace antlr; namespace CVC4 { namespace parser { -Parser::Parser(ExprManager* em) : - d_expr_manager(em), d_done(false) { -} - void Parser::setDone(bool done) { d_done = done; } @@ -43,5 +41,88 @@ bool Parser::done() const { return d_done; } +Command* Parser::parseNextCommand() throw (ParserException) { + Command* cmd = 0; + if(!done()) { + try { + cmd = d_antlrParser->parseCommand(); + if(cmd == 0) { + setDone(); + cmd = new EmptyCommand("EOF"); + } + } catch(antlr::ANTLRException& e) { + setDone(); + throw ParserException(e.toString()); + } + } + return cmd; +} + +Expr Parser::parseNextExpression() throw (ParserException) { + Expr result; + if(!done()) { + try { + result = d_antlrParser->parseExpr(); + if(result.isNull()) + setDone(); + } catch(antlr::ANTLRException& e) { + setDone(); + throw ParserException(e.toString()); + } + } + return result; +} + +Parser::~Parser() { + delete d_antlrParser; + delete d_antlrLexer; + if (d_deleteInput) delete d_input; +} + +Parser::Parser(istream* input, AntlrParser* antlrParser, CharScanner* antlrLexer, bool deleteInput) : + d_done(false), d_input(input), d_antlrParser(antlrParser), d_antlrLexer(antlrLexer), d_deleteInput(deleteInput) { +} + +Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang, + istream* input, string filename, bool deleteInput) { + + AntlrParser* antlrParser = 0; + antlr::CharScanner* antlrLexer = 0; + + switch(lang) { + case LANG_CVC4: { + antlrLexer = new AntlrCvcLexer(*input); + antlrLexer->setFilename(filename); + antlrParser = new AntlrCvcParser(*antlrLexer); + antlrParser->setFilename(filename); + antlrParser->setExpressionManager(em); + break; + } + case LANG_SMTLIB: { + antlrLexer = new AntlrSmtLexer(*input); + antlrLexer->setFilename(filename); + antlrParser = new AntlrSmtParser(*antlrLexer); + antlrParser->setFilename(filename); + antlrParser->setExpressionManager(em); + break; + } + default: + Unhandled("Unknown Input language!"); + } + + return new Parser(input, antlrParser, antlrLexer, deleteInput); +} + +Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang, + string filename) { + istream* input = new ifstream(filename.c_str()); + return getNewParser(em, lang, input, filename, true); +} + +Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang, + istream& input) { + return getNewParser(em, lang, &input, "", false); +} + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser.h b/src/parser/parser.h index b448cd2a6..d6180b9a3 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -18,9 +18,13 @@ #include #include -#include #include "cvc4_config.h" #include "parser_exception.h" +#include "antlr_parser.h" + +namespace antlr { + class CharScanner; +} namespace CVC4 { @@ -31,57 +35,88 @@ class ExprManager; namespace parser { -class AntlrSmtLexer; -class AntlrSmtParser; -class AntlrCvcLexer; -class AntlrCvcParser; - /** - * The parser. + * The parser. The parser should be obtained by calling the static methods + * getNewParser, and should be deleted when done. */ class CVC4_PUBLIC Parser { public: - /** - * Construct the parser that uses the given expression manager. - * @param em the expression manager. - */ - Parser(ExprManager* em); + /** The input language option */ + enum InputLanguage { + /** The SMTLIB input language */ + LANG_SMTLIB, + /** The CVC4 input language */ + LANG_CVC4, + /** Auto-detect the language */ + LANG_AUTO + }; + + static Parser* getNewParser(ExprManager* em, InputLanguage lang, std::string filename); + static Parser* getNewParser(ExprManager* em, InputLanguage lang, std::istream& input); /** * Destructor. */ - virtual ~Parser() { - } + ~Parser(); /** - * Parse the next command of the input + * Parse the next command of the input. If EOF is encountered a EmptyCommand + * is returned and done flag is set. */ - virtual Command* parseNextCommand() throw (ParserException) = 0; + Command* parseNextCommand() throw (ParserException); /** - * Parse the next expression of the stream + * Parse the next expression of the stream. If EOF is encountered a null + * expression is returned and done flag is set. + * @return the parsed expression */ - virtual Expr parseNextExpression() throw (ParserException) = 0; + Expr parseNextExpression() throw (ParserException); /** - * Check if we are done -- either the end of input has been reached. + * Check if we are done -- either the end of input has been reached, or some + * error has been encountered. + * @return true if parser is done */ bool done() const; -protected: +private: + + /** + * Create a new parser. + * @param em the expression manager to usee + * @param lang the language to parse + * @param input the input stream to parse + * @param filename the filename to attach to the stream + * @param deleteInput wheather to delete the input + * @return the parser + */ + static Parser* getNewParser(ExprManager* em, InputLanguage lang, std::istream* input, std::string filename, bool deleteInput); + + /** + * Create a new parser given the actual antlr parser. + * @param antlrParser the antlr parser to user + */ + Parser(std::istream* input, AntlrParser* antlrParser, antlr::CharScanner* antlrLexer, bool deleteInput); /** Sets the done flag */ void setDone(bool done = true); - /** Expression manager the parser will be using */ - ExprManager* d_expr_manager; - /** Are we done */ bool d_done; -}; // end of class Parser + /** The antlr parser */ + AntlrParser* d_antlrParser; + + /** The entlr lexer */ + antlr::CharScanner* d_antlrLexer; + + /** The input stream we are using */ + std::istream* d_input; + + /** Wherther to de-allocate the input */ + bool d_deleteInput;}; // end of class Parser }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index 6f5f1bfd4..96ad9c27f 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -24,8 +24,6 @@ ANTLR_STUFF = \ libparsersmt_la_SOURCES = \ smt_lexer.g \ smt_parser.g \ - smt_parser.h \ - smt_parser.cpp \ $(ANTLR_STUFF) BUILT_SOURCES = $(ANTLR_STUFF) diff --git a/src/parser/smt/Makefile.in b/src/parser/smt/Makefile.in index 721ff0e2b..6145b4c4e 100644 --- a/src/parser/smt/Makefile.in +++ b/src/parser/smt/Makefile.in @@ -56,7 +56,7 @@ am__objects_1 = am__objects_2 = AntlrSmtLexer.lo $(am__objects_1) am__objects_3 = AntlrSmtParser.lo am__objects_4 = $(am__objects_2) $(am__objects_3) -am_libparsersmt_la_OBJECTS = smt_parser.lo $(am__objects_4) +am_libparsersmt_la_OBJECTS = $(am__objects_4) libparsersmt_la_OBJECTS = $(am_libparsersmt_la_OBJECTS) DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) depcomp = $(SHELL) $(top_srcdir)/config/depcomp @@ -249,8 +249,6 @@ ANTLR_STUFF = \ libparsersmt_la_SOURCES = \ smt_lexer.g \ smt_parser.g \ - smt_parser.h \ - smt_parser.cpp \ $(ANTLR_STUFF) BUILT_SOURCES = $(ANTLR_STUFF) @@ -310,7 +308,6 @@ distclean-compile: @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrSmtLexer.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/AntlrSmtParser.Plo@am__quote@ -@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/smt_parser.Plo@am__quote@ .cpp.o: @am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< diff --git a/src/parser/smt/smt_parser.cpp b/src/parser/smt/smt_parser.cpp deleted file mode 100644 index 8c5773e32..000000000 --- a/src/parser/smt/smt_parser.cpp +++ /dev/null @@ -1,79 +0,0 @@ -/********************* -*- C++ -*- */ -/** smt_parser.cpp - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** SMT-LIB language parser implementation. - **/ - -#include -#include - -#include "parser/parser.h" -#include "util/command.h" -#include "util/Assert.h" -#include "parser/parser_exception.h" -#include "parser/antlr_parser.h" -#include "parser/smt/smt_parser.h" -#include "parser/smt/generated/AntlrSmtParser.hpp" -#include "parser/smt/generated/AntlrSmtLexer.hpp" - -using namespace std; - -namespace CVC4 { -namespace parser { - -Command* SmtParser::parseNextCommand() throw(ParserException) { - Command* cmd = 0; - if(!done()) { - try { - cmd = d_antlr_parser->benchmark(); - setDone(); - } catch(antlr::ANTLRException& e) { - setDone(); - throw ParserException(e.toString()); - } - } - return cmd; -} - -Expr SmtParser::parseNextExpression() throw(ParserException) { - Expr result; - if(!done()) { - try { - result = d_antlr_parser->an_formula(); - } catch(antlr::ANTLRException& e) { - setDone(); - throw ParserException(e.toString()); - } - } - return result; -} - -SmtParser::~SmtParser() { - delete d_antlr_parser; - delete d_antlr_lexer; -} - -SmtParser::SmtParser(ExprManager* em, istream& input, const char* file_name) : - Parser(em), d_input(input) { - if(!d_input) { - throw ParserException(string("Read error") + - ((file_name != NULL) ? (string(" on ") + file_name) : "")); - } - d_antlr_lexer = new AntlrSmtLexer(input); - d_antlr_lexer->setFilename(file_name); - d_antlr_parser = new AntlrSmtParser(*d_antlr_lexer); - d_antlr_parser->setExpressionManager(d_expr_manager); - d_antlr_parser->setFilename(file_name); -} - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index 6e0051821..f7045fa7e 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -27,6 +27,108 @@ options { defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions k = 2; } + +/** + * Parses an expression. + * @return the parsed expression + */ +parseExpr returns [CVC4::Expr expr] + : expr = annotatedFormula + ; + +/** + * Parses a command (the whole benchmark) + * @return the command of the benchmark + */ +parseCommand returns [CVC4::Command* cmd] + : cmd = benchmark + ; + +/** + * Matches the whole SMT-LIB benchmark. + * @return the sequence command containing the whole problem + */ +benchmark returns [Command* cmd] + : LPAREN BENCHMARK IDENTIFIER cmd = benchAttributes RPAREN + | EOF { cmd = 0; } + ; + +/** + * Matchecs sequence of benchmark attributes and returns a pointer to a command + * sequence command. + * @return the command sequence + */ +benchAttributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()] +{ + Command* cmd; +} + : (cmd = benchAttribute { if (cmd) cmd_seq->addCommand(cmd); } )+ + ; + +/** + * Matches a benchmark attribute, sucha as ':logic', ':formula', and returns + * a corresponding command + * @retrurn a command corresponding to the attribute + */ +benchAttribute returns [ Command* smt_command = 0] +{ + Expr formula; + string logic; + SetBenchmarkStatusCommand::BenchmarkStatus b_status = SetBenchmarkStatusCommand::SMT_UNKNOWN; +} + : C_LOGIC logic = identifier { smt_command = new SetBenchmarkLogicCommand(logic); } + | C_ASSUMPTION formula = annotatedFormula { smt_command = new AssertCommand(formula); } + | C_FORMULA formula = annotatedFormula { smt_command = new CheckSatCommand(formula); } + | C_STATUS b_status = status { smt_command = new SetBenchmarkStatusCommand(b_status); } + | C_EXTRAPREDS LPAREN (pred_symb_decl)+ RPAREN + | C_NOTES STRING_LITERAL + | annotation + ; + +/** + * Matches an identifier and returns a string. + * @param check what kinds of check to do on the symbol + * @return the id string + */ +identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id] + : x:IDENTIFIER { checkDeclation(x->getText(), check) }? + { + id = x->getText(); + } + exception catch [antlr::SemanticException& ex] { + switch (check) { + case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared"); + case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared"); + default: throw ex; + } + } + ; + +/** + * Matches an annotated formula. + * @return the expression representing the formula + */ +annotatedFormula returns [CVC4::Expr formula] +{ + Kind kind; + vector children; +} + : formula = annotatedAtom + | LPAREN kind = boolConnective annotatedFormulas[children] RPAREN { formula = mkExpr(kind, children); } + ; + +/** + * Matches an annotated proposition atom, which is either a propositional atom + * or built of other atoms using a predicate symbol. + */ +annotatedAtom returns [CVC4::Expr atom] + : atom = propositionalAtom + ; + + + + + /** * Matches an attribute name from the input (:attribute_name). @@ -34,7 +136,7 @@ options { attribute : C_IDENTIFIER ; - + /** * Matches the sort symbol, which can be an arbitrary identifier. */ @@ -60,7 +162,7 @@ pred_symb returns [std::string p] /** * Matches a propositional atom. */ -prop_atom returns [CVC4::Expr atom] +propositionalAtom returns [CVC4::Expr atom] { std::string p; } @@ -71,22 +173,11 @@ prop_atom returns [CVC4::Expr atom] | TRUE { atom = getTrueExpr(); } | FALSE { atom = getFalseExpr(); } ; - -/** - * Matches an annotated proposition atom, which is either a propositional atom - * or built of other atoms using a predicate symbol. Annotation can be added if - * enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined - * here in order to get rid of the ugly antlr non-determinism warnings. - */ - // [chris 12/15/2009] FIXME: Where is the annotation? -an_atom returns [CVC4::Expr atom] - : atom = prop_atom - ; - + /** * Matches on of the unary Boolean connectives. */ -bool_connective returns [CVC4::Kind kind] +boolConnective returns [CVC4::Kind kind] : NOT { kind = CVC4::NOT; } | IMPLIES { kind = CVC4::IMPLIES; } | AND { kind = CVC4::AND; } @@ -94,24 +185,12 @@ bool_connective returns [CVC4::Kind kind] | XOR { kind = CVC4::XOR; } | IFF { kind = CVC4::IFF; } ; - -/** - * Matches an annotated formula. - */ -an_formula returns [CVC4::Expr formula] -{ - Kind kind; - vector children; -} - : formula = an_atom - | LPAREN kind = bool_connective an_formulas[children] RPAREN { formula = newExpression(kind, children); } - ; - -an_formulas[std::vector& formulas] + +annotatedFormulas[std::vector& formulas] { Expr f; } - : ( f = an_formula { formulas.push_back(f); } )+ + : ( f = annotatedFormula { formulas.push_back(f); } )+ ; /** @@ -138,44 +217,8 @@ sort_symbs[std::vector& sorts] /** * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'. */ -status returns [ AntlrParser::BenchmarkStatus status ] - : SAT { status = SMT_SATISFIABLE; } - | UNSAT { status = SMT_UNSATISFIABLE; } - | UNKNOWN { status = SMT_UNKNOWN; } - ; - -/** - * Matches a benchmark attribute, sucha as ':logic', ':formula', etc. - */ -bench_attribute returns [ Command* smt_command = 0] -{ - BenchmarkStatus b_status = SMT_UNKNOWN; - Expr formula; - vector sorts; -} - : C_LOGIC IDENTIFIER - | C_ASSUMPTION formula = an_formula { smt_command = new AssertCommand(formula); } - | C_FORMULA formula = an_formula { smt_command = new CheckSatCommand(formula); } - | C_STATUS b_status = status { setBenchmarkStatus(b_status); } - | C_EXTRASORTS LPAREN sort_symbs[sorts] RPAREN { addExtraSorts(sorts); } - | C_EXTRAPREDS LPAREN (pred_symb_decl)+ RPAREN - | C_NOTES STRING_LITERAL - | annotation - ; - -/** - * Returns a pointer to a command sequence command. - */ -bench_attributes returns [CVC4::CommandSequence* cmd_seq = new CommandSequence()] -{ - Command* cmd; -} - : (cmd = bench_attribute { if (cmd) cmd_seq->addCommand(cmd); } )+ - ; - -/** - * Matches the whole SMT-LIB benchmark. - */ -benchmark returns [Command* cmd] - : LPAREN BENCHMARK IDENTIFIER cmd = bench_attributes RPAREN - ; +status returns [ SetBenchmarkStatusCommand::BenchmarkStatus status ] + : SAT { status = SetBenchmarkStatusCommand::SMT_SATISFIABLE; } + | UNSAT { status = SetBenchmarkStatusCommand::SMT_UNSATISFIABLE; } + | UNKNOWN { status = SetBenchmarkStatusCommand::SMT_UNKNOWN; } + ; \ No newline at end of file diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h deleted file mode 100644 index 21c278a37..000000000 --- a/src/parser/smt/smt_parser.h +++ /dev/null @@ -1,79 +0,0 @@ -/********************* -*- C++ -*- */ -/** smt_parser.h - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): cconway, dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** SMT-LIB language parser abstraction. - **/ - -#ifndef __CVC4__PARSER__SMT_PARSER_H -#define __CVC4__PARSER__SMT_PARSER_H - -#include -#include -#include -#include "cvc4_config.h" -#include "parser/parser_exception.h" -#include "parser/parser.h" - -namespace CVC4 { -namespace parser { - -/** - * The SMT parser. - */ -class CVC4_PUBLIC SmtParser : public Parser { - -public: - - /** - * Construct the parser that uses the given expression manager and input stream. - * @param em the expression manager to use - * @param input the input stream to parse - * @param file_name the name of the file (for diagnostic output) - */ - SmtParser(ExprManager* em, std::istream& input, const char* file_name = ""); - - /** - * Destructor. - */ - ~SmtParser(); - - /** - * Parses the next command. By default, the SMT-LIB parser produces - * one CommandSequence command. If parsing is successful, we should - * be done after the first call to this command. - * @return the CommandSequence command that includes the whole - * benchmark - */ - Command* parseNextCommand() throw(ParserException); - - /** - * Parses the next complete expression of the stream. - * @return the expression parsed - */ - Expr parseNextExpression() throw(ParserException); - -protected: - - /** The ANTLR smt lexer */ - AntlrSmtLexer* d_antlr_lexer; - - /** The ANTLR smt parser */ - AntlrSmtParser* d_antlr_parser; - - /** The file stream we might be using */ - std::istream& d_input; -}; - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__PARSER__SMT_PARSER_H */ diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h index 66d5727d6..8c9582762 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -49,7 +49,7 @@ private: typedef typename LookupTable::const_iterator const_table_iterator; /** Bindings for the names */ - LookupTable d_name_bindings; + LookupTable d_nameBindings; public: @@ -58,18 +58,18 @@ public: * has been bind before, this will redefine it until its undefined. */ void bindName(const std::string name, const ObjectType& obj) throw () { - d_name_bindings[name].push(obj); + d_nameBindings[name].push(obj); } /** * Unbinds the last binding of the name to the expression. */ void unbindName(const std::string name) throw () { - table_iterator find = d_name_bindings.find(name); - if(find != d_name_bindings.end()) { + table_iterator find = d_nameBindings.find(name); + if(find != d_nameBindings.end()) { find->second.pop(); if(find->second.empty()) { - d_name_bindings.erase(find); + d_nameBindings.erase(find); } } } @@ -79,9 +79,10 @@ public: */ ObjectType getObject(const std::string name) throw () { ObjectType result; - table_iterator find = d_name_bindings.find(name); - if(find != d_name_bindings.end()) + table_iterator find = d_nameBindings.find(name); + if(find != d_nameBindings.end()) { result = find->second.top(); + } return result; } @@ -89,8 +90,8 @@ public: * Returns true is name is bound to an expression. */ bool isBound(const std::string name) const throw () { - const_table_iterator find = d_name_bindings.find(name); - return (find != d_name_bindings.end()); + const_table_iterator find = d_nameBindings.find(name); + return (find != d_nameBindings.end()); } }; diff --git a/src/util/command.cpp b/src/util/command.cpp index 5a5b766cb..b80851233 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -20,8 +20,9 @@ * Author: dejan */ -#include +#include #include "util/command.h" +#include "util/Assert.h" #include "smt/smt_engine.h" using namespace std; @@ -29,10 +30,16 @@ using namespace std; namespace CVC4 { ostream& operator<<(ostream& out, const Command& c) { - c.toString(out); + c.toStream(out); return out; } +std::string Command::toString() const { + stringstream ss; + toStream(ss); + return ss.str(); +} + EmptyCommand::EmptyCommand(string name) : d_name(name) { } @@ -87,26 +94,26 @@ void CommandSequence::addCommand(Command* cmd) { d_command_sequence.push_back(cmd); } -void EmptyCommand::toString(ostream& out) const { +void EmptyCommand::toStream(ostream& out) const { out << "EmptyCommand(" << d_name << ")"; } -void AssertCommand::toString(ostream& out) const { +void AssertCommand::toStream(ostream& out) const { out << "Assert(" << d_expr << ")"; } -void CheckSatCommand::toString(ostream& out) const { +void CheckSatCommand::toStream(ostream& out) const { if(d_expr.isNull()) out << "CheckSat()"; else out << "CheckSat(" << d_expr << ")"; } -void QueryCommand::toString(ostream& out) const { +void QueryCommand::toStream(ostream& out) const { out << "Query(" << d_expr << ")"; } -void CommandSequence::toString(ostream& out) const { +void CommandSequence::toStream(ostream& out) const { out << "CommandSequence[" << endl; for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i) { out << *d_command_sequence[i] << endl; @@ -114,4 +121,58 @@ void CommandSequence::toString(ostream& out) const { out << "]"; } +DeclarationCommand::DeclarationCommand(const std::vector& ids) : + d_declaredSymbols(ids) { +} + +void DeclarationCommand::toStream(std::ostream& out) const { + out << "Declare("; + bool first = true; + for(unsigned i = 0; i < d_declaredSymbols.size(); ++i) { + if(first) { + out << ", "; + first = false; + } + out << d_declaredSymbols[i]; + } + out << ")"; +} + +SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) : + d_status(status) { +} + +void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) { + // TODO: something to be done with the status +} + +void SetBenchmarkStatusCommand::toStream(std::ostream& out) const { + out << "SetBenchmarkStatus("; + switch(d_status) { + case SMT_SATISFIABLE: + out << "sat"; + break; + case SMT_UNSATISFIABLE: + out << "unsat"; + break; + case SMT_UNKNOWN: + out << "unknown"; + break; + default: + Unhandled("Unknown benchmark status"); + } + out << ")"; +} + +SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(string logic) : d_logic(logic) + {} + +void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) { + // TODO: something to be done with the logic +} + +void SetBenchmarkLogicCommand::toStream(std::ostream& out) const { + out << "SetBenchmarkLogic(" << d_logic << ")"; +} + }/* CVC4 namespace */ diff --git a/src/util/command.h b/src/util/command.h index 9cc009d01..b41be4592 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -35,14 +35,15 @@ class CVC4_PUBLIC Command { public: virtual void invoke(CVC4::SmtEngine* smt_engine) = 0; virtual ~Command() {}; - virtual void toString(std::ostream&) const = 0; + virtual void toStream(std::ostream&) const = 0; + std::string toString() const; };/* class Command */ class CVC4_PUBLIC EmptyCommand : public Command { public: EmptyCommand(std::string name = ""); void invoke(CVC4::SmtEngine* smt_engine); - void toString(std::ostream& out) const; + void toStream(std::ostream& out) const; private: std::string d_name; };/* class EmptyCommand */ @@ -52,18 +53,26 @@ class CVC4_PUBLIC AssertCommand : public Command { public: AssertCommand(const BoolExpr& e); void invoke(CVC4::SmtEngine* smt_engine); - void toString(std::ostream& out) const; + void toStream(std::ostream& out) const; protected: BoolExpr d_expr; };/* class AssertCommand */ +class CVC4_PUBLIC DeclarationCommand : public EmptyCommand { +public: + DeclarationCommand(const std::vector& ids); + void toStream(std::ostream& out) const; +protected: + std::vector d_declaredSymbols; +}; + class CVC4_PUBLIC CheckSatCommand : public Command { public: CheckSatCommand(); CheckSatCommand(const BoolExpr& e); void invoke(SmtEngine* smt); - void toString(std::ostream& out) const; + void toStream(std::ostream& out) const; protected: BoolExpr d_expr; };/* class CheckSatCommand */ @@ -73,19 +82,48 @@ class CVC4_PUBLIC QueryCommand : public Command { public: QueryCommand(const BoolExpr& e); void invoke(SmtEngine* smt); - void toString(std::ostream& out) const; + void toStream(std::ostream& out) const; protected: BoolExpr d_expr; };/* class QueryCommand */ +class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { +public: + /** The status an SMT benchmark can have */ + enum BenchmarkStatus { + /** Benchmark is satisfiable */ + SMT_SATISFIABLE, + /** Benchmark is unsatisfiable */ + SMT_UNSATISFIABLE, + /** The status of the benchmark is unknown */ + SMT_UNKNOWN + }; + SetBenchmarkStatusCommand(BenchmarkStatus status); + void invoke(SmtEngine* smt); + void toStream(std::ostream& out) const; +protected: + BenchmarkStatus d_status; +};/* class QueryCommand */ + +class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { +public: + SetBenchmarkLogicCommand(std::string logic); + void invoke(SmtEngine* smt); + void toStream(std::ostream& out) const; +protected: + std::string d_logic; +};/* class QueryCommand */ + + + class CVC4_PUBLIC CommandSequence : public Command { public: CommandSequence(); ~CommandSequence(); void invoke(SmtEngine* smt); void addCommand(Command* cmd); - void toString(std::ostream& out) const; + void toStream(std::ostream& out) const; private: /** All the commands to be executed (in sequence) */ std::vector d_command_sequence; diff --git a/src/util/options.h b/src/util/options.h index 2bfbf675f..d6c4e9009 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -13,11 +13,12 @@ ** Global (command-line or equivalent) tuning parameters. **/ -#include - #ifndef __CVC4__OPTIONS_H #define __CVC4__OPTIONS_H +#include +#include "parser/parser.h" + namespace CVC4 { struct Options { @@ -48,7 +49,7 @@ struct Options { }; /** The input language */ - InputLanguage lang; + parser::Parser::InputLanguage lang; Options() : binary_name(), smtcomp_mode(false), @@ -56,7 +57,7 @@ struct Options { out(0), err(0), verbosity(0), - lang(LANG_AUTO) + lang(parser::Parser::LANG_AUTO) {} };/* struct Options */ -- 2.30.2