Move sygus grammar utilities to separate file. (#1184)

* Move sygus grammar utilities to separate file.

* Minor

* Move includes

7 files changed, 712 insertions, 577 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 7b9a607a1..cfb8e379d 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -414,6 +414,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/relevant_domain.h \
 	theory/quantifiers/rewrite_engine.cpp \
 	theory/quantifiers/rewrite_engine.h \
+	theory/quantifiers/sygus_grammar_cons.cpp \
+	theory/quantifiers/sygus_grammar_cons.h \
 	theory/quantifiers/symmetry_breaking.cpp \
 	theory/quantifiers/symmetry_breaking.h \
 	theory/quantifiers/term_database.cpp \
diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index e53a95a2b..0fe246964 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -46,218 +46,58 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe)
   d_refine_count = 0;
   d_ceg_si = new CegConjectureSingleInv(qe, this);
   d_ceg_pbe = new CegConjecturePbe(qe, this);
+  d_ceg_gc = new CegGrammarConstructor(qe);
 }
 
 CegConjecture::~CegConjecture() {
   delete d_ceg_si;
   delete d_ceg_pbe;
+  delete d_ceg_gc;
 }
 
-Node CegConjecture::convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars, std::map< Node, Node >& visited ){
-  std::map< Node, Node >::iterator it = visited.find( n );
-  if( it==visited.end() ){
-    Node ret = n;
-    
-    std::vector< Node > children;
-    bool childChanged = false;
-    bool madeOp = false;
-    Kind ret_k = n.getKind();
-    Node op;
-    if( n.getNumChildren()>0 ){
-      if( n.getKind()==kind::APPLY_UF ){
-        op = n.getOperator();
-      }
-    }else{
-      op = n;
-    }
-    // is it a synth function?
-    std::map< Node, Node >::iterator its = synth_fun_vars.find( op );
-    if( its!=synth_fun_vars.end() ){
-      Assert( its->second.getType().isDatatype() );
-      // make into evaluation function
-      const Datatype& dt = ((DatatypeType)its->second.getType().toType()).getDatatype();
-      Assert( dt.isSygus() );
-      children.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) );
-      children.push_back( its->second );
-      madeOp = true;
-      childChanged = true;
-      ret_k = kind::APPLY_UF;
-    }
-    if( n.getNumChildren()>0 || childChanged ){
-      if( !madeOp ){
-        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-          children.push_back( n.getOperator() );
-        }
-      }
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        Node nc = convertToEmbedding( n[i], synth_fun_vars, visited ); 
-        childChanged = childChanged || nc!=n[i];
-        children.push_back( nc );
-      }
-      if( childChanged ){
-        ret = NodeManager::currentNM()->mkNode( ret_k, children );
-      }
-    }
-    visited[n] = ret;
-    return ret;
-  }else{
-    return it->second;
-  }
-}
-
-void CegConjecture::collectConstants( Node n, std::map< TypeNode, std::vector< Node > >& consts, std::map< Node, bool >& visited ) {
-  if( visited.find( n )==visited.end() ){
-    visited[n] = true;
-    if( n.isConst() ){
-      TypeNode tn = n.getType();
-      Node nc = n;
-      if( tn.isReal() ){
-        nc = NodeManager::currentNM()->mkConst( n.getConst<Rational>().abs() );
-      }
-      if( std::find( consts[tn].begin(), consts[tn].end(), nc )==consts[tn].end() ){
-        Trace("cegqi-debug") << "...consider const : " << nc << std::endl;
-        consts[tn].push_back( nc );
-      }
-    }
-    
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      collectConstants( n[i], consts, visited );
-    }
-  }
-}
-
-
 void CegConjecture::assign( Node q ) {
   Assert( d_embed_quant.isNull() );
   Assert( q.getKind()==FORALL );
   Trace("cegqi") << "CegConjecture : assign : " << q << std::endl;
   d_quant = q;
 
-  Node simp_quant = q;
+  std::map< Node, Node > templates; 
+  std::map< Node, Node > templates_arg;
   //register with single invocation if applicable
   if( d_qe->getTermDatabase()->isQAttrSygus( d_quant ) ){
     d_ceg_si->initialize( d_quant );
-    simp_quant = d_ceg_si->getSimplifiedConjecture();
-  }
-
-  // convert to deep embedding and finalize single invocation here
-  // now, construct the grammar
-  Trace("cegqi") << "CegConjecture : convert to deep embedding..." << std::endl;
-  std::map< TypeNode, std::vector< Node > > extra_cons;
-  Trace("cegqi") << "CegConjecture : collect constants..." << std::endl;
-  if( options::sygusAddConstGrammar() ){
-    std::map< Node, bool > visited;
-    collectConstants( q[1], extra_cons, visited );
-  }
-  bool has_ites = true;
-  bool is_syntax_restricted = false;
-  std::vector< Node > qchildren;
-  std::map< Node, Node > visited;
-  std::map< Node, Node > synth_fun_vars;
-  std::vector< Node > ebvl;
-  Node qbody_subs = simp_quant[1];
-  for( unsigned i=0; i<simp_quant[0].getNumChildren(); i++ ){
-    Node v = simp_quant[0][i];
-    Node sf = v.getAttribute(SygusSynthFunAttribute());
-    Assert( !sf.isNull() );
-    Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute());
-    // sfvl may be null for constant synthesis functions
-    Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl;
-    TypeNode tn;
-    std::stringstream ss;
-    ss << sf;
-    if( v.getType().isDatatype() && ((DatatypeType)v.getType().toType()).getDatatype().isSygus() ){
-      tn = v.getType();
-    }else{
-      // make the default grammar
-      tn = d_qe->getTermDatabaseSygus()->mkSygusDefaultType( v.getType(), sfvl, ss.str(), extra_cons );
-    }
-    Node templ = d_ceg_si->getTemplate( sf );
-    if( !templ.isNull() ){
-      TNode templ_arg = d_ceg_si->getTemplateArg( sf );
-      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") << "  embed this template as a grammar..." << std::endl;
-        tn = d_qe->getTermDatabaseSygus()->mkSygusTemplateType( templ, templ_arg, tn, sfvl, ss.str() );
-      }else{
-        // otherwise, apply it as a preprocessing pass 
-        Trace("cegqi-debug") << "  apply this template as a substituion during preprocess..." << std::endl;
-        std::vector< Node > schildren;
-        std::vector< Node > largs;
-        for( unsigned j=0; j<sfvl.getNumChildren(); j++ ){
-          schildren.push_back( sfvl[j] );
-          largs.push_back( NodeManager::currentNM()->mkBoundVar( sfvl[j].getType() ) );
-        }
-        std::vector< Node > subsfn_children;
-        subsfn_children.push_back( sf );
-        subsfn_children.insert( subsfn_children.end(), schildren.begin(), schildren.end() );
-        Node subsfn = NodeManager::currentNM()->mkNode( kind::APPLY_UF, subsfn_children );
-        TNode subsf = subsfn;
-        Trace("cegqi-debug") << "  substitute arg : " << templ_arg << " -> " << subsf << std::endl;
-        templ = templ.substitute( templ_arg, subsf );
-        // substitute lambda arguments
-        templ = templ.substitute( schildren.begin(), schildren.end(), largs.begin(), largs.end() );
-        Node subsn = NodeManager::currentNM()->mkNode( kind::LAMBDA, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, largs ), templ );
-        TNode var = sf;
-        TNode subs = subsn;
-        Trace("cegqi-debug") << "  substitute : " << var << " -> " << subs << std::endl;
-        qbody_subs = qbody_subs.substitute( var, subs );
-        Trace("cegqi-debug") << "  body is now : " << qbody_subs << std::endl;
-      }
-    }
-    d_qe->getTermDatabaseSygus()->registerSygusType( tn );
-    // check grammar restrictions
-    if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){
-      if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){
-        has_ites = false;
+    q = d_ceg_si->getSimplifiedConjecture();
+    // carry the templates
+    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+      Node v = q[0][i];
+      Node sf = v.getAttribute(SygusSynthFunAttribute());
+      Node templ = d_ceg_si->getTemplate(sf);
+      if( !templ.isNull() ){
+        templates[sf] = templ;
+        templates_arg[sf] = d_ceg_si->getTemplateArg(sf);
       }
     }
