Allow predetermined first-order variables when constructing deep embedding. (#1757)

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<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] ){
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<Node, Node>& templates,
-              std::map<Node, Node>& templates_arg);
+              const std::map<Node, Node>& templates,
+              const std::map<Node, Node>& 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<Node, Node>& templates,
+              const std::map<Node, Node>& templates_arg,
+              const std::vector<Node>& ebvl);
  /** is the syntax restricted? */
  bool isSyntaxRestricted() { return d_is_syntax_restricted; }
  /** does the syntax allow ITE expressions? */