diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-28 11:28:25 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-28 11:28:25 -0400 |
commit | b01a91bb5690b2648a5b8d91f940a6746cba34a3 (patch) | |
tree | 9c4881ead1f7bce2bdd522765a648b6ed896d5c3 /src/parser | |
parent | 3fc61e7f2b84765dc547634463198b30516ed432 (diff) | |
parent | 698f5a09b1c0177abfd2eaa2b110de100fd108ef (diff) |
Merge remote-tracking branch 'upstream/master' into sets
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 2 | ||||
-rw-r--r-- | src/parser/smt1/smt1.h | 3 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 63 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 1 |
4 files changed, 53 insertions, 16 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 792c3cf9d..f9055f5db 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -2018,7 +2018,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes] params.push_back( t ); } )* RBRACKET )? - { datatypes.push_back(Datatype(id, params)); + { datatypes.push_back(Datatype(id, params, false)); if(!PARSER_STATE->isUnresolvedType(id)) { // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT); diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h index f96a4e810..c19b0f872 100644 --- a/src/parser/smt1/smt1.h +++ b/src/parser/smt1/smt1.h @@ -84,7 +84,8 @@ public: THEORY_REALS, THEORY_REALS_INTS, THEORY_STRINGS, - THEORY_QUANTIFIERS + THEORY_QUANTIFIERS, + THEORY_CARDINALITY_CONSTRAINT }; private: diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 659fc97d9..8dcebc5ee 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -344,6 +344,28 @@ command returns [CVC4::Command* cmd = NULL] Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); $cmd = new DefineFunctionCommand(name, func, terms, expr); } + | DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(name); } + sortSymbol[t,CHECK_DECLARED] + { /* add variables to parser state before parsing term */ + Debug("parser") << "define const: '" << name << "'" << std::endl; + PARSER_STATE->pushScope(true); + for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = + sortedVarNames.begin(), iend = sortedVarNames.end(); + i != iend; + ++i) { + terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second)); + } + } + term[expr, expr2] + { PARSER_STATE->popScope(); + // declare the name down here (while parsing term, signature + // must not be extended with the name itself; no recursion + // permitted) + Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); + $cmd = new DefineFunctionCommand(name, func, terms, expr); + } | /* value query */ GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( LPAREN_TOK termList[terms,expr] RPAREN_TOK @@ -464,17 +486,8 @@ extendedCommand[CVC4::Command*& cmd] } /* Extended SMT-LIB set of commands syntax, not permitted in * --smtlib2 compliance mode. */ - : DECLARE_DATATYPES_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { /* open a scope to keep the UnresolvedTypes contained */ - PARSER_STATE->pushScope(true); } - LPAREN_TOK /* parametric sorts */ - ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { - sorts.push_back( PARSER_STATE->mkSort(name) ); } - )* - RPAREN_TOK - LPAREN_TOK ( LPAREN_TOK datatypeDef[dts, sorts] RPAREN_TOK )+ RPAREN_TOK - { PARSER_STATE->popScope(); - cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } + : DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] + | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] | /* get model */ GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd = new GetModelCommand(); } @@ -496,7 +509,7 @@ extendedCommand[CVC4::Command*& cmd] sortSymbol[t,CHECK_DECLARED] { Expr c = PARSER_STATE->mkVar(name, t); $cmd = new DeclareFunctionCommand(name, c, t); } - + | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); } { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) && @@ -603,6 +616,26 @@ extendedCommand[CVC4::Command*& cmd] { cmd = new SimplifyCommand(e); } ; + +datatypesDefCommand[bool isCo, CVC4::Command*& cmd] +@declarations { + std::vector<CVC4::Datatype> dts; + std::string name; + std::vector<Type> sorts; +} + : { PARSER_STATE->checkThatLogicIsSet(); + /* open a scope to keep the UnresolvedTypes contained */ + PARSER_STATE->pushScope(true); } + LPAREN_TOK /* parametric sorts */ + ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { + sorts.push_back( PARSER_STATE->mkSort(name) ); } + )* + RPAREN_TOK + LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK + { PARSER_STATE->popScope(); + cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } + ; + rewriterulesCommand[CVC4::Command*& cmd] @declarations { std::vector<std::pair<std::string, Type> > sortedVarNames; @@ -1530,7 +1563,7 @@ nonemptyNumeralList[std::vector<uint64_t>& numerals] /** * Parses a datatype definition */ -datatypeDef[std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4::Type >& params] +datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4::Type >& params] @init { std::string id; } @@ -1548,7 +1581,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4::Type >& p params.push_back( t ); } )* ']' )?*/ //AJR: this isn't necessary if we use z3's style - { datatypes.push_back(Datatype(id,params)); + { datatypes.push_back(Datatype(id,params,isCo)); if(!PARSER_STATE->isUnresolvedType(id)) { // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT); @@ -1623,6 +1656,7 @@ AS_TOK : 'as'; // extended commands DECLARE_DATATYPES_TOK : 'declare-datatypes'; +DECLARE_CODATATYPES_TOK : 'declare-codatatypes'; GET_MODEL_TOK : 'get-model'; ECHO_TOK : 'echo'; REWRITE_RULE_TOK : 'assert-rewrite'; @@ -1633,6 +1667,7 @@ DECLARE_FUNS_TOK : 'declare-funs'; DECLARE_PREDS_TOK : 'declare-preds'; DEFINE_TOK : 'define'; DECLARE_CONST_TOK : 'declare-const'; +DEFINE_CONST_TOK : 'define-const'; SIMPLIFY_TOK : 'simplify'; INCLUDE_TOK : 'include'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 64b321613..e9e6ba857 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -158,6 +158,7 @@ void Smt2::addTheory(Theory theory) { Parser::addOperator(kind::APPLY_CONSTRUCTOR); Parser::addOperator(kind::APPLY_TESTER); Parser::addOperator(kind::APPLY_SELECTOR); + Parser::addOperator(kind::APPLY_SELECTOR_TOTAL); break; case THEORY_STRINGS: |