-    Assert( tn.isDatatype() );
-    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-    Assert( dt.isSygus() );
-    if( !dt.getSygusAllowAll() ){
-      is_syntax_restricted = true;
-    }
-
-    // ev is the first-order variable corresponding to this synth fun
-    std::stringstream ssf;
-    ssf << "f" << sf;
-    Node ev = NodeManager::currentNM()->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( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, ebvl ) );
-  if( qbody_subs!=simp_quant[1] ){
-    Trace("cegqi") << "...rewriting : " << qbody_subs << std::endl;
-    qbody_subs = Rewriter::rewrite( qbody_subs );
-    Trace("cegqi") << "...got : " << qbody_subs << std::endl;
-  }
-  qchildren.push_back( convertToEmbedding( qbody_subs, synth_fun_vars, visited ) );
-  if( q.getNumChildren()==3 ){
-    qchildren.push_back( q[2] );
-  }
-  q = NodeManager::currentNM()->mkNode( kind::FORALL, qchildren );
-  Trace("cegqi") << "CegConjecture : converted to embedding : " << q << std::endl;
-  d_embed_quant = q;
+
+  // convert to deep embedding and finalize single invocation here
+  d_embed_quant = d_ceg_gc->process( q, templates, templates_arg );
+  Trace("cegqi") << "CegConjecture : converted to embedding : " << d_embed_quant << std::endl;
 
   // we now finalize the single invocation module, based on the syntax restrictions
   if( d_qe->getTermDatabase()->isQAttrSygus( d_quant ) ){
-    d_ceg_si->finishInit( is_syntax_restricted, has_ites );
+    d_ceg_si->finishInit( d_ceg_gc->isSyntaxRestricted(), d_ceg_gc->hasSyntaxITE() );
   }
 
   Assert( d_candidates.empty() );
   std::vector< Node > vars;
-  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-    vars.push_back( q[0][i] );
-    Node e = NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() );
+  for( unsigned i=0; i<d_embed_quant[0].getNumChildren(); i++ ){
+    vars.push_back( d_embed_quant[0][i] );
+    Node e = NodeManager::currentNM()->mkSkolem( "e", d_embed_quant[0][i].getType() );
     d_candidates.push_back( e );
   }
-  Trace("cegqi") << "Base quantified formula is : " << q << std::endl;
+  Trace("cegqi") << "Base quantified formula is : " << d_embed_quant << std::endl;
   //construct base instantiation
-  d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( q, vars, d_candidates ) );
+  d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( d_embed_quant, vars, d_candidates ) );
   
   // register this term with sygus database
   std::vector< Node > guarded_lemmas;
