diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 14:06:52 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 14:07:11 -0500 |
commit | f3590092818d9eab9d961ea602093029ff472a85 (patch) | |
tree | 1401f00df0d9659ba2321ea2088fe0c3f4de9f52 /src/parser | |
parent | d598a9644862d176632071bca8448765d9cc3cc1 (diff) |
Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 8 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 132 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 541 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 23 |
4 files changed, 119 insertions, 585 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 622fa9c00..c865332e2 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1616,7 +1616,7 @@ tupleStore[CVC4::Expr& f] const Datatype & dt = ((DatatypeType)t).getDatatype(); args.push_back( dt[0][k].getSelector() ); args.push_back( f ); - f2 = MK_EXPR(CVC4::kind::APPLY_SELECTOR_TOTAL,args); + f2 = MK_EXPR(CVC4::kind::APPLY_SELECTOR,args); } ( ( arrayStore[f2] | DOT ( tupleStore[f2] @@ -1651,7 +1651,7 @@ recordStore[CVC4::Expr& f] const Datatype & dt = ((DatatypeType)t).getDatatype(); args.push_back( dt[0][id].getSelector() ); args.push_back( f ); - f2 = MK_EXPR(CVC4::kind::APPLY_SELECTOR_TOTAL,args); + f2 = MK_EXPR(CVC4::kind::APPLY_SELECTOR,args); } ( ( arrayStore[f2] | DOT ( tupleStore[f2] @@ -1802,7 +1802,7 @@ postfixTerm[CVC4::Expr& f] std::vector<Expr> sargs; sargs.push_back( dt[0][id].getSelector() ); sargs.push_back( f ); - f = MK_EXPR(CVC4::kind::APPLY_SELECTOR_TOTAL,sargs); + f = MK_EXPR(CVC4::kind::APPLY_SELECTOR,sargs); } | k=numeral { Type t = f.getType(); @@ -1819,7 +1819,7 @@ postfixTerm[CVC4::Expr& f] std::vector<Expr> sargs; sargs.push_back( dt[0][k].getSelector() ); sargs.push_back( f ); - f = MK_EXPR(CVC4::kind::APPLY_SELECTOR_TOTAL,sargs); + f = MK_EXPR(CVC4::kind::APPLY_SELECTOR,sargs); } ) )* diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 8194e1933..5d24ec024 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -578,6 +578,7 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd] std::map< CVC4::Type, CVC4::Type > sygus_to_builtin; std::map< CVC4::Type, CVC4::Expr > sygus_to_builtin_expr; int startIndex = -1; + Expr synth_fun; } : /* declare-var */ DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -601,7 +602,25 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd] { PARSER_STATE->checkThatLogicIsSet(); } symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK - { seq.reset(new CommandSequence()); + ( sortSymbol[range,CHECK_DECLARED] )? { + if( range.isNull() ){ + PARSER_STATE->parseError("Must supply return type for synth-fun."); + } + 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 ); + } + 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; + } + synth_fun = PARSER_STATE->mkVar(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; @@ -616,11 +635,12 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd] } terms.clear(); terms.push_back(bvl); - } - ( sortSymbol[range,CHECK_DECLARED] )? { - if( range.isNull() ){ - PARSER_STATE->parseError("Must supply return type for synth-fun."); - } + // 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); } ( LPAREN_TOK ( LPAREN_TOK @@ -664,18 +684,11 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd] )+ RPAREN_TOK { read_syntax = true; } )? - { + { // the sygus sym type specifies the required grammar for synth_fun, expressed as a type + Type sygus_sym_type; if( !read_syntax ){ - //create the default grammar - Debug("parser-sygus") << "Make default grammar..." << std::endl; - PARSER_STATE->mkSygusDefaultGrammar( - range, terms[0], fun, datatypes, sorts, ops, sygus_vars, - startIndex); - //set start index - Debug("parser-sygus") << "Set start index " << startIndex << "..." - << std::endl; - PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts, - ops); + sygus_sym_type = range; + PARSER_STATE->popScope(); }else{ Debug("parser-sygus") << "--- Process " << sgts.size() << " sygus gterms..." << std::endl; @@ -708,57 +721,32 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd] datatypes[i], ops[i], cnames[i], cargs[i], unresolved_gterm_sym[i], sygus_to_builtin ); } - PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts, - ops); - } - //only care about datatypes/sorts/ops past here - PARSER_STATE->popScope(); - Debug("parser-sygus") << "--- Make " << datatypes.size() - << " mutual datatypes..." << std::endl; - for( unsigned i=0; i<datatypes.size(); i++ ){ - Debug("parser-sygus") << " " << i << " : " << datatypes[i].getName() - << std::endl; - } - std::vector<DatatypeType> datatypeTypes = - PARSER_STATE->mkMutualDatatypeTypes(datatypes); - seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes)); - std::map<DatatypeType, Expr> evals; - if( sorts[0]!=range ){ - PARSER_STATE->parseError(std::string("Bad return type in grammar for " - "SyGuS function ") + fun); - } - // make all the evals first, since they are mutually referential - for(size_t i = 0; i < datatypeTypes.size(); ++i) { - DatatypeType dtt = datatypeTypes[i]; - const Datatype& dt = dtt.getDatatype(); - Expr eval = dt.getSygusEvaluationFunc(); - Debug("parser-sygus") << "Make eval " << eval << " for " << dt.getName() - << std::endl; - evals.insert(std::make_pair(dtt, eval)); - if(i == 0) { - PARSER_STATE->addSygusFun(fun, eval); + PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts, ops); + //only care about datatypes/sorts/ops past here + PARSER_STATE->popScope(); + Debug("parser-sygus") << "--- Make " << datatypes.size() + << " mutual datatypes..." << std::endl; + for( unsigned i=0; i<datatypes.size(); i++ ){ + Debug("parser-sygus") << " " << i << " : " << datatypes[i].getName() << std::endl; } - } - // now go through and settle everything - for(size_t i = 0; i < datatypeTypes.size(); ++i) { - DatatypeType dtt = datatypeTypes[i]; - const Datatype& dt = dtt.getDatatype(); - Expr eval = evals[dtt]; - Debug("parser-sygus") << "Sygus : process grammar : " << dt - << std::endl; - for(size_t j = 0; j < dt.getNumConstructors(); ++j) { - Expr assertion = PARSER_STATE->getSygusAssertion( - datatypeTypes, ops, evals, terms, eval, dt, i, j ); - seq->addCommand(new AssertCommand(assertion)); + std::vector<DatatypeType> datatypeTypes = + PARSER_STATE->mkMutualDatatypeTypes(datatypes); + seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes)); + if( sorts[0]!=range ){ + PARSER_STATE->parseError(std::string("Bad return type in grammar for " + "SyGuS function ") + fun); } + sygus_sym_type = datatypeTypes[0]; } + + // store a dummy variable which stands for second-order quantification, linked to synth fun by an attribute + PARSER_STATE->addSygusFunSymbol( sygus_sym_type, synth_fun ); cmd->reset(seq.release()); } | /* constraint */ CONSTRAINT_TOK { PARSER_STATE->checkThatLogicIsSet(); Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl; - PARSER_STATE->defineSygusFuns(); Debug("parser-sygus") << "Sygus : read constraint..." << std::endl; } term[expr, expr2] @@ -769,7 +757,6 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd] | INV_CONSTRAINT_TOK { PARSER_STATE->checkThatLogicIsSet(); Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl; - PARSER_STATE->defineSygusFuns(); Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl; } ( symbol[name,CHECK_NONE,SYM_VARIABLE] { @@ -796,9 +783,8 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd] } //make relevant terms for( unsigned i=0; i<4; i++ ){ - Debug("parser-sygus") << "Make inv-constraint term #" << i << "..." - << std::endl; Expr op = terms[i]; + Debug("parser-sygus") << "Make inv-constraint term #" << i << " : " << op << "..." << std::endl; std::vector< Expr > children; children.push_back( op ); if( i==2 ){ @@ -806,13 +792,13 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd] }else{ children.insert( children.end(), primed[0].begin(), primed[0].end() ); } - terms[i] = EXPR_MANAGER->mkExpr(kind::APPLY,children); + terms[i] = EXPR_MANAGER->mkExpr( i==0 ? kind::APPLY_UF : kind::APPLY,children); if( i==0 ){ std::vector< Expr > children2; children2.push_back( op ); children2.insert(children2.end(), primed[1].begin(), primed[1].end()); - terms.push_back( EXPR_MANAGER->mkExpr(kind::APPLY,children2) ); + terms.push_back( EXPR_MANAGER->mkExpr(kind::APPLY_UF,children2) ); } } //make constraints @@ -832,7 +818,7 @@ sygusCommand [CVC4::PtrCloser<CVC4::Command>* cmd] } | /* check-synth */ CHECK_SYNTH_TOK - { PARSER_STATE->checkThatLogicIsSet(); PARSER_STATE->defineSygusFuns(); } + { 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); @@ -900,6 +886,12 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] k = CVC4::kind::BITVECTOR_UDIV_TOTAL; }else if( k==CVC4::kind::BITVECTOR_UREM ){ k = CVC4::kind::BITVECTOR_UREM_TOTAL; + }else if( k==CVC4::kind::DIVISION ){ + k = CVC4::kind::DIVISION_TOTAL; + }else if( k==CVC4::kind::INTS_DIVISION ){ + k = CVC4::kind::INTS_DIVISION_TOTAL; + }else if( k==CVC4::kind::INTS_MODULUS ){ + k = CVC4::kind::INTS_MODULUS_TOTAL; } sgt.d_name = kind::kindToString(k); sgt.d_gterm_type = SygusGTerm::gterm_op; @@ -952,6 +944,12 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] k = CVC4::kind::BITVECTOR_UDIV_TOTAL; }else if( k==CVC4::kind::BITVECTOR_UREM ){ k = CVC4::kind::BITVECTOR_UREM_TOTAL; + }else if( k==CVC4::kind::DIVISION ){ + k = CVC4::kind::DIVISION_TOTAL; + }else if( k==CVC4::kind::INTS_DIVISION ){ + k = CVC4::kind::INTS_DIVISION_TOTAL; + }else if( k==CVC4::kind::INTS_MODULUS ){ + k = CVC4::kind::INTS_MODULUS_TOTAL; } sgt.d_name = kind::kindToString(k); sgt.d_gterm_type = SygusGTerm::gterm_op; @@ -2084,6 +2082,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] if( args.size()!=dtc.getNumArgs() ){ PARSER_STATE->parseError("Bad number of arguments for application of constructor in pattern."); } + //FIXME: make MATCH a kind and make this a rewrite // build a lambda std::vector<Expr> largs; largs.push_back( MK_EXPR( CVC4::kind::BOUND_VAR_LIST, args ) ); @@ -2092,7 +2091,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] aargs.push_back( MK_EXPR( CVC4::kind::LAMBDA, largs ) ); for( unsigned i=0; i<dtc.getNumArgs(); i++ ){ //can apply total version since we will be guarded by ITE condition - aargs.push_back( MK_EXPR( CVC4::kind::APPLY_SELECTOR_TOTAL, dtc[i].getSelector(), expr ) ); + // however, we need to apply partial version since we don't have the internal selector available + aargs.push_back( MK_EXPR( CVC4::kind::APPLY_SELECTOR, dtc[i].getSelector(), expr ) ); } patexprs.push_back( MK_EXPR( CVC4::kind::APPLY, aargs ) ); patconds.push_back( MK_EXPR( CVC4::kind::APPLY_TESTER, dtc.getTester(), expr ) ); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 7fa71890e..fe5eb3ac8 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -33,8 +33,7 @@ namespace parser { Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : Parser(exprManager,input,strictMode,parseOnly), - d_logicSet(false), - d_nextSygusFun(0) { + d_logicSet(false) { d_unsatCoreNames.push(std::map<Expr, std::string>()); if( !strictModeEnabled() ) { addTheory(Smt2::THEORY_CORE); @@ -541,246 +540,6 @@ Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed) return e; } -void collectSygusGrammarTypesFor( Type range, std::vector< Type >& types, std::map< Type, std::vector< DatatypeConstructorArg > >& sels ){ - if( !range.isBoolean() ){ - if( std::find( types.begin(), types.end(), range )==types.end() ){ - Debug("parser-sygus") << "...will make grammar for " << range << std::endl; - types.push_back( range ); - if( range.isDatatype() ){ - const Datatype& dt = ((DatatypeType)range).getDatatype(); - for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ - for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ - Type crange = ((SelectorType)dt[i][j].getType()).getRangeType(); - sels[crange].push_back( dt[i][j] ); - collectSygusGrammarTypesFor( crange, types, sels ); - } - } - } - } - } -} - -void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes, - std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex ) { - - //if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){ - // parseError("No default grammar for type."); - //} - startIndex = -1; - Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl; - std::map< CVC4::Type, CVC4::Type > sygus_to_builtin; - - std::vector< Type > types; - std::map< Type, std::vector< DatatypeConstructorArg > > sels; - //types for each of the variables - for( unsigned i=0; i<sygus_vars.size(); i++ ){ - collectSygusGrammarTypesFor( sygus_vars[i].getType(), types, sels ); - } - //types connected to range - collectSygusGrammarTypesFor( range, types, sels ); - - //name of boolean sort - std::stringstream ssb; - ssb << fun << "_Bool"; - std::string dbname = ssb.str(); - Type unres_bt = mkUnresolvedType(ssb.str()); - - std::vector< Type > unres_types; - std::map< Type, Type > type_to_unres; - for( unsigned i=0; i<types.size(); i++ ){ - std::stringstream ss; - ss << fun << "_" << types[i]; - std::string dname = ss.str(); - datatypes.push_back(Datatype(dname)); - ops.push_back(std::vector<Expr>()); - //make unresolved type - Type unres_t = mkUnresolvedType(dname); - unres_types.push_back(unres_t); - type_to_unres[types[i]] = unres_t; - sygus_to_builtin[unres_t] = types[i]; - } - for( unsigned i=0; i<types.size(); i++ ){ - Debug("parser-sygus") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl; - std::vector<std::string> cnames; - std::vector<std::vector<CVC4::Type> > cargs; - std::vector<std::string> unresolved_gterm_sym; - Type unres_t = unres_types[i]; - //add variables - for( unsigned j=0; j<sygus_vars.size(); j++ ){ - if( sygus_vars[j].getType()==types[i] ){ - std::stringstream ss; - ss << sygus_vars[j]; - Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl; - ops[i].push_back( sygus_vars[j] ); - cnames.push_back( ss.str() ); - cargs.push_back( std::vector< CVC4::Type >() ); - } - } - //add constants - std::vector< Expr > consts; - mkSygusConstantsForType( types[i], consts ); - for( unsigned j=0; j<consts.size(); j++ ){ - std::stringstream ss; - ss << consts[j]; - Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl; - ops[i].push_back( consts[j] ); - cnames.push_back( ss.str() ); - cargs.push_back( std::vector< CVC4::Type >() ); - } - //ITE - CVC4::Kind k = kind::ITE; - Debug("parser-sygus") << "...add for " << k << std::endl; - ops[i].push_back(getExprManager()->operatorOf(k)); - cnames.push_back( kind::kindToString(k) ); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_bt); - cargs.back().push_back(unres_t); - cargs.back().push_back(unres_t); - - if( types[i].isInteger() ){ - for( unsigned j=0; j<2; j++ ){ - CVC4::Kind k = j==0 ? kind::PLUS : kind::MINUS; - Debug("parser-sygus") << "...add for " << k << std::endl; - ops[i].push_back(getExprManager()->operatorOf(k)); - cnames.push_back(kind::kindToString(k)); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_t); - cargs.back().push_back(unres_t); - } - }else if( types[i].isDatatype() ){ - Debug("parser-sygus") << "...add for constructors" << std::endl; - const Datatype& dt = ((DatatypeType)types[i]).getDatatype(); - for( unsigned k=0; k<dt.getNumConstructors(); k++ ){ - Debug("parser-sygus") << "...for " << dt[k].getName() << std::endl; - ops[i].push_back( dt[k].getConstructor() ); - cnames.push_back( dt[k].getName() ); - cargs.push_back( std::vector< CVC4::Type >() ); - for( unsigned j=0; j<dt[k].getNumArgs(); j++ ){ - Type crange = ((SelectorType)dt[k][j].getType()).getRangeType(); - //Assert( type_to_unres.find(crange)!=type_to_unres.end() ); - cargs.back().push_back( type_to_unres[crange] ); - } - } - }else{ - std::stringstream sserr; - sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl; - warning(sserr.str()); - } - //add for all selectors to this type - if( !sels[types[i]].empty() ){ - Debug("parser-sygus") << "...add for selectors" << std::endl; - for( unsigned j=0; j<sels[types[i]].size(); j++ ){ - Debug("parser-sygus") << "...for " << sels[types[i]][j].getName() << std::endl; - Type arg_type = ((SelectorType)sels[types[i]][j].getType()).getDomain(); - ops[i].push_back( sels[types[i]][j].getSelector() ); - cnames.push_back( sels[types[i]][j].getName() ); - cargs.push_back( std::vector< CVC4::Type >() ); - //Assert( type_to_unres.find(arg_type)!=type_to_unres.end() ); - cargs.back().push_back( type_to_unres[arg_type] ); - } - } - Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl; - datatypes[i].setSygus( types[i], bvl, true, true ); - mkSygusDatatype( datatypes[i], ops[i], cnames, cargs, unresolved_gterm_sym, sygus_to_builtin ); - sorts.push_back( types[i] ); - //set start index if applicable - if( types[i]==range ){ - startIndex = i; - } - } - - //make Boolean type - Type btype = getExprManager()->booleanType(); - datatypes.push_back(Datatype(dbname)); - ops.push_back(std::vector<Expr>()); - std::vector<std::string> cnames; - std::vector<std::vector<CVC4::Type> > cargs; - std::vector<std::string> unresolved_gterm_sym; - Debug("parser-sygus") << "Make grammar for " << btype << " " << datatypes.back() << std::endl; - //add variables - for( unsigned i=0; i<sygus_vars.size(); i++ ){ - if( sygus_vars[i].getType().isBoolean() ){ - std::stringstream ss; - ss << sygus_vars[i]; - Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl; - ops.back().push_back( sygus_vars[i] ); - cnames.push_back( ss.str() ); - cargs.push_back( std::vector< CVC4::Type >() ); - } - } - //add constants if no variables and no connected types - if( ops.back().empty() && types.empty() ){ - std::vector< Expr > consts; - mkSygusConstantsForType( btype, consts ); - for( unsigned j=0; j<consts.size(); j++ ){ - std::stringstream ss; - ss << consts[j]; - Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl; - ops.back().push_back( consts[j] ); - cnames.push_back( ss.str() ); - cargs.push_back( std::vector< CVC4::Type >() ); - } - } - //add operators - for( unsigned i=0; i<3; i++ ){ - CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : kind::OR ); - Debug("parser-sygus") << "...add for " << k << std::endl; - ops.back().push_back(getExprManager()->operatorOf(k)); - cnames.push_back(kind::kindToString(k)); - cargs.push_back( std::vector< CVC4::Type >() ); - if( k==kind::NOT ){ - cargs.back().push_back(unres_bt); - }else if( k==kind::AND || k==kind::OR ){ - cargs.back().push_back(unres_bt); - cargs.back().push_back(unres_bt); - } - } - //add predicates for types - for( unsigned i=0; i<types.size(); i++ ){ - Debug("parser-sygus") << "...add predicates for " << types[i] << std::endl; - //add equality per type - CVC4::Kind k = kind::EQUAL; - Debug("parser-sygus") << "...add for " << k << std::endl; - ops.back().push_back(getExprManager()->operatorOf(k)); - std::stringstream ss; - ss << kind::kindToString(k) << "_" << types[i]; - cnames.push_back(ss.str()); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_types[i]); - cargs.back().push_back(unres_types[i]); - //type specific predicates - if( types[i].isInteger() ){ - CVC4::Kind k = kind::LEQ; - Debug("parser-sygus") << "...add for " << k << std::endl; - ops.back().push_back(getExprManager()->operatorOf(k)); - cnames.push_back(kind::kindToString(k)); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_types[i]); - cargs.back().push_back(unres_types[i]); - }else if( types[i].isDatatype() ){ - //add for testers - Debug("parser-sygus") << "...add for testers" << std::endl; - const Datatype& dt = ((DatatypeType)types[i]).getDatatype(); - for( unsigned k=0; k<dt.getNumConstructors(); k++ ){ - Debug("parser-sygus") << "...for " << dt[k].getTesterName() << std::endl; - ops.back().push_back(dt[k].getTester()); - cnames.push_back(dt[k].getTesterName()); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_types[i]); - } - } - } - if( range==btype ){ - startIndex = sorts.size(); - } - Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl; - datatypes.back().setSygus( btype, bvl, true, true ); - mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs, unresolved_gterm_sym, sygus_to_builtin ); - sorts.push_back( btype ); - - Debug("parser-sygus") << "...finished make default grammar for " << fun << " " << range << std::endl; -} - void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) { if( type.isInteger() ){ ops.push_back(getExprManager()->mkConst(Rational(0))); @@ -1152,77 +911,22 @@ void Smt2::setSygusStartIndex( std::string& fun, int startIndex, } } -void Smt2::defineSygusFuns() { - // only define each one once - while(d_nextSygusFun < d_sygusFuns.size()) { - std::pair<std::string, Expr> p = d_sygusFuns[d_nextSygusFun]; - std::string fun = p.first; - Debug("parser-sygus") << "Sygus : define fun " << fun << std::endl; - Expr eval = p.second; - FunctionType evalType = eval.getType(); - std::vector<Type> argTypes = evalType.getArgTypes(); - Type rangeType = evalType.getRangeType(); - Debug("parser-sygus") << "...eval type : " << evalType << ", #args=" << argTypes.size() << std::endl; - - // first make the function type - std::vector<Expr> sygusVars; - std::vector<Type> funType; - for(size_t j = 1; j < argTypes.size(); ++j) { - funType.push_back(argTypes[j]); - std::stringstream ss; - ss << fun << "_v_" << j; - sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), argTypes[j])); - } - Type funt; - if( !funType.empty() ){ - funt = getExprManager()->mkFunctionType(funType, rangeType); - Debug("parser-sygus") << "...eval function type : " << funt << std::endl; - - // copy the bound vars - /* - std::vector<Expr> sygusVars; - //std::vector<Type> types; - for(size_t i = 0; i < d_sygusVars.size(); ++i) { - std::stringstream ss; - ss << d_sygusVars[i]; - Type type = d_sygusVars[i].getType(); - sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type)); - //types.push_back(type); - } - Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl; - */ - - //Type t = getExprManager()->mkFunctionType(types, rangeType); - //Debug("parser-sygus") << "...function type : " << t << std::endl; - }else{ - funt = rangeType; - } - Expr lambda = mkFunction(fun, funt, ExprManager::VAR_FLAG_DEFINED); - Debug("parser-sygus") << "...made function : " << lambda << std::endl; - std::vector<Expr> applyv; - Expr funbv = getExprManager()->mkBoundVar(std::string("f") + fun, argTypes[0]); - d_sygusFunSymbols.push_back(funbv); - applyv.push_back(eval); - applyv.push_back(funbv); - for(size_t i = 0; i < sygusVars.size(); ++i) { - applyv.push_back(sygusVars[i]); - } - Expr apply = getExprManager()->mkExpr(kind::APPLY_UF, applyv); - Debug("parser-sygus") << "...made apply " << apply << std::endl; - Debug("parser-sygus") << "--> Define " << fun << " as " << lambda << " " << apply << std::endl; - Command* cmd = new DefineFunctionCommand(fun, lambda, sygusVars, apply); - preemptCommand(cmd); - - ++d_nextSygusFun; - } -} - void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs, std::vector<std::string>& unresolved_gterm_sym, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ) { Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl; Debug("parser-sygus") << " add constructors..." << std::endl; + std::vector<std::string> df_name; + std::vector<CVC4::Expr> df_op; + std::vector< std::vector<Expr> > df_let_args; + std::vector< Expr > df_let_body; + //dt.mkSygusConstructors( ops, cnames, cargs, sygus_to_builtin, + // d_sygus_let_func_to_vars, d_sygus_let_func_to_body, d_sygus_let_func_to_num_input_vars, + // df_name, df_op, df_let_args, df_let_body ); + + Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl; + Debug("parser-sygus") << " add constructors..." << std::endl; for( int i=0; i<(int)cnames.size(); i++ ){ bool is_dup = false; bool is_dup_op = false; @@ -1283,9 +987,15 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, //replace operator and name ops[i] = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); cnames[i] = ss.str(); - d_sygus_defined_funs.push_back( ops[i] ); - preemptCommand( new DefineFunctionCommand(ss.str(), ops[i], let_args, let_body) ); - addSygusDatatypeConstructor( dt, ops[i], cnames[i], cargs[i], let_body, let_args, 0 ); + // indicate we need a define function + df_name.push_back( ss.str() ); + df_op.push_back( ops[i] ); + df_let_args.push_back( let_args ); + df_let_body.push_back( let_body ); + + //d_sygus_defined_funs.push_back( ops[i] ); + //preemptCommand( new DefineFunctionCommand(ss.str(), ops[i], let_args, let_body) ); + dt.addSygusConstructor( ops[i], cnames[i], cargs[i], let_body, let_args, 0 ); }else{ std::map< CVC4::Expr, CVC4::Expr >::iterator it = d_sygus_let_func_to_body.find( ops[i] ); if( it!=d_sygus_let_func_to_body.end() ){ @@ -1293,9 +1003,10 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, let_args.insert( let_args.end(), d_sygus_let_func_to_vars[ops[i]].begin(), d_sygus_let_func_to_vars[ops[i]].end() ); let_num_input_args = d_sygus_let_func_to_num_input_vars[ops[i]]; } - addSygusDatatypeConstructor( dt, ops[i], cnames[i], cargs[i], let_body, let_args, let_num_input_args ); + dt.addSygusConstructor( ops[i], cnames[i], cargs[i], let_body, let_args, let_num_input_args ); } } + Debug("parser-sygus") << " add constructors for unresolved symbols..." << std::endl; if( !unresolved_gterm_sym.empty() ){ std::vector< Type > types; @@ -1320,12 +1031,18 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, std::stringstream ssid; ssid << unresolved_gterm_sym[i] << "_id"; Expr id_op = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED); - d_sygus_defined_funs.push_back( id_op ); - preemptCommand( new DefineFunctionCommand(ssid.str(), id_op, let_args, let_body) ); + // indicate we need a define function + df_name.push_back( ssid.str() ); + df_op.push_back( id_op ); + df_let_args.push_back( let_args ); + df_let_body.push_back( let_body ); + + //d_sygus_defined_funs.push_back( id_op ); + //preemptCommand( new DefineFunctionCommand(ssid.str(), id_op, let_args, let_body) ); //make the sygus argument list std::vector< Type > id_carg; id_carg.push_back( t ); - addSygusDatatypeConstructor( dt, id_op, unresolved_gterm_sym[i], id_carg, let_body, let_args, 0 ); + dt.addSygusConstructor( id_op, unresolved_gterm_sym[i], id_carg, let_body, let_args, 0 ); //add to operators ops.push_back( id_op ); } @@ -1334,187 +1051,12 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, } } } - -} - -void Smt2::addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs, - CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ) { - Debug("parser-sygus") << "--> Add constructor " << cname << " to " << dt.getName() << std::endl; - if( !let_body.isNull() ){ - Debug("parser-sygus") << " let body = " << let_body << ", args = " << let_args.size() << "," << let_num_input_args << std::endl; - //TODO : remove arguments not occurring in body - //if this is a self identity function, ignore - if( let_args.size()==0 && let_args[0]==let_body ){ - Debug("parser-sygus") << " identity function " << cargs[0] << " to " << dt.getName() << std::endl; - //TODO - } - } - std::string name = dt.getName() + "_" + cname; - std::string testerId("is-"); - testerId.append(name); - checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); - checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); - CVC4::DatatypeConstructor c(name, testerId ); - c.setSygus( op, let_body, let_args, let_num_input_args ); - for( unsigned j=0; j<cargs.size(); j++ ){ - Debug("parser-sygus-debug") << " arg " << j << " : " << cargs[j] << std::endl; - std::stringstream sname; - sname << name << "_" << j; - c.addArg(sname.str(), cargs[j]); - } - dt.addConstructor(c); -} - - -// i is index in datatypes/ops -// j is index is datatype -Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops, - std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms, - Expr eval, const Datatype& dt, size_t i, size_t j ) { - const DatatypeConstructor& ctor = dt[j]; - Debug("parser-sygus") << "Sygus : process constructor " << j << " : " << dt[j] << std::endl; - std::vector<Expr> bvs, extraArgs; - for(size_t k = 0; k < ctor.getNumArgs(); ++k) { - std::string vname = "v_" + ctor[k].getName(); - Expr bv = getExprManager()->mkBoundVar(vname, SelectorType(ctor[k].getType()).getRangeType()); - bvs.push_back(bv); - extraArgs.push_back(bv); - } - if( !terms[0].isNull() ){ - bvs.insert(bvs.end(), terms[0].begin(), terms[0].end()); - } - Expr bvl; - if( !bvs.empty() ){ - bvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, bvs); - } - Debug("parser-sygus") << "...made bv list " << bvl << std::endl; - std::vector<Expr> patv; - patv.push_back(eval); - std::vector<Expr> applyv; - applyv.push_back(ctor.getConstructor()); - applyv.insert(applyv.end(), extraArgs.begin(), extraArgs.end()); - for(size_t k = 0; k < applyv.size(); ++k) { - } - Expr cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv); - Debug("parser-sygus") << "...made eval ctor apply " << cpatv << std::endl; - patv.push_back(cpatv); - if( !terms[0].isNull() ){ - patv.insert(patv.end(), terms[0].begin(), terms[0].end()); - } - Expr evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv); - Debug("parser-sygus") << "...made eval apply " << evalApply << std::endl; - std::vector<Expr> builtApply; - for(size_t k = 0; k < extraArgs.size(); ++k) { - std::vector<Expr> patvb; - patvb.push_back(evals[DatatypeType(extraArgs[k].getType())]); - patvb.push_back(extraArgs[k]); - if( !terms[0].isNull() ){ - patvb.insert(patvb.end(), terms[0].begin(), terms[0].end()); - } - Debug("parser-sygus-debug") << "...add to built apply " << evals[DatatypeType(extraArgs[k].getType())] << " " << extraArgs[k] << " " << extraArgs[k].getType() << std::endl; - builtApply.push_back(getExprManager()->mkExpr(kind::APPLY_UF, patvb)); - Debug("parser-sygus-debug") << "...added " << builtApply.back() << std::endl; - } - for(size_t k = 0; k < builtApply.size(); ++k) { - } - Expr builtTerm; - Debug("parser-sygus") << "...operator is : " << ops[i][j] << ", type = " << ops[i][j].getType() << ", kind = " << ops[i][j].getKind() << ", is defined = " << isDefinedFunction( ops[i][j] ) << std::endl; - if( ops[i][j].getKind() != kind::BUILTIN ){ - Kind ok = kind::UNDEFINED_KIND; - if( isDefinedFunction( ops[i][j] ) || std::find( d_sygus_defined_funs.begin(), d_sygus_defined_funs.end(), ops[i][j] )!=d_sygus_defined_funs.end() ){ - ok = kind::APPLY; - }else{ - Type t = ops[i][j].getType(); - if( t.isConstructor() ){ - ok = kind::APPLY_CONSTRUCTOR; - }else if( t.isSelector() ){ - ok = kind::APPLY_SELECTOR; - }else if( t.isTester() ){ - ok = kind::APPLY_TESTER; - }else{ - ok = getExprManager()->operatorToKind( ops[i][j] ); - } - } - Debug("parser-sygus") << "...processed operator kind : " << ok << std::endl; - if( ok!=kind::UNDEFINED_KIND ){ - builtTerm = getExprManager()->mkExpr(ok, ops[i][j], builtApply); - }else{ - builtTerm = ops[i][j]; - } - }else{ - if( !builtApply.empty() ){ - builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply); - }else{ - builtTerm = ops[i][j]; - } - } - Debug("parser-sygus") << "...made built term " << builtTerm << std::endl; - Expr assertion = getExprManager()->mkExpr(kind::EQUAL, evalApply, builtTerm); - if( !bvl.isNull() ){ - Expr pattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply); - pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern); - assertion = getExprManager()->mkExpr(kind::FORALL, bvl, assertion, pattern); - } - Debug("parser-sygus") << "...made assertion " << assertion << std::endl; - - //linearize multiplication if possible - if( builtTerm.getKind()==kind::MULT ){ - for(size_t k = 0; k < ctor.getNumArgs(); ++k) { - Type at = SelectorType(ctor[k].getType()).getRangeType(); - if( at.isDatatype() ){ - DatatypeType atd = (DatatypeType)SelectorType(ctor[k].getType()).getRangeType(); - Debug("parser-sygus") << "Argument " << k << " " << atd << std::endl; - std::vector<DatatypeType>::iterator itd = std::find( datatypeTypes.begin(), datatypeTypes.end(), atd ); - if( itd!=datatypeTypes.end() ){ - Debug("parser-sygus2") << "Exists in datatypeTypes." << std::endl; - unsigned index = itd-datatypeTypes.begin(); - Debug("parser-sygus2") << "index = " << index << std::endl; - bool isConst = true; - for( unsigned cc = 0; cc < ops[index].size(); cc++ ){ - Debug("parser-sygus2") << "ops[" << cc << "]=" << ops[index][cc] << std::endl; - if( ops[index][cc].getKind() != kind::CONST_RATIONAL ){ - isConst = false; - break; - } - } - if( isConst ){ - Debug("parser-sygus") << "Linearize multiplication " << ctor << " based on argument " << k << std::endl; - const Datatype & atdd = atd.getDatatype(); - std::vector<Expr> assertions; - std::vector<Expr> nbvs; - for( unsigned a=0; a<bvl.getNumChildren(); a++ ){ - if( a!=k ){ - nbvs.push_back( bvl[a] ); - } - } - Expr nbvl = getExprManager()->mkExpr( kind::BOUND_VAR_LIST, nbvs ); - for( unsigned cc = 0; cc < ops[index].size(); cc++ ){ - //Make new assertion based on partially instantiating existing - applyv[k+1] = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, atdd[cc].getConstructor()); - Debug("parser-sygus") << "applyv " << applyv[k+1] << std::endl; - cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv); - Debug("parser-sygus") << "cpatv " << cpatv << std::endl; - patv[1] = cpatv; - evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv); - Debug("parser-sygus") << "evalApply " << evalApply << std::endl; - builtApply[k] = ops[index][cc]; - Debug("parser-sygus") << "builtApply " << builtApply[k] << std::endl; - builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply); - Debug("parser-sygus") << "builtTerm " << builtTerm << std::endl; - Expr eassertion = getExprManager()->mkExpr(kind::EQUAL, evalApply, builtTerm); - Expr epattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply); - epattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, epattern); - eassertion = getExprManager()->mkExpr(kind::FORALL, nbvl, eassertion, epattern); - assertions.push_back( eassertion ); - } - assertion = assertions.size()==1 ? assertions[0] : getExprManager()->mkExpr( kind::AND, assertions ); - Debug("parser-sygus") << "...(linearized) assertion is: " << assertion << std::endl; - } - } - } - } + + + for( unsigned i=0; i<df_name.size(); i++ ){ + d_sygus_defined_funs.push_back( df_op[i] ); + preemptCommand( new DefineFunctionCommand(df_name[i], df_op[i], df_let_args[i], df_let_body[i]) ); } - return assertion; } const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) { @@ -1531,5 +1073,16 @@ const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) { } } +const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){ + Expr sym = mkBoundVar("sfproxy", t); + d_sygusFunSymbols.push_back(sym); + + std::vector< Expr > attr_value; + attr_value.push_back( synth_fun ); + Command* cattr = new SetUserAttributeCommand("sygus-synth-fun", sym, attr_value); + cattr->setMuted(true); + preemptCommand(cattr); +} + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 8222ac3a3..3eed0e871 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -62,10 +62,9 @@ private: std::pair<Expr, std::string> d_lastNamedTerm; // this is a user-context stack std::stack< std::map<Expr, std::string> > d_unsatCoreNames; + // for sygus std::vector<Expr> d_sygusVars, d_sygusConstraints, d_sygusFunSymbols; - std::vector< std::pair<std::string, Expr> > d_sygusFuns; std::map< Expr, bool > d_sygusVarPrimed; - size_t d_nextSygusFun; protected: Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); @@ -179,9 +178,6 @@ public: Expr mkSygusVar(const std::string& name, const Type& type, bool isPrimed = false); - void mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes, - std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars, int& startIndex ); - void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ); void processSygusGTerm( CVC4::SygusGTerm& sgt, int index, @@ -218,24 +214,11 @@ public: std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops ); - void addSygusFun(const std::string& fun, Expr eval) { - d_sygusFuns.push_back(std::make_pair(fun, eval)); - } - - void defineSygusFuns(); - void mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops, std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs, std::vector<std::string>& unresolved_gterm_sym, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin ); - // i is index in datatypes/ops - // j is index is datatype - Expr getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vector< std::vector<Expr> >& ops, - std::map<DatatypeType, Expr>& evals, std::vector<Expr>& terms, - Expr eval, const Datatype& dt, size_t i, size_t j ); - - void addSygusConstraint(Expr constraint) { d_sygusConstraints.push_back(constraint); @@ -254,6 +237,7 @@ public: } const void getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ); + const void addSygusFunSymbol( Type t, Expr synth_fun ); const std::vector<Expr>& getSygusFunSymbols() { return d_sygusFunSymbols; } @@ -327,9 +311,6 @@ private: void collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs ); - void addSygusDatatypeConstructor( CVC4::Datatype& dt, CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs, - CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ); - Type processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, std::vector< CVC4::Datatype >& datatypes, std::vector< CVC4::Type>& sorts, std::vector< std::vector<CVC4::Expr> >& ops, |