diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_grammar_cons.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 79 |
1 files changed, 59 insertions, 20 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 322d49af6..b6a780b6c 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -87,9 +87,10 @@ void CegGrammarConstructor::collectTerms( Node n, std::map< TypeNode, std::vecto } while (!visit.empty()); } - - -Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, std::map< Node, Node >& templates_arg ) { +Node CegGrammarConstructor::process(Node q, + const std::map<Node, Node>& templates, + const std::map<Node, Node>& templates_arg) +{ // convert to deep embedding and finalize single invocation here // now, construct the grammar Trace("cegqi") << "CegConjecture : convert to deep embedding..." << std::endl; @@ -101,10 +102,7 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, NodeManager* nm = NodeManager::currentNM(); - std::vector< Node > qchildren; - std::map< Node, Node > synth_fun_vars; std::vector< Node > ebvl; - Node qbody_subs = q[1]; for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ Node sf = q[0][i]; // if non-null, v encodes the syntactic restrictions (via an inductive @@ -161,19 +159,68 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, // normalize type SygusGrammarNorm sygus_norm(d_qe); tn = sygus_norm.normalizeSygusType(tn, sfvl); - // check if there is a template - std::map< Node, Node >::iterator itt = templates.find( sf ); + + std::map<Node, Node>::const_iterator itt = templates.find(sf); if( itt!=templates.end() ){ Node templ = itt->second; - TNode templ_arg = templates_arg[sf]; + std::map<Node, Node>::const_iterator itta = templates_arg.find(sf); + Assert(itta != templates_arg.end()); + TNode templ_arg = itta->second; Assert( !templ_arg.isNull() ); - Trace("cegqi-debug") << "Template for " << sf << " is : " << templ << " with arg " << templ_arg << std::endl; // if there is a template for this argument, make a sygus type on top of it if( options::sygusTemplEmbedGrammar() ){ + Trace("cegqi-debug") << "Template for " << sf << " is : " << templ + << " with arg " << templ_arg << std::endl; Trace("cegqi-debug") << " embed this template as a grammar..." << std::endl; tn = mkSygusTemplateType( templ, templ_arg, tn, sfvl, ss.str() ); - }else{ - // otherwise, apply it as a preprocessing pass + } + } + + // ev is the first-order variable corresponding to this synth fun + std::stringstream ssf; + ssf << "f" << sf; + Node ev = nm->mkBoundVar(ssf.str(), tn); + ebvl.push_back(ev); + Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev + << std::endl; + } + return process(q, templates, templates_arg, ebvl); +} + +Node CegGrammarConstructor::process(Node q, + const std::map<Node, Node>& templates, + const std::map<Node, Node>& templates_arg, + const std::vector<Node>& ebvl) +{ + Assert(q[0].getNumChildren() == ebvl.size()); + + NodeManager* nm = NodeManager::currentNM(); + + std::vector<Node> qchildren; + Node qbody_subs = q[1]; + std::map<Node, Node> synth_fun_vars; + for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++) + { + Node sf = q[0][i]; + synth_fun_vars[sf] = ebvl[i]; + Node sfvl = getSygusVarList(sf); + TypeNode tn = ebvl[i].getType(); + // check if there is a template + std::map<Node, Node>::const_iterator itt = templates.find(sf); + if (itt != templates.end()) + { + Node templ = itt->second; + std::map<Node, Node>::const_iterator itta = templates_arg.find(sf); + Assert(itta != templates_arg.end()); + TNode templ_arg = itta->second; + Assert(!templ_arg.isNull()); + // if there is a template for this argument, make a sygus type on top of + // it + if (!options::sygusTemplEmbedGrammar()) + { + // otherwise, apply it as a preprocessing pass + Trace("cegqi-debug") << "Template for " << sf << " is : " << templ + << " with arg " << templ_arg << std::endl; Trace("cegqi-debug") << " apply this template as a substituion during preprocess..." << std::endl; std::vector< Node > schildren; std::vector< Node > largs; @@ -212,14 +259,6 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, if( !dt.getSygusAllowAll() ){ d_is_syntax_restricted = true; } - - // ev is the first-order variable corresponding to this synth fun - std::stringstream ssf; - ssf << "f" << sf; - Node ev = nm->mkBoundVar(ssf.str(), tn); - ebvl.push_back( ev ); - synth_fun_vars[sf] = ev; - Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev << std::endl; } qchildren.push_back(nm->mkNode(kind::BOUND_VAR_LIST, ebvl)); if( qbody_subs!=q[1] ){ |