@@ -271,7 +111,7 @@ void CegConjecture::assign( Node q ) {
         std::vector< std::vector< Node > > exs;
         std::vector< Node > exos;
         std::vector< Node > exts;
-        // use the PBE examples, regardless of the search algorith, since these help search space pruning
+        // use the PBE examples, regardless of the search algorithm, since these help search space pruning
         if( d_ceg_pbe->getPbeExamples( e, exs, exos, exts ) ){
           d_qe->getTermDatabaseSygus()->registerPbeExamples( e, exs, exos, exts );
         }
diff --git a/src/theory/quantifiers/ce_guided_conjecture.h b/src/theory/quantifiers/ce_guided_conjecture.h
index 1263778d3..c99867ac7 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/ce_guided_conjecture.h
@@ -18,9 +18,9 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H
 #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_CONJECTURE_H
 
-#include "context/cdhashmap.h"
 #include "theory/quantifiers/ce_guided_single_inv.h"
 #include "theory/quantifiers/ce_guided_pbe.h"
+#include "theory/quantifiers/sygus_grammar_cons.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
@@ -103,6 +103,8 @@ private:
   CegConjectureSingleInv * d_ceg_si;
   /** program by examples utility */
   CegConjecturePbe * d_ceg_pbe;
+  /** grammar utility */
+  CegGrammarConstructor * d_ceg_gc;
   /** list of constants for quantified formula */
   std::vector< Node > d_candidates;
   /** base instantiation */
@@ -131,10 +133,6 @@ private:
   std::map< Node, CandidateInfo > d_cinfo;  
   /** number of times we have called doRefine */
   unsigned d_refine_count;
-  /** 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, std::map< Node, Node >& visited );
-  /** collect constants */
-  void collectConstants( Node n, std::map< TypeNode, std::vector< Node > >& consts, std::map< Node, bool >& visited );
   /** construct candidates */
   bool constructCandidates( std::vector< Node >& clist, std::vector< Node >& model_values, 
                             std::vector< Node >& candidate_values, std::vector< Node >& lems );
diff --git a/src/theory/quantifiers/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus_grammar_cons.cpp
new file mode 100644
index 000000000..194e32b61
--- /dev/null
+++ b/src/theory/quantifiers/sygus_grammar_cons.cpp
@@ -0,0 +1,594 @@
+/*********************                                                        */
+/*! \file sygus_grammar_cons.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief implementation of class for constructing inductive datatypes that correspond to
+ ** grammars that encode syntactic restrictions for SyGuS.
+ **/
+#include "theory/quantifiers/sygus_grammar_cons.h"
+
+#include <stack>
+
+#include "expr/datatype.h"
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/term_database_sygus.h"
+
+using namespace CVC4::kind;
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+
+CegGrammarConstructor::CegGrammarConstructor( QuantifiersEngine * qe ) : 
+d_qe( qe ), d_is_syntax_restricted(false), d_has_ite(true){
+
+}
+
+void CegGrammarConstructor::collectTerms( Node n, std::map< TypeNode, std::vector< Node > >& consts ){
+  std::unordered_map<TNode, bool, TNodeHashFunction> visited;
+  std::unordered_map<TNode, bool, TNodeHashFunction>::iterator it;
+  std::stack<TNode> visit;
+  TNode cur;
+  visit.push(n);
+  do {
+    cur = visit.top();
+    visit.pop();
+    it = visited.find(cur);
+    if (it == visited.end()) {
+      visited[cur] = true;
+      // is this a constant?
+      if( cur.isConst() ){
+        TypeNode tn = cur.getType();
+        Node c = cur;
+        if( tn.isReal() ){
+          c = NodeManager::currentNM()->mkConst( c.getConst<Rational>().abs() );
+        }
+        if( std::find( consts[tn].begin(), consts[tn].end(), c )==consts[tn].end() ){
+          Trace("cegqi-debug") << "...consider const : " << c << std::endl;
+          consts[tn].push_back( c );
+        }
+      }
+      // recurse
+      for (unsigned i = 0; i < cur.getNumChildren(); i++) {
+        visit.push(cur[i]);
+      }
+    }
+  } while (!visit.empty());
+}
+
+
+
+Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates, 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;
+  std::map< TypeNode, std::vector< Node > > extra_cons;
+  if( options::sygusAddConstGrammar() ){
+    Trace("cegqi") << "CegConjecture : collect constants..." << std::endl;
+    collectTerms( q[1], extra_cons );
+  }
+
+  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 v = q[0][i];
+    Node sf = v.getAttribute(SygusSynthFunAttribute());
+    Assert( !sf.isNull() );
+    Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute());
+    // sfvl may be null for constant synthesis functions
+    Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl;
+    TypeNode tn;
+    std::stringstream ss;
+    ss << sf;
+    if( v.getType().isDatatype() && ((DatatypeType)v.getType().toType()).getDatatype().isSygus() ){
+      tn = v.getType();
+    }else{
+      // make the default grammar
+      tn = mkSygusDefaultType( v.getType(), sfvl, ss.str(), extra_cons );
+    }
+    // check if there is a template
+    std::map< Node, Node >::iterator itt = templates.find( sf );
+    if( itt!=templates.end() ){
+      Node templ = itt->second;
+      TNode templ_arg = templates_arg[sf];
+      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") << "  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 
+        Trace("cegqi-debug") << "  apply this template as a substituion during preprocess..." << std::endl;
+        std::vector< Node > schildren;
+        std::vector< Node > largs;
+        for( unsigned j=0; j<sfvl.getNumChildren(); j++ ){
+          schildren.push_back( sfvl[j] );
+          largs.push_back( NodeManager::currentNM()->mkBoundVar( sfvl[j].getType() ) );
+        }
+        std::vector< Node > subsfn_children;
+        subsfn_children.push_back( sf );
+        subsfn_children.insert( subsfn_children.end(), schildren.begin(), schildren.end() );
+        Node subsfn = NodeManager::currentNM()->mkNode( kind::APPLY_UF, subsfn_children );
+        TNode subsf = subsfn;
+        Trace("cegqi-debug") << "  substitute arg : " << templ_arg << " -> " << subsf << std::endl;
+        templ = templ.substitute( templ_arg, subsf );
+        // substitute lambda arguments
+        templ = templ.substitute( schildren.begin(), schildren.end(), largs.begin(), largs.end() );
+        Node subsn = NodeManager::currentNM()->mkNode( kind::LAMBDA, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, largs ), templ );
+        TNode var = sf;
+        TNode subs = subsn;
+        Trace("cegqi-debug") << "  substitute : " << var << " -> " << subs << std::endl;
+        qbody_subs = qbody_subs.substitute( var, subs );
+        Trace("cegqi-debug") << "  body is now : " << qbody_subs << std::endl;
+      }
+    }
+    d_qe->getTermDatabaseSygus()->registerSygusType( tn );
+    // check grammar restrictions
+    if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){
+      if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){
+        d_has_ite = false;
+      }
+    }
+    Assert( tn.isDatatype() );
+    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+    Assert( dt.isSygus() );
+    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 = NodeManager::currentNM()->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( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, ebvl ) );
+  if( qbody_subs!=q[1] ){
+    Trace("cegqi") << "...rewriting : " << qbody_subs << std::endl;
+    qbody_subs = Rewriter::rewrite( qbody_subs );
+    Trace("cegqi") << "...got : " << qbody_subs << std::endl;
+  }
+  qchildren.push_back( convertToEmbedding( qbody_subs, synth_fun_vars ) );
+  if( q.getNumChildren()==3 ){
+    qchildren.push_back( q[2] );
+  }
+  return NodeManager::currentNM()->mkNode( kind::FORALL, qchildren );
+}
+  
+Node CegGrammarConstructor::convertToEmbedding( Node n, std::map< Node, Node >& synth_fun_vars ){
+  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::stack<TNode> visit;
+  TNode cur;
+  visit.push(n);
+  do {
+    cur = visit.top();
+    visit.pop();
+    it = visited.find(cur);
+    if (it == visited.end()) {
+      visited[cur] = Node::null();
+      visit.push(cur);
+      for (unsigned i = 0; i < cur.getNumChildren(); i++) {
+        visit.push(cur[i]);
+      }
+    } else if (it->second.isNull()) {
+      Node ret = cur;
+      Kind ret_k = cur.getKind();
+      Node op;
+      bool childChanged = false;
+      std::vector<Node> children;
+      // get the potential operator
+      if( cur.getNumChildren()>0 ){
+        if( cur.getKind()==kind::APPLY_UF ){
+          op = cur.getOperator();
+        }
+      }else{
+        op = cur;
+      }
+      // is the operator a synth function?
+      if( !op.isNull() ){
+        std::map< Node, Node >::iterator its = synth_fun_vars.find( op );
+        if( its!=synth_fun_vars.end() ){
+          Assert( its->second.getType().isDatatype() );
+          // will make into an application of an evaluation function
+          const Datatype& dt = ((DatatypeType)its->second.getType().toType()).getDatatype();
+          Assert( dt.isSygus() );
+          children.push_back( Node::fromExpr( dt.getSygusEvaluationFunc() ) );
+          children.push_back( its->second );
+          childChanged = true;
+          ret_k = kind::APPLY_UF;
+        }
+      }
+      if( !childChanged ){
+        // otherwise, we apply the previous operator
+        if( cur.getMetaKind() == kind::metakind::PARAMETERIZED ){
+          children.push_back( cur.getOperator() );
+        }
+      }
+      for (unsigned i = 0; i < cur.getNumChildren(); i++) {
+        it = visited.find(cur[i]);
+        Assert(it != visited.end());
+        Assert(!it->second.isNull());
+        childChanged = childChanged || cur[i] != it->second;
+        children.push_back(it->second);
+      }
+      if (childChanged) {
+        ret = NodeManager::currentNM()->mkNode(ret_k, children);
+      }
+      visited[cur] = ret;
+    }
+  } while (!visit.empty());
+  Assert(visited.find(n) != visited.end());
+  Assert(!visited.find(n)->second.isNull());
+  return visited[n];
+}
+
+
+TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name, std::set<Type>& unres) {
+  TypeNode unresolved = NodeManager::currentNM()->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER);
+  unres.insert( unresolved.toType() );
+  return unresolved;
+}
+
+void CegGrammarConstructor::mkSygusConstantsForType( TypeNode type, std::vector<CVC4::Node>& ops ) {
+  if( type.isInteger() ){
+    ops.push_back(NodeManager::currentNM()->mkConst(Rational(0)));
+    ops.push_back(NodeManager::currentNM()->mkConst(Rational(1)));
+  }else if( type.isBitVector() ){
+    unsigned sz = ((BitVectorType)type.toType()).getSize();
+    BitVector bval0(sz, (unsigned int)0);
+    ops.push_back( NodeManager::currentNM()->mkConst(bval0) );
+    BitVector bval1(sz, (unsigned int)1);
+    ops.push_back( NodeManager::currentNM()->mkConst(bval1) );
+  }else if( type.isBoolean() ){
+    ops.push_back(NodeManager::currentNM()->mkConst(true));
+    ops.push_back(NodeManager::currentNM()->mkConst(false));
+  }
+  //TODO : others?
+}
+
+void CegGrammarConstructor::collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ){
+  if( !range.isBoolean() ){
+    if( std::find( types.begin(), types.end(), range )==types.end() ){
+      Trace("sygus-grammar-def") << "...will make grammar for " << range << std::endl;
+      types.push_back( range );
+      if( range.isDatatype() ){
+        const Datatype& dt = ((DatatypeType)range.toType()).getDatatype();
+        for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+          for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
+            TypeNode crange = TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() );
+            sels[crange].push_back( dt[i][j] );
+            collectSygusGrammarTypesFor( crange, types, sels );
+          }
+        }
+      }
+    }
+  }
+}
+
+void CegGrammarConstructor::mkSygusDefaultGrammar( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons, 
+                                         std::vector< CVC4::Datatype >& datatypes, std::set<Type>& unres ) {
+  // collect the variables
+  std::vector<Node> sygus_vars;
+  if( !bvl.isNull() ){
+    for( unsigned i=0; i<bvl.getNumChildren(); i++ ){
+      sygus_vars.push_back( bvl[i] );
+    }
+  }
+  //if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){
+  //  parseError("No default grammar for type.");
+  //}
+  std::vector< std::vector< Expr > > ops;
+  int startIndex = -1;
+  Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " " << range << std::endl;
+  std::map< Type, Type > sygus_to_builtin;
+
+  std::vector< TypeNode > types;
+  std::map< TypeNode, std::vector< DatatypeConstructorArg > > sels;
+  //types for each of the variables of parametric sort
+  for( unsigned i=0; i<sygus_vars.size(); i++ ){
+    collectSygusGrammarTypesFor( sygus_vars[i].getType(), types, sels );
+  }
+  //types connected to range
+  collectSygusGrammarTypesFor( range, types, sels );
+
+  //name of boolean sort
+  std::stringstream ssb;
+  ssb << fun << "_Bool";
+  std::string dbname = ssb.str();
+  Type unres_bt = mkUnresolvedType(ssb.str(), unres).toType();
+
+  std::vector< Type > unres_types;
+  std::map< TypeNode, Type > type_to_unres;
+  for( unsigned i=0; i<types.size(); i++ ){
+    std::stringstream ss;
+    ss << fun << "_" << types[i];
+    std::string dname = ss.str();
+    datatypes.push_back(Datatype(dname));
+    ops.push_back(std::vector< Expr >());
+    //make unresolved type
+    Type unres_t = mkUnresolvedType(dname, unres).toType();
+    unres_types.push_back(unres_t);
+    type_to_unres[types[i]] = unres_t;
+    sygus_to_builtin[unres_t] = types[i].toType();
+  }
+  for( unsigned i=0; i<types.size(); i++ ){
+    Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl;
+    std::vector<std::string> cnames;
+    std::vector<std::vector<CVC4::Type> > cargs;
+    Type unres_t = unres_types[i];
+    //add variables
+    for( unsigned j=0; j<sygus_vars.size(); j++ ){
+      if( sygus_vars[j].getType()==types[i] ){
+        std::stringstream ss;
+        ss << sygus_vars[j];
+        Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl;
+        ops[i].push_back( sygus_vars[j].toExpr() );
+        cnames.push_back( ss.str() );
+        cargs.push_back( std::vector< CVC4::Type >() );
+      }
+    }
+    //add constants
+    std::vector< Node > consts;
+    mkSygusConstantsForType( types[i], consts );
+    std::map< TypeNode, std::vector< Node > >::iterator itec = extra_cons.find( types[i] );
+    if( itec!=extra_cons.end() ){
+      //consts.insert( consts.end(), itec->second.begin(), itec->second.end() );
+      for( unsigned j=0; j<itec->second.size(); j++ ){
+        if( std::find( consts.begin(), consts.end(), itec->second[j] )==consts.end() ){
+          consts.push_back( itec->second[j] );
+        }
+      }
+    }
+    for( unsigned j=0; j<consts.size(); j++ ){
+      std::stringstream ss;
+      ss << consts[j];
+      Trace("sygus-grammar-def") << "...add for constant " << ss.str() << std::endl;
+      ops[i].push_back( consts[j].toExpr() );
+      cnames.push_back( ss.str() );
+      cargs.push_back( std::vector< CVC4::Type >() );
+    }
+    //ITE
+    CVC4::Kind k = kind::ITE;
+    Trace("sygus-grammar-def") << "...add for " << k << std::endl;
+    ops[i].push_back(NodeManager::currentNM()->operatorOf(k).toExpr());
+    cnames.push_back( kind::kindToString(k) );
+    cargs.push_back( std::vector< CVC4::Type >() );
+    cargs.back().push_back(unres_bt);
+    cargs.back().push_back(unres_t);
+    cargs.back().push_back(unres_t);
+
+    if( types[i].isInteger() ){
+      for( unsigned j=0; j<2; j++ ){
+        CVC4::Kind k = j==0 ? kind::PLUS : kind::MINUS;
+        Trace("sygus-grammar-def") << "...add for " << k << std::endl;
+        ops[i].push_back(NodeManager::currentNM()->operatorOf(k).toExpr());
+        cnames.push_back(kind::kindToString(k));
+        cargs.push_back( std::vector< CVC4::Type >() );
+        cargs.back().push_back(unres_t);
+        cargs.back().push_back(unres_t);
+      }
+    }else if( types[i].isDatatype() ){
+      Trace("sygus-grammar-def") << "...add for constructors" << std::endl;
+      const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype();
+      for( unsigned k=0; k<dt.getNumConstructors(); k++ ){
+        Trace("sygus-grammar-def") << "...for " << dt[k].getName() << std::endl;
+        ops[i].push_back( dt[k].getConstructor() );
+        cnames.push_back( dt[k].getName() );
+        cargs.push_back( std::vector< CVC4::Type >() );
+        for( unsigned j=0; j<dt[k].getNumArgs(); j++ ){
+          TypeNode crange = TypeNode::fromType( ((SelectorType)dt[k][j].getType()).getRangeType() );
+          //Assert( type_to_unres.find(crange)!=type_to_unres.end() );
+          cargs.back().push_back( type_to_unres[crange] );
+        }
+      }
+    }else{
+      std::stringstream sserr;
+      sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl;
+      //AlwaysAssert( false, sserr.str() );
+      // FIXME
+      AlwaysAssert( false );
+    }
+    //add for all selectors to this type
+    if( !sels[types[i]].empty() ){
+      Trace("sygus-grammar-def") << "...add for selectors" << std::endl;
+      for( unsigned j=0; j<sels[types[i]].size(); j++ ){
+        Trace("sygus-grammar-def") << "...for " << sels[types[i]][j].getName() << std::endl;
+        TypeNode arg_type = TypeNode::fromType( ((SelectorType)sels[types[i]][j].getType()).getDomain() );
+        ops[i].push_back( sels[types[i]][j].getSelector() );
+        cnames.push_back( sels[types[i]][j].getName() );
+        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] );
+      }
+    }
+    Trace("sygus-grammar-def") << "...make datatype " << datatypes.back() << std::endl;
+    datatypes[i].setSygus( types[i].toType(), bvl.toExpr(), true, true );
+    for( unsigned j=0; j<ops[i].size(); j++ ){
+      datatypes[i].addSygusConstructor( ops[i][j], cnames[j], cargs[j] );
+    }
+    //sorts.push_back( types[i] );
+    //set start index if applicable
+    if( types[i]==range ){
+      startIndex = i;
+    }
+  }
+
+  //make Boolean type
+  TypeNode btype = NodeManager::currentNM()->booleanType();
+  datatypes.push_back(Datatype(dbname));
+  ops.push_back(std::vector<Expr>());
+  std::vector<std::string> cnames;
+  std::vector<std::vector< Type > > cargs;
+  Trace("sygus-grammar-def") << "Make grammar for " << btype << " " << datatypes.back() << std::endl;
+  //add variables
+  for( unsigned i=0; i<sygus_vars.size(); i++ ){
+    if( sygus_vars[i].getType().isBoolean() ){
+      std::stringstream ss;
+      ss << sygus_vars[i];
+      Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl;
+      ops.back().push_back( sygus_vars[i].toExpr() );
+      cnames.push_back( ss.str() );
+      cargs.push_back( std::vector< CVC4::Type >() );
+    }
+  }
+  //add constants if no variables and no connected types
+  if( ops.back().empty() && types.empty() ){
+    std::vector< Node > consts;
+    mkSygusConstantsForType( btype, consts );
+    for( unsigned j=0; j<consts.size(); j++ ){
+      std::stringstream ss;
+      ss << consts[j];
+      Trace("sygus-grammar-def") << "...add for constant " << ss.str() << std::endl;
+      ops.back().push_back( consts[j].toExpr() );
+      cnames.push_back( ss.str() );
+      cargs.push_back( std::vector< CVC4::Type >() );
+    }
+  }
+  //add operators
+  for( unsigned i=0; i<3; i++ ){
+    CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : kind::OR );
+    Trace("sygus-grammar-def") << "...add for " << k << std::endl;
+    ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr());
+    cnames.push_back(kind::kindToString(k));
+    cargs.push_back( std::vector< CVC4::Type >() );
+    if( k==kind::NOT ){
+      cargs.back().push_back(unres_bt);
+    }else if( k==kind::AND || k==kind::OR ){
+      cargs.back().push_back(unres_bt);
+      cargs.back().push_back(unres_bt);
+    }
+  }
+  //add predicates for types
+  for( unsigned i=0; i<types.size(); i++ ){
+    Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl;
+    //add equality per type
+    CVC4::Kind k = kind::EQUAL;
+    Trace("sygus-grammar-def") << "...add for " << k << std::endl;
+    ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr());
+    std::stringstream ss;
+    ss << kind::kindToString(k) << "_" << types[i];
+    cnames.push_back(ss.str());
+    cargs.push_back( std::vector< CVC4::Type >() );
+    cargs.back().push_back(unres_types[i]);
+    cargs.back().push_back(unres_types[i]);
+    //type specific predicates
+    if( types[i].isInteger() ){
+      CVC4::Kind k = kind::LEQ;
+      Trace("sygus-grammar-def") << "...add for " << k << std::endl;
+      ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr());
+      cnames.push_back(kind::kindToString(k));
+      cargs.push_back( std::vector< CVC4::Type >() );
+      cargs.back().push_back(unres_types[i]);
+      cargs.back().push_back(unres_types[i]);
+    }else if( types[i].isDatatype() ){
+      //add for testers
+      Trace("sygus-grammar-def") << "...add for testers" << std::endl;
+      const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype();
+      for( unsigned k=0; k<dt.getNumConstructors(); k++ ){
+        Trace("sygus-grammar-def") << "...for " << dt[k].getTesterName() << std::endl;
+        ops.back().push_back(dt[k].getTester());
+        cnames.push_back(dt[k].getTesterName());
+        cargs.push_back( std::vector< CVC4::Type >() );
+        cargs.back().push_back(unres_types[i]);
+      }
+    }
+  }
+  if( range==btype ){
+    startIndex = datatypes.size()-1;
+  }
+  Trace("sygus-grammar-def") << "...make datatype " << datatypes.back() << std::endl;
+  datatypes.back().setSygus( btype.toType(), bvl.toExpr(), true, true );
+  for( unsigned j=0; j<ops.back().size(); j++ ){
+    datatypes.back().addSygusConstructor( ops.back()[j], cnames[j], cargs[j] );
+  }
+  //sorts.push_back( btype );
+  Trace("sygus-grammar-def") << "...finished make default grammar for " << fun << " " << range << std::endl;
+  
+  if( startIndex>0 ){
+    CVC4::Datatype tmp_dt = datatypes[0];
+    datatypes[0] = datatypes[startIndex];
+    datatypes[startIndex] = tmp_dt;
+  }
+}
+
+
+TypeNode CegGrammarConstructor::mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, 
+                                          std::map< TypeNode, std::vector< Node > >& extra_cons ) {
+  Trace("sygus-grammar-def") << "*** Make sygus default type " << range << ", make datatypes..." << std::endl;
+  for( std::map< TypeNode, std::vector< Node > >::iterator it = extra_cons.begin(); it != extra_cons.end(); ++it ){
+    Trace("sygus-grammar-def") << "    ...using " << it->second.size() << " extra constants for " << it->first << std::endl;
+  }
+  std::set<Type> unres;
+  std::vector< CVC4::Datatype > datatypes;
+  mkSygusDefaultGrammar( range, bvl, fun, extra_cons, datatypes, unres );
+  Trace("sygus-grammar-def")  << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl;
+  Assert( !datatypes.empty() );
+  std::vector<DatatypeType> types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres);
+  Assert( types.size()==datatypes.size() );
+  return TypeNode::fromType( types[0] );
+}
+
+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 ) );
+    return templ_arg_sygus_type;
+  }else{
+    tcount++;
+    std::set<Type> unres;
+    std::vector< CVC4::Datatype > datatypes;
+    std::stringstream ssd;
+    ssd << fun << "_templ_" << tcount;
+    std::string dbname = ssd.str();
+    datatypes.push_back(Datatype(dbname));
+    Node op;
+    std::vector< Type > argTypes;
+    if( templ.getNumChildren()==0 ){
+      // TODO : can short circuit to this case when !TermDb::containsTerm( templ, templ_arg )
+      op = templ;
+    }else{
+      Assert( templ.hasOperator() );
+      op = templ.getOperator();
+      // make constructor taking arguments types from children
+      for( unsigned i=0; i<templ.getNumChildren(); i++ ){
+        //recursion depth bound by the depth of SyGuS template expressions (low)
+        TypeNode tnc = mkSygusTemplateTypeRec( templ[i], templ_arg, templ_arg_sygus_type, bvl, fun, tcount );
+        argTypes.push_back( tnc.toType() );
+      }
+    }
+    std::stringstream ssdc;
+    ssdc << fun << "_templ_cons_" << tcount;
+    std::string cname = ssdc.str();
+    // we have a single sygus constructor that encodes the template
+    datatypes.back().addSygusConstructor( op.toExpr(), cname, argTypes );
+    datatypes.back().setSygus( templ.getType().toType(), bvl.toExpr(), true, true );
+    std::vector<DatatypeType> types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres);
+    Assert( types.size()==1 );
+    return TypeNode::fromType( types[0] );
+  }
+}
+
+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 );
+}
+
+}/* namespace CVC4::theory::quantifiers */
+}/* namespace CVC4::theory */
+}/* namespace CVC4 */
diff --git a/src/theory/quantifiers/sygus_grammar_cons.h b/src/theory/quantifiers/sygus_grammar_cons.h
new file mode 100644
index 000000000..e8b09293c
--- /dev/null
+++ b/src/theory/quantifiers/sygus_grammar_cons.h
@@ -0,0 +1,89 @@
+/*********************                                                        */
+/*! \file sygus_grammar_cons.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief class for constructing inductive datatypes that correspond to
+ ** grammars that encode syntactic restrictions for SyGuS.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
+
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** utility for constructing datatypes that correspond to syntactic restrictions,
+* and applying the deep embedding from Section 4 of Reynolds et al CAV 2015.
+*/
+class CegGrammarConstructor
+{
+public:
+  CegGrammarConstructor( QuantifiersEngine * qe );
+  ~CegGrammarConstructor(){}
+  /** convert node n based on deep embedding (Section 4 of Reynolds et al CAV 2015) */
+  Node process( Node q, std::map< Node, Node >& templates, std::map< Node, Node >& templates_arg );
+  /** is the syntax restricted? */
+  bool isSyntaxRestricted() { return d_is_syntax_restricted; }
+  /** does the syntax allow ITE expressions? */
+  bool hasSyntaxITE() { return d_has_ite; }
+  // make the default sygus datatype type corresponding to builtin type range
+  //   bvl is the set of free variables to include in the grammar
+  //   fun is for naming
+  //   extra_cons is a set of extra constant symbols to include in the grammar
+  static TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons );
+  // make the default sygus datatype type corresponding to builtin type range
+  static TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun ){
+    std::map< TypeNode, std::vector< Node > > extra_cons;
+    return mkSygusDefaultType( range, bvl, fun, extra_cons );
+  }
+  // make the sygus datatype type that encodes the solution space (lambda templ_arg. templ[templ_arg]) where templ_arg
+  // has syntactic restrictions encoded by sygus type templ_arg_sygus_type
+  //   bvl is the set of free variables to include in the frammar
+  //   fun is for naming
+  static TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun );
+private:
+  /** reference to quantifier engine */
+  QuantifiersEngine * d_qe;
+  /** is the syntax restricted? */
+  bool d_is_syntax_restricted;
+  /** does the syntax allow ITE expressions? */
+  bool d_has_ite;
+  /** 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);
+  // make the builtin constants for type type that should be included in a sygus grammar
+  static void mkSygusConstantsForType( TypeNode type, std::vector<CVC4::Node>& ops );
+  // collect the list of types that depend on type range
+  static void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels );
+  // helper function for function mkSygusDefaultGrammar
+  //   collects a set of mutually recursive datatypes "datatypes" corresponding to encoding type "range" to SyGuS
+  //   unres is used for the resulting call to mkMutualDatatypeTypes
+  static void mkSygusDefaultGrammar( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons, 
+                                     std::vector< CVC4::Datatype >& datatypes, std::set<Type>& unres );
+  // helper function for mkSygusTemplateType
+  static TypeNode mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, 
+                                          const std::string& fun, unsigned& tcount );
+  //---------------- end grammar construction
+};
+
+} /* namespace CVC4::theory::quantifiers */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
+
+#endif
diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp
index a0af545e1..61bb20987 100644
--- a/src/theory/quantifiers/term_database_sygus.cpp
+++ b/src/theory/quantifiers/term_database_sygus.cpp
@@ -2694,361 +2694,6 @@ Node TermDbSygus::extendedRewrite( Node n ) {
 }
 
 
-
-
-
-
-TypeNode TermDbSygus::mkUnresolvedType(const std::string& name, std::set<Type>& unres) {
-  TypeNode unresolved = NodeManager::currentNM()->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER);
-  unres.insert( unresolved.toType() );
-  return unresolved;
-}
-
-void TermDbSygus::mkSygusConstantsForType( TypeNode type, std::vector<CVC4::Node>& ops ) {
-  if( type.isInteger() ){
-    ops.push_back(NodeManager::currentNM()->mkConst(Rational(0)));
-    ops.push_back(NodeManager::currentNM()->mkConst(Rational(1)));
-  }else if( type.isBitVector() ){
-    unsigned sz = ((BitVectorType)type.toType()).getSize();
-    BitVector bval0(sz, (unsigned int)0);
-    ops.push_back( NodeManager::currentNM()->mkConst(bval0) );
-    BitVector bval1(sz, (unsigned int)1);
-    ops.push_back( NodeManager::currentNM()->mkConst(bval1) );
-  }else if( type.isBoolean() ){
-    ops.push_back(NodeManager::currentNM()->mkConst(true));
-    ops.push_back(NodeManager::currentNM()->mkConst(false));
-  }
-  //TODO : others?
-}
-
-void TermDbSygus::collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ){
-  if( !range.isBoolean() ){
-    if( std::find( types.begin(), types.end(), range )==types.end() ){
-      Trace("sygus-grammar-def") << "...will make grammar for " << range << std::endl;
-      types.push_back( range );
-      if( range.isDatatype() ){
-        const Datatype& dt = ((DatatypeType)range.toType()).getDatatype();
-        for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-          for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
-            TypeNode crange = TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() );
-            sels[crange].push_back( dt[i][j] );
-            collectSygusGrammarTypesFor( crange, types, sels );
-          }
-        }
-      }
-    }
-  }
-}
-
-void TermDbSygus::mkSygusDefaultGrammar( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons, 
-                                         std::vector< CVC4::Datatype >& datatypes, std::set<Type>& unres ) {
-  // collect the variables
-  std::vector<Node> sygus_vars;
-  if( !bvl.isNull() ){
-    for( unsigned i=0; i<bvl.getNumChildren(); i++ ){
-      sygus_vars.push_back( bvl[i] );
-    }
-  }
-  //if( !range.isBoolean() && !range.isInteger() && !range.isBitVector() && !range.isDatatype() ){
-  //  parseError("No default grammar for type.");
-  //}
-  std::vector< std::vector< Expr > > ops;
-  int startIndex = -1;
-  Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " " << range << std::endl;
-  std::map< Type, Type > sygus_to_builtin;
-
-  std::vector< TypeNode > types;
-  std::map< TypeNode, std::vector< DatatypeConstructorArg > > sels;
-  //types for each of the variables of parametric sort
-  for( unsigned i=0; i<sygus_vars.size(); i++ ){
-    collectSygusGrammarTypesFor( sygus_vars[i].getType(), types, sels );
-  }
-  //types connected to range
-  collectSygusGrammarTypesFor( range, types, sels );
-
-  //name of boolean sort
-  std::stringstream ssb;
-  ssb << fun << "_Bool";
-  std::string dbname = ssb.str();
-  Type unres_bt = mkUnresolvedType(ssb.str(), unres).toType();
-
-  std::vector< Type > unres_types;
-  std::map< TypeNode, Type > type_to_unres;
-  for( unsigned i=0; i<types.size(); i++ ){
-    std::stringstream ss;
-    ss << fun << "_" << types[i];
-    std::string dname = ss.str();
-    datatypes.push_back(Datatype(dname));
-    ops.push_back(std::vector< Expr >());
-    //make unresolved type
-    Type unres_t = mkUnresolvedType(dname, unres).toType();
-    unres_types.push_back(unres_t);
-    type_to_unres[types[i]] = unres_t;
-    sygus_to_builtin[unres_t] = types[i].toType();
-  }
-  for( unsigned i=0; i<types.size(); i++ ){
-    Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl;
-    std::vector<std::string> cnames;
-    std::vector<std::vector<CVC4::Type> > cargs;
-    Type unres_t = unres_types[i];
-    //add variables
-    for( unsigned j=0; j<sygus_vars.size(); j++ ){
-      if( sygus_vars[j].getType()==types[i] ){
-        std::stringstream ss;
-        ss << sygus_vars[j];
-        Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl;
-        ops[i].push_back( sygus_vars[j].toExpr() );
-        cnames.push_back( ss.str() );
-        cargs.push_back( std::vector< CVC4::Type >() );
-      }
-    }
-    //add constants
-    std::vector< Node > consts;
-    mkSygusConstantsForType( types[i], consts );
-    std::map< TypeNode, std::vector< Node > >::iterator itec = extra_cons.find( types[i] );
-    if( itec!=extra_cons.end() ){
-      //consts.insert( consts.end(), itec->second.begin(), itec->second.end() );
-      for( unsigned j=0; j<itec->second.size(); j++ ){
-        if( std::find( consts.begin(), consts.end(), itec->second[j] )==consts.end() ){
-          consts.push_back( itec->second[j] );
-        }
-      }
-    }
-    for( unsigned j=0; j<consts.size(); j++ ){
-      std::stringstream ss;
-      ss << consts[j];
-      Trace("sygus-grammar-def") << "...add for constant " << ss.str() << std::endl;
-      ops[i].push_back( consts[j].toExpr() );
-      cnames.push_back( ss.str() );
-      cargs.push_back( std::vector< CVC4::Type >() );
-    }
-    //ITE
-    CVC4::Kind k = kind::ITE;
-    Trace("sygus-grammar-def") << "...add for " << k << std::endl;
-    ops[i].push_back(NodeManager::currentNM()->operatorOf(k).toExpr());
-    cnames.push_back( kind::kindToString(k) );
-    cargs.push_back( std::vector< CVC4::Type >() );
-    cargs.back().push_back(unres_bt);
-    cargs.back().push_back(unres_t);
-    cargs.back().push_back(unres_t);
-
-    if( types[i].isInteger() ){
-      for( unsigned j=0; j<2; j++ ){
-        CVC4::Kind k = j==0 ? kind::PLUS : kind::MINUS;
-        Trace("sygus-grammar-def") << "...add for " << k << std::endl;
-        ops[i].push_back(NodeManager::currentNM()->operatorOf(k).toExpr());
-        cnames.push_back(kind::kindToString(k));
-        cargs.push_back( std::vector< CVC4::Type >() );
-        cargs.back().push_back(unres_t);
-        cargs.back().push_back(unres_t);
-      }
-    }else if( types[i].isDatatype() ){
-      Trace("sygus-grammar-def") << "...add for constructors" << std::endl;
-      const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype();
-      for( unsigned k=0; k<dt.getNumConstructors(); k++ ){
-        Trace("sygus-grammar-def") << "...for " << dt[k].getName() << std::endl;
-        ops[i].push_back( dt[k].getConstructor() );
-        cnames.push_back( dt[k].getName() );
-        cargs.push_back( std::vector< CVC4::Type >() );
-        for( unsigned j=0; j<dt[k].getNumArgs(); j++ ){
-          TypeNode crange = TypeNode::fromType( ((SelectorType)dt[k][j].getType()).getRangeType() );
-          //Assert( type_to_unres.find(crange)!=type_to_unres.end() );
-          cargs.back().push_back( type_to_unres[crange] );
-        }
-      }
-    }else{
-      std::stringstream sserr;
-      sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl;
-      //AlwaysAssert( false, sserr.str() );
-      // FIXME
-      AlwaysAssert( false );
-    }
-    //add for all selectors to this type
-    if( !sels[types[i]].empty() ){
-      Trace("sygus-grammar-def") << "...add for selectors" << std::endl;
-      for( unsigned j=0; j<sels[types[i]].size(); j++ ){
-        Trace("sygus-grammar-def") << "...for " << sels[types[i]][j].getName() << std::endl;
-        TypeNode arg_type = TypeNode::fromType( ((SelectorType)sels[types[i]][j].getType()).getDomain() );
-        ops[i].push_back( sels[types[i]][j].getSelector() );
-        cnames.push_back( sels[types[i]][j].getName() );
-        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] );
-      }
-    }
-    Trace("sygus-grammar-def") << "...make datatype " << datatypes.back() << std::endl;
-    datatypes[i].setSygus( types[i].toType(), bvl.toExpr(), true, true );
-    for( unsigned j=0; j<ops[i].size(); j++ ){
-      datatypes[i].addSygusConstructor( ops[i][j], cnames[j], cargs[j] );
-    }
-    //sorts.push_back( types[i] );
-    //set start index if applicable
-    if( types[i]==range ){
-      startIndex = i;
-    }
-  }
-
-  //make Boolean type
-  TypeNode btype = NodeManager::currentNM()->booleanType();
-  datatypes.push_back(Datatype(dbname));
-  ops.push_back(std::vector<Expr>());
-  std::vector<std::string> cnames;
-  std::vector<std::vector< Type > > cargs;
-  Trace("sygus-grammar-def") << "Make grammar for " << btype << " " << datatypes.back() << std::endl;
-  //add variables
-  for( unsigned i=0; i<sygus_vars.size(); i++ ){
-    if( sygus_vars[i].getType().isBoolean() ){
-      std::stringstream ss;
-      ss << sygus_vars[i];
-      Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl;
-      ops.back().push_back( sygus_vars[i].toExpr() );
-      cnames.push_back( ss.str() );
-      cargs.push_back( std::vector< CVC4::Type >() );
-    }
-  }
-  //add constants if no variables and no connected types
-  if( ops.back().empty() && types.empty() ){
-    std::vector< Node > consts;
-    mkSygusConstantsForType( btype, consts );
-    for( unsigned j=0; j<consts.size(); j++ ){
-      std::stringstream ss;
-      ss << consts[j];
-      Trace("sygus-grammar-def") << "...add for constant " << ss.str() << std::endl;
-      ops.back().push_back( consts[j].toExpr() );
-      cnames.push_back( ss.str() );
-      cargs.push_back( std::vector< CVC4::Type >() );
-    }
-  }
-  //add operators
-  for( unsigned i=0; i<3; i++ ){
-    CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : kind::OR );
-    Trace("sygus-grammar-def") << "...add for " << k << std::endl;
-    ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr());
-    cnames.push_back(kind::kindToString(k));
-    cargs.push_back( std::vector< CVC4::Type >() );
-    if( k==kind::NOT ){
-      cargs.back().push_back(unres_bt);
-    }else if( k==kind::AND || k==kind::OR ){
-      cargs.back().push_back(unres_bt);
-      cargs.back().push_back(unres_bt);
-    }
-  }
-  //add predicates for types
-  for( unsigned i=0; i<types.size(); i++ ){
-    Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl;
-    //add equality per type
-    CVC4::Kind k = kind::EQUAL;
-    Trace("sygus-grammar-def") << "...add for " << k << std::endl;
-    ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr());
-    std::stringstream ss;
-    ss << kind::kindToString(k) << "_" << types[i];
-    cnames.push_back(ss.str());
-    cargs.push_back( std::vector< CVC4::Type >() );
-    cargs.back().push_back(unres_types[i]);
-    cargs.back().push_back(unres_types[i]);
-    //type specific predicates
-    if( types[i].isInteger() ){
-      CVC4::Kind k = kind::LEQ;
-      Trace("sygus-grammar-def") << "...add for " << k << std::endl;
-      ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr());
-      cnames.push_back(kind::kindToString(k));
-      cargs.push_back( std::vector< CVC4::Type >() );
-      cargs.back().push_back(unres_types[i]);
-      cargs.back().push_back(unres_types[i]);
-    }else if( types[i].isDatatype() ){
-      //add for testers
-      Trace("sygus-grammar-def") << "...add for testers" << std::endl;
-      const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype();
-      for( unsigned k=0; k<dt.getNumConstructors(); k++ ){
-        Trace("sygus-grammar-def") << "...for " << dt[k].getTesterName() << std::endl;
-        ops.back().push_back(dt[k].getTester());
-        cnames.push_back(dt[k].getTesterName());
-        cargs.push_back( std::vector< CVC4::Type >() );
-        cargs.back().push_back(unres_types[i]);
-      }
-    }
-  }
-  if( range==btype ){
-    startIndex = datatypes.size()-1;
-  }
-  Trace("sygus-grammar-def") << "...make datatype " << datatypes.back() << std::endl;
-  datatypes.back().setSygus( btype.toType(), bvl.toExpr(), true, true );
-  for( unsigned j=0; j<ops.back().size(); j++ ){
-    datatypes.back().addSygusConstructor( ops.back()[j], cnames[j], cargs[j] );
-  }
-  //sorts.push_back( btype );
-  Trace("sygus-grammar-def") << "...finished make default grammar for " << fun << " " << range << std::endl;
-  
-  if( startIndex>0 ){
-    CVC4::Datatype tmp_dt = datatypes[0];
-    datatypes[0] = datatypes[startIndex];
-    datatypes[startIndex] = tmp_dt;
-  }
-}
-
-
-TypeNode TermDbSygus::mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, 
-                                          std::map< TypeNode, std::vector< Node > >& extra_cons ) {
-  Trace("sygus-grammar-def") << "*** Make sygus default type " << range << ", make datatypes..." << std::endl;
-  for( std::map< TypeNode, std::vector< Node > >::iterator it = extra_cons.begin(); it != extra_cons.end(); ++it ){
-    Trace("sygus-grammar-def") << "    ...using " << it->second.size() << " extra constants for " << it->first << std::endl;
-  }
-  std::set<Type> unres;
-  std::vector< CVC4::Datatype > datatypes;
-  mkSygusDefaultGrammar( range, bvl, fun, extra_cons, datatypes, unres );
-  Trace("sygus-grammar-def")  << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl;
-  Assert( !datatypes.empty() );
-  std::vector<DatatypeType> types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres);
-  Assert( types.size()==datatypes.size() );
-  return TypeNode::fromType( types[0] );
-}
-
-TypeNode TermDbSygus::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 ) );
-    return templ_arg_sygus_type;
-  }else{
-    tcount++;
-    std::set<Type> unres;
-    std::vector< CVC4::Datatype > datatypes;
-    std::stringstream ssd;
-    ssd << fun << "_templ_" << tcount;
-    std::string dbname = ssd.str();
-    datatypes.push_back(Datatype(dbname));
-    Node op;
-    std::vector< Type > argTypes;
-    if( templ.getNumChildren()==0 ){
-      // TODO : can short circuit to this case when !TermDb::containsTerm( templ, templ_arg )
-      op = templ;
-    }else{
-      Assert( templ.hasOperator() );
-      op = templ.getOperator();
-      // make constructor taking arguments types from children
-      for( unsigned i=0; i<templ.getNumChildren(); i++ ){
-        //recursion depth bound by the depth of SyGuS template expressions (low)
-        TypeNode tnc = mkSygusTemplateTypeRec( templ[i], templ_arg, templ_arg_sygus_type, bvl, fun, tcount );
-        argTypes.push_back( tnc.toType() );
-      }
-    }
-    std::stringstream ssdc;
-    ssdc << fun << "_templ_cons_" << tcount;
-    std::string cname = ssdc.str();
-    // we have a single sygus constructor that encodes the template
-    datatypes.back().addSygusConstructor( op.toExpr(), cname, argTypes );
-    datatypes.back().setSygus( templ.getType().toType(), bvl.toExpr(), true, true );
-    std::vector<DatatypeType> types = NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(datatypes, unres);
-    Assert( types.size()==1 );
-    return TypeNode::fromType( types[0] );
-  }
-}
-
-TypeNode TermDbSygus::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 );
-}
-
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/term_database_sygus.h b/src/theory/quantifiers/term_database_sygus.h
index 0ddfbaa75..8f55f55bd 100644
--- a/src/theory/quantifiers/term_database_sygus.h
+++ b/src/theory/quantifiers/term_database_sygus.h
@@ -295,39 +295,6 @@ private:
   Node extendedRewritePullIte( Node n );
 public:
   Node extendedRewrite( Node n );
