From 245b73861187696d86bb7a6a6fdb281de89c26e4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 8 Apr 2018 16:17:07 -0500 Subject: [PATCH] Allow predetermined first-order variables when constructing deep embedding. (#1757) --- .../quantifiers/sygus/sygus_grammar_cons.cpp | 79 ++++++++++++++----- .../quantifiers/sygus/sygus_grammar_cons.h | 14 +++- 2 files changed, 71 insertions(+), 22 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& templates, + const std::map& 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& 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::const_iterator itt = templates.find(sf); if( itt!=templates.end() ){ Node templ = itt->second; - TNode templ_arg = templates_arg[sf]; + std::map::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& templates, + const std::map& templates_arg, + const std::vector& ebvl) +{ + Assert(q[0].getNumChildren() == ebvl.size()); + + NodeManager* nm = NodeManager::currentNM(); + + std::vector qchildren; + Node qbody_subs = q[1]; + std::map 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::const_iterator itt = templates.find(sf); + if (itt != templates.end()) + { + Node templ = itt->second; + std::map::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] ){ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 16f4672b0..39f95527f 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -35,6 +35,7 @@ public: CegGrammarConstructor(QuantifiersEngine* qe, CegConjecture* p); ~CegGrammarConstructor() {} /** process + * * This converts node q based on its deep embedding * (Section 4 of Reynolds et al CAV 2015). * The syntactic restrictions are associated with @@ -48,8 +49,17 @@ public: * for some t if !templates[i].isNull(). */ Node process(Node q, - std::map& templates, - std::map& templates_arg); + const std::map& templates, + const std::map& templates_arg); + /** + * Same as above, but we have already determined that the set of first-order + * datatype variables that will quantify the deep embedding conjecture are + * the vector ebvl. + */ + Node process(Node q, + const std::map& templates, + const std::map& templates_arg, + const std::vector& ebvl); /** is the syntax restricted? */ bool isSyntaxRestricted() { return d_is_syntax_restricted; } /** does the syntax allow ITE expressions? */ -- 2.30.2