From bff00f51cd0d2f59262aa18ff3e217a78503ae7a Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Mon, 21 May 2018 12:21:33 -0500 Subject: [PATCH] Assign weight 1 for Boolean variables in SyGuS default grammars (#1948) --- .../quantifiers/sygus/sygus_grammar_cons.cpp | 48 ++++++++++++++++--- 1 file changed, 42 insertions(+), 6 deletions(-) diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 3d8052ae4..d745cb6da 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -270,7 +270,7 @@ Node CegGrammarConstructor::process(Node q, } return nm->mkNode(kind::FORALL, qchildren); } - + Node CegGrammarConstructor::convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars ){ std::unordered_map visited; std::unordered_map::iterator it; @@ -451,6 +451,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl; std::vector cnames; std::vector > cargs; + /* Print callbacks for each constructor */ + std::vector> pcs; + /* Weights for each constructor */ + std::vector weights; Type unres_t = unres_types[i]; //add variables for( unsigned j=0; j() ); + pcs.push_back(nullptr); + weights.push_back(-1); } } //add constants @@ -482,6 +488,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( ops[i].push_back( consts[j].toExpr() ); cnames.push_back( ss.str() ); cargs.push_back( std::vector< CVC4::Type >() ); + pcs.push_back(nullptr); + weights.push_back(-1); } //ITE CVC4::Kind k = kind::ITE; @@ -492,6 +500,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( cargs.back().push_back(unres_bt); cargs.back().push_back(unres_t); cargs.back().push_back(unres_t); + pcs.push_back(nullptr); + weights.push_back(-1); if (types[i].isReal()) { @@ -504,6 +514,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( cargs.push_back(std::vector()); cargs.back().push_back(unres_t); cargs.back().push_back(unres_t); + pcs.push_back(nullptr); + weights.push_back(-1); } if (!types[i].isInteger()) { @@ -551,6 +563,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( cargs.push_back(std::vector()); cargs.back().push_back(unres_t); cargs.back().push_back(unres_pos_int_t); + pcs.push_back(nullptr); + weights.push_back(-1); } }else if( types[i].isDatatype() ){ Trace("sygus-grammar-def") << "...add for constructors" << std::endl; @@ -565,6 +579,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( //Assert( type_to_unres.find(crange)!=type_to_unres.end() ); cargs.back().push_back( type_to_unres[crange] ); } + pcs.push_back(nullptr); + weights.push_back(-1); } }else{ std::stringstream sserr; @@ -584,6 +600,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( 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] ); + pcs.push_back(nullptr); + weights.push_back(-1); } } Trace("sygus-grammar-def") << "...make datatype " << datatypes[i] << std::endl; @@ -598,7 +616,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( || std::find(itexc->second.begin(), itexc->second.end(), opn) == itexc->second.end()) { - datatypes[i].addSygusConstructor(ops[i][j], cnames[j], cargs[j]); + datatypes[i].addSygusConstructor( + ops[i][j], cnames[j], cargs[j], pcs[j], weights[j]); } } Trace("sygus-grammar-def") @@ -616,6 +635,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( ops.push_back(std::vector()); std::vector cnames; std::vector > cargs; + /* Print callbacks for each constructor */ + std::vector> pcs; + /* Weights for each constructor */ + std::vector weights; Trace("sygus-grammar-def") << "Make grammar for " << btype << " " << datatypes.back() << std::endl; //add variables for( unsigned i=0; i() ); + pcs.push_back(nullptr); + weights.push_back(1); } } //add constants @@ -640,6 +665,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( ops.back().push_back(consts[j].toExpr()); cnames.push_back(ss.str()); cargs.push_back(std::vector()); + pcs.push_back(nullptr); + weights.push_back(-1); } //add operators for (unsigned i = 0; i < 4; i++) @@ -667,6 +694,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( cargs.back().push_back(unres_bt); } } + pcs.push_back(nullptr); + weights.push_back(-1); } //add predicates for types for( unsigned i=0; i() ); cargs.back().push_back(unres_types[i]); cargs.back().push_back(unres_types[i]); + pcs.push_back(nullptr); + weights.push_back(-1); //type specific predicates if (types[i].isReal()) { @@ -691,6 +722,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( cargs.push_back( std::vector< CVC4::Type >() ); cargs.back().push_back(unres_types[i]); cargs.back().push_back(unres_types[i]); + pcs.push_back(nullptr); + weights.push_back(-1); }else if( types[i].isDatatype() ){ //add for testers Trace("sygus-grammar-def") << "...add for testers" << std::endl; @@ -701,6 +734,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( cnames.push_back(dt[k].getTesterName()); cargs.push_back( std::vector< CVC4::Type >() ); cargs.back().push_back(unres_types[i]); + pcs.push_back(nullptr); + weights.push_back(-1); } } } @@ -710,11 +745,12 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Trace("sygus-grammar-def") << "...make datatype " << datatypes.back() << std::endl; datatypes.back().setSygus( btype.toType(), bvl.toExpr(), true, true ); for( unsigned j=0; j0 ){ CVC4::Datatype tmp_dt = datatypes[0]; datatypes[0] = datatypes[startIndex]; @@ -751,7 +787,7 @@ TypeNode CegGrammarConstructor::mkSygusDefaultType( return TypeNode::fromType( types[0] ); } -TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, +TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun, unsigned& tcount ) { if( templ==templ_arg ){ //Assert( templ_arg.getType()==sygusToBuiltinType( templ_arg_sygus_type ) ); @@ -791,7 +827,7 @@ TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_a } } -TypeNode CegGrammarConstructor::mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, +TypeNode CegGrammarConstructor::mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun ) { unsigned tcount = 0; return mkSygusTemplateTypeRec( templ, templ_arg, templ_arg_sygus_type, bvl, fun, tcount ); -- 2.30.2