-  
-// for grammar construction
-private:
-  // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction)
-  TypeNode mkUnresolvedType(const std::string& name, std::set<Type>& unres);
-  // make the builtin constants for type type that should be included in a sygus grammar
-  void mkSygusConstantsForType( TypeNode type, std::vector<CVC4::Node>& ops );
-  // collect the list of types that depend on type range
-  void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels );
-  // helper function for function mkSygusDefaultGrammar below
-  //   collects a set of mutually recursive datatypes "datatypes" corresponding to encoding type "range" to SyGuS
-  //   unres is used for the resulting call to mkMutualDatatypeTypes
-  void mkSygusDefaultGrammar( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons, 
-                              std::vector< CVC4::Datatype >& datatypes, std::set<Type>& unres );
-  // helper function for mkSygusTemplateType
-  TypeNode mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, 
-                                const std::string& fun, unsigned& tcount );
-public:
-  // make the default sygus datatype type corresponding to builtin type range
-  //   bvl is the set of free variables to include in the grammar
-  //   fun is for naming
-  //   extra_cons is a set of extra constant symbols to include in the grammar
-  TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun, std::map< TypeNode, std::vector< Node > >& extra_cons );
-  // make the default sygus datatype type corresponding to builtin type range
-  TypeNode mkSygusDefaultType( TypeNode range, Node bvl, const std::string& fun ){
-    std::map< TypeNode, std::vector< Node > > extra_cons;
-    return mkSygusDefaultType( range, bvl, fun, extra_cons );
-  }
-  // make the sygus datatype type that encodes the solution space (lambda templ_arg. templ[templ_arg]) where templ_arg
-  // has syntactic restrictions encoded by sygus type templ_arg_sygus_type
-  //   bvl is the set of free variables to include in the frammar
-  //   fun is for naming
-  TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun );
 };
 
 }/* CVC4::theory::quantifiers namespace */