(Refactor) Document and clean single invocation partition. (#1364)

* Documenting single invocation partiion.

* More

* More encapsulation.

* More, documentation complete.

* Split to own file.

* Format

* Fully encapsulate.

* Format

* Improvements to doc.

* Format

* Address

* Format

* Missed comment

* Newline

* Address

* Format

8 files changed, 991 insertions, 555 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 75fdd32ae..acd94a90a 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -433,6 +433,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/relevant_domain.h \
 	theory/quantifiers/rewrite_engine.cpp \
 	theory/quantifiers/rewrite_engine.h \
+	theory/quantifiers/single_inv_partition.cpp \
+	theory/quantifiers/single_inv_partition.h \
 	theory/quantifiers/skolemize.cpp \
 	theory/quantifiers/skolemize.h \
 	theory/quantifiers/sygus_explain.cpp \
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d703e8e83..1a35c9901 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -93,6 +93,7 @@
 #include "theory/quantifiers/fun_def_process.h"
 #include "theory/quantifiers/macros.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/single_inv_partition.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/sort_inference.h"
 #include "theory/strings/theory_strings.h"
@@ -4631,14 +4632,18 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) {
         Trace("smt-synth") << "Property is non-ground single invocation, run "
                               "QE to obtain single invocation."
                            << std::endl;
+        NodeManager* nm = NodeManager::currentNM();
         // partition variables
+        std::vector<Node> all_vars;
+        sip.getAllVariables(all_vars);
+        std::vector<Node> si_vars;
+        sip.getSingleInvocationVariables(si_vars);
         std::vector<Node> qe_vars;
         std::vector<Node> nqe_vars;
-        for (unsigned i = 0; i < sip.d_all_vars.size(); i++)
+        for (unsigned i = 0, size = all_vars.size(); i < size; i++)
         {
-          Node v = sip.d_all_vars[i];
-          if (std::find(sip.d_si_vars.begin(), sip.d_si_vars.end(), v)
-              == sip.d_si_vars.end())
+          Node v = all_vars[i];
+          if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end())
           {
             qe_vars.push_back(v);
           }
@@ -4652,27 +4657,29 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) {
         // skolemize non-qe variables
         for (unsigned i = 0; i < nqe_vars.size(); i++)
         {
-          Node k = NodeManager::currentNM()->mkSkolem(
-              "k",
-              nqe_vars[i].getType(),
-              "qe for non-ground single invocation");
+          Node k = nm->mkSkolem("k",
+                                nqe_vars[i].getType(),
+                                "qe for non-ground single invocation");
           orig.push_back(nqe_vars[i]);
           subs.push_back(k);
           Trace("smt-synth") << "  subs : " << nqe_vars[i] << " -> " << k
                              << std::endl;
         }
-        for (std::map<Node, bool>::iterator it = sip.d_funcs.begin();
-             it != sip.d_funcs.end();
-             ++it)
+        std::vector<Node> funcs;
+        sip.getFunctions(funcs);
+        for (unsigned i = 0, size = funcs.size(); i < size; i++)
         {
-          orig.push_back(sip.d_func_inv[it->first]);
-          Node k = NodeManager::currentNM()->mkSkolem(
-              "k",
-              sip.d_func_fo_var[it->first].getType(),
-              "qe for function in non-ground single invocation");
+          Node f = funcs[i];
+          Node fi = sip.getFunctionInvocationFor(f);
+          Node fv = sip.getFirstOrderVariableForFunction(f);
+          Assert(!fi.isNull());
+          orig.push_back(fi);
+          Node k =
+              nm->mkSkolem("k",
+                           fv.getType(),
+                           "qe for function in non-ground single invocation");
           subs.push_back(k);
-          Trace("smt-synth") << "  subs : " << sip.d_func_inv[it->first]
-                             << " -> " << k << std::endl;
+          Trace("smt-synth") << "  subs : " << fi << " -> " << k << std::endl;
         }
         Node conj_se_ngsi = sip.getFullSpecification();
         Trace("smt-synth") << "Full specification is " << conj_se_ngsi
@@ -4680,10 +4687,10 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) {
         Node conj_se_ngsi_subs = conj_se_ngsi.substitute(
             orig.begin(), orig.end(), subs.begin(), subs.end());
         Assert(!qe_vars.empty());
-        conj_se_ngsi_subs = NodeManager::currentNM()->mkNode(
-            kind::EXISTS,
-            NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, qe_vars),
-            conj_se_ngsi_subs.negate());
+        conj_se_ngsi_subs =
+            nm->mkNode(kind::EXISTS,
+                       nm->mkNode(kind::BOUND_VAR_LIST, qe_vars),
+                       conj_se_ngsi_subs.negate());
 
         Trace("smt-synth") << "Run quantifier elimination on "
                            << conj_se_ngsi_subs << std::endl;
@@ -4697,14 +4704,12 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) {
             subs.begin(), subs.end(), orig.begin(), orig.end());
         if (!nqe_vars.empty())
         {
-          qe_res_n = NodeManager::currentNM()->mkNode(
-              kind::EXISTS,
-              NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, nqe_vars),
-              qe_res_n);
+          qe_res_n = nm->mkNode(kind::EXISTS,
+                                nm->mkNode(kind::BOUND_VAR_LIST, nqe_vars),
+                                qe_res_n);
         }
         Assert(conj.getNumChildren() == 3);
-        qe_res_n = NodeManager::currentNM()->mkNode(
-            kind::FORALL, conj[0], qe_res_n, conj[2]);
+        qe_res_n = nm->mkNode(kind::FORALL, conj[0], qe_res_n, conj[2]);
         Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n
                            << std::endl;
         e_check = qe_res_n.toExpr();
diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp
index 681c168f2..1303b7627 100644
--- a/src/theory/quantifiers/anti_skolem.cpp
+++ b/src/theory/quantifiers/anti_skolem.cpp
@@ -116,9 +116,15 @@ void QuantAntiSkolem::check(Theory::Effort e, QEffort quant_e)
         }
         if( success ){
           //sort the argument variables
-          d_ask_types[q].insert( d_ask_types[q].end(), d_quant_sip[q].d_arg_types.begin(), d_quant_sip[q].d_arg_types.end() );
+          std::vector<Node> sivars;
+          d_quant_sip[q].getSingleInvocationVariables(sivars);
+          for (const Node& v : sivars)
+          {
+            d_ask_types[q].push_back(v.getType());
+          }
           std::map< TypeNode, std::vector< unsigned > > indices;
-          for( unsigned j=0; j<d_ask_types[q].size(); j++ ){
+          for (unsigned j = 0, size = d_ask_types[q].size(); j < size; j++)
+          {
             indices[d_ask_types[q][j]].push_back( j );
           }
           sortTypeOrder sto;
@@ -165,8 +171,10 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool
       for( unsigned i=0; i<quants.size(); i++ ){
         Node q = quants[i];
         std::vector< int > eqcs;
-        for( std::map< Node, bool >::iterator it = d_quant_sip[q].d_funcs.begin(); it != d_quant_sip[q].d_funcs.end(); ++it ){
-          Node f = it->first;
+        std::vector<Node> funcs;
+        d_quant_sip[q].getFunctions(funcs);
+        for (const Node& f : funcs)
+        {
           std::map< Node, int >::iterator itf = func_to_eqc.find( f );
           if( itf == func_to_eqc.end() ){
             if( eqcs.empty() ){
@@ -222,7 +230,8 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool
     std::vector< Node > outer_vars;
     std::vector< Node > inner_vars;
     Node q = quants[0];
-    for( unsigned i=0; i<d_ask_types[q].size(); i++ ){
+    for (unsigned i = 0, size = d_ask_types[q].size(); i < size; i++)
+    {
       Node v = NodeManager::currentNM()->mkBoundVar( d_ask_types[q][i] );
       Trace("anti-sk-debug") << "Outer var " << i << " : " << v << std::endl;
       outer_vars.push_back( v );
@@ -237,15 +246,22 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool
       std::vector< Node > subs_rhs;
       //get outer variable substitution
       Assert( d_ask_types_index[q].size()==d_ask_types[q].size() );
-      for( unsigned j=0; j<d_ask_types_index[q].size(); j++ ){
-        Trace("anti-sk-debug") << " o_subs : " << d_quant_sip[q].d_si_vars[d_ask_types_index[q][j]] << " -> " << outer_vars[j] << std::endl;
-        subs_lhs.push_back( d_quant_sip[q].d_si_vars[d_ask_types_index[q][j]] );
+      std::vector<Node> sivars;
+      d_quant_sip[q].getSingleInvocationVariables(sivars);
+      for (unsigned j = 0, size = d_ask_types_index[q].size(); j < size; j++)
+      {
+        Trace("anti-sk-debug")
+            << " o_subs : " << sivars[d_ask_types_index[q][j]] << " -> "
+            << outer_vars[j] << std::endl;
+        subs_lhs.push_back(sivars[d_ask_types_index[q][j]]);
         subs_rhs.push_back( outer_vars[j] );
       }
       //get function substitution
-      for( std::map< Node, bool >::iterator it = d_quant_sip[q].d_funcs.begin(); it != d_quant_sip[q].d_funcs.end(); ++it ){
-        Node f = it->first;
-        Node fv = d_quant_sip[q].d_func_fo_var[it->first];
+      std::vector<Node> funcs;
+      d_quant_sip[q].getFunctions(funcs);
+      for (const Node& f : funcs)
+      {
+        Node fv = d_quant_sip[q].getFirstOrderVariableForFunction(f);
         if( func_to_var.find( f )==func_to_var.end() ){
           Node v = NodeManager::currentNM()->mkBoundVar( fv.getType() );
           Trace("anti-sk-debug") << "Inner var for " << f << " : " << v << std::endl;
diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h
index bad98c04b..bf8b99f1c 100644
--- a/src/theory/quantifiers/anti_skolem.h
+++ b/src/theory/quantifiers/anti_skolem.h
@@ -20,11 +20,11 @@
 #include <map>
 #include <vector>
 
-#include "expr/node.h"
-#include "expr/type_node.h"
 #include "context/cdhashset.h"
 #include "context/cdo.h"
-#include "theory/quantifiers/ce_guided_single_inv.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/quantifiers/single_inv_partition.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index c810ed5cf..03026069f 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -14,16 +14,10 @@
  **/
 #include "theory/quantifiers/ce_guided_single_inv.h"
 
-#include "expr/datatype.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
-#include "theory/quantifiers/ce_guided_instantiation.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/term_database_sygus.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/trigger.h"
-#include "theory/theory_engine.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -153,11 +147,11 @@ void CegConjectureSingleInv::initialize( Node q ) {
       std::map< Node, Node > single_inv_app_map;
       for( unsigned j=0; j<progs.size(); j++ ){
         Node prog = progs[j];
-        std::map< Node, Node >::iterator it_fov = d_sip->d_func_fo_var.find( prog );
-        if( it_fov!=d_sip->d_func_fo_var.end() ){
-          Node pv = it_fov->second;
-          Assert( d_sip->d_func_inv.find( prog )!=d_sip->d_func_inv.end() );
-          Node inv = d_sip->d_func_inv[prog];
+        Node pv = d_sip->getFirstOrderVariableForFunction(prog);
+        if (!pv.isNull())
+        {
+          Node inv = d_sip->getFunctionInvocationFor(prog);
+          Assert(!inv.isNull());
           single_inv_app_map[prog] = inv;
           Trace("cegqi-si") << "  " << pv << ", " << inv << " is associated with program " << prog << std::endl;
           d_prog_to_sol_index[prog] = order_vars.size();
@@ -166,14 +160,10 @@ void CegConjectureSingleInv::initialize( Node q ) {
           Trace("cegqi-si") << "  " << prog << " has no fo var." << std::endl;
         }
       }
-      //reorder the variables
-      Assert( d_sip->d_func_vars.size()==order_vars.size() );
-      d_sip->d_func_vars.clear();
-      d_sip->d_func_vars.insert( d_sip->d_func_vars.begin(), order_vars.begin(), order_vars.end() );
-      
 
       //check if it is single invocation
-      if( !d_sip->d_conjuncts[1].empty() ){
+      if (!d_sip->isPurelySingleInvocation())
+      {
         if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){
           //if we are doing invariant templates, then construct the template
           Trace("cegqi-si") << "- Do transition inference..." << std::endl;
@@ -188,17 +178,25 @@ void CegConjectureSingleInv::initialize( Node q ) {
             d_trans_post[prog] = d_ti[q].getComponent( -1 );
             Trace("cegqi-inv") << "   precondition : " << d_trans_pre[prog] << std::endl;
             Trace("cegqi-inv") << "  postcondition : " << d_trans_post[prog] << std::endl;
+            std::vector<Node> sivars;
+            d_sip->getSingleInvocationVariables(sivars);
             Node invariant = single_inv_app_map[prog];
-            invariant = invariant.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), prog_templ_vars.begin(), prog_templ_vars.end() );
+            invariant = invariant.substitute(sivars.begin(),
+                                             sivars.end(),
+                                             prog_templ_vars.begin(),
+                                             prog_templ_vars.end());
             Trace("cegqi-inv") << "      invariant : " << invariant << std::endl;
             
             // store simplified version of quantified formula
-            d_simp_quant = d_sip->d_conjuncts[2].size()==1 ? d_sip->d_conjuncts[2][0] : NodeManager::currentNM()->mkNode( AND, d_sip->d_conjuncts[2] );
+            d_simp_quant = d_sip->getFullSpecification();
             std::vector< Node > new_bv;
-            for( unsigned j=0; j<d_sip->d_si_vars.size(); j++ ){
-              new_bv.push_back( NodeManager::currentNM()->mkBoundVar( d_sip->d_si_vars[j].getType() ) );
+            for (unsigned j = 0, size = sivars.size(); j < size; j++)
+            {
+              new_bv.push_back(
+                  NodeManager::currentNM()->mkBoundVar(sivars[j].getType()));
             }
-            d_simp_quant = d_simp_quant.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), new_bv.begin(), new_bv.end() );
+            d_simp_quant = d_simp_quant.substitute(
+                sivars.begin(), sivars.end(), new_bv.begin(), new_bv.end());
             Assert( q[1].getKind()==NOT && q[1][0].getKind()==FORALL );
             for( unsigned j=0; j<q[1][0][0].getNumChildren(); j++ ){
               new_bv.push_back( q[1][0][0][j] );
@@ -283,17 +281,26 @@ void CegConjectureSingleInv::finishInit( bool syntaxRestricted, bool hasItes ) {
   if( d_single_invocation ){
     d_single_inv = d_sip->getSingleInvocation();
     d_single_inv = TermUtil::simpleNegate( d_single_inv );
-    if( !d_sip->d_func_vars.empty() ){
-      Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, d_sip->d_func_vars );
+    std::vector<Node> func_vars;
+    d_sip->getFunctionVariables(func_vars);
+    if (!func_vars.empty())
+    {
+      Node pbvl = NodeManager::currentNM()->mkNode(BOUND_VAR_LIST, func_vars);
       d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, d_single_inv );
     }
     //now, introduce the skolems
-    for( unsigned i=0; i<d_sip->d_si_vars.size(); i++ ){
-      Node v = NodeManager::currentNM()->mkSkolem( "a", d_sip->d_si_vars[i].getType(), "single invocation arg" );
+    std::vector<Node> sivars;
+    d_sip->getSingleInvocationVariables(sivars);
+    for (unsigned i = 0, size = sivars.size(); i < size; i++)
+    {
+      Node v = NodeManager::currentNM()->mkSkolem(
+          "a", sivars[i].getType(), "single invocation arg");
       d_single_inv_arg_sk.push_back( v );
     }
-    d_single_inv = d_single_inv.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(),
-                                            d_single_inv_arg_sk.begin(), d_single_inv_arg_sk.end() );
+    d_single_inv = d_single_inv.substitute(sivars.begin(),
+                                           sivars.end(),
+                                           d_single_inv_arg_sk.begin(),
+                                           d_single_inv_arg_sk.end());
     Trace("cegqi-si") << "Single invocation formula is : " << d_single_inv << std::endl;
     if( options::cbqiPreRegInst() && d_single_inv.getKind()==FORALL ){
       //just invoke the presolve now
@@ -317,10 +324,9 @@ bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){
   if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){
     siss << "  * single invocation: " << std::endl;
     for( unsigned j=0; j<d_single_inv_sk.size(); j++ ){
-      Assert( d_sip->d_fo_var_to_func.find( d_single_inv[0][j] )!=d_sip->d_fo_var_to_func.end() );
-      Node op = d_sip->d_fo_var_to_func[d_single_inv[0][j]];
-      Node prog = op;
-      siss << "    * " << prog;
+      Node op = d_sip->getFunctionForFirstOrderVariable(d_single_inv[0][j]);
+      Assert(!op.isNull());
+      siss << "    * " << op;
       siss << " (" << d_single_inv_sk[j] << ")";
       siss << " -> " << subs[j] << std::endl;
     }
@@ -616,431 +622,6 @@ void CegConjectureSingleInv::preregisterConjecture( Node q ) {
   d_orig_conjecture = q;
 }
 
-bool SingleInvocationPartition::init( Node n ) {
-  //first, get types of arguments for functions
-  std::vector< TypeNode > typs;
-  std::map< Node, bool > visited;
-  std::vector< Node > funcs;
-  if( inferArgTypes( n, typs, visited ) ){
-    return init( funcs, typs, n, false );
-  }else{
-    Trace("si-prt") << "Could not infer argument types." << std::endl;
-    return false;
-  }
-}
-
-// gets the argument type list for the first APPLY_UF we see
-bool SingleInvocationPartition::inferArgTypes( Node n, std::vector< TypeNode >& typs, std::map< Node, bool >& visited ) {
-  if( visited.find( n )==visited.end() ){
-    visited[n] = true;
-    if( n.getKind()!=FORALL ){
-      if( n.getKind()==APPLY_UF ){
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          typs.push_back( n[i].getType() );
-        }
-        return true;
-      }else{
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          if( inferArgTypes( n[i], typs, visited ) ){
-            return true;
-          }
-        }
-      }
-    }
-  }
-  return false;
-}
-
-bool SingleInvocationPartition::init( std::vector< Node >& funcs, Node n ) {
-  Trace("si-prt") << "Initialize with " << funcs.size() << " input functions..." << std::endl;
-  std::vector< TypeNode > typs;
-  if( !funcs.empty() ){
-    TypeNode tn0 = funcs[0].getType();
-    for( unsigned i=1; i<funcs.size(); i++ ){
-      if( funcs[i].getType()!=tn0 ){
-        // can't anti-skolemize functions of different sort
-        Trace("si-prt") << "...type mismatch" << std::endl;
-        return false;
-      }
-    }
-    if( tn0.getNumChildren()>1 ){
-      for( unsigned j=0; j<tn0.getNumChildren()-1; j++ ){
-        typs.push_back( tn0[j] );
-      }
-    }
-  }
-  Trace("si-prt") << "#types = " << typs.size() << std::endl;
-  return init( funcs, typs, n, true );  
-}
-
-bool SingleInvocationPartition::init( std::vector< Node >& funcs, std::vector< TypeNode >& typs, Node n, bool has_funcs ){
-  Assert( d_arg_types.empty() );
-  Assert( d_input_funcs.empty() );
-  Assert( d_si_vars.empty() );
-  d_has_input_funcs = has_funcs;
-  d_arg_types.insert( d_arg_types.end(), typs.begin(), typs.end() );
-  d_input_funcs.insert( d_input_funcs.end(), funcs.begin(), funcs.end() );
-  Trace("si-prt") << "Initialize..." << std::endl;
-  for( unsigned j=0; j<d_arg_types.size(); j++ ){
-    std::stringstream ss;
-    ss << "s_" << j;
-    Node si_v = NodeManager::currentNM()->mkBoundVar( ss.str(), d_arg_types[j] );
-    d_si_vars.push_back( si_v );
-  }
-  Trace("si-prt") << "Process the formula..." << std::endl;
-  process( n );
-  return true;
-}
-
-
-void SingleInvocationPartition::process( Node n ) {
-  Assert( d_si_vars.size()==d_arg_types.size() );
-  Trace("si-prt") << "SingleInvocationPartition::process " << n << std::endl;
-  Trace("si-prt") << "Get conjuncts..." << std::endl;
-  std::vector< Node > conj;
-  if( collectConjuncts( n, true, conj ) ){
-    Trace("si-prt") << "...success." << std::endl;
-    for( unsigned i=0; i<conj.size(); i++ ){
-      std::vector< Node > si_terms;
-      std::vector< Node > si_subs;
-      Trace("si-prt") << "Process conjunct : " << conj[i] << std::endl;
-      //do DER on conjunct
-      Node cr = TermUtil::getQuantSimplify( conj[i] );
-      if( cr!=conj[i] ){
-        Trace("si-prt-debug") << "...rewritten to " << cr << std::endl;
-      }
-      std::map< Node, bool > visited;
-      // functions to arguments
-      std::vector< Node > args;
-      std::vector< Node > terms;
-      std::vector< Node > subs;
-      bool singleInvocation = true;
-      bool ngroundSingleInvocation = false;
-      if( processConjunct( cr, visited, args, terms, subs ) ){
-        for( unsigned j=0; j<terms.size(); j++ ){
-          si_terms.push_back( subs[j] );
-          Node op = subs[j].hasOperator() ? subs[j].getOperator() : subs[j];
-          Assert( d_func_fo_var.find( op )!=d_func_fo_var.end() );
-          si_subs.push_back( d_func_fo_var[op] );
-        }
-        std::map< Node, Node > subs_map;
-        std::map< Node, Node > subs_map_rev;
-        std::vector< Node > funcs;
-        //normalize the invocations
-        if( !terms.empty() ){
-          Assert( terms.size()==subs.size() );
-          cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
-        }
-        std::vector< Node > children;
-        children.push_back( cr );
-        terms.clear();
-        subs.clear();
-        Trace("si-prt") << "...single invocation, with arguments: " << std::endl;
-        for( unsigned j=0; j<args.size(); j++ ){
-          Trace("si-prt") << args[j] << " ";
-          if( args[j].getKind()==BOUND_VARIABLE && std::find( terms.begin(), terms.end(), args[j] )==terms.end() ){
-            terms.push_back( args[j] );
-            subs.push_back( d_si_vars[j] );
-          }else{
-            children.push_back( d_si_vars[j].eqNode( args[j] ).negate() );
-          }
-        }
-        Trace("si-prt") << std::endl;
-        cr = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
-        Assert( terms.size()==subs.size() );
-        cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
-        Trace("si-prt-debug") << "...normalized invocations to " << cr << std::endl;
-        //now must check if it has other bound variables
-        std::vector< Node > bvs;
-        TermUtil::getBoundVars( cr, bvs );
-        if( bvs.size()>d_si_vars.size() ){
-          // getBoundVars also collects functions in the rare case that we are synthesizing a function with 0 arguments
-          // take these into account below.
-          unsigned n_const_synth_fun = 0;
-          for( unsigned j=0; j<bvs.size(); j++ ){
-            if( std::find( d_input_funcs.begin(), d_input_funcs.end(), bvs[j] )!=d_input_funcs.end() ){
-              n_const_synth_fun++;
-            }
-          }
-          if( bvs.size()-n_const_synth_fun>d_si_vars.size() ){
-            Trace("si-prt") << "...not ground single invocation." << std::endl;
-            ngroundSingleInvocation = true;
-            singleInvocation = false;
-          }else{
-            Trace("si-prt") << "...ground single invocation : success, after removing 0-arg synth functions." << std::endl;
-          }
-        }else{
-          Trace("si-prt") << "...ground single invocation : success." << std::endl;
-        }
-      }else{
-        Trace("si-prt") << "...not single invocation." << std::endl;
-        singleInvocation = false;
-        //rename bound variables with maximal overlap with si_vars
-        std::vector< Node > bvs;
-        TermUtil::getBoundVars( cr, bvs );
-        std::vector< Node > terms;
-        std::vector< Node > subs;
-        for( unsigned j=0; j<bvs.size(); j++ ){
-          TypeNode tn = bvs[j].getType();
-          Trace("si-prt-debug") << "Fit bound var #" << j << " : " << bvs[j] << " with si." << std::endl;
-          for( unsigned k=0; k<d_si_vars.size(); k++ ){
-            if( tn==d_arg_types[k] ){
-              if( std::find( subs.begin(), subs.end(), d_si_vars[k] )==subs.end() ){
-                terms.push_back( bvs[j] );
-                subs.push_back( d_si_vars[k] );
-                Trace("si-prt-debug") << "  ...use " << d_si_vars[k] << std::endl;
-                break;
-              }
-            }
-          }
-        }
-        Assert( terms.size()==subs.size() );
-        cr = cr.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
-      }
-      cr = Rewriter::rewrite( cr );
-      Trace("si-prt") << ".....got si=" << singleInvocation << ", result : " << cr << std::endl;
-      d_conjuncts[2].push_back( cr );
-      TermUtil::getBoundVars( cr, d_all_vars );
-      if( singleInvocation ){
-        //replace with single invocation formulation
-        Assert( si_terms.size()==si_subs.size() );
-        cr = cr.substitute( si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end() );
-        cr = Rewriter::rewrite( cr );
-        Trace("si-prt") << ".....si version=" << cr << std::endl;
-        d_conjuncts[0].push_back( cr );
-      }else{
-        d_conjuncts[1].push_back( cr );
-        if( ngroundSingleInvocation ){
-          d_conjuncts[3].push_back( cr );
-        }
-      }
-    }
-  }else{
-    Trace("si-prt") << "...failed." << std::endl;
-  }
-}
-
-bool SingleInvocationPartition::collectConjuncts( Node n, bool pol, std::vector< Node >& conj ) {
-  if( ( !pol && n.getKind()==OR ) || ( pol && n.getKind()==AND ) ){
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( !collectConjuncts( n[i], pol, conj ) ){
-        return false;
-      }
-    }
-  }else if( n.getKind()==NOT ){
-    return collectConjuncts( n[0], !pol, conj );
-  }else if( n.getKind()==FORALL ){
-    return false;
-  }else{
-    if( !pol ){
-      n = TermUtil::simpleNegate( n );
-    }
-    Trace("si-prt") << "Conjunct : " << n << std::endl;
-    conj.push_back( n );
-  }
-  return true;
-}
-
-bool SingleInvocationPartition::processConjunct( Node n, std::map< Node, bool >& visited, std::vector< Node >& args,
-                                                 std::vector< Node >& terms, std::vector< Node >& subs ) {
-  std::map< Node, bool >::iterator it = visited.find( n );
-  if( it!=visited.end() ){
-    return true;
-  }else{
-    bool ret = true;
-    //if( TermUtil::hasBoundVarAttr( n ) ){
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        if( !processConjunct( n[i], visited, args, terms, subs ) ){
-          ret = false;
-        }
-      }
-      if( ret ){
-        Node f;
-        bool success = false;
-        if( d_has_input_funcs ){
-          f = n.hasOperator() ? n.getOperator() : n;
-          if( std::find( d_input_funcs.begin(), d_input_funcs.end(), f )!=d_input_funcs.end() ){
-            success = true;
-          }
-        }else{
-          if( n.getKind()==kind::APPLY_UF ){
-            f = n.getOperator();
-            success = true;
-          }
-        }
-        if( success ){
-          if( std::find( terms.begin(), terms.end(), n )==terms.end() ){
-            //check if it matches the type requirement
-            if( isAntiSkolemizableType( f ) ){
-              if( args.empty() ){
-                //record arguments
-                for( unsigned i=0; i<n.getNumChildren(); i++ ){
-                  args.push_back( n[i] );
-                }
-              }else{
-                //arguments must be the same as those already recorded
-                for( unsigned i=0; i<n.getNumChildren(); i++ ){
-                  if( args[i]!=n[i] ){
-                    Trace("si-prt-debug") << "...bad invocation : " << n << " at arg " << i << "." << std::endl;
-                    ret = false;
-                    break;
-                  }
-                }
-              }
-              if( ret ){
-                terms.push_back( n );
-                subs.push_back( d_func_inv[f] );
-              }
-            }else{
-              Trace("si-prt-debug") << "... " << f << " is a bad operator." << std::endl;
-              ret = false;
-            }
-          }
-        }
-      }
-    //}
-    visited[n] = ret;
-    return ret;
-  }
-}
-
-bool SingleInvocationPartition::isAntiSkolemizableType( Node f ) {
-  std::map< Node, bool >::iterator it = d_funcs.find( f );
-  if( it!=d_funcs.end() ){
-    return it->second;
-  }else{
-    TypeNode tn = f.getType();
-    bool ret = false;
-    if( tn.getNumChildren()==d_arg_types.size()+1 || ( d_arg_types.empty() && tn.getNumChildren()==0 ) ){
-      ret = true;
-      std::vector< Node > children;
-      children.push_back( f );
-      //TODO: permutations of arguments
-      for( unsigned i=0; i<d_arg_types.size(); i++ ){
-        children.push_back( d_si_vars[i] );
-        if( tn[i]!=d_arg_types[i] ){
-          ret = false;
-          break;
-        }
-      }
-      if( ret ){
-        Node t;
-        if( children.size()>1 ){
-          t = NodeManager::currentNM()->mkNode( kind::APPLY_UF, children );
-        }else{
-          t = children[0];
-        }
-        d_func_inv[f] = t;
-        d_inv_to_func[t] = f;
-        std::stringstream ss;
-        ss << "F_" << f;
-        TypeNode rt;
-        if( d_arg_types.empty() ){
-          rt = tn;
-        }else{
-          rt = tn.getRangeType();
-        }
-        Node v = NodeManager::currentNM()->mkBoundVar( ss.str(), rt );
-        d_func_fo_var[f] = v;
-        d_fo_var_to_func[v] = f;
-        d_func_vars.push_back( v );
-      }
-    }
-    d_funcs[f] = ret;
-    return ret;
-  }
-}
-
-Node SingleInvocationPartition::getConjunct( int index ) {
-  return d_conjuncts[index].empty() ? NodeManager::currentNM()->mkConst( true ) :
-          ( d_conjuncts[index].size()==1 ? d_conjuncts[index][0] : NodeManager::currentNM()->mkNode( AND, d_conjuncts[index] ) );
-}
-
-Node SingleInvocationPartition::getSpecificationInst( Node n, std::map< Node, Node >& lam, std::map< Node, Node >& visited ) {
-  std::map< Node, Node >::iterator it = visited.find( n );
-  if( it!=visited.end() ){
-    return it->second;
-  }else{
-    bool childChanged = false;
-    std::vector< Node > children;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      Node nn = getSpecificationInst( n[i], lam, visited );
-      children.push_back( nn );
-      childChanged = childChanged || ( nn!=n[i] );
-    }
-    Node ret;
-    Node f;
-    bool success = false;
-    if( d_has_input_funcs ){
-      f = n.hasOperator() ? n.getOperator() : n;
-      if( std::find( d_input_funcs.begin(), d_input_funcs.end(), f )!=d_input_funcs.end() ){
-        success = true;
-      }
-    }else{
-      if( n.getKind()==APPLY_UF ){
-        f = n.getOperator();
-        success = true;
-      }
-    }
-    if( success ){
-      std::map< Node, Node >::iterator itl = lam.find( f );
-      if( itl!=lam.end() ){
-        Assert( itl->second[0].getNumChildren()==children.size() );
-        std::vector< Node > terms;
-        std::vector< Node > subs;
-        for( unsigned i=0; i<itl->second[0].getNumChildren(); i++ ){
-          terms.push_back( itl->second[0][i] );
-          subs.push_back( children[i] );
-        }
-        ret = itl->second[1].substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
-        ret = Rewriter::rewrite( ret );
-      }
-    }
-    if( ret.isNull() ){
-      ret = n;
-      if( childChanged ){
-        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-          children.insert( children.begin(), n.getOperator() );
-        }
-        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
-      }
-    }
-    return ret;
-  }
-}
-
-Node SingleInvocationPartition::getSpecificationInst( int index, std::map< Node, Node >& lam ) {
-  Node conj = getConjunct( index );
-  std::map< Node, Node > visited;
-  return getSpecificationInst( conj, lam, visited );
-}
-
-void SingleInvocationPartition::debugPrint( const char * c ) {
-  Trace(c) << "Single invocation variables : ";
-  for( unsigned i=0; i<d_si_vars.size(); i++ ){
-    Trace(c) << d_si_vars[i] << " ";
-  }
-  Trace(c) << std::endl;
-  Trace(c) << "Functions : " << std::endl;
-  for( std::map< Node, bool >::iterator it = d_funcs.begin(); it != d_funcs.end(); ++it ){
-    Trace(c) << "  " << it->first << " : ";
-    if( it->second ){
-      Trace(c) << d_func_inv[it->first] << " " << d_func_fo_var[it->first] << std::endl;
-    }else{
-      Trace(c) << "not incorporated." << std::endl;
-    }
-  }
-  for( unsigned i=0; i<4; i++ ){
-    Trace(c) << ( i==0 ? "Single invocation" : ( i==1 ? "Non-single invocation" : ( i==2 ? "All" : "Non-ground single invocation" ) ) );
-    Trace(c) << " conjuncts: " << std::endl;
-    for( unsigned j=0; j<d_conjuncts[i].size(); j++ ){
-      Trace(c) << "  " << (j+1) << " : " << d_conjuncts[i][j] << std::endl;
-    }
-  }
-  Trace(c) << std::endl;
-}
-
-
 bool DetTrace::DetTraceTrie::add( Node loc, std::vector< Node >& val, unsigned index ){
   if( index==val.size() ){
     if( d_children.empty() ){
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index ffcdb7075..8e63e8909 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -17,11 +17,12 @@
 #ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
 #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
 
-#include "context/cdhashmap.h"
 #include "context/cdchunk_list.h"
-#include "theory/quantifiers_engine.h"
+#include "context/cdhashmap.h"
 #include "theory/quantifiers/ce_guided_single_inv_sol.h"
 #include "theory/quantifiers/inst_strategy_cbqi.h"
+#include "theory/quantifiers/single_inv_partition.h"
+#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
@@ -41,9 +42,6 @@ public:
   bool addLemma( Node lem );
 };
 
-
-class SingleInvocationPartition;
-
 class DetTrace {
 private:
   class DetTraceTrie {
@@ -243,57 +241,6 @@ class CegConjectureSingleInv {
   }
 };
 
-// A utility to group formulas into single invocation/non-single
-// invocation parts. Only processes functions having argument types exactly matching
-// "d_arg_types", and all invocations are in the same order across all
-// functions
-class SingleInvocationPartition {
-private:
-  bool d_has_input_funcs;
-  std::vector< Node > d_input_funcs;
-  //options
-  bool inferArgTypes( Node n, std::vector< TypeNode >& typs, std::map< Node, bool >& visited );
-  void process( Node n );
-  bool collectConjuncts( Node n, bool pol, std::vector< Node >& conj );
-  bool processConjunct( Node n, std::map< Node, bool >& visited, std::vector< Node >& args,
-                        std::vector< Node >& terms, std::vector< Node >& subs );
-  Node getSpecificationInst( Node n, std::map< Node, Node >& lam, std::map< Node, Node >& visited );
-  bool init( std::vector< Node >& funcs, std::vector< TypeNode >& typs, Node n, bool has_funcs );
-public:
-  SingleInvocationPartition() : d_has_input_funcs( false ){}
-  ~SingleInvocationPartition(){}
-  bool init( Node n );
-  bool init( std::vector< Node >& funcs, Node n );
-
-  //outputs (everything is with bound var)
-  std::vector< TypeNode > d_arg_types;
-  std::map< Node, bool > d_funcs;
-  std::map< Node, Node > d_func_inv;
-  std::map< Node, Node > d_inv_to_func;
-  std::map< Node, Node > d_func_fo_var;
-  std::map< Node, Node > d_fo_var_to_func;
-  std::vector< Node > d_func_vars; //the first-order variables corresponding to all functions
-  std::vector< Node > d_si_vars;   //the arguments that we based the anti-skolemization on
-  std::vector< Node > d_all_vars;  //every free variable of conjuncts[2]
-  // si, nsi, all, non-ground si
-  std::vector< Node > d_conjuncts[4];
-
-  bool isAntiSkolemizableType( Node f );
-
-  Node getConjunct( int index );
-  Node getSingleInvocation() { return getConjunct( 0 ); }
-  Node getNonSingleInvocation() { return getConjunct( 1 ); }
-  Node getFullSpecification() { return getConjunct( 2 ); }
-
-  Node getSpecificationInst( int index, std::map< Node, Node >& lam );
-
-  bool isPurelySingleInvocation() { return d_conjuncts[1].empty(); }
-  bool isNonGroundSingleInvocation() { return d_conjuncts[3].size()==d_conjuncts[1].size(); }
-
-  void debugPrint( const char * c );
-};
-
-
 }/* namespace CVC4::theory::quantifiers */
 }/* namespace CVC4::theory */
 }/* namespace CVC4 */
diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp
new file mode 100644
index 000000000..890b7fcd3
--- /dev/null
+++ b/src/theory/quantifiers/single_inv_partition.cpp
@@ -0,0 +1,590 @@
+/*********************                                                        */
+/*! \file single_inv_partition.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Tim King
+ ** 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 utility for processing single invocation synthesis conjectures
+ **
+ **/
+#include "theory/quantifiers/single_inv_partition.h"
+
+#include "theory/quantifiers/term_util.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+bool SingleInvocationPartition::init(Node n)
+{
+  // first, get types of arguments for functions
+  std::vector<TypeNode> typs;
+  std::map<Node, bool> visited;
+  std::vector<Node> funcs;
+  if (inferArgTypes(n, typs, visited))
+  {
+    return init(funcs, typs, n, false);
+  }
+  else
+  {
+    Trace("si-prt") << "Could not infer argument types." << std::endl;
+    return false;
+  }
+}
+
+Node SingleInvocationPartition::getFirstOrderVariableForFunction(Node f) const
+{
+  std::map<Node, Node>::const_iterator it = d_func_fo_var.find(f);
+  if (it != d_func_fo_var.end())
+  {
+    return it->second;
+  }
+  return Node::null();
+}
+
+Node SingleInvocationPartition::getFunctionForFirstOrderVariable(Node v) const
+{
+  std::map<Node, Node>::const_iterator it = d_fo_var_to_func.find(v);
+  if (it != d_fo_var_to_func.end())
+  {
+    return it->second;
+  }
+  return Node::null();
+}
+
+Node SingleInvocationPartition::getFunctionInvocationFor(Node f) const
+{
+  std::map<Node, Node>::const_iterator it = d_func_inv.find(f);
+  if (it != d_func_inv.end())
+  {
+    return it->second;
+  }
+  return Node::null();
+}
+
+void SingleInvocationPartition::getFunctionVariables(
+    std::vector<Node>& fvars) const
+{
+  fvars.insert(fvars.end(), d_func_vars.begin(), d_func_vars.end());
+}
+
+void SingleInvocationPartition::getFunctions(std::vector<Node>& fs) const
+{
+  fs.insert(fs.end(), d_all_funcs.begin(), d_all_funcs.end());
+}
+
+void SingleInvocationPartition::getSingleInvocationVariables(
+    std::vector<Node>& sivars) const
+{
+  sivars.insert(sivars.end(), d_si_vars.begin(), d_si_vars.end());
+}
+
+void SingleInvocationPartition::getAllVariables(std::vector<Node>& vars) const
+{
+  vars.insert(vars.end(), d_all_vars.begin(), d_all_vars.end());
+}
+
+// gets the argument type list for the first APPLY_UF we see
+bool SingleInvocationPartition::inferArgTypes(Node n,
+                                              std::vector<TypeNode>& typs,
+                                              std::map<Node, bool>& visited)
+{
+  if (visited.find(n) == visited.end())
+  {
+    visited[n] = true;
+    if (n.getKind() != FORALL)
+    {
+      if (n.getKind() == APPLY_UF)
+      {
+        for (unsigned i = 0; i < n.getNumChildren(); i++)
+        {
+          typs.push_back(n[i].getType());
+        }
+        return true;
+      }
+      else
+      {
+        for (unsigned i = 0; i < n.getNumChildren(); i++)
+        {
+          if (inferArgTypes(n[i], typs, visited))
+          {
+            return true;
+          }
+        }
+      }
+    }
+  }
+  return false;
+}
+
+bool SingleInvocationPartition::init(std::vector<Node>& funcs, Node n)
+{
+  Trace("si-prt") << "Initialize with " << funcs.size() << " input functions..."
+                  << std::endl;
+  std::vector<TypeNode> typs;
+  if (!funcs.empty())
+  {
+    TypeNode tn0 = funcs[0].getType();
+    for (unsigned i = 1; i < funcs.size(); i++)
+    {
+      if (funcs[i].getType() != tn0)
+      {
+        // can't anti-skolemize functions of different sort
+        Trace("si-prt") << "...type mismatch" << std::endl;
+        return false;
+      }
+    }
+    if (tn0.getNumChildren() > 1)
+    {
+      for (unsigned j = 0; j < tn0.getNumChildren() - 1; j++)
+      {
+        typs.push_back(tn0[j]);
+      }
+    }
+  }
+  Trace("si-prt") << "#types = " << typs.size() << std::endl;
+  return init(funcs, typs, n, true);
+}
+
+bool SingleInvocationPartition::init(std::vector<Node>& funcs,
+                                     std::vector<TypeNode>& typs,
+                                     Node n,
+                                     bool has_funcs)
+{
+  Assert(d_arg_types.empty());
+  Assert(d_input_funcs.empty());
+  Assert(d_si_vars.empty());
+  d_has_input_funcs = has_funcs;
+  d_arg_types.insert(d_arg_types.end(), typs.begin(), typs.end());
+  d_input_funcs.insert(d_input_funcs.end(), funcs.begin(), funcs.end());
+  Trace("si-prt") << "Initialize..." << std::endl;
+  for (unsigned j = 0; j < d_arg_types.size(); j++)
+  {
+    std::stringstream ss;
+    ss << "s_" << j;
+    Node si_v = NodeManager::currentNM()->mkBoundVar(ss.str(), d_arg_types[j]);
+    d_si_vars.push_back(si_v);
+  }
+  Assert(d_si_vars.size() == d_arg_types.size());
+  Trace("si-prt") << "SingleInvocationPartition::process " << n << std::endl;
+  Trace("si-prt") << "Get conjuncts..." << std::endl;
+  std::vector<Node> conj;
+  if (collectConjuncts(n, true, conj))
+  {
+    Trace("si-prt") << "...success." << std::endl;
+    for (unsigned i = 0; i < conj.size(); i++)
+    {
+      std::vector<Node> si_terms;
+      std::vector<Node> si_subs;
+      Trace("si-prt") << "Process conjunct : " << conj[i] << std::endl;
+      // do DER on conjunct
+      Node cr = TermUtil::getQuantSimplify(conj[i]);
+      if (cr != conj[i])
+      {
+        Trace("si-prt-debug") << "...rewritten to " << cr << std::endl;
+      }
+      std::map<Node, bool> visited;
+      // functions to arguments
+      std::vector<Node> args;
+      std::vector<Node> terms;
+      std::vector<Node> subs;
+      bool singleInvocation = true;
+      bool ngroundSingleInvocation = false;
+      if (processConjunct(cr, visited, args, terms, subs))
+      {
+        for (unsigned j = 0; j < terms.size(); j++)
+        {
+          si_terms.push_back(subs[j]);
+          Node op = subs[j].hasOperator() ? subs[j].getOperator() : subs[j];
+          Assert(d_func_fo_var.find(op) != d_func_fo_var.end());
+          si_subs.push_back(d_func_fo_var[op]);
+        }
+        std::map<Node, Node> subs_map;
+        std::map<Node, Node> subs_map_rev;
+        std::vector<Node> funcs;
+        // normalize the invocations
+        if (!terms.empty())
+        {
+          Assert(terms.size() == subs.size());
+          cr = cr.substitute(
+              terms.begin(), terms.end(), subs.begin(), subs.end());
+        }
+        std::vector<Node> children;
+        children.push_back(cr);
+        terms.clear();
+        subs.clear();
+        Trace("si-prt") << "...single invocation, with arguments: "
+                        << std::endl;
+        for (unsigned j = 0; j < args.size(); j++)
+        {
+          Trace("si-prt") << args[j] << " ";
+          if (args[j].getKind() == BOUND_VARIABLE
+              && std::find(terms.begin(), terms.end(), args[j]) == terms.end())
+          {
+            terms.push_back(args[j]);
+            subs.push_back(d_si_vars[j]);
+          }
+          else
+          {
+            children.push_back(d_si_vars[j].eqNode(args[j]).negate());
+          }
+        }
+        Trace("si-prt") << std::endl;
+        cr = children.size() == 1
+                 ? children[0]
+                 : NodeManager::currentNM()->mkNode(OR, children);
+        Assert(terms.size() == subs.size());
+        cr =
+            cr.substitute(terms.begin(), terms.end(), subs.begin(), subs.end());
+        Trace("si-prt-debug") << "...normalized invocations to " << cr
+                              << std::endl;
+        // now must check if it has other bound variables
+        std::vector<Node> bvs;
+        TermUtil::getBoundVars(cr, bvs);
+        if (bvs.size() > d_si_vars.size())
+        {
+          // getBoundVars also collects functions in the rare case that we are
+          // synthesizing a function with 0 arguments
+          // take these into account below.
+          unsigned n_const_synth_fun = 0;
+          for (unsigned j = 0; j < bvs.size(); j++)
+          {
+            if (std::find(d_input_funcs.begin(), d_input_funcs.end(), bvs[j])
+                != d_input_funcs.end())
+            {
+              n_const_synth_fun++;
+            }
+          }
+          if (bvs.size() - n_const_synth_fun > d_si_vars.size())
+          {
+            Trace("si-prt") << "...not ground single invocation." << std::endl;
+            ngroundSingleInvocation = true;
+            singleInvocation = false;
+          }
+          else
+          {
+            Trace("si-prt") << "...ground single invocation : success, after "
+                               "removing 0-arg synth functions."
+                            << std::endl;
+          }
+        }
+        else
+        {
+          Trace("si-prt") << "...ground single invocation : success."
+                          << std::endl;
+        }
+      }
+      else
+      {
+        Trace("si-prt") << "...not single invocation." << std::endl;
+        singleInvocation = false;
+        // rename bound variables with maximal overlap with si_vars
+        std::vector<Node> bvs;
+        TermUtil::getBoundVars(cr, bvs);
+        std::vector<Node> terms;
+        std::vector<Node> subs;
+        for (unsigned j = 0; j < bvs.size(); j++)
+        {
+          TypeNode tn = bvs[j].getType();
+          Trace("si-prt-debug") << "Fit bound var #" << j << " : " << bvs[j]
+                                << " with si." << std::endl;
+          for (unsigned k = 0; k < d_si_vars.size(); k++)
+          {
+            if (tn == d_arg_types[k])
+            {
+              if (std::find(subs.begin(), subs.end(), d_si_vars[k])
+                  == subs.end())
+              {
+                terms.push_back(bvs[j]);
+                subs.push_back(d_si_vars[k]);
+                Trace("si-prt-debug") << "  ...use " << d_si_vars[k]
+                                      << std::endl;
+                break;
+              }
+            }
+          }
+        }
+        Assert(terms.size() == subs.size());
+        cr =
+            cr.substitute(terms.begin(), terms.end(), subs.begin(), subs.end());
+      }
+      cr = Rewriter::rewrite(cr);
+      Trace("si-prt") << ".....got si=" << singleInvocation
+                      << ", result : " << cr << std::endl;
+      d_conjuncts[2].push_back(cr);
+      TermUtil::getBoundVars(cr, d_all_vars);
+      if (singleInvocation)
+      {
+        // replace with single invocation formulation
+        Assert(si_terms.size() == si_subs.size());
+        cr = cr.substitute(
+            si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end());
+        cr = Rewriter::rewrite(cr);
+        Trace("si-prt") << ".....si version=" << cr << std::endl;
+        d_conjuncts[0].push_back(cr);
+      }
+      else
+      {
+        d_conjuncts[1].push_back(cr);
+        if (ngroundSingleInvocation)
+        {
+          d_conjuncts[3].push_back(cr);
+        }
+      }
+    }
+  }
+  else
+  {
+    Trace("si-prt") << "...failed." << std::endl;
+  }
+  return true;
+}
+
+bool SingleInvocationPartition::collectConjuncts(Node n,
+                                                 bool pol,
+                                                 std::vector<Node>& conj)
+{
+  if ((!pol && n.getKind() == OR) || (pol && n.getKind() == AND))
+  {
+    for (unsigned i = 0; i < n.getNumChildren(); i++)
+    {
+      if (!collectConjuncts(n[i], pol, conj))
+      {
+        return false;
+      }
+    }
+  }
+  else if (n.getKind() == NOT)
+  {
+    return collectConjuncts(n[0], !pol, conj);
+  }
+  else if (n.getKind() == FORALL)
+  {
+    return false;
+  }
+  else
+  {
+    if (!pol)
+    {
+      n = TermUtil::simpleNegate(n);
+    }
+    Trace("si-prt") << "Conjunct : " << n << std::endl;
+    conj.push_back(n);
+  }
+  return true;
+}
+
+bool SingleInvocationPartition::processConjunct(Node n,
+                                                std::map<Node, bool>& visited,
+                                                std::vector<Node>& args,
+                                                std::vector<Node>& terms,
+                                                std::vector<Node>& subs)
+{
+  std::map<Node, bool>::iterator it = visited.find(n);
+  if (it != visited.end())
+  {
+    return true;
+  }
+  else
+  {
+    bool ret = true;
+    // if( TermUtil::hasBoundVarAttr( n ) ){
+    for (unsigned i = 0; i < n.getNumChildren(); i++)
+    {
+      if (!processConjunct(n[i], visited, args, terms, subs))
+      {
+        ret = false;
+      }
+    }
+    if (ret)
+    {
+      Node f;
+      bool success = false;
+      if (d_has_input_funcs)
+      {
+        f = n.hasOperator() ? n.getOperator() : n;
+        if (std::find(d_input_funcs.begin(), d_input_funcs.end(), f)
+            != d_input_funcs.end())
+        {
+          success = true;
+        }
+      }
+      else
+      {
+        if (n.getKind() == kind::APPLY_UF)
+        {
+          f = n.getOperator();
+          success = true;
+        }
+      }
+      if (success)
+      {
+        if (std::find(terms.begin(), terms.end(), n) == terms.end())
+        {
+          // check if it matches the type requirement
+          if (isAntiSkolemizableType(f))
+          {
+            if (args.empty())
+            {
+              // record arguments
+              for (unsigned i = 0; i < n.getNumChildren(); i++)
+              {
+                args.push_back(n[i]);
+              }
+            }
+            else
+            {
+              // arguments must be the same as those already recorded
+              for (unsigned i = 0; i < n.getNumChildren(); i++)
+              {
+                if (args[i] != n[i])
+                {
+                  Trace("si-prt-debug") << "...bad invocation : " << n
+                                        << " at arg " << i << "." << std::endl;
+                  ret = false;
+                  break;
+                }
+              }
+            }
+            if (ret)
+            {
+              terms.push_back(n);
+              subs.push_back(d_func_inv[f]);
+            }
+          }
+          else
+          {
+            Trace("si-prt-debug") << "... " << f << " is a bad operator."
+                                  << std::endl;
+            ret = false;
+          }
+        }
+      }
+    }
+    //}
+    visited[n] = ret;
+    return ret;
+  }
+}
+
+bool SingleInvocationPartition::isAntiSkolemizableType(Node f)
+{
+  std::map<Node, bool>::iterator it = d_funcs.find(f);
+  if (it != d_funcs.end())
+  {
+    return it->second;
+  }
+  else
+  {
+    TypeNode tn = f.getType();
+    bool ret = false;
+    if (tn.getNumChildren() == d_arg_types.size() + 1
+        || (d_arg_types.empty() && tn.getNumChildren() == 0))
+    {
+      ret = true;
+      std::vector<Node> children;
+      children.push_back(f);
+      // TODO: permutations of arguments
+      for (unsigned i = 0; i < d_arg_types.size(); i++)
+      {
+        children.push_back(d_si_vars[i]);
+        if (tn[i] != d_arg_types[i])
+        {
+          ret = false;
+          break;
+        }
+      }
+      if (ret)
+      {
+        Node t;
+        if (children.size() > 1)
+        {
+          t = NodeManager::currentNM()->mkNode(kind::APPLY_UF, children);
+        }
+        else
+        {
+          t = children[0];
+        }
+        d_func_inv[f] = t;
+        std::stringstream ss;
+        ss << "F_" << f;
+        TypeNode rt;
+        if (d_arg_types.empty())
+        {
+          rt = tn;
+        }
+        else
+        {
+          rt = tn.getRangeType();
+        }
+        Node v = NodeManager::currentNM()->mkBoundVar(ss.str(), rt);
+        d_func_fo_var[f] = v;
+        d_fo_var_to_func[v] = f;
+        d_func_vars.push_back(v);
+        d_all_funcs.push_back(f);
+      }
+    }
+    d_funcs[f] = ret;
+    return ret;
+  }
+}
+
+Node SingleInvocationPartition::getConjunct(int index)
+{
+  return d_conjuncts[index].empty() ? NodeManager::currentNM()->mkConst(true)
+                                    : (d_conjuncts[index].size() == 1
+                                           ? d_conjuncts[index][0]
+                                           : NodeManager::currentNM()->mkNode(
+                                                 AND, d_conjuncts[index]));
+}
+
+void SingleInvocationPartition::debugPrint(const char* c)
+{
+  Trace(c) << "Single invocation variables : ";
+  for (unsigned i = 0; i < d_si_vars.size(); i++)
+  {
+    Trace(c) << d_si_vars[i] << " ";
+  }
+  Trace(c) << std::endl;
+  Trace(c) << "Functions : " << std::endl;
+  for (std::map<Node, bool>::iterator it = d_funcs.begin(); it != d_funcs.end();
+       ++it)
+  {
+    Trace(c) << "  " << it->first << " : ";
+    if (it->second)
+    {
+      Trace(c) << d_func_inv[it->first] << " " << d_func_fo_var[it->first]
+               << std::endl;
+    }
+    else
+    {
+      Trace(c) << "not incorporated." << std::endl;
+    }
+  }
+  for (unsigned i = 0; i < 4; i++)
+  {
+    Trace(c) << (i == 0 ? "Single invocation"
+                        : (i == 1 ? "Non-single invocation"
+                                  : (i == 2 ? "All"
+                                            : "Non-ground single invocation")));
+    Trace(c) << " conjuncts: " << std::endl;
+    for (unsigned j = 0; j < d_conjuncts[i].size(); j++)
+    {
+      Trace(c) << "  " << (j + 1) << " : " << d_conjuncts[i][j] << std::endl;
+    }
+  }
+  Trace(c) << std::endl;
+}
+
+} /* namespace CVC4::theory::quantifiers */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h
new file mode 100644
index 000000000..f346285fa
--- /dev/null
+++ b/src/theory/quantifiers/single_inv_partition.h
@@ -0,0 +1,295 @@
+/*********************                                                        */
+/*! \file single_inv_partition.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Tim King
+ ** 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 utility for single invocation partitioning
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
+#define __CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
+
+#include <map>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** single invocation partition
+ *
+ * This is a utility to group formulas into single invocation/non-single
+ * invocation parts, relative to a set of "input functions".
+ * It can be used when either the set of input functions is fixed,
+ * or is unknown.
+ *
+ * (EX1) For example, if input functions are { f },
+ * then the formula is ( f( x, y ) = g( y ) V f( x, y ) = b )
+ * is single invocation since there is only one
+ * unique application of f, that is, f( x, y ).
+ * Notice that
+ *   exists f. forall xy. f( x, y ) = g( y ) V f( x, y ) = b
+ * is equivalent to:
+ *   forall xy. exists z. z = g( y ) V z = b
+ *
+ * When handling multiple input functions, we only infer a formula
+ * is single invocation if all (relevant) input functions have the
+ * same argument types. An input function is relevant if it is
+ * specified by the input in a call to init() or occurs in the
+ * formula we are processing.
+ *
+ * Notice that this class may introduce auxiliary variables to
+ * coerce a formula into being single invocation. For example,
+ * see Example 5 of Reynolds et al. SYNT 2017.
+ *
+ */
+class SingleInvocationPartition
+{
+ public:
+  SingleInvocationPartition() : d_has_input_funcs(false) {}
+  ~SingleInvocationPartition() {}
+  /** initialize this partition for formula n, with input functions funcs
+   *
+   * This initializes this class to check whether formula n is single
+   * invocation with respect to the input functions in funcs only.
+   * Below, the "processed formula" is a formula generated by this
+   * call that is equivalent to n (if this call is successful).
+   *
+   * This method returns true if all input functions have identical
+   * argument types, and false otherwise. Notice that all
+   * access functions below are only valid if this class is
+   * successfully initialized.
+   */
+  bool init(std::vector<Node>& funcs, Node n);
+
+  /** initialize this partition for formula n
+   *
+   * In contrast to the above method, this version assumes that
+   * all uninterpreted functions are input functions. That is, this
+   * method is equivalent to the above function with funcs containing
+   * all uninterpreted functions occurring in n.
+   */
+  bool init(Node n);
+
+  /** is the processed formula purely single invocation?
+   *
+   * A formula is purely single invocation if it is equivalent to:
+   *   t[ f1( x ), ..., fn( x ), x ],
+   * for some F, where f1...fn are the input functions.
+   * Notice that the free variables of t are exactly x.
+   */
+  bool isPurelySingleInvocation() { return d_conjuncts[1].empty(); }
+  /** is the processed formula non-ground single invocation?
+   *
+   * A formula is non-ground single invocation if it is equivalent to:
+   *   F[ f1( x ), ..., fn( x ), x, y ],
+   * for some F, where f1...fn are the input functions.
+   */
+  bool isNonGroundSingleInvocation()
+  {
+    return d_conjuncts[3].size() == d_conjuncts[1].size();
+  }
+
+  /** Get the (portion of) the processed formula that is single invocation
+   *
+   * Notice this method returns the anti-skolemized version of the input
+   * formula. In (EX1), this method returns:
+   *   z = g( y ) V z = b
+   * where z is the first-order variable for f (see
+   * getFirstOrderVariableForFunction).
+   */
+  Node getSingleInvocation() { return getConjunct(0); }
+  /** Get the (portion of) the processed formula that is not single invocation
+   *
+   * This formula and the above form a partition of the conjuncts of the
+   * processed formula, that is:
+   *   getSingleInvocation() * sigma ^ getNonSingleInvocation()
+   * is equivalent to the processed formula, where sigma is a substitution of
+   * the form:
+   *   z_1 -> f_1( x ) .... z_n -> f_n( x )
+   * where z_i are the first-order variables for input functions f_i
+   * for all i=1,...,n, and x are the single invocation arguments of the input
+   * formulas (see d_si_vars).
+   */
+  Node getNonSingleInvocation() { return getConjunct(1); }
+  /** get full specification
+   *
+   * This returns getSingleInvocation() * sigma ^ getNonSingleInvocation(),
+   * which is equivalent to the processed formula, where sigma is the
+   * substitution described above.
+   */
+  Node getFullSpecification() { return getConjunct(2); }
+  /** get first order variable for input function f
+   *
+   * This corresponds to the variable that we used when anti-skolemizing
+   * function f. For example, in (EX1), if getSingleInvocation() returns:
+   *   z = g( y ) V z = b
+   * Then, getFirstOrderVariableForFunction(f) = z.
+   */
+  Node getFirstOrderVariableForFunction(Node f) const;
+
+  /** get function for first order variable
+   *
+   * Opposite direction of above, where:
+   *   getFunctionForFirstOrderVariable(z) = f.
+   */
+  Node getFunctionForFirstOrderVariable(Node v) const;
+
+  /** get function invocation for
+   *
+   * Returns f( x ) where x are the single invocation arguments of the input
+   * formulas (see d_si_vars). If f is not an input function, it returns null.
+   */
+  Node getFunctionInvocationFor(Node f) const;
+
+  /** get single invocation variables, appends them to sivars */
+  void getSingleInvocationVariables(std::vector<Node>& sivars) const;
+
+  /** get all variables
+   *
+   * Appends all free variables of the processed formula to vars.
+   */
+  void getAllVariables(std::vector<Node>& vars) const;
+
+  /** get function variables
+   *
+   * Appends all first-order variables corresponding to input functions to
+   * fvars.
+   */
+  void getFunctionVariables(std::vector<Node>& fvars) const;
+
+  /** get functions
+   *
+   * Gets all input functions. This has the same order as the list of
+   * function variables above.
+   */
+  void getFunctions(std::vector<Node>& fs) const;
+
+  /** print debugging information on Trace c */
+  void debugPrint(const char* c);
+
+ private:
+  /** map from input functions to whether they have an anti-skolemizable type
+   * An anti-skolemizable type is one of the form:
+   *   ( T1, ..., Tn ) -> T
+   * where Ti = d_arg_types[i] for i = 1,...,n.
+   */
+  std::map<Node, bool> d_funcs;
+
+  /** map from functions to the invocation we inferred for them */
+  std::map<Node, Node> d_func_inv;
+
+  /** the list of first-order variables for functions
+   * In (EX1), this is the list { z }.
+   */
+  std::vector<Node> d_func_vars;
+
+  /** the arguments that we based the anti-skolemization on.
+   * In (EX1), this is the list { x, y }.
+   */
+  std::vector<Node> d_si_vars;
+
+  /** every free variable of conjuncts[2] */
+  std::vector<Node> d_all_vars;
+  /** map from functions to first-order variables that anti-skolemized them */
+  std::map<Node, Node> d_func_fo_var;
+  /** map from first-order variables to the function it anti-skolemized */
+  std::map<Node, Node> d_fo_var_to_func;
+
+  /** The argument types for this single invocation partition.
+   * These are the argument types of the input functions we are
+   * processing, where notice that:
+   *   d_si_vars[i].getType()==d_arg_types[i]
+   */
+  std::vector<TypeNode> d_arg_types;
+
+  /** the list of conjuncts with various properties :
+   * 0 : the single invocation conjuncts (stored in anti-skolemized form),
+   * 1 : the non-single invocation conjuncts,
+   * 2 : all conjuncts,
+   * 3 : non-ground single invocation conjuncts.
+   */
+  std::vector<Node> d_conjuncts[4];
+
+  /** did we initialize this class with input functions? */
+  bool d_has_input_funcs;
+  /** the input functions we initialized this class with */
+  std::vector<Node> d_input_funcs;
+  /** all input functions */
+  std::vector<Node> d_all_funcs;
+
+  /** infer the argument types of uninterpreted function applications
+   *
+   * If this method returns true, then typs contains the list of types of
+   * the arguments (in order) of all uninterpreted functions in n.
+   * If this method returns false, then there exists (at least) two
+   * uninterpreted functions in n whose argument types are not identical.
+   */
+  bool inferArgTypes(Node n,
+                     std::vector<TypeNode>& typs,
+                     std::map<Node, bool>& visited);
+
+  /** is anti-skolemizable type
+   *
+   * This method returns true if f's argument types are equal to the
+   * argument types we have fixed in this class (see d_arg_types).
+   */
+  bool isAntiSkolemizableType(Node f);
+
+  /**
+   * This is the entry point for initializing this class,
+   * which is called by the public init(...) methods.
+   *   funcs are the input functions (if any were explicitly provide),
+   *   typs is the types of the arguments of funcs,
+   *   n is the formula to process,
+   *   has_funcs is whether input functions were explicitly provided.
+   */
+  bool init(std::vector<Node>& funcs,
+            std::vector<TypeNode>& typs,
+            Node n,
+            bool has_funcs);
+
+  /**
+   * Collect the top-level conjuncts of the formula (equivalent to)
+   * n or the negation of n if pol=false, and store them in conj.
+   */
+  bool collectConjuncts(Node n, bool pol, std::vector<Node>& conj);
+
+  /** process conjunct n
+   *
+   * This function is called when n is a top-level conjunction in a
+   * formula that is equivalent to the input formula given to this
+   * class via init.
+   *
+   * args : stores the arguments (if any) that we have seen in an application
+   *   of an application of an input function in this conjunct.
+   * terms/subs : this stores a term substitution with entries of the form:
+   *     f(args) -> z
+   *   where z is the first-order variable for input function f.
+   */
+  bool processConjunct(Node n,
+                       std::map<Node, bool>& visited,
+                       std::vector<Node>& args,
+                       std::vector<Node>& terms,
+                       std::vector<Node>& subs);
+
+  /** get the and node corresponding to d_conjuncts[index] */
+  Node getConjunct(int index);
+};
+
+} /* namespace CVC4::theory::quantifiers */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */