Squashed merge of SygusComp 2015 branch.

12 files changed, 490 insertions, 91 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 5f3498f49..045407bf0 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -70,7 +70,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
 }
 
 void CegConjecture::initializeGuard( QuantifiersEngine * qe ){
-  if( d_guard.isNull() ){
+  if( isAssigned() && d_guard.isNull() ){
     d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
     //specify guard behavior
     d_guard = qe->getValuation().ensureLiteral( d_guard );
@@ -137,6 +137,10 @@ bool CegConjecture::isSingleInvocation() {
   return d_ceg_si->isSingleInvocation();
 }
 
+bool CegConjecture::needsCheck() {
+  return d_active && !d_infeasible && ( !isSingleInvocation() || d_ceg_si->needsCheck() );
+}
+
 CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
   d_conj = new CegConjecture( qe->getSatContext() );
   d_last_inst_si = false;
@@ -155,7 +159,7 @@ void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
     Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl;
     Trace("cegqi-engine-debug") << std::endl;
     Trace("cegqi-engine-debug") << "Current conjecture status : active : " << d_conj->d_active << " feasible : " << !d_conj->d_infeasible << std::endl;
-    if( d_conj->d_active && !d_conj->d_infeasible ){
+    if( d_conj->needsCheck() ){
       checkCegConjecture( d_conj );
     }
     Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl;
@@ -213,29 +217,32 @@ void CegInstantiation::assertNode( Node n ) {
 }
 
 Node CegInstantiation::getNextDecisionRequest() {
-  d_conj->initializeGuard( d_quantEngine );
-  bool value;
-  if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) {
-    //if( d_conj->d_guard_split.isNull() ){
-    //  Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard );
-    //  d_quantEngine->getOutputChannel().lemma( lem );
-    //}
-    Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl;
-    return d_conj->d_guard;
-  }
   //enforce fairness
-  if( d_conj->isAssigned() && d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
-    Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
-    if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) {
-      if( !value ){
-        d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 );
-        lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
-        Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl;
+  if( d_conj->isAssigned() ){
+    d_conj->initializeGuard( d_quantEngine );
+    bool value;
+    if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) {
+      //if( d_conj->d_guard_split.isNull() ){
+      //  Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard );
+      //  d_quantEngine->getOutputChannel().lemma( lem );
+      //}
+      Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl;
+      return d_conj->d_guard;
+    }
+    
+    if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){
+      Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
+      if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) {
+        if( !value ){
+          d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 );
+          lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
+          Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl;
+          return lit;
+        }
+      }else{
+        Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl;
         return lit;
       }
-    }else{
-      Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl;
-      return lit;
     }
   }
 
@@ -484,7 +491,8 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le
 }
 
 void CegInstantiation::printSynthSolution( std::ostream& out ) {
-  if( d_conj ){
+  if( d_conj->isAssigned() ){
+    Trace("cegqi-debug") << "Printing synth solution..." << std::endl;
     //if( !(Trace.isOn("cegqi-stats")) ){
     //  out << "Solution:" << std::endl;
     //}
@@ -530,6 +538,8 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
         out << ")" << std::endl;
       }
     }
+  }else{
+    Assert( false );
   }
 }
 
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 74e9b0aba..5f393626c 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -83,6 +83,8 @@ public:  //for fairness
   CegqiFairMode getCegqiFairMode();
   /** is single invocation */
   bool isSingleInvocation();
+  /** needs check */
+  bool needsCheck();
 };
 
 
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 0a434e4ca..b7bbf8a93 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -742,29 +742,38 @@ CegConjectureSingleInv::CegConjectureSingleInv( CegConjecture * p ) : d_parent(
   d_sol = NULL;
   d_c_inst_match_trie = NULL;
   d_cinst = NULL;
+  d_has_ites = true;
 }
 
 Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) {
   if( !d_single_inv.isNull() ) {
-    Assert( d_single_inv.getKind()==FORALL );
     d_single_inv_var.clear();
     d_single_inv_sk.clear();
-    for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
-      std::stringstream ss;
-      ss << "k_" << d_single_inv[0][i];
-      Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" );
-      d_single_inv_var.push_back( d_single_inv[0][i] );
-      d_single_inv_sk.push_back( k );
-      d_single_inv_sk_index[k] = i;
+    Node inst;
+    if( d_single_inv.getKind()==FORALL ){
+      for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
+        std::stringstream ss;
+        ss << "k_" << d_single_inv[0][i];
+        Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" );
+        d_single_inv_var.push_back( d_single_inv[0][i] );
+        d_single_inv_sk.push_back( k );
+        d_single_inv_sk_index[k] = i;
+      }
+      inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
+    }else{
+      inst = d_single_inv;
     }
-    Node inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
     inst = TermDb::simpleNegate( inst );
     Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl;
 
     //initialize the instantiator for this
-    CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this );
-    d_cinst = new CegInstantiator( d_qe, cosi );
-    d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
+    if( !d_single_inv_sk.empty() ){
+      CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this );
+      d_cinst = new CegInstantiator( d_qe, cosi );
+      d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() );
+    }else{
+      d_cinst = NULL;
+    }
 
     return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst );
   }else{
@@ -790,6 +799,14 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
   std::map< Node, std::map< Node, bool > > contains;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     progs.push_back( q[0][i] );
+    //check whether all types have ITE
+    TypeNode tn = q[0][i].getType();
+    d_qe->getTermDatabaseSygus()->registerSygusType( tn );
+    if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){
+      if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){
+        d_has_ites = false;
+      }
+    }
   }
   //collect information about conjunctions
   bool singleInvocation = false;
