From 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 2 Sep 2011 20:41:08 +0000 Subject: Merge from my post-smtcomp branch. Includes: Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated. --- src/parser/Makefile.am | 2 + src/parser/antlr_input.cpp | 2 +- src/parser/antlr_input.h | 4 +- src/parser/bounded_token_factory.cpp | 2 +- src/parser/bounded_token_factory.h | 2 +- src/parser/cvc/Cvc.g | 99 ++++++++------ src/parser/cvc/cvc_input.cpp | 2 +- src/parser/cvc/cvc_input.h | 2 +- src/parser/input.cpp | 2 +- src/parser/memory_mapped_input_buffer.cpp | 2 +- src/parser/memory_mapped_input_buffer.h | 2 +- src/parser/parser.cpp | 21 +-- src/parser/parser.h | 7 +- src/parser/smt/Smt.g | 92 ++++++++----- src/parser/smt/smt.cpp | 15 ++- src/parser/smt/smt.h | 4 +- src/parser/smt/smt_input.cpp | 2 +- src/parser/smt/smt_input.h | 2 +- src/parser/smt2/Smt2.g | 210 ++++++++++++++++++++++++------ src/parser/smt2/smt2_input.cpp | 2 +- src/parser/smt2/smt2_input.h | 6 +- 21 files changed, 331 insertions(+), 151 deletions(-) (limited to 'src/parser') diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 2b90da502..f1802c6c5 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -20,7 +20,9 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) SUBDIRS = smt smt2 cvc nobase_lib_LTLIBRARIES = libcvc4parser.la +if HAVE_CXXTESTGEN noinst_LTLIBRARIES = libcvc4parser_noinst.la +endif libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) \ -version-info $(LIBCVC4PARSER_VERSION) diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 74157acd7..c51d4b8c3 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 4ae063266..913dd8013 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): mdeters, dejan + ** Minor contributors (to current version): dejan, mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/parser/bounded_token_factory.cpp b/src/parser/bounded_token_factory.cpp index 5f42f0f29..71b8849e5 100644 --- a/src/parser/bounded_token_factory.cpp +++ b/src/parser/bounded_token_factory.cpp @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/parser/bounded_token_factory.h b/src/parser/bounded_token_factory.h index 4d510c9e3..84697fd3e 100644 --- a/src/parser/bounded_token_factory.h +++ b/src/parser/bounded_token_factory.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 75a59c6e0..1f817350c 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: mdeters - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): dejan, ajreynol ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -64,6 +64,7 @@ tokens { PRINT_TYPE_TOK = 'PRINT_TYPE'; CALL_TOK = 'CALL'; ECHO_TOK = 'ECHO'; + EXIT_TOK = 'EXIT'; INCLUDE_TOK = 'INCLUDE'; DUMP_PROOF_TOK = 'DUMP_PROOF'; DUMP_ASSUMPTIONS_TOK = 'DUMP_ASSUMPTIONS'; @@ -84,7 +85,6 @@ tokens { AND_TOK = 'AND'; BOOLEAN_TOK = 'BOOLEAN'; - ECHO_TOK = 'ECHO'; ELSEIF_TOK = 'ELSIF'; ELSE_TOK = 'ELSE'; ENDIF_TOK = 'ENDIF'; @@ -448,38 +448,39 @@ namespace CVC4 { /** * This class is just here to get around an unfortunate bit of Antlr. * We use strings below as return values from rules, which require - * them to be constructible by a uintptr_t. So we derive the string + * them to be constructible by a void*. So we derive the string * class to provide just such a conversion. */ class myString : public std::string { public: myString(const std::string& s) : std::string(s) {} - myString(uintptr_t) : std::string() {} + myString(void*) : std::string() {} myString() : std::string() {} };/* class myString */ /** - * Just exists to give us the uintptr_t construction that + * Just exists to give us the void* construction that * ANTLR requires. */ class mySubrangeBound : public CVC4::SubrangeBound { public: mySubrangeBound() : CVC4::SubrangeBound() {} - mySubrangeBound(uintptr_t) : CVC4::SubrangeBound() {} + mySubrangeBound(void*) : CVC4::SubrangeBound() {} mySubrangeBound(const Integer& i) : CVC4::SubrangeBound(i) {} mySubrangeBound(const SubrangeBound& b) : CVC4::SubrangeBound(b) {} };/* class mySubrangeBound */ /** - * Just exists to give us the uintptr_t construction that + * Just exists to give us the void* construction that * ANTLR requires. */ struct myExpr : public CVC4::Expr { myExpr() : CVC4::Expr() {} - myExpr(uintptr_t) : CVC4::Expr() {} + myExpr(void*) : CVC4::Expr() {} myExpr(const Expr& e) : CVC4::Expr(e) {} myExpr(const myExpr& e) : CVC4::Expr(e) {} };/* struct myExpr */ + }/* CVC4::parser::cvc namespace */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ @@ -532,7 +533,7 @@ using namespace CVC4::parser; * Parses an expression. * @return the parsed expression */ -parseExpr returns [CVC4::parser::cvc::myExpr expr] +parseExpr returns [CVC4::Expr expr = CVC4::Expr()] : formula[expr] | EOF ; @@ -541,7 +542,7 @@ parseExpr returns [CVC4::parser::cvc::myExpr expr] * Parses a command (the whole benchmark) * @return the command of the benchmark */ -parseCommand returns [CVC4::Command* cmd] +parseCommand returns [CVC4::Command* cmd = NULL] : c=command { $cmd = c; } | EOF { $cmd = NULL; } ; @@ -580,7 +581,6 @@ mainCommand[CVC4::Command*& cmd] std::vector dts; Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl; std::string s; - k = 0; } /* our bread & butter */ : ASSERT_TOK formula[f] { cmd = new AssertCommand(f); } @@ -696,6 +696,9 @@ mainCommand[CVC4::Command*& cmd] | { Message() << std::endl; } ) + | EXIT_TOK + { cmd = new QuitCommand(); } + | INCLUDE_TOK ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) { UNSUPPORTED("INCLUDE command"); } @@ -752,15 +755,15 @@ toplevelDeclaration[CVC4::Command*& cmd] Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) << std::endl; } : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON - ( declareVariables[t,ids,true] { cmd = new DeclarationCommand(ids, t); } - | declareTypes[ids] { cmd = new DeclarationCommand(ids, EXPR_MANAGER->kindType()); } ) + ( declareVariables[cmd,t,ids,true] + | declareTypes[cmd,ids] ) ; /** * A bound variable declaration. */ boundVarDecl[std::vector& ids, CVC4::Type& t] - : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON declareVariables[t,ids,false] + : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON declareVariables[*(Command**)NULL,t,ids,false] ; /** @@ -808,13 +811,14 @@ boundVarDeclReturn[std::vector& terms, * because type declarations are always top-level, except for * type-lets, which don't use this rule. */ -declareTypes[const std::vector& idList] +declareTypes[CVC4::Command*& cmd, const std::vector& idList] @init { Type t; } /* A sort declaration (e.g., "T : TYPE") */ : TYPE_TOK - { for(std::vector::const_iterator i = idList.begin(); + { DeclarationSequence* seq = new DeclarationSequence(); + for(std::vector::const_iterator i = idList.begin(); i != idList.end(); ++i) { // Don't allow a type variable to clash with a previously @@ -822,8 +826,11 @@ declareTypes[const std::vector& idList] // non-type variable can clash unambiguously. Break from CVC3 // behavior here. PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_SORT); + Type sort = PARSER_STATE->mkSort(*i); + Command* decl = new DeclareTypeCommand(*i, 0, sort); + seq->addCommand(decl); } - PARSER_STATE->mkSorts(idList); + cmd = seq; } /* A type alias "T : TYPE = foo..." */ @@ -843,16 +850,20 @@ declareTypes[const std::vector& idList] * re-declared if topLevel is true (CVC allows re-declaration if the * types are compatible---if they aren't compatible, an error is * thrown). Also if topLevel is true, variable definitions are - * permitted. + * permitted and "cmd" is output. */ -declareVariables[CVC4::Type& t, const std::vector& idList, bool topLevel] +declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector& idList, bool topLevel] @init { Expr f; Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl; } /* A variable declaration (or definition) */ : type[t,CHECK_DECLARED] ( EQUAL_TOK formula[f] )? - { if(f.isNull()) { + { DeclarationSequence* seq = NULL; + if(topLevel) { + cmd = seq = new DeclarationSequence(); + } + if(f.isNull()) { Debug("parser") << "working on " << idList.front() << " : " << t << std::endl; // CVC language allows redeclaration of variables if types are the same for(std::vector::const_iterator i = idList.begin(), @@ -877,6 +888,10 @@ declareVariables[CVC4::Type& t, const std::vector& idList, bool top } else { Debug("parser") << " " << *i << " not declared" << std::endl; PARSER_STATE->mkVar(*i, t); + if(topLevel) { + Command* decl = new DeclareFunctionCommand(*i, t); + seq->addCommand(decl); + } } } } else { @@ -892,6 +907,8 @@ declareVariables[CVC4::Type& t, const std::vector& idList, bool top ++i) { PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE); PARSER_STATE->defineFunction(*i, f); + Command* decl = new DefineFunctionCommand(*i, Expr(), f); + seq->addCommand(decl); } } } @@ -1007,10 +1024,10 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, /* named types */ : identifier[id,check,SYM_SORT] parameterization[check,types]? - { + { if(check == CHECK_DECLARED || PARSER_STATE->isDeclared(id, SYM_SORT)) { - Debug("parser-param") << "param: getSort " << id << " " << types.size() << " " << PARSER_STATE->getArity( id ) + Debug("parser-param") << "param: getSort " << id << " " << types.size() << " " << PARSER_STATE->getArity( id ) << " " << PARSER_STATE->isDeclared(id, SYM_SORT) << std::endl; if( types.size()>0 ){ t = PARSER_STATE->getSort(id, types); @@ -1024,7 +1041,7 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, }else{ t = PARSER_STATE->mkUnresolvedTypeConstructor(id,types); t = SortConstructorType(t).instantiate( types ); - Debug("parser-param") << "param: make unres param type " << id << " " << types.size() << " " + Debug("parser-param") << "param: make unres param type " << id << " " << types.size() << " " << PARSER_STATE->getArity( id ) << std::endl; } } @@ -1095,7 +1112,7 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, } ; -parameterization[CVC4::parser::DeclarationCheck check, +parameterization[CVC4::parser::DeclarationCheck check, std::vector& params] @init { Type t; @@ -1146,7 +1163,7 @@ formula[CVC4::Expr& f] ; morecomparisons[std::vector& expressions, - std::vector& operators] returns [size_t i] + std::vector& operators] returns [size_t i = 0] @init { unsigned op; Expr f; @@ -1165,10 +1182,7 @@ morecomparisons[std::vector& expressions, ; /** Matches 0 or more NOTs. */ -nots returns [size_t n] -@init { - $n = 0; -} +nots returns [size_t n = 0] : ( NOT_TOK { ++$n; } )* ; @@ -1208,8 +1222,9 @@ prefixFormula[CVC4::Expr& f] RPAREN COLON formula[f] { PARSER_STATE->popScope(); Type t = EXPR_MANAGER->mkFunctionType(types, f.getType()); - Expr func = PARSER_STATE->mkAnonymousFunction("lambda", t); - Command* cmd = new DefineFunctionCommand(func, terms, f); + std::string name = "lambda"; + Expr func = PARSER_STATE->mkAnonymousFunction(name, t); + Command* cmd = new DefineFunctionCommand(name, func, terms, f); PARSER_STATE->preemptCommand(cmd); f = func; } @@ -1735,17 +1750,18 @@ datatypeDef[std::vector& datatypes] Type t; std::vector< Type > params; } - /* This really needs to be CHECK_NONE, or mutually-recursive datatypes - * won't work, because this type will already be "defined" as an - * unresolved type; don't worry, we check below. */ + /* This really needs to be CHECK_NONE, or mutually-recursive + * datatypes won't work, because this type will already be + * "defined" as an unresolved type; don't worry, we check + * below. */ : identifier[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); } - ( LBRACKET identifier[id2,CHECK_UNDECLARED,SYM_SORT] { + ( LBRACKET identifier[id2,CHECK_UNDECLARED,SYM_SORT] { t = PARSER_STATE->mkSort(id2); - params.push_back( t ); + params.push_back( t ); } - ( COMMA identifier[id2,CHECK_UNDECLARED,SYM_SORT] { + ( COMMA identifier[id2,CHECK_UNDECLARED,SYM_SORT] { t = PARSER_STATE->mkSort(id2); - params.push_back( t ); } + params.push_back( t ); } )* RBRACKET )? { datatypes.push_back(Datatype(id,params)); @@ -1768,8 +1784,7 @@ constructorDef[CVC4::Datatype& type] CVC4::Datatype::Constructor* ctor = NULL; } : identifier[id,CHECK_UNDECLARED,SYM_SORT] - { - // make the tester + { // make the tester std::string testerId("is_"); testerId.append(id); PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT); @@ -1826,7 +1841,7 @@ DECIMAL_LITERAL * in the BVPLUS/BVMINUS/BVMULT rules where $INTEGER_LITERAL was * returning a reference to the wrong token?! */ -numeral returns [unsigned k] +numeral returns [unsigned k = 0] : INTEGER_LITERAL { $k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); } ; @@ -1834,7 +1849,7 @@ numeral returns [unsigned k] /** * Similar to numeral but for arbitrary-precision, signed integer. */ -integer returns [CVC4::Integer k] +integer returns [CVC4::Integer k = 0] : INTEGER_LITERAL { $k = AntlrInput::tokenToInteger($INTEGER_LITERAL); } | MINUS_TOK INTEGER_LITERAL diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index 541ac0eac..d91a13bee 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index efe0a522f..9a1f24fde 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 36e96516f..27b207342 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -5,7 +5,7 @@ ** Major contributors: mdeters, cconway ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp index aad5aaec0..dad38c913 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/parser/memory_mapped_input_buffer.h b/src/parser/memory_mapped_input_buffer.h index 18618a090..ccbe04059 100644 --- a/src/parser/memory_mapped_input_buffer.h +++ b/src/parser/memory_mapped_input_buffer.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 78e70572a..3f2ec107a 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: dejan ** Major contributors: cconway, mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): ajreynol ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -227,15 +227,6 @@ Parser::mkSortConstructor(const std::string& name, size_t arity) { return type; } -std::vector -Parser::mkSorts(const std::vector& names) { - std::vector types; - for(unsigned i = 0; i < names.size(); ++i) { - types.push_back(mkSort(names[i])); - } - return types; -} - SortType Parser::mkUnresolvedType(const std::string& name) { SortType unresolved = mkSort(name); d_unresolved.insert(unresolved); @@ -243,7 +234,7 @@ SortType Parser::mkUnresolvedType(const std::string& name) { } SortConstructorType -Parser::mkUnresolvedTypeConstructor(const std::string& name, +Parser::mkUnresolvedTypeConstructor(const std::string& name, size_t arity) { SortConstructorType unresolved = mkSortConstructor(name,arity); d_unresolved.insert(unresolved); @@ -251,7 +242,7 @@ Parser::mkUnresolvedTypeConstructor(const std::string& name, } SortConstructorType -Parser::mkUnresolvedTypeConstructor(const std::string& name, +Parser::mkUnresolvedTypeConstructor(const std::string& name, const std::vector& params) { Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; @@ -356,13 +347,15 @@ void Parser::checkDeclaration(const std::string& varName, switch(check) { case CHECK_DECLARED: if( !isDeclared(varName, type) ) { - parseError("Symbol " + varName + " not declared as a " + (type == SYM_VARIABLE ? "variable" : "type")); + parseError("Symbol " + varName + " not declared as a " + + (type == SYM_VARIABLE ? "variable" : "type")); } break; case CHECK_UNDECLARED: if( isDeclared(varName, type) ) { - parseError("Symbol " + varName + " previously declared as a " + (type == SYM_VARIABLE ? "variable" : "type")); + parseError("Symbol " + varName + " previously declared as a " + + (type == SYM_VARIABLE ? "variable" : "type")); } break; diff --git a/src/parser/parser.h b/src/parser/parser.h index b2f76b39d..5ce016b85 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: cconway ** Major contributors: mdeters - ** Minor contributors (to current version): dejan + ** Minor contributors (to current version): dejan, ajreynol ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -367,11 +367,6 @@ public: */ SortConstructorType mkSortConstructor(const std::string& name, size_t arity); - /** - * Creates new sorts with the given names (all of arity 0). - */ - std::vector mkSorts(const std::vector& names); - /** * Creates a new "unresolved type," used only during parsing. */ diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 2a3a79125..da20c68a2 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -2,7 +2,7 @@ /*! \file Smt.g ** \verbatim ** Original author: cconway - ** Major contributors: mdeters, dejan + ** Major contributors: dejan, mdeters ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) @@ -143,7 +143,7 @@ parseExpr returns [CVC4::parser::smt::myExpr expr] * Parses a command (the whole benchmark) * @return the command of the benchmark */ -parseCommand returns [CVC4::Command* cmd] +parseCommand returns [CVC4::Command* cmd = NULL] : b = benchmark { $cmd = b; } ; @@ -151,7 +151,7 @@ parseCommand returns [CVC4::Command* cmd] * Matches the whole SMT-LIB benchmark. * @return the sequence command containing the whole problem */ -benchmark returns [CVC4::Command* cmd] +benchmark returns [CVC4::Command* cmd = NULL] : LPAREN_TOK BENCHMARK_TOK IDENTIFIER c = benchAttributes RPAREN_TOK { $cmd = c; } | EOF { $cmd = 0; } @@ -162,7 +162,7 @@ benchmark returns [CVC4::Command* cmd] * command sequence. * @return the command sequence */ -benchAttributes returns [CVC4::CommandSequence* cmd_seq] +benchAttributes returns [CVC4::CommandSequence* cmd_seq = NULL] @init { cmd_seq = new CommandSequence(); } @@ -174,26 +174,42 @@ benchAttributes returns [CVC4::CommandSequence* cmd_seq] * a corresponding command * @return a command corresponding to the attribute */ -benchAttribute returns [CVC4::Command* smt_command] +benchAttribute returns [CVC4::Command* smt_command = NULL] @declarations { std::string name; BenchmarkStatus b_status; Expr expr; + Command* c; } : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE] - { PARSER_STATE->setLogic(name); - smt_command = new SetBenchmarkLogicCommand(name); } + { PARSER_STATE->preemptCommand(new SetBenchmarkLogicCommand(name)); + PARSER_STATE->setLogic(name); + smt_command = new EmptyCommand(); + } | ASSUMPTION_TOK annotatedFormula[expr] - { smt_command = new AssertCommand(expr); } + { smt_command = new AssertCommand(expr); } | FORMULA_TOK annotatedFormula[expr] { smt_command = new CheckSatCommand(expr); } | STATUS_TOK status[b_status] { smt_command = new SetBenchmarkStatusCommand(b_status); } - | EXTRAFUNS_TOK LPAREN_TOK (functionDeclaration)+ RPAREN_TOK - | EXTRAPREDS_TOK LPAREN_TOK (predicateDeclaration)+ RPAREN_TOK - | EXTRASORTS_TOK LPAREN_TOK sortDeclaration+ RPAREN_TOK + | EXTRAFUNS_TOK LPAREN_TOK + ( { smt_command = new CommandSequence(); } + functionDeclaration[c] + { ((CommandSequence*) smt_command)->addCommand(c); } + )+ RPAREN_TOK + | EXTRAPREDS_TOK LPAREN_TOK + ( { smt_command = new CommandSequence(); } + predicateDeclaration[c] + { ((CommandSequence*) smt_command)->addCommand(c); } + )+ RPAREN_TOK + | EXTRASORTS_TOK LPAREN_TOK + ( { smt_command = new CommandSequence(); } + sortDeclaration[c] + { ((CommandSequence*) smt_command)->addCommand(c); } + )+ RPAREN_TOK | NOTES_TOK STRING_LITERAL - | annotation + { smt_command = new CommentCommand(AntlrInput::tokenText($STRING_LITERAL)); } + | annotation[smt_command] ; /** @@ -417,11 +433,12 @@ functionSymbol[CVC4::Expr& fun] /** * Matches an attribute name from the input (:attribute_name). */ -attribute +attribute[std::string& s] : ATTR_IDENTIFIER + { s = AntlrInput::tokenText($ATTR_IDENTIFIER); } ; -functionDeclaration +functionDeclaration[CVC4::Command*& smt_command] @declarations { std::string name; std::vector sorts; @@ -435,13 +452,15 @@ functionDeclaration } else { t = EXPR_MANAGER->mkFunctionType(sorts); } - PARSER_STATE->mkVar(name, t); } + PARSER_STATE->mkVar(name, t); + smt_command = new DeclareFunctionCommand(name, t); + } ; /** * Matches the declaration of a predicate and declares it */ -predicateDeclaration +predicateDeclaration[CVC4::Command*& smt_command] @declarations { std::string name; std::vector p_sorts; @@ -453,16 +472,20 @@ predicateDeclaration } else { t = EXPR_MANAGER->mkPredicateType(p_sorts); } - PARSER_STATE->mkVar(name, t); } + PARSER_STATE->mkVar(name, t); + smt_command = new DeclareFunctionCommand(name, t); + } ; -sortDeclaration +sortDeclaration[CVC4::Command*& smt_command] @declarations { std::string name; } : sortName[name,CHECK_UNDECLARED] { Debug("parser") << "sort decl: '" << name << "'" << std::endl; - PARSER_STATE->mkSort(name); } + Type type = PARSER_STATE->mkSort(name); + smt_command = new DeclareTypeCommand(name, 0, type); + } ; /** @@ -503,8 +526,19 @@ status[ CVC4::BenchmarkStatus& status ] /** * Matches an annotation, which is an attribute name, with an optional user */ -annotation - : attribute (USER_VALUE)? +annotation[CVC4::Command*& smt_command] +@init { + std::string key; + smt_command = NULL; +} + : attribute[key] + ( USER_VALUE + { smt_command = new SetInfoCommand(key, AntlrInput::tokenText($USER_VALUE)); } + )? + { if(smt_command == NULL) { + smt_command = new EmptyCommand(std::string("annotation: ") + key); + } + } ; /** @@ -676,21 +710,20 @@ FLET_IDENTIFIER ; /** - * Matches the value of user-defined annotations or attributes. The only constraint imposed on a user-defined value is that it start with - * an open brace and end with closed brace. + * Matches the value of user-defined annotations or attributes. The + * only constraint imposed on a user-defined value is that it start + * with an open brace and end with closed brace. */ USER_VALUE - : '{' - ( '\\{' | '\\}' | ~('{' | '}') )* - '}' + : '{' ( '\\{' | '\\}' | ~('{' | '}') )* '}' ; - /** * Matches and skips whitespace in the input. */ WHITESPACE - : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP();; } + : (' ' | '\t' | '\f' | '\r' | '\n')+ + { SKIP(); } ; /** @@ -716,7 +749,8 @@ STRING_LITERAL * Matches the comments and ignores them */ COMMENT - : ';' (~('\n' | '\r'))* { SKIP();; } + : ';' (~('\n' | '\r'))* + { SKIP(); } ; diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index a8dabeffe..a6e716b77 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -2,8 +2,8 @@ /*! \file smt.cpp ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -20,6 +20,7 @@ namespace std { } #include "expr/type.h" +#include "expr/command.h" #include "parser/parser.h" #include "parser/smt/smt.h" @@ -80,6 +81,10 @@ void Smt::addTheory(Theory theory) { case THEORY_ARRAYS_EX: { Type indexType = mkSort("Index"); Type elementType = mkSort("Element"); + DeclarationSequence* seq = new DeclarationSequence(); + seq->addCommand(new DeclareTypeCommand("Index", 0, indexType)); + seq->addCommand(new DeclareTypeCommand("Element", 0, elementType)); + preemptCommand(seq); defineType("Array", getExprManager()->mkArrayType(indexType,elementType)); @@ -88,9 +93,11 @@ void Smt::addTheory(Theory theory) { break; } - case THEORY_EMPTY: - mkSort("U"); + case THEORY_EMPTY: { + Type sort = mkSort("U"); + preemptCommand(new DeclareTypeCommand("U", 0, sort)); break; + } case THEORY_REALS_INTS: defineType("Real", getExprManager()->realType()); diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h index 98ebf6410..11a30c2fc 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt/smt.h @@ -2,8 +2,8 @@ /*! \file smt.h ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp index d062683d3..d368339f5 100644 --- a/src/parser/smt/smt_input.cpp +++ b/src/parser/smt/smt_input.cpp @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h index 2fb037f06..b976a3b6a 100644 --- a/src/parser/smt/smt_input.h +++ b/src/parser/smt/smt_input.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 091e6c93c..5ae04adea 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -143,7 +143,7 @@ parseExpr returns [CVC4::parser::smt2::myExpr expr] * Parses a command * @return the parsed command, or NULL if we've reached the end of the input */ -parseCommand returns [CVC4::Command* cmd] +parseCommand returns [CVC4::Command* cmd = NULL] : LPAREN_TOK c = command RPAREN_TOK { $cmd = c; } | EOF { $cmd = 0; } ; @@ -151,7 +151,7 @@ parseCommand returns [CVC4::Command* cmd] /** * Parse the internal portion of the command, ignoring the surrounding parentheses. */ -command returns [CVC4::Command* cmd] +command returns [CVC4::Command* cmd = NULL] @declarations { std::string name; std::vector names; @@ -192,11 +192,11 @@ command returns [CVC4::Command* cmd] << "' arity=" << n << std::endl; unsigned arity = AntlrInput::tokenToUnsigned(n); if(arity == 0) { - PARSER_STATE->mkSort(name); - $cmd = new DeclarationCommand(name, EXPR_MANAGER->kindType()); + Type type = PARSER_STATE->mkSort(name); + $cmd = new DeclareTypeCommand(name, 0, type); } else { - PARSER_STATE->mkSortConstructor(name, arity); - $cmd = new DeclarationCommand(name, EXPR_MANAGER->kindType()); + Type type = PARSER_STATE->mkSortConstructor(name, arity); + $cmd = new DeclareTypeCommand(name, arity, type); } } | /* sort definition */ @@ -216,7 +216,7 @@ command returns [CVC4::Command* cmd] // Do NOT call mkSort, since that creates a new sort! // This name is not its own distinct sort, it's an alias. PARSER_STATE->defineParameterizedType(name, sorts, t); - $cmd = new EmptyCommand; + $cmd = new DefineTypeCommand(name, sorts, t); } | /* function declaration */ DECLARE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] @@ -227,7 +227,7 @@ command returns [CVC4::Command* cmd] t = EXPR_MANAGER->mkFunctionType(sorts, t); } PARSER_STATE->mkVar(name, t); - $cmd = new DeclarationCommand(name,t); } + $cmd = new DeclareFunctionCommand(name, t); } | /* function definition */ DEFINE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK @@ -259,10 +259,16 @@ command returns [CVC4::Command* cmd] // must not be extended with the name itself; no recursion // permitted) Expr func = PARSER_STATE->mkFunction(name, t); - $cmd = new DefineFunctionCommand(func, terms, expr); + $cmd = new DefineFunctionCommand(name, func, terms, expr); } | /* value query */ - GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK + ( GET_VALUE_TOK | + EVAL_TOK + { if(PARSER_STATE->strictModeEnabled()) { + PARSER_STATE->parseError("Strict compliance mode doesn't recognize \"eval\". Maybe you want (get-value...)?"); + } + } ) + LPAREN_TOK termList[terms,expr] RPAREN_TOK { if(terms.size() == 1) { $cmd = new GetValueCommand(terms[0]); } else { @@ -289,36 +295,86 @@ command returns [CVC4::Command* cmd] GET_ASSERTIONS_TOK { cmd = new GetAssertionsCommand; } | /* push */ - PUSH_TOK k=INTEGER_LITERAL - { unsigned n = AntlrInput::tokenToUnsigned(k); - if(n == 0) { - cmd = new EmptyCommand; - } else if(n == 1) { - cmd = new PushCommand; - } else { - CommandSequence* seq = new CommandSequence; - do { - seq->addCommand(new PushCommand); - } while(--n > 0); - cmd = seq; + PUSH_TOK + ( k=INTEGER_LITERAL + { unsigned n = AntlrInput::tokenToUnsigned(k); + if(n == 0) { + cmd = new EmptyCommand; + } else if(n == 1) { + cmd = new PushCommand; + } else { + CommandSequence* seq = new CommandSequence; + do { + seq->addCommand(new PushCommand); + } while(--n > 0); + cmd = seq; + } } - } - | POP_TOK k=INTEGER_LITERAL - { unsigned n = AntlrInput::tokenToUnsigned(k); - if(n == 0) { - cmd = new EmptyCommand; - } else if(n == 1) { - cmd = new PopCommand; - } else { - CommandSequence* seq = new CommandSequence; - do { - seq->addCommand(new PopCommand); - } while(--n > 0); - cmd = seq; + | { if(PARSER_STATE->strictModeEnabled()) { + PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to PUSH. Maybe you want (push 1)?"); + } else { + cmd = new PushCommand; + } + } ) + | POP_TOK + ( k=INTEGER_LITERAL + { unsigned n = AntlrInput::tokenToUnsigned(k); + if(n == 0) { + cmd = new EmptyCommand; + } else if(n == 1) { + cmd = new PopCommand; + } else { + CommandSequence* seq = new CommandSequence; + do { + seq->addCommand(new PopCommand); + } while(--n > 0); + cmd = seq; + } } - } + | { if(PARSER_STATE->strictModeEnabled()) { + PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to POP. Maybe you want (pop 1)?"); + } else { + cmd = new PopCommand; + } + } ) | EXIT_TOK { cmd = new QuitCommand; } + + /* CVC4-extended SMT-LIBv2 commands */ + | extendedCommand[cmd] + { if(PARSER_STATE->strictModeEnabled()) { + PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode."); + } + } + ; + +extendedCommand[CVC4::Command*& cmd] +@declarations { + std::vector dts; + Expr e; +} + /* Z3's extended SMT-LIBv2 set of commands syntax */ + : DECLARE_DATATYPES_TOK + { /* open a scope to keep the UnresolvedTypes contained */ + PARSER_STATE->pushScope(); } + LPAREN_TOK ( LPAREN_TOK datatypeDef[dts] RPAREN_TOK )+ RPAREN_TOK + { PARSER_STATE->popScope(); + cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } + + + | DECLARE_SORTS_TOK + | DECLARE_FUNS_TOK + | DECLARE_PREDS_TOK + | DEFINE_TOK + | DEFINE_SORTS_TOK + | DECLARE_CONST_TOK + + | SIMPLIFY_TOK term[e] + { cmd = new SimplifyCommand(e); } + | ECHO_TOK + ( STRING_LITERAL + { Message() << AntlrInput::tokenText($STRING_LITERAL) << std::endl; } + | { Message() << std::endl; } ) ; symbolicExpr[CVC4::SExpr& sexpr] @@ -441,7 +497,7 @@ term[CVC4::Expr& expr] Expr func = PARSER_STATE->mkFunction(name, expr.getType()); // bind name to expr with define-fun Command* c = - new DefineNamedFunctionCommand(func, std::vector(), expr); + new DefineNamedFunctionCommand(name, func, std::vector(), expr); PARSER_STATE->preemptCommand(c); } else { std::stringstream ss; @@ -716,6 +772,73 @@ nonemptyNumeralList[std::vector& numerals] )+ ; +/** + * Parses a datatype definition + */ +datatypeDef[std::vector& datatypes] +@init { + std::string id, id2; + Type t; + std::vector< Type > params; +} + /* This really needs to be CHECK_NONE, or mutually-recursive + * datatypes won't work, because this type will already be + * "defined" as an unresolved type; don't worry, we check + * below. */ + : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); } + ( '[' symbol[id2,CHECK_UNDECLARED,SYM_SORT] { + t = PARSER_STATE->mkSort(id2); + params.push_back( t ); + } + ( symbol[id2,CHECK_UNDECLARED,SYM_SORT] { + t = PARSER_STATE->mkSort(id2); + params.push_back( t ); } + )* ']' + )? + { datatypes.push_back(Datatype(id,params)); + if(!PARSER_STATE->isUnresolvedType(id)) { + // if not unresolved, must be undeclared + PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT); + } + } + ( LPAREN_TOK constructorDef[datatypes.back()] RPAREN_TOK )+ + { PARSER_STATE->popScope(); } + ; + +/** + * Parses a constructor defintion for type + */ +constructorDef[CVC4::Datatype& type] +@init { + std::string id; + CVC4::Datatype::Constructor* ctor = NULL; +} + : symbol[id,CHECK_UNDECLARED,SYM_SORT] + { // make the tester + std::string testerId("is_"); + testerId.append(id); + PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT); + ctor = new CVC4::Datatype::Constructor(id, testerId); + } + ( LPAREN_TOK selector[*ctor] RPAREN_TOK )* + { // make the constructor + type.addConstructor(*ctor); + Debug("parser-idt") << "constructor: " << id.c_str() << std::endl; + delete ctor; + } + ; + +selector[CVC4::Datatype::Constructor& ctor] +@init { + std::string id; + Type t, t2; +} + : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t] + { ctor.addArg(id, t); + Debug("parser-idt") << "selector: " << id.c_str() << std::endl; + } + ; + // Base SMT-LIB tokens ASSERT_TOK : 'assert'; CHECKSAT_TOK : 'check-sat'; @@ -741,6 +864,18 @@ GET_OPTION_TOK : 'get-option'; PUSH_TOK : 'push'; POP_TOK : 'pop'; +// extended commands +DECLARE_DATATYPES_TOK : 'declare-datatypes'; +DECLARE_SORTS_TOK : 'declare-sorts'; +DECLARE_FUNS_TOK : 'declare-funs'; +DECLARE_PREDS_TOK : 'declare-preds'; +DEFINE_TOK : 'define'; +DEFINE_SORTS_TOK : 'define-sorts'; +DECLARE_CONST_TOK : 'declare-const'; +SIMPLIFY_TOK : 'simplify'; +EVAL_TOK : 'eval'; +ECHO_TOK : 'echo'; + // operators (NOTE: theory symbols go here) AMPERSAND_TOK : '&'; AND_TOK : 'and'; @@ -759,7 +894,6 @@ MINUS_TOK : '-'; NOT_TOK : 'not'; OR_TOK : 'or'; PERCENT_TOK : '%'; -PIPE_TOK : '|'; PLUS_TOK : '+'; POUND_TOK : '#'; SELECT_TOK : 'select'; diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 9a349785c..acd0e17f6 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 04fe48fe1..05a62c30d 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -2,10 +2,10 @@ /*! \file smt2_input.h ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 -- cgit v1.2.3