diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/parser/cvc | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/parser/cvc')
-rw-r--r-- | src/parser/cvc/Cvc.g | 57 |
1 files changed, 40 insertions, 17 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 1f0e6b890..2988ae4ef 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1066,13 +1066,13 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, PARSER_STATE->isDeclared(id, SYM_SORT)) { Debug("parser-param") << "param: getSort " << id << " " << types.size() << " " << PARSER_STATE->getArity( id ) << " " << PARSER_STATE->isDeclared(id, SYM_SORT) << std::endl; - if( types.size()>0 ){ + if(types.size() > 0) { t = PARSER_STATE->getSort(id, types); }else{ t = PARSER_STATE->getSort(id); } } else { - if( types.empty() ){ + if(types.empty()) { t = PARSER_STATE->mkUnresolvedType(id); Debug("parser-param") << "param: make unres type " << id << std::endl; }else{ @@ -1236,22 +1236,36 @@ prefixFormula[CVC4::Expr& f] std::vector<std::string> ids; std::vector<Expr> terms; std::vector<Type> types; + std::vector<Expr> bvs; Type t; + Kind k; + Expr ipl; } /* quantifiers */ - : FORALL_TOK { PARSER_STATE->pushScope(); } LPAREN - boundVarDecl[ids,t] (COMMA boundVarDecl[ids,t])* RPAREN - COLON instantiationPatterns? formula[f] - { PARSER_STATE->popScope(); - UNSUPPORTED("quantifiers not supported yet"); - f = EXPR_MANAGER->mkVar(EXPR_MANAGER->booleanType()); + : ( FORALL_TOK { k = kind::FORALL; } | EXISTS_TOK { k = kind::EXISTS; } ) + { PARSER_STATE->pushScope(); } LPAREN + boundVarDecl[ids,t] + { for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) { + bvs.push_back(PARSER_STATE->mkVar(*i, t)); + } + ids.clear(); } - | EXISTS_TOK { PARSER_STATE->pushScope(); } LPAREN - boundVarDecl[ids,t] (COMMA boundVarDecl[ids,t])* RPAREN - COLON instantiationPatterns? formula[f] + ( COMMA boundVarDecl[ids,t] + { + for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) { + bvs.push_back(PARSER_STATE->mkVar(*i, t)); + } + ids.clear(); + } + )* RPAREN { + terms.push_back( EXPR_MANAGER->mkExpr( kind::BOUND_VAR_LIST, bvs ) ); } + COLON instantiationPatterns[ipl]? formula[f] { PARSER_STATE->popScope(); - UNSUPPORTED("quantifiers not supported yet"); - f = EXPR_MANAGER->mkVar(EXPR_MANAGER->booleanType()); + terms.push_back(f); + if(! ipl.isNull()) { + terms.push_back(ipl); + } + f = MK_EXPR(k, terms); } /* lets: letDecl defines the variables and functionss, we just @@ -1283,11 +1297,20 @@ prefixFormula[CVC4::Expr& f] } ; -instantiationPatterns +instantiationPatterns[ CVC4::Expr& expr ] @init { + std::vector<Expr> args; Expr f; + std::vector<Expr> patterns; } - : ( PATTERN_TOK LPAREN formula[f] (COMMA formula[f])* RPAREN COLON )+ + : ( PATTERN_TOK LPAREN formula[f] { args.push_back( f ); } (COMMA formula[f] { args.push_back( f ); } )* RPAREN COLON + { patterns.push_back( EXPR_MANAGER->mkExpr( kind::INST_PATTERN, args ) ); + args.clear(); + } )+ + { if(! patterns.empty()) { + expr = EXPR_MANAGER->mkExpr( kind::INST_PATTERN_LIST, patterns ); + } + } ; /** @@ -1417,7 +1440,7 @@ tupleStore[CVC4::Expr& f] Expr f2; } : k=numeral ASSIGN_TOK uminusTerm[f2] - { + { Type t = f.getType(); if(! t.isDatatype()) { PARSER_STATE->parseError("tuple-update applied to non-tuple"); @@ -1456,7 +1479,7 @@ recordStore[CVC4::Expr& f] Expr f2; } : identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK uminusTerm[f2] - { + { Type t = f.getType(); if(! t.isDatatype()) { PARSER_STATE->parseError("record-update applied to non-record"); |