@@ -881,8 +898,10 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
       //construct the single invocation version of the property
       Trace("cegqi-si") << "Single invocation formula conjuncts are : " << std::endl;
       //std::vector< Node > si_conj;
-      Assert( !pbvs.empty() );
-      Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
+      Node pbvl;
+      if( !pbvs.empty() ){
+        pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs );
+      }
       for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){
         //should hold since we prevent miniscoping
         Assert( d_single_inv.isNull() );
@@ -978,9 +997,14 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
 
         if( singleInvocation ){
           Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts );
-          d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
+          if( pbvl.isNull() ){
+            d_single_inv = bd;
+          }else{
+            d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
+          }
           Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl;
-          if( options::eMatching.wasSetByUser() ){
+          /*
+          if( options::eMatching() && options::eMatching.wasSetByUser() ){
             Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv );
             std::vector< Node > patTerms;
             std::vector< Node > exclude;
@@ -992,6 +1016,7 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
               }
             }
           }
+          */
         }
       }
     }
@@ -999,9 +1024,68 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) {
   if( !singleInvocation ){
     Trace("cegqi-si") << "Property is not single invocation." << std::endl;
     if( options::cegqiSingleInvAbort() ){
-      Message() << "Property is not single invocation." << std::endl;
+      Notice() << "Property is not single invocation." << std::endl;
       exit( 0 );
     }
+  }else{
+    if( options::cegqiSingleInvPreRegInst() && d_single_inv.getKind()==FORALL ){
+      Trace("cegqi-si-presolve") << "Check " << d_single_inv << std::endl;
+      //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing
+      std::vector< Node > vars;
+      std::map< Node, std::vector< Node > > teq;
+      for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){
+        vars.push_back( d_single_inv[0][i] );
+        teq[d_single_inv[0][i]].clear();
+      }
+      collectPresolveEqTerms( d_single_inv[1], teq );
+      std::vector< Node > terms;
+      std::vector< Node > conj;
+      getPresolveEqConjuncts( vars, terms, teq, d_single_inv, conj );
+
+      if( !conj.empty() ){
+        Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
+        Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
+        lem = NodeManager::currentNM()->mkNode( OR, g, lem );
+        d_qe->getOutputChannel().lemma( lem, false, true );
+      }
+    }
+  }
+}
+
+void CegConjectureSingleInv::collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ) {
+  if( n.getKind()==EQUAL ){
+    for( unsigned i=0; i<2; i++ ){
+      std::map< Node, std::vector< Node > >::iterator it = teq.find( n[i] );
+      if( it!=teq.end() ){
+        Node nn = n[ i==0 ? 1 : 0 ];
+        if( std::find( it->second.begin(), it->second.end(), nn )==it->second.end() ){
+          it->second.push_back( nn );
+          Trace("cegqi-si-presolve") << "  - " << n[i] << " = " << nn << std::endl;
+        }
+      }
+    }
+  }
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    collectPresolveEqTerms( n[i], teq );
+  }
+}
+
+void CegConjectureSingleInv::getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms,
+                                                     std::map< Node, std::vector< Node > >& teq, Node f, std::vector< Node >& conj ) {
+  if( conj.size()<1000 ){
+    if( terms.size()==f[0].getNumChildren() ){
+      Node c = f[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
+      conj.push_back( c );
+    }else{
+      unsigned i = terms.size();
+      Node v = f[0][i];
+      terms.push_back( Node::null() );
+      for( unsigned j=0; j<teq[v].size(); j++ ){
+        terms[i] = teq[v][j];
+        getPresolveEqConjuncts( vars, terms, teq, f, conj );
+      }
+      terms.pop_back();
+    }
   }
 }
 
@@ -1171,8 +1255,7 @@ bool CegConjectureSingleInv::addLemma( Node n ) {
 }
 
 void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
-  if( !d_single_inv.isNull() ) {
-    Assert( d_cinst!=NULL );
+  if( !d_single_inv.isNull() && d_cinst!=NULL ) {
     d_curr_lemmas.clear();
     //check if there are delta lemmas
     d_cinst->getDeltaLemmas( lems );
@@ -1186,20 +1269,61 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
   }
 }
 
-Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) {
+Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index ) {
   Assert( index<d_inst.size() );
   Assert( i<d_inst[index].size() );
+  unsigned uindex = indices[index];
   if( index==d_inst.size()-1 ){
-    return d_inst[index][i];
+    return d_inst[uindex][i];
   }else{
-    Node cond = d_lemmas_produced[index];
+    Node cond = d_lemmas_produced[uindex];
     cond = TermDb::simpleNegate( cond );
-    Node ite1 = d_inst[index][i];
-    Node ite2 = constructSolution( i, index+1 );
+    Node ite1 = d_inst[uindex][i];
+    Node ite2 = constructSolution( indices, i, index+1 );
     return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 );
   }
 }
 
