diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r-- | src/parser/smt2/Smt2.g | 182 |
1 files changed, 50 insertions, 132 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index ebf50283d..b8b05f7dd 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -356,8 +356,8 @@ command [std::unique_ptr<CVC4::Command>* cmd] if (PARSER_STATE->sygus()) { // it is a higher-order universal variable - PARSER_STATE->mkSygusVar(name, t); - cmd->reset(new EmptyCommand()); + Expr func = PARSER_STATE->mkBoundVar(name, t); + cmd->reset(new DeclareSygusFunctionCommand(name, func, t)); } else { @@ -605,111 +605,99 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd] std::vector<Expr> terms; std::vector<Expr> sygus_vars; std::vector<std::pair<std::string, Type> > sortedVarNames; - SExpr sexpr; - std::unique_ptr<CVC4::CommandSequence> seq; Type sygus_ret; - int startIndex = -1; Expr synth_fun; Type sygus_type; + bool isInv; } : /* declare-var */ DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); } symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } sortSymbol[t,CHECK_DECLARED] - { PARSER_STATE->mkSygusVar(name, t); - cmd->reset(new EmptyCommand()); + { + Expr var = PARSER_STATE->mkBoundVar(name, t); + cmd->reset(new DeclareSygusVarCommand(name, var, t)); } | /* declare-primed-var */ DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); } symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } sortSymbol[t,CHECK_DECLARED] - { PARSER_STATE->mkSygusVar(name, t, true); - cmd->reset(new EmptyCommand()); + { + // spurious command, we do not need to create a variable. We only keep + // track of the command for sanity checking / dumping + cmd->reset(new DeclareSygusPrimedVarCommand(name, t)); } | /* synth-fun */ - ( SYNTH_FUN_TOK | SYNTH_INV_TOK { range = EXPR_MANAGER->booleanType(); } ) + ( SYNTH_FUN_TOK { isInv = false; } + | SYNTH_INV_TOK { isInv = true; range = EXPR_MANAGER->booleanType(); } + ) { PARSER_STATE->checkThatLogicIsSet(); } symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK - ( sortSymbol[range,CHECK_DECLARED] )? { - if( range.isNull() ){ + ( sortSymbol[range,CHECK_DECLARED] )? + { + if (range.isNull()) + { PARSER_STATE->parseError("Must supply return type for synth-fun."); } - if( range.isFunction() ){ - PARSER_STATE->parseError("Cannot use synth-fun with function return type."); + if (range.isFunction()) + { + PARSER_STATE->parseError( + "Cannot use synth-fun with function return type."); } - seq.reset(new CommandSequence()); std::vector<Type> var_sorts; - for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = - sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; - ++i) { - var_sorts.push_back( (*i).second ); + for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames) + { + var_sorts.push_back(p.second); } Debug("parser-sygus") << "Define synth fun : " << fun << std::endl; - Type synth_fun_type; - if( var_sorts.size()>0 ){ - synth_fun_type = EXPR_MANAGER->mkFunctionType(var_sorts, range); - }else{ - synth_fun_type = range; - } + Type synth_fun_type = var_sorts.size() > 0 + ? EXPR_MANAGER->mkFunctionType(var_sorts, range) + : range; // we do not allow overloading for synth fun synth_fun = PARSER_STATE->mkBoundVar(fun, synth_fun_type); - // we add a declare function command here - // this is the single unmuted command in the sequence generated by this smt2 command - // TODO (as part of #1170) : make this a standard command. - seq->addCommand(new DeclareFunctionCommand(fun, synth_fun, synth_fun_type)); - PARSER_STATE->pushScope(true); - for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = - sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; - ++i) { - Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second); - sygus_vars.push_back( v ); - } - Expr bvl; - if (!sygus_vars.empty()) - { - bvl = MK_EXPR(kind::BOUND_VAR_LIST, sygus_vars); - } - // associate this variable list with the synth fun - std::vector< Expr > attr_val_bvl; - attr_val_bvl.push_back( bvl ); - Command* cattr_bvl = new SetUserAttributeCommand("sygus-synth-fun-var-list", synth_fun, attr_val_bvl); - cattr_bvl->setMuted(true); - PARSER_STATE->preemptCommand(cattr_bvl); // set the sygus type to be range by default, which is overwritten below // if a grammar is provided sygus_type = range; + // create new scope for parsing the grammar, if any + PARSER_STATE->pushScope(true); + for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames) + { + sygus_vars.push_back(PARSER_STATE->mkBoundVar(p.first, p.second)); + } } ( // optionally, read the sygus grammar + // + // the sygus type specifies the required grammar for synth_fun, expressed + // as a type sygusGrammar[sygus_type, sygus_vars, fun] )? - { // the sygus sym type specifies the required grammar for synth_fun, expressed as a type + { PARSER_STATE->popScope(); - // store a dummy variable which stands for second-order quantification, linked to synth fun by an attribute - PARSER_STATE->addSygusFunSymbol(sygus_type, synth_fun); - cmd->reset(seq.release()); + Debug("parser-sygus") << "...read synth fun " << fun << std::endl; + cmd->reset( + new SynthFunCommand(fun, synth_fun, sygus_type, isInv, sygus_vars)); } | /* constraint */ - CONSTRAINT_TOK { + CONSTRAINT_TOK { PARSER_STATE->checkThatLogicIsSet(); Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl; Debug("parser-sygus") << "Sygus : read constraint..." << std::endl; } term[expr, expr2] { Debug("parser-sygus") << "...read constraint " << expr << std::endl; - PARSER_STATE->addSygusConstraint(expr); - cmd->reset(new EmptyCommand()); + cmd->reset(new SygusConstraintCommand(expr)); } - | INV_CONSTRAINT_TOK { + | INV_CONSTRAINT_TOK { PARSER_STATE->checkThatLogicIsSet(); Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl; Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl; } - ( symbol[name,CHECK_NONE,SYM_VARIABLE] { + ( symbol[name,CHECK_NONE,SYM_VARIABLE] { if( !terms.empty() ){ if( !PARSER_STATE->isDefinedFunction(name) ){ std::stringstream ss; @@ -724,85 +712,14 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd] PARSER_STATE->parseError("Bad syntax for inv-constraint: expected 4 " "arguments."); } - // get variables (regular and their respective primed versions) - std::vector<Expr> vars, primed_vars; - PARSER_STATE->getSygusInvVars(terms[0].getType(), vars, primed_vars); - // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post - for (unsigned i = 0; i < 4; ++i) - { - Expr op = terms[i]; - Debug("parser-sygus") - << "Make inv-constraint term #" << i << " : " << op << " with type " - << op.getType() << "..." << std::endl; - std::vector<Expr> children; - children.push_back(op); - // transition relation applied over both variable lists - if (i == 2) - { - children.insert(children.end(), vars.begin(), vars.end()); - children.insert( - children.end(), primed_vars.begin(), primed_vars.end()); - } - else - { - children.insert(children.end(), vars.begin(), vars.end()); - } - terms[i] = EXPR_MANAGER->mkExpr(i == 0 ? kind::APPLY_UF : kind::APPLY, - children); - // make application of Inv on primed variables - if (i == 0) - { - children.clear(); - children.push_back(op); - children.insert( - children.end(), primed_vars.begin(), primed_vars.end()); - terms.push_back(EXPR_MANAGER->mkExpr(kind::APPLY_UF, children)); - } - } - //make constraints - std::vector< Expr > conj; - conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[1], - terms[0] ) ); - const Expr term0_and_2 = EXPR_MANAGER->mkExpr(kind::AND, terms[0], - terms[2] ); - conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, term0_and_2, - terms[4] ) ); - conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[0], terms[3]) ); - Expr ic = EXPR_MANAGER->mkExpr( kind::AND, conj ); - Debug("parser-sygus") << "...read invariant constraint " << ic - << std::endl; - PARSER_STATE->addSygusConstraint(ic); - cmd->reset(new EmptyCommand()); + + cmd->reset(new SygusInvConstraintCommand(terms)); } | /* check-synth */ CHECK_SYNTH_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { Expr sygusVar = EXPR_MANAGER->mkVar("sygus", EXPR_MANAGER->booleanType()); - Expr inst_attr =EXPR_MANAGER->mkExpr(kind::INST_ATTRIBUTE, sygusVar); - Expr sygusAttr = EXPR_MANAGER->mkExpr(kind::INST_PATTERN_LIST, inst_attr); - std::vector<Expr> bodyv; - Debug("parser-sygus") << "Sygus : Constructing sygus constraint..." - << std::endl; - Expr body = EXPR_MANAGER->mkExpr(kind::NOT, - PARSER_STATE->getSygusConstraints()); - Debug("parser-sygus") << "...constructed sygus constraint " << body - << std::endl; - if( !PARSER_STATE->getSygusVars().empty() ){ - Expr boundVars = EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, - PARSER_STATE->getSygusVars()); - body = EXPR_MANAGER->mkExpr(kind::EXISTS, boundVars, body); - Debug("parser-sygus") << "...constructed exists " << body << std::endl; - } - if( !PARSER_STATE->getSygusFunSymbols().empty() ){ - Expr boundVars = EXPR_MANAGER->mkExpr( - kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()); - body = EXPR_MANAGER->mkExpr(kind::FORALL, boundVars, body, sygusAttr); - } - Debug("parser-sygus") << "...constructed forall " << body << std::endl; - Command* c = new SetUserAttributeCommand("sygus", sygusVar); - c->setMuted(true); - PARSER_STATE->preemptCommand(c); - cmd->reset(new CheckSynthCommand(body)); + { + cmd->reset(new CheckSynthCommand()); } | command[cmd] ; @@ -818,7 +735,8 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd] */ sygusGrammar[CVC4::Type & ret, std::vector<CVC4::Expr>& sygus_vars, - std::string& fun] @declarations + std::string& fun] +@declarations { Type t; std::string name; |