From 8d3ea75e7895bbb169a2b7bd02c8fe3b626bdb5e Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 28 Nov 2018 17:57:18 -0600
Subject: [PATCH] Improve interface for sygus grammar cons (#2727)

---
 .../quantifiers/sygus/sygus_grammar_cons.cpp  | 20 ++++++++++---------
 .../quantifiers/sygus/sygus_grammar_cons.h    | 17 ++++++++++++++--
 2 files changed, 26 insertions(+), 11 deletions(-)

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index b0471147d..67fa1398e 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -194,17 +194,17 @@ Node CegGrammarConstructor::process(Node q,
                                     const std::vector<Node>& ebvl)
 {
   Assert(q[0].getNumChildren() == ebvl.size());
+  Assert(d_synth_fun_vars.empty());
 
   NodeManager* nm = NodeManager::currentNM();
 
   std::vector<Node> qchildren;
   Node qbody_subs = q[1];
-  std::map<Node, Node> synth_fun_vars;
   TermDbSygus* tds = d_qe->getTermDatabaseSygus();
   for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++)
   {
     Node sf = q[0][i];
-    synth_fun_vars[sf] = ebvl[i];
+    d_synth_fun_vars[sf] = ebvl[i];
     Node sfvl = getSygusVarList(sf);
     TypeNode tn = ebvl[i].getType();
     // check if there is a template
@@ -262,14 +262,15 @@ Node CegGrammarConstructor::process(Node q,
     qbody_subs = Rewriter::rewrite( qbody_subs );
     Trace("cegqi") << "...got : " << qbody_subs << std::endl;
   }
-  qchildren.push_back( convertToEmbedding( qbody_subs, synth_fun_vars ) );
+  qchildren.push_back(convertToEmbedding(qbody_subs));
   if( q.getNumChildren()==3 ){
     qchildren.push_back( q[2] );
   }
   return nm->mkNode(kind::FORALL, qchildren);
 }
 
-Node CegGrammarConstructor::convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars ){
+Node CegGrammarConstructor::convertToEmbedding(Node n)
+{
   NodeManager* nm = NodeManager::currentNM();
   std::unordered_map<TNode, Node, TNodeHashFunction> visited;
   std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
@@ -303,8 +304,9 @@ Node CegGrammarConstructor::convertToEmbedding( Node n, std::map< Node, Node >&
       // is the operator a synth function?
       bool makeEvalFun = false;
       if( !op.isNull() ){
-        std::map< Node, Node >::iterator its = synth_fun_vars.find( op );
-        if( its!=synth_fun_vars.end() ){
+        std::map<Node, Node>::iterator its = d_synth_fun_vars.find(op);
+        if (its != d_synth_fun_vars.end())
+        {
           children.push_back( its->second );
           makeEvalFun = true;
         }
@@ -741,9 +743,9 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         weights[i].push_back(-1);
       }
     }else{
-      std::stringstream sserr;
-      sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl;
-      throw LogicException(sserr.str());
+      Warning()
+          << "Warning: No implementation for default Sygus grammar of type "
+          << types[i] << std::endl;
     }
   }
   // make datatypes
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index 3afc4c689..bf377bd33 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -113,6 +113,16 @@ public:
    * sygus grammar, add them to vector ops.
    */
   static void mkSygusConstantsForType(TypeNode type, std::vector<Node>& ops);
+  /**
+   * Convert node n based on deep embedding, see Section 4 of Reynolds et al
+   * CAV 2015.
+   *
+   * This returns the result of converting n to its deep embedding based on
+   * the mapping from functions to datatype variables, stored in
+   * d_synth_fun_vars. This method should be called only after calling process
+   * above.
+   */
+  Node convertToEmbedding(Node n);
 
  private:
   /** reference to quantifier engine */
@@ -121,12 +131,15 @@ public:
   * This contains global information about the synthesis conjecture.
   */
   SynthConjecture* d_parent;
+  /**
+   * Maps each synthesis function to its corresponding (first-order) sygus
+   * datatype variable. This map is initialized by the process methods.
+   */
+  std::map<Node, Node> d_synth_fun_vars;
   /** is the syntax restricted? */
   bool d_is_syntax_restricted;
   /** collect terms */
   void collectTerms( Node n, std::map< TypeNode, std::vector< Node > >& consts );
-  /** convert node n based on deep embedding (Section 4 of Reynolds et al CAV 2015) */
-  Node convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars );
   //---------------- grammar construction
   // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction)
   static TypeNode mkUnresolvedType(const std::string& name, std::set<Type>& unres);
-- 
2.30.2