diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /src/parser/smt2 | |
parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) |
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.
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 210 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.cpp | 2 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.h | 6 |
3 files changed, 176 insertions, 42 deletions
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<std::string> 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<CVC4::Datatype> 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>(), expr); + new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr); PARSER_STATE->preemptCommand(c); } else { std::stringstream ss; @@ -716,6 +772,73 @@ nonemptyNumeralList[std::vector<uint64_t>& numerals] )+ ; +/** + * Parses a datatype definition + */ +datatypeDef[std::vector<CVC4::Datatype>& 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 |