From 406bcd32cbf8a1ee48af02fc6cddc618158762f0 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 18 Oct 2018 10:07:18 -0500 Subject: Introducing internal commands for SyGuS commands (#2627) --- src/parser/smt2/Smt2.g | 182 +++++++++++++---------------------------------- src/parser/smt2/smt2.cpp | 67 ----------------- src/parser/smt2/smt2.h | 29 -------- 3 files changed, 50 insertions(+), 228 deletions(-) (limited to 'src/parser') 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* 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* cmd] std::vector terms; std::vector sygus_vars; std::vector > sortedVarNames; - SExpr sexpr; - std::unique_ptr 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 var_sorts; - for(std::vector >::const_iterator i = - sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; - ++i) { - var_sorts.push_back( (*i).second ); + for (const std::pair& 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 >::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& 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* cmd] PARSER_STATE->parseError("Bad syntax for inv-constraint: expected 4 " "arguments."); } - // get variables (regular and their respective primed versions) - std::vector 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 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 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* cmd] */ sygusGrammar[CVC4::Type & ret, std::vector& sygus_vars, - std::string& fun] @declarations + std::string& fun] +@declarations { Type t; std::string name; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index c4046b7c2..2fd61aabc 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -630,20 +630,6 @@ void Smt2::includeFile(const std::string& filename) { } } -void Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed) -{ - if (!isPrimed) - { - d_sygusVars.push_back(mkBoundVar(name, type)); - } -#ifdef CVC4_ASSERTIONS - else - { - d_sygusVarPrimed.push_back(mkBoundVar(name, type)); - } -#endif -} - void Smt2::mkSygusConstantsForType( const Type& type, std::vector& ops ) { if( type.isInteger() ){ ops.push_back(getExprManager()->mkConst(Rational(0))); @@ -1234,59 +1220,6 @@ Expr Smt2::makeSygusBoundVarList(Datatype& dt, return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars); } -const void Smt2::getSygusInvVars(FunctionType t, - std::vector& vars, - std::vector& primed_vars) -{ - std::vector argTypes = t.getArgTypes(); - ExprManager* em = getExprManager(); - for (const Type& ti : argTypes) - { - vars.push_back(em->mkBoundVar(ti)); - d_sygusVars.push_back(vars.back()); - std::stringstream ss; - ss << vars.back() << "'"; - primed_vars.push_back(em->mkBoundVar(ss.str(), ti)); - d_sygusVars.push_back(primed_vars.back()); -#ifdef CVC4_ASSERTIONS - bool find_new_declared_var = false; - for (const Expr& e : d_sygusVarPrimed) - { - if (e.getType() == ti) - { - d_sygusVarPrimed.erase( - std::find(d_sygusVarPrimed.begin(), d_sygusVarPrimed.end(), e)); - find_new_declared_var = true; - break; - } - } - if (!find_new_declared_var) - { - ss.str(""); - ss << "warning: decleared primed variables do not match invariant's " - "type\n"; - warning(ss.str()); - } -#endif - } -} - -const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){ - // When constructing the synthesis conjecture, we quantify on the - // (higher-order) bound variable synth_fun. - d_sygusFunSymbols.push_back(synth_fun); - - // Variable "sfproxy" carries the type, which may be a SyGuS datatype - // that corresponds to syntactic restrictions. - Expr sym = mkBoundVar("sfproxy", t); - std::vector< Expr > attr_value; - attr_value.push_back(sym); - Command* cattr = - new SetUserAttributeCommand("sygus-synth-grammar", synth_fun, attr_value); - cattr->setMuted(true); - preemptCommand(cattr); -} - InputLanguage Smt2::getLanguage() const { ExprManager* em = getExprManager(); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 80bd8df83..2d57332af 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -273,35 +273,6 @@ private: std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ); - void addSygusConstraint(Expr constraint) { - d_sygusConstraints.push_back(constraint); - } - - Expr getSygusConstraints() { - switch(d_sygusConstraints.size()) { - case 0: return getExprManager()->mkConst(bool(true)); - case 1: return d_sygusConstraints[0]; - default: return getExprManager()->mkExpr(kind::AND, d_sygusConstraints); - } - } - - const std::vector& getSygusVars() { - return d_sygusVars; - } - /** retrieves the invariant variables (both regular and primed) - * - * To ensure that the variable list represent the correct argument type order - * the type of the invariant predicate is used during the variable retrieval - */ - const void getSygusInvVars(FunctionType t, - std::vector& vars, - std::vector& primed_vars); - - const void addSygusFunSymbol( Type t, Expr synth_fun ); - const std::vector& getSygusFunSymbols() { - return d_sygusFunSymbols; - } - /** * Smt2 parser provides its own checkDeclaration, which does the * same as the base, but with some more helpful errors. -- cgit v1.2.3