+//TODO: use term size?
+struct sortSiInstanceIndices {
+  CegConjectureSingleInv* d_ccsi;
+  int d_i;
+  bool operator() (unsigned i, unsigned j) {
+    if( d_ccsi->d_inst[i][d_i].isConst() && !d_ccsi->d_inst[j][d_i].isConst() ){
+      return true;
+    }else{
+      return false;
+    }
+  }
+};
+
+/*
+Node removeBooleanIte( Node n ){
+  if( n.getKind()==ITE && n.getType().isBoolean() ){
+    Node n1 = removeBooleanIte( n[1] );
+    Node n2 = removeBooleanIte( n[2] );
+    return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n[0], n1 ),
+                                                 NodeManager::currentNM()->mkNode( AND, n[0].negate(), n2 ) );
+  }else{
+    bool childChanged = false;
+    std::vector< Node > children;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      Node nn = removeBooleanIte( n[i] );
+      children.push_back( nn );
+      childChanged = childChanged || nn!=n[i];
+    }
+    if( childChanged ){
+      if( n.hasOperator() ){
+        children.insert( children.begin(), n.getOperator() );
+      }
+      return NodeManager::currentNM()->mkNode( n.getKind(), children );
+    }else{
+      return n;
+    }
+  }
+}
+*/
+
 Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ){
   Assert( d_sol!=NULL );
   Assert( !d_lemmas_produced.empty() );
@@ -1225,7 +1349,21 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
     d_sol->d_varList.push_back( varList[i-1] );
   }
   //construct the solution
-  Node s = constructSolution( sol_index, 0 );
+  Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl;
+  Assert( d_lemmas_produced.size()==d_inst.size() );
+  std::vector< unsigned > indices;
+  for( unsigned i=0; i<d_lemmas_produced.size(); i++ ){
+    Assert( sol_index<d_inst[i].size() );
+    indices.push_back( i );
+  }
+  //sort indices based on heuristic : currently, do all constant returns first (leads to simpler conditions)
+  // TODO : to minimize solution size, put the largest term last
+  sortSiInstanceIndices ssii;
+  ssii.d_ccsi = this;
+  ssii.d_i = sol_index;
+  std::sort( indices.begin(), indices.end(), ssii );
+  Trace("csi-sol") << "Construct solution" << std::endl;
+  Node s = constructSolution( indices, sol_index, 0 );
   s = s.substitute( vars.begin(), vars.end(), d_varList.begin(), d_varList.end() );
   d_orig_solution = s;
 
@@ -1242,6 +1380,10 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
     if( reconstructed==1 ){
       Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl;
     }
+  }else{
+    ////remove boolean ITE (not allowed for sygus comp 2015)
+    //d_solution = removeBooleanIte( d_solution );
+    //Trace("csi-sol") << "Solution (after remove boolean ITE) : " << d_solution << std::endl;
   }
 
 
@@ -1278,4 +1420,13 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
   }
 }
 
+bool CegConjectureSingleInv::needsCheck() {
+  if( options::cegqiSingleInvMultiInstAbort() ){
+    if( !hasITEs() ){
+      return d_inst.empty();
+    }
+  }
+  return true;
+}
+
 }
\ No newline at end of file
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index eb33c479e..f8e3879ac 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -111,8 +111,11 @@ private:
   bool processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals );
   bool doVariableElimination( Node v, std::vector< Node >& conjuncts );
   bool getVariableEliminationTerm( bool pol, bool active, Node v, Node n, TNode& s, int& status );
+  //presolve
+  void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq );
+  void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj );
   //constructing solution
-  Node constructSolution( unsigned i, unsigned index );
+  Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index );
 private:
   //map from programs to variables in single invocation property
   std::map< Node, Node > d_single_inv_map;
@@ -127,8 +130,6 @@ private:
   //list of skolems for each program
   std::vector< Node > d_single_inv_var;
   //lemmas produced
-  std::vector< Node > d_lemmas_produced;
-  std::vector< std::vector< Node > > d_inst;
   inst::InstMatchTrie d_inst_match_trie;
   inst::CDInstMatchTrie * d_c_inst_match_trie;
   // solution
@@ -136,6 +137,11 @@ private:
   Node d_orig_solution;
   Node d_solution;
   Node d_sygus_solution;
+  bool d_has_ites;
+public:
+  //lemmas produced
+  std::vector< Node > d_lemmas_produced;
+  std::vector< std::vector< Node > > d_inst; 
 private:
   std::vector< Node > d_curr_lemmas;
   //add instantiation
@@ -159,8 +165,12 @@ public:
   void check( std::vector< Node >& lems );
   //get solution
   Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed );
+  // has ites
+  bool hasITEs() { return d_has_ites; }
   // is single invocation
   bool isSingleInvocation() { return !d_single_inv.isNull(); }
+  //needs check
+  bool needsCheck();
 };
 
 }
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index 0429abac9..413fd9ba2 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -86,8 +86,11 @@ Node CegConjectureSingleInvSol::pullITEs( Node s ) {
         Trace("csi-sol-debug") << "For " << s << ", can pull " << cond << " -> " << t << " with remainder " << rem << std::endl;
         t = pullITEs( t );
         rem = pullITEs( rem );
+        Trace("csi-pull-ite") << "PI: Rewrite : " << s << std::endl;
+        Node prev = s;
         s = NodeManager::currentNM()->mkNode( ITE, TermDb::simpleNegate( cond ), t, rem );
-        //Trace("csi-debug-sol") << "Now : " << s << std::endl;
+        Trace("csi-pull-ite") << "PI: Rewrite Now : " << s << std::endl;
+        Trace("csi-pull-ite") << "(= " << prev << " " << s << ")" << std::endl;
         success = true;
       }
     }while( success );
@@ -99,11 +102,13 @@ Node CegConjectureSingleInvSol::pullITEs( Node s ) {
 bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::vector< Node >& conj, Node& t, Node& rem, int depth ) {
   Assert( n_ite.getKind()==ITE );
   std::vector< Node > curr_conj;
+  std::vector< Node > orig_conj;
   bool isAnd;
   if( n_ite[0].getKind()==AND || n_ite[0].getKind()==OR ){
     isAnd = n_ite[0].getKind()==AND;
     for( unsigned i=0; i<n_ite[0].getNumChildren(); i++ ){
       Node cond = n_ite[0][i];
+      orig_conj.push_back( cond );
       if( n_ite[0].getKind()==OR ){
         cond = TermDb::simpleNegate( cond );
       }
@@ -112,12 +117,15 @@ bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::ve
   }else{
     Node neg = n_ite[0].negate();
     if( std::find( conj.begin(), conj.end(), neg )!=conj.end() ){
+      //if negation of condition exists, use it
       isAnd = false;
       curr_conj.push_back( neg );
     }else{
+      //otherwise, use condition
       isAnd = true;
       curr_conj.push_back( n_ite[0] );
     }
+    orig_conj.push_back( n_ite[0] );
   }
   // take intersection with current conditions
   std::vector< Node > new_conj;
@@ -162,13 +170,14 @@ bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::ve
     //make remainder : strip out conditions in conj
     Assert( !conj.empty() );
     std::vector< Node > cond_c;
+    Assert( orig_conj.size()==curr_conj.size() );
     for( unsigned i=0; i<curr_conj.size(); i++ ){
       if( std::find( conj.begin(), conj.end(), curr_conj[i] )==conj.end() ){
-        cond_c.push_back( curr_conj[i] );
+        cond_c.push_back( orig_conj[i] );
       }
     }
     if( cond_c.empty() ){
-      rem = isAnd ? tval : rem;
+      rem = tval;
     }else{
       Node new_cond = cond_c.size()==1 ? cond_c[0] : NodeManager::currentNM()->mkNode( n_ite[0].getKind(), cond_c );
       rem = NodeManager::currentNM()->mkNode( ITE, new_cond, isAnd ? tval : rem, isAnd ? rem : tval );
@@ -437,7 +446,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st
               ret = NodeManager::currentNM()->mkNode( ITE, exp_c, ret[1], ret[2] );
             }
             if( !d_qe->getTermDatabaseSygus()->hasKind( stnc[0], ret[0].getKind() ) ){
-              Trace("csi-sol") << "Flatten based on " << ret[0] << "." << std::endl;
+              Trace("csi-simp-debug") << "Flatten based on " << ret[0] << "." << std::endl;
               ret = flattenITEs( ret, false );
             }
           }
@@ -510,7 +519,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st
       }
       if( !new_vars.empty() ){
         if( !inc.empty() ){
-          Node ret = inc.size()==1 ? sol[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc );
+          Node ret = inc.size()==1 ? inc[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc );
           Trace("csi-simp") << "Base return is : " << ret << std::endl;
           // apply substitution
           ret = ret.substitute( new_vars.begin(), new_vars.end(), new_subs.begin(), new_subs.end() );
@@ -848,12 +857,10 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in
                     }
                   }while( !new_t.isNull() );
                 }
+                //get decompositions
                 for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
                   Kind k = d_qe->getTermDatabaseSygus()->getArgKind( stn, i );
-                  if( k==AND || k==OR ){
-                    equiv.push_back( NodeManager::currentNM()->mkNode( k, min_t, min_t ) );
-                    equiv.push_back( NodeManager::currentNM()->mkNode( k, min_t, NodeManager::currentNM()->mkConst( k==AND ) ) );
-                  }
+                  getEquivalentTerms( k, min_t, equiv );
                 }
                 //assign ids to terms
                 Trace("csi-rcons-debug") << "Term " << id << " is equivalent to " << equiv.size() << " terms : " << std::endl;
@@ -1046,4 +1053,62 @@ void CegConjectureSingleInvSol::setReconstructed( int id, Node n ) {
   }
 }
 
+void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv ) {
+  if( k==AND || k==OR ){
+    equiv.push_back( NodeManager::currentNM()->mkNode( k, n, n ) );
+    equiv.push_back( NodeManager::currentNM()->mkNode( k, n, NodeManager::currentNM()->mkConst( k==AND ) ) );
+  }
+  //multiplication for integers
+  //TODO for bitvectors
+  Kind mk = ( k==PLUS || k==MINUS ) ? MULT : UNDEFINED_KIND;
+  if( mk!=UNDEFINED_KIND ){
+    if( n.getKind()==mk && n[0].isConst() && n[0].getType().isInteger() ){
+      bool success = true;
+      for( unsigned i=0; i<2; i++ ){
+        Node eq;
+        if( k==PLUS || k==MINUS ){
+          Node oth = NodeManager::currentNM()->mkConst( Rational(i==0 ? 1000 : -1000) );
+          eq = i==0 ? NodeManager::currentNM()->mkNode( LEQ, n[0], oth ) : NodeManager::currentNM()->mkNode( GEQ, n[0], oth );
+        }
+        if( !eq.isNull() ){
+          eq = Rewriter::rewrite( eq );
+          if( eq!=d_qe->getTermDatabase()->d_true ){
+            success = false;
+            break;
+          }
+        }
+      }
+      if( success ){
+        Node var = n[1];
+        Node rem;
+        if( k==PLUS || k==MINUS ){
+          int rem_coeff = (int)n[0].getConst<Rational>().getNumerator().getSignedInt();
+          if( rem_coeff>0 && k==PLUS ){
+            rem_coeff--;
+          }else if( rem_coeff<0 && k==MINUS ){
+            rem_coeff++;
+          }else{
+            success = false;
+          }
+          if( success ){
+            rem = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(rem_coeff) ), var );
+            rem = Rewriter::rewrite( rem );
+          }
+        }
+        if( !rem.isNull() ){
+          equiv.push_back( NodeManager::currentNM()->mkNode( k, rem, var ) );
+        }
+      }
+    }
+  }
+  //negative constants
+  if( k==MINUS ){
+    if( n.isConst() && n.getType().isInteger() && n.getConst<Rational>().getNumerator().strictlyNegative() ){
+      Node nn = NodeManager::currentNM()->mkNode( UMINUS, n );
+      nn = Rewriter::rewrite( nn );
+      equiv.push_back( NodeManager::currentNM()->mkNode( MINUS, NodeManager::currentNM()->mkConst( Rational(0) ), nn ) );
+    }
+  }  
+}
+  
 }
diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.h b/src/theory/quantifiers/ce_guided_single_inv_sol.h
index 6a4b6f90f..1d84986b4 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.h
@@ -78,6 +78,8 @@ private:
   bool collectReconstructNodes( int pid, std::vector< Node >& ts, const DatatypeConstructor& dtc, std::vector< int >& ids, int& status );
   bool getPathToRoot( int id );
   void setReconstructed( int id, Node n );
+  //get equivalent terms to n with top symbol k
+  void getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv );
 public:
   Node reconstructSolution( Node sol, TypeNode stn, int& reconstructed );
 public:
diff --git a/src/theory/quantifiers/fun_def_engine.cpp b/src/theory/quantifiers/fun_def_engine.cpp
new file mode 100644
index 000000000..56214f540
--- /dev/null
+++ b/src/theory/quantifiers/fun_def_engine.cpp
@@ -0,0 +1,54 @@
+/*********************                                                        */
+/*! \file fun_def_process.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** This class implements specialized techniques for (recursively) defined functions
+ **/
+
+#include <vector>
+
+#include "theory/quantifiers/fun_def_engine.h"
+#include "theory/rewriter.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace CVC4;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+FunDefEngine::FunDefEngine( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ) {
+  
+}
+
+/* whether this module needs to check this round */
+bool FunDefEngine::needsCheck( Theory::Effort e ) { 
+  return e>=Theory::EFFORT_LAST_CALL; 
+}
+
+/* reset at a round */
+void FunDefEngine::reset_round( Theory::Effort e ){
+  //TODO
+}
+
+/* Call during quantifier engine's check */
+void FunDefEngine::check( Theory::Effort e, unsigned quant_e ) {
+  //TODO
+}
+
+/* Called for new quantifiers */
+void FunDefEngine::registerQuantifier( Node q ) {
+  //TODO
+}
+
+/** called for everything that gets asserted */
+void FunDefEngine::assertNode( Node n ) {
+  //TODO
+}
diff --git a/src/theory/quantifiers/fun_def_engine.h b/src/theory/quantifiers/fun_def_engine.h
new file mode 100644
index 000000000..be73d51a9
--- /dev/null
+++ b/src/theory/quantifiers/fun_def_engine.h
@@ -0,0 +1,59 @@
+/*********************                                                        */
+/*! \file fun_def_engine.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Specialized techniques for (recursively) defined functions
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANTIFIERS_FUN_DEF_ENGINE_H
+#define __CVC4__QUANTIFIERS_FUN_DEF_ENGINE_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+//module for handling (recursively) defined functions
+class FunDefEngine : public QuantifiersModule {
+private:
+
+public:
+  FunDefEngine( QuantifiersEngine * qe, context::Context* c );
+  ~FunDefEngine(){}
+
+  /* whether this module needs to check this round */
+  bool needsCheck( Theory::Effort e );
+  /* reset at a round */
+  void reset_round( Theory::Effort e );
+  /* Call during quantifier engine's check */
+  void check( Theory::Effort e, unsigned quant_e );
+  /* Called for new quantifiers */
+  void registerQuantifier( Node q );
+  /** called for everything that gets asserted */
+  void assertNode( Node n );
+  /** Identify this module (for debugging, dynamic configuration, etc..) */
+  std::string identify() const { return "FunDefEngine"; }
+};
+
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 391abe9eb..ab0526471 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -220,8 +220,12 @@ option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true
   reconstruct solutions for single invocation conjectures in original grammar
 option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true
   include constants when reconstruct solutions for single invocation conjectures in original grammar
+option cegqiSingleInvPreRegInst --cegqi-si-prereg-inst bool :default true
+  preregister ground instantiations when single invocation
 option cegqiSingleInvAbort --cegqi-si-abort bool :default false
-  abort if our synthesis conjecture is not single invocation
+  abort if synthesis conjecture is not single invocation
+option cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false
+  abort if synthesis conjecture is single invocation with no ITE in grammar and multiple instantiations are tried
   
 option sygusNormalForm --sygus-nf bool :default true
   only search for sygus builtin terms that are in normal form
@@ -259,5 +263,10 @@ option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false
 
 option quantAlphaEquiv --quant-alpha-equiv bool :default true
   infer alpha equivalence between quantified formulas
+
+### recursive function options
+
+#option funDefs --fun-defs bool :default false
+#  enable specialized techniques for recursive function definitions
  
 endmodule
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 0198e014f..6a95e243d 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -905,7 +905,21 @@ Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >&
 
 Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){
   std::vector< Node > activeArgs;
-  computeArgVec2( args, activeArgs, body, ipl );
+  //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables 
+  if( options::ceGuidedInst() && !ipl.isNull() ){
+    for( unsigned i=0; i<ipl.getNumChildren(); i++ ){
+      Trace("quant-attr-debug") << "Check : " << ipl[i] << " " << ipl[i].getKind() << std::endl;
+      if( ipl[i].getKind()==INST_ATTRIBUTE ){
+        Node avar = ipl[i][0];
+        if( avar.getAttribute(SygusAttribute()) ){
+          activeArgs.insert( activeArgs.end(), args.begin(), args.end() );
+        }
+      }
+    }
+  }
+  if( activeArgs.empty() ){
+    computeArgVec2( args, activeArgs, body, ipl );
+  }
   if( activeArgs.empty() ){
     return body;
   }else{
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index cc8ae4db0..fa0e211b3 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -23,6 +23,7 @@
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/rewrite_engine.h"
+#include "theory/quantifiers/fun_def_engine.h"
 
 //for sygus
 #include "theory/bv/theory_bv_utils.h"
@@ -1431,6 +1432,7 @@ void TermDb::computeAttributes( Node q ) {
             exit( 0 );
           }
           d_fun_defs[f] = true;
+          d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine() );
         }
         if( avar.getAttribute(SygusAttribute()) ){
           //not necessarily nested existential
@@ -1578,7 +1580,7 @@ TNode TermDbSygus::getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count
   }
 }
 
