diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-01-17 18:15:03 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-01-17 18:15:03 +0000 |
commit | b0ac192fd4e8b1ff707e0e3cc9df92ab385f1fd4 (patch) | |
tree | edb8ee5edacadc90060cfab122e06f91bda5ccdd /src/parser | |
parent | 9f5e56a0460c2668e8c5547d616fb34a58ff6d88 (diff) |
updates to smt2 parser to support datatypes, minor updates to datatypes theory/rewriter to support datatypes with non-datatype subdata
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 38 |
1 files changed, 29 insertions, 9 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a093aa1ef..791e550b9 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -212,7 +212,7 @@ command returns [CVC4::Command* cmd = NULL] sorts.push_back(PARSER_STATE->mkSort(*i)); } } - sortSymbol[t] + sortSymbol[t,CHECK_DECLARED] { PARSER_STATE->popScope(); // Do NOT call mkSort, since that creates a new sort! // This name is not its own distinct sort, it's an alias. @@ -222,7 +222,7 @@ command returns [CVC4::Command* cmd = NULL] | /* function declaration */ DECLARE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] LPAREN_TOK sortList[sorts] RPAREN_TOK - sortSymbol[t] + sortSymbol[t,CHECK_DECLARED] { Debug("parser") << "declare fun: '" << name << "'" << std::endl; if( sorts.size() > 0 ) { t = EXPR_MANAGER->mkFunctionType(sorts, t); @@ -232,7 +232,7 @@ command returns [CVC4::Command* cmd = NULL] | /* function definition */ DEFINE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK - sortSymbol[t] + sortSymbol[t,CHECK_DECLARED] { /* add variables to parser state before parsing term */ Debug("parser") << "define fun: '" << name << "'" << std::endl; if( sortedVarNames.size() > 0 ) { @@ -462,7 +462,16 @@ term[CVC4::Expr& expr] kind = CVC4::kind::APPLY; } else { expr = PARSER_STATE->getVariable(name); - kind = CVC4::kind::APPLY_UF; + Type t = expr.getType(); + if( t.isConstructor() ){ + kind = CVC4::kind::APPLY_CONSTRUCTOR; + }else if( t.isSelector() ){ + kind = CVC4::kind::APPLY_SELECTOR; + }else if( t.isTester() ){ + kind = CVC4::kind::APPLY_TESTER; + }else{ + kind = CVC4::kind::APPLY_UF; + } } args.push_back(expr); } @@ -495,6 +504,11 @@ term[CVC4::Expr& expr] PARSER_STATE->getFunction(name)); } else { expr = PARSER_STATE->getVariable(name); + Type t = PARSER_STATE->getType(name); + if(t.isConstructor() && ConstructorType(t).getArity() == 0) { + // don't require parentheses, immediately turn it into an apply + expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr); + } } } @@ -688,7 +702,7 @@ sortList[std::vector<CVC4::Type>& sorts] @declarations { Type t; } - : ( sortSymbol[t] { sorts.push_back(t); } )* + : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )* ; /** @@ -700,7 +714,7 @@ sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars] std::string name; Type t; } - : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t] RPAREN_TOK + : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED] RPAREN_TOK { sortedVars.push_back(make_pair(name, t)); } )* ; @@ -713,14 +727,20 @@ sortName[std::string& name, CVC4::parser::DeclarationCheck check] : symbol[name,check,SYM_SORT] ; -sortSymbol[CVC4::Type& t] +sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] @declarations { std::string name; std::vector<CVC4::Type> args; std::vector<uint64_t> numerals; } : sortName[name,CHECK_NONE] - { t = PARSER_STATE->getSort(name); } + { + if( check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT) ){ + t = PARSER_STATE->getSort(name); + }else{ + t = PARSER_STATE->mkUnresolvedType(name); + } + } | LPAREN_TOK INDEX_TOK symbol[name,CHECK_NONE,SYM_SORT] nonemptyNumeralList[numerals] RPAREN_TOK { if( name == "BitVec" ) { @@ -846,7 +866,7 @@ selector[CVC4::DatatypeConstructor& ctor] std::string id; Type t, t2; } - : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t] + : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t,CHECK_NONE] { ctor.addArg(id, t); Debug("parser-idt") << "selector: " << id.c_str() << std::endl; } |