diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-27 19:27:45 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-27 19:27:45 +0000 |
| commit | 9a994c449d65e64d574a423ad9caad519f8c2148 (patch) | |
| tree | 3c4571098d1771f8d277406c9f6e9c5b09dcd1da /src/parser | |
| parent | 4bfa927dac67bbcadf219f70e61f1d123e33944b (diff) | |
merging fmf-devel branch, includes refactored datatype theory, updates to model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding. Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 56fa93a94..93d596264 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -384,6 +384,7 @@ extendedCommand[CVC4::Command*& cmd] : DECLARE_DATATYPES_TOK { PARSER_STATE->checkThatLogicIsSet(); } { /* open a scope to keep the UnresolvedTypes contained */ PARSER_STATE->pushScope(); } + LPAREN_TOK RPAREN_TOK //TODO: parametric datatypes LPAREN_TOK ( LPAREN_TOK datatypeDef[dts] RPAREN_TOK )+ RPAREN_TOK { PARSER_STATE->popScope(); cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } @@ -569,7 +570,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] Expr f, f2; std::string attr; Expr attexpr; - std::vector<Expr> attexprs; + std::vector<Expr> patexprs; std::hash_set<std::string, StringHashFunction> names; std::vector< std::pair<std::string, Expr> > binders; } @@ -714,8 +715,10 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] /* attributed expressions */ | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2] ( attribute[expr, attexpr,attr] - { if(! attexpr.isNull()) { - attexprs.push_back(attexpr); + { if( attr == ":pattern" && ! attexpr.isNull()) { + patexprs.push_back( attexpr ); + }else if( attr==":axiom" ){ + //do this? } } )+ RPAREN_TOK @@ -745,10 +748,15 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] else PARSER_STATE->parseError("Error parsing rewrite rule."); expr = MK_EXPR( kind, args ); - } else if(! attexprs.empty()) { - if(attexprs[0].getKind() == kind::INST_PATTERN) { - expr2 = MK_EXPR(kind::INST_PATTERN_LIST, attexprs); + } else if(! patexprs.empty()) { + if( !f2.isNull() && f2.getKind()==kind::INST_PATTERN_LIST ){ + for( size_t i=0; i<f2.getNumChildren(); i++ ){ + patexprs.push_back( f2[i] ); + } } + expr2 = MK_EXPR(kind::INST_PATTERN_LIST, patexprs); + }else{ + expr2 = f2; } } /* constants */ |