-TypeNode TermDbSygus::getSygusType( Node v ) {
+TypeNode TermDbSygus::getSygusTypeForVar( Node v ) {
   Assert( d_fv_stype.find( v )!=d_fv_stype.end() );
   return d_fv_stype[v];
 }
@@ -1740,7 +1742,7 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int
       Node n = NodeManager::currentNM()->mkNode( APPLY, children );
       //must expand definitions
       Node ne = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( n.toExpr() ) );
-      Trace("sygus-util-debug") << "Expanded definitions in " << n << " to " << ne << std::endl;
+      Trace("sygus-db-debug") << "Expanded definitions in " << n << " to " << ne << std::endl;
       return ne;
       */
     }
@@ -2093,10 +2095,10 @@ void TermDbSygus::registerSygusType( TypeNode tn ){
       d_register[tn] = TypeNode::null();
     }else{
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      Trace("sygus-util") << "Register type " << dt.getName() << "..." << std::endl;
+      Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl;
       d_register[tn] = TypeNode::fromType( dt.getSygusType() );
       if( d_register[tn].isNull() ){
-        Trace("sygus-util") << "...not sygus." << std::endl;
+        Trace("sygus-db") << "...not sygus." << std::endl;
       }else{
         //for constant reconstruction
         Kind ck = getComparisonKind( TypeNode::fromType( dt.getSygusType() ) );
@@ -2107,14 +2109,14 @@ void TermDbSygus::registerSygusType( TypeNode tn ){
           Expr sop = dt[i].getSygusOp();
           Assert( !sop.isNull() );
           Node n = Node::fromExpr( sop );
-          Trace("sygus-util") << "  Operator #" << i << " : " << sop;
+          Trace("sygus-db") << "  Operator #" << i << " : " << sop;
           if( sop.getKind() == kind::BUILTIN ){
             Kind sk = NodeManager::operatorToKind( n );
-            Trace("sygus-util") << ", kind = " << sk;
+            Trace("sygus-db") << ", kind = " << sk;
             d_kinds[tn][sk] = i;
             d_arg_kind[tn][i] = sk;
           }else if( sop.isConst() ){
-            Trace("sygus-util") << ", constant";
+            Trace("sygus-db") << ", constant";
             d_consts[tn][n] = i;
             d_arg_const[tn][i] = n;
             d_const_list[tn].push_back( n );
@@ -2127,7 +2129,7 @@ void TermDbSygus::registerSygusType( TypeNode tn ){
           }
           d_ops[tn][n] = i;
           d_arg_ops[tn][i] = n;
-          Trace("sygus-util") << std::endl;
+          Trace("sygus-db") << std::endl;
         }
         //sort the constant list
         if( !d_const_list[tn].empty() ){
@@ -2137,12 +2139,12 @@ void TermDbSygus::registerSygusType( TypeNode tn ){
             sc.d_tds = this;
             std::sort( d_const_list[tn].begin(), d_const_list[tn].end(), sc );
           }
-          Trace("sygus-util") << "Type has " << d_const_list[tn].size() << " constants..." << std::endl << "  ";
+          Trace("sygus-db") << "Type has " << d_const_list[tn].size() << " constants..." << std::endl << "  ";
           for( unsigned i=0; i<d_const_list[tn].size(); i++ ){
-            Trace("sygus-util") << d_const_list[tn][i] << " ";
+            Trace("sygus-db") << d_const_list[tn][i] << " ";
           }
-          Trace("sygus-util") << std::endl;
-          Trace("sygus-util") << "Of these, " << d_const_list_pos[tn] << " are marked as positive." << std::endl;
+          Trace("sygus-db") << std::endl;
+          Trace("sygus-db") << "Of these, " << d_const_list_pos[tn] << " are marked as positive." << std::endl;
         }
         //register connected types
         for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
@@ -2159,6 +2161,11 @@ bool TermDbSygus::isRegistered( TypeNode tn ) {
   return d_register.find( tn )!=d_register.end();
 }
 
+TypeNode TermDbSygus::sygusToBuiltinType( TypeNode tn ) {
+  Assert( isRegistered( tn ) );
+  return d_register[tn];
+}
+
 int TermDbSygus::getKindArg( TypeNode tn, Kind k ) {
   Assert( isRegistered( tn ) );
   std::map< TypeNode, std::map< Kind, int > >::iterator itt = d_kinds.find( tn );
@@ -2348,6 +2355,7 @@ bool TermDbSygus::doCompare( Node a, Node b, Kind k ) {
   return com==d_true;
 }
 
+
 void doStrReplace(std::string& str, const std::string& oldStr, const std::string& newStr){
   size_t pos = 0;
   while((pos = str.find(oldStr, pos)) != std::string::npos){
@@ -2367,7 +2375,20 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
         if( n.getNumChildren()>0 ){
           out << "(";
         }
-        out << dt[cIndex].getSygusOp();
+        Node op = dt[cIndex].getSygusOp();
+        if( op.getType().isBitVector() && op.isConst() ){
+          //print in the style it was given
+          Trace("sygus-print-bvc") << "[Print " << op << " " << dt[cIndex].getName() << "]" << std::endl;
+          std::stringstream ss;
+          ss << dt[cIndex].getName();
+          std::string str = ss.str();
+          std::size_t found = str.find_last_of("_");
+          Assert( found!=std::string::npos );
+          std::string name = std::string( str.begin() + found +1, str.end() );
+          out << name;
+        }else{
+          out << op;
+        }
         if( n.getNumChildren()>0 ){
           for( unsigned i=0; i<n.getNumChildren(); i++ ){
             out << " ";
@@ -2376,9 +2397,10 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
           out << ")";
         }
       }else{
+        std::stringstream let_out;
         //print as let term
         if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
-          out << "(let (";
+          let_out << "(let (";
         }
         std::vector< Node > subs_lvs;
         std::vector< Node > new_lvs;
@@ -2392,22 +2414,25 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
           //map free variables to proper terms
           if( i<dt[cIndex].getNumSygusLetInputArgs() ){
             //it should be printed as a let argument
-            out << "(";
-            out << lv << " " << lv.getType() << " ";
-            printSygusTerm( out, n[i], lvs );
-            out << ")";
+            let_out << "(";
+            let_out << lv << " " << lv.getType() << " ";
+            printSygusTerm( let_out, n[i], lvs );
+            let_out << ")";
           }
         }
         if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
-          out << ") ";
+          let_out << ") ";
         }
         //print the body
         Node let_body = Node::fromExpr( dt[cIndex].getSygusLetBody() );
         let_body = let_body.substitute( subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end() );
         new_lvs.insert( new_lvs.end(), lvs.begin(), lvs.end() );
-        std::stringstream body_out;
-        printSygusTerm( body_out, let_body, new_lvs );
-        std::string body = body_out.str();
+        printSygusTerm( let_out, let_body, new_lvs );
+        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
+          let_out << ")";
+        }
+        //do variable substitutions since ASSUMING : let_vars are interpreted literally and do not represent a class of variables
+        std::string lbody = let_out.str();
         for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){
           std::stringstream old_str;
           old_str << new_lvs[i];
@@ -2417,12 +2442,9 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
           }else{
             new_str << Node::fromExpr( dt[cIndex].getSygusLetArg( i ) );
           }
-          doStrReplace( body, old_str.str().c_str(), new_str.str().c_str() );
-        }
-        out << body;
-        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
-          out << ")";
+          doStrReplace( lbody, old_str.str().c_str(), new_str.str().c_str() );
         }
+        out << lbody;
       }
       return;
     }
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index e61552713..1ffe0e29e 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -433,7 +433,7 @@ public:
   bool getMatch( Node n, TypeNode st, int& index_found, std::vector< Node >& args, int index_exc = -1, int index_start = 0 );
 private:
   //information for sygus types
-  std::map< TypeNode, TypeNode > d_register;  //stores sygus type
+  std::map< TypeNode, TypeNode > d_register;  //stores sygus -> builtin type
   std::map< TypeNode, std::map< int, Kind > > d_arg_kind;
   std::map< TypeNode, std::map< Kind, int > > d_kinds;
   std::map< TypeNode, std::map< int, Node > > d_arg_const;
@@ -455,6 +455,7 @@ private:
 public:
   TermDbSygus();
   bool isRegistered( TypeNode tn );
+  TypeNode sygusToBuiltinType( TypeNode tn );
   int getKindArg( TypeNode tn, Kind k );
   int getConstArg( TypeNode tn, Node n );
   int getOpArg( TypeNode tn, Node n );
@@ -485,7 +486,7 @@ public:
   Node getTypeValueOffset( TypeNode tn, Node val, int offset, int& status );
   /** get value */
   Node getTypeMaxValue( TypeNode tn );
-  TypeNode getSygusType( Node v );
+  TypeNode getSygusTypeForVar( Node v );
   Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre );
   Node sygusToBuiltin( Node n, TypeNode tn );
   Node builtinToSygusConst( Node c, TypeNode tn, int rcons_depth = 0 );