Infrastructure for partially single invocation properties. Bug fix for unconstrained functions in sygus solver.

7 files changed, 607 insertions, 84 deletions

diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 19cf9b008..914c0614f 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -57,6 +57,12 @@ CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * qe, CegConje
   d_cinst = new CegInstantiator( qe, cosi, false, false );
 
   d_sol = new CegConjectureSingleInvSol( qe );
+  
+  if( options::cegqiSingleInvPartial() ){
+    d_sip = new SingleInvocationPartition;
+  }else{
+    d_sip = NULL;
+  }
 }
 
 void CegConjectureSingleInv::getSingleInvLemma( Node guard, std::vector< Node >& lems ) {
@@ -109,6 +115,88 @@ void CegConjectureSingleInv::initialize( Node q ) {
       }
     }
   }
+  if( options::cegqiSingleInvPartial() ){
+    Node qq = q[1];
+    if( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ){
+      qq = q[1][0][1];
+    }else{
+      qq = TermDb::simpleNegate( qq );
+    }
+    //remove the deep embedding
+    std::map< Node, Node > visited;
+    std::vector< TypeNode > types;
+    std::vector< Node > order_vars;
+    int type_valid = 0;
+    qq = removeDeepEmbedding( qq, progs, types, type_valid, visited );
+    Trace("cegqi-si-debug") << "- Remove deep embedding, got : " << qq << ", type valid = " << type_valid << std::endl;
+    bool singleInvocation = true;
+    if( type_valid==0 ){
+      //process the single invocation-ness of the property
+      d_sip->init( types );
+      d_sip->process( qq );
+      Trace("cegqi-si") << "- Partitioned to single invocation parts : " << std::endl;
+      d_sip->debugPrint( "cegqi-si" );
+      //map from program to bound variables
+      for( unsigned j=0; j<progs.size(); j++ ){
+        Node prog = progs[j];
+        std::map< Node, Node >::iterator it_nsi = d_nsi_op_map.find( prog );
+        if( it_nsi!=d_nsi_op_map.end() ){
+          Node op = it_nsi->second;
+          std::map< Node, Node >::iterator it_fov = d_sip->d_func_fo_var.find( op );
+          if( it_fov!=d_sip->d_func_fo_var.end() ){
+            Node pv = it_fov->second;
+            d_single_inv_map[prog] = pv;
+            d_single_inv_map_to_prog[pv] = prog;
+            Assert( d_sip->d_func_inv.find( op )!=d_sip->d_func_inv.end() );
+            Node inv = d_sip->d_func_inv[op];
+            d_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();
+            order_vars.push_back( pv );
+          }
+        }else{
+          //does not mention the function
+        }
+      }
+      //check if it is single invocation
+      if( !d_sip->d_conjuncts[1].empty() ){
+        singleInvocation = false;
+        //TODO if we are doing invariant templates, then construct the template
+      }else{
+        //we are fully single invocation
+      }
+    }else{
+      Trace("cegqi-si") << "...property is not single invocation, involves functions with different argument sorts." << std::endl;
+      singleInvocation = false;
+    }
+    if( singleInvocation ){
+      d_single_inv = d_sip->getSingleInvocation();
+      d_single_inv = TermDb::simpleNegate( d_single_inv );
+      if( !order_vars.empty() ){
+        Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, order_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" );
+        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() );
+      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
+        d_cinst->presolve( d_single_inv );
+      }
+    }else{
+      Trace("cegqi-si") << "Formula is not single invocation." << std::endl;
+      if( options::cegqiSingleInvAbort() ){
+        Notice() << "Property is not single invocation." << std::endl;
+        exit( 0 );
+      }
+    }
+    return;
+  }
+  
   //collect information about conjunctions
   bool singleInvocation = false;
   bool invExtractPrePost = false;
@@ -153,7 +241,7 @@ void CegConjectureSingleInv::initialize( Node q ) {
       }
     }
     if( singleInvocation || invExtractPrePost ){
-      //no value in extracting pre/post if we are single invocation
+      //no value in extracting pre/post if we are (partially) single invocation
       if( singleInvocation ){
         invExtractPrePost = false;
       }
@@ -174,6 +262,7 @@ void CegConjectureSingleInv::initialize( Node q ) {
         Node pv = NodeManager::currentNM()->mkBoundVar( ss.str(), inv.getType() );
         d_single_inv_map[prog] = pv;
         d_single_inv_map_to_prog[pv] = prog;
+        d_prog_to_sol_index[prog] = pbvs.size();
         pbvs.push_back( pv );
         Trace("cegqi-si-debug2") << "Make variable " << pv << " for " << prog << std::endl;
         for( unsigned k=1; k<inv.getNumChildren(); k++ ){
@@ -241,7 +330,7 @@ void CegConjectureSingleInv::initialize( Node q ) {
                 terms.push_back( inv );
                 subs.push_back( d_single_inv_map[prog] );
                 progs.push_back( prog );
-                Trace("cegqi-si-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[prog] << std::endl;
+                Trace("cegqi-si-debug2") << "subs : " << inv << " -> (var for " << prog << ") : " << d_single_inv_map[prog] << std::endl;
               }
             }
             if( singleInvocation ){
@@ -417,11 +506,9 @@ void CegConjectureSingleInv::initialize( Node q ) {
           }
 
           if( singleInvocation ){
-            Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts );
-            if( pbvl.isNull() ){
-              d_single_inv = bd;
-            }else{
-              d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
+            d_single_inv = conjuncts.empty() ? d_qe->getTermDatabase()->d_true : ( conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts ) );
+            if( !pbvl.isNull() ){
+              d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, d_single_inv );
             }
             Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl;
             /*
@@ -483,18 +570,14 @@ bool CegConjectureSingleInv::getVariableEliminationTerm( bool pol, bool hasPol,
   if( hasPol ){
     if( n.getKind()==NOT ){
       return getVariableEliminationTerm( !pol, true, v, n[0], s, status );
-    }else if( pol && n.getKind()==EQUAL ){
-      for( unsigned r=0; r<2; r++ ){
-        if( n[r]==v ){
-          status = 1;
-          Node ss = n[r==0 ? 1 : 0];
-          if( s.isNull() ){
-            s = ss;
-          }
-          return ss==s;
+    }else if( pol && ( n.getKind()==EQUAL || n.getKind()==IFF ) ){
+      Node ss = QuantArith::solveEqualityFor( n, v );
+      if( !ss.isNull() ){
+        if( s.isNull() ){
+          s = ss;
         }
+        return ss==s;
       }
-      //did not match, now see if it contains v
     }else if( ( n.getKind()==OR && !pol ) || ( n.getKind()==AND && pol ) ){
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
         if( getVariableEliminationTerm( pol, true, v, n[i], s, status ) ){
@@ -571,6 +654,66 @@ Node CegConjectureSingleInv::substituteInvariantTemplates( Node n, std::map< Nod
   }
 }
 
+Node CegConjectureSingleInv::removeDeepEmbedding( Node n, std::vector< Node >& progs, std::vector< TypeNode >& types, int& type_valid,
+                                                  std::map< Node, Node >& visited ) {
+  std::map< Node, Node >::iterator itv = visited.find( n );
+  if( itv!=visited.end() ){
+    return itv->second;
+  }else{
+    std::vector< Node > children;
+    bool childChanged = false;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      Node ni = removeDeepEmbedding( n[i], progs, types, type_valid, visited );
+      childChanged = childChanged || n[i]!=ni;
+      children.push_back( ni );
+    }
+    Node ret;
+    if( n.getKind()==APPLY_UF ){
+      Assert( n.getNumChildren()>0 );
+      if( std::find( progs.begin(), progs.end(), n[0] )!=progs.end() ){
+        std::map< Node, Node >::iterator it = d_nsi_op_map.find( n[0] );
+        Node op;
+        if( it==d_nsi_op_map.end() ){
+          bool checkTypes = !types.empty();
+          std::vector< TypeNode > argTypes;
+          for( unsigned j=1; j<n.getNumChildren(); j++ ){
+            TypeNode tn = n[j].getType();
+            argTypes.push_back( tn );
+            if( checkTypes ){
+              if( j>=types.size()+1 || tn!=types[j-1] ){
+                type_valid = -1;
+              }
+            }else{
+              types.push_back( tn );
+            }
+          }
+          TypeNode ft = argTypes.empty() ? n.getType() : NodeManager::currentNM()->mkFunctionType( argTypes, n.getType() );
+          std::stringstream ss2;
+          ss2 << "O_" << n[0];
+          op = NodeManager::currentNM()->mkSkolem( ss2.str(), ft, "was created for non-single invocation reasoning" );
+          d_nsi_op_map[n[0]] = op;
+          Trace("cegqi-si-debug2") << "Make operator " << op << " for " << n[0] << std::endl;
+        }else{
+          op = it->second;
+        }
+        children[0] = d_nsi_op_map[n[0]];
+        ret = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+      }
+    }
+    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 );
+      }
+    }
+    visited[n] = ret;
+    return ret;
+  }
+}
+
 bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children,
                                                    std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
                                                    std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) {
@@ -755,42 +898,81 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
   const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
   Node varList = Node::fromExpr( dt.getSygusVarList() );
   Node prog = d_quant[0][sol_index];
-  Node prog_app = d_single_inv_app_map[prog];
-  //get variables
   std::vector< Node > vars;
-  Trace("csi-sol") << "Get solution for " << prog << ", which is applied as " << prog_app << std::endl;
-  Assert( prog_app.getNumChildren()==varList.getNumChildren()+1 );
-  d_varList.clear();
-  d_sol->d_varList.clear();
-  for( unsigned i=1; i<prog_app.getNumChildren(); i++ ){
-    if( varList[i-1].getType().isBoolean() ){
-      //TODO force boolean term conversion mode
-      Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
-      vars.push_back( prog_app[i].eqNode( c ) );
+  bool success = true;
+  if( options::cegqiSingleInvPartial() ){
+    Trace("csi-sol") << "Get solution for " << prog << ", with skolems : ";
+    if( d_prog_to_sol_index.find( prog )==d_prog_to_sol_index.end() ){
+      success = false;
     }else{
-      vars.push_back( prog_app[i] );
+      sol_index = d_prog_to_sol_index[prog];
+      d_varList.clear();
+      d_sol->d_varList.clear();
+      Assert( d_single_inv_arg_sk.size()==varList.getNumChildren() );
+      for( unsigned i=0; i<d_single_inv_arg_sk.size(); i++ ){
+        Trace("csi-sol") << d_single_inv_arg_sk[i] << " ";
+        if( varList[i].getType().isBoolean() ){
+          //TODO force boolean term conversion mode
+          Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+          vars.push_back( d_single_inv_arg_sk[i].eqNode( c ) );
+        }else{
+          vars.push_back( d_single_inv_arg_sk[i] );
+        }
+        d_varList.push_back( varList[i] );
+        d_sol->d_varList.push_back( varList[i] );
+      }
+    }
+    Trace("csi-sol") << std::endl;
+  }else{
+    Node prog_app = d_single_inv_app_map[prog];
+    //get variables
+    Trace("csi-sol") << "Get solution for " << prog << ", which is applied as " << prog_app << std::endl;
+    if( prog_app.isNull() ){
+      Assert( d_prog_to_sol_index.find( prog )==d_prog_to_sol_index.end() );
+      success = false;
+    }else{
+      Assert( d_prog_to_sol_index.find( prog )!=d_prog_to_sol_index.end() );
+      Assert( prog_app.getNumChildren()==varList.getNumChildren()+1 );
+      sol_index = d_prog_to_sol_index[prog];
+      d_varList.clear();
+      d_sol->d_varList.clear();
+      for( unsigned i=1; i<prog_app.getNumChildren(); i++ ){
+        if( varList[i-1].getType().isBoolean() ){
+          //TODO force boolean term conversion mode
+          Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+          vars.push_back( prog_app[i].eqNode( c ) );
+        }else{
+          vars.push_back( prog_app[i] );
+        }
+        d_varList.push_back( varList[i-1] );
+        d_sol->d_varList.push_back( varList[i-1] );
+      }
     }
-    d_varList.push_back( varList[i-1] );
-    d_sol->d_varList.push_back( varList[i-1] );
   }
   //construct the solution
-  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;
+  Node s;
+  if( success ){
+    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;
+    s = constructSolution( indices, sol_index, 0 );
+    s = s.substitute( vars.begin(), vars.end(), d_varList.begin(), d_varList.end() );
+    d_orig_solution = s;
+  }else{
+    //function is unconstrained : make ground term of correct sort
+    s = d_qe->getTermDatabase()->getEnumerateTerm( TypeNode::fromType( dt.getSygusType() ), 0 );
+  }
 
   //simplify the solution
   Trace("csi-sol") << "Solution (pre-simplification): " << d_orig_solution << std::endl;
@@ -864,4 +1046,226 @@ void CegConjectureSingleInv::preregisterConjecture( Node q ) {
   d_orig_conjecture = q;
 }
 
+void SingleInvocationPartition::init( std::vector< TypeNode >& typs ){
+  Assert( d_arg_types.empty() );
+  Assert( d_si_vars.empty() );
+  d_arg_types.insert( d_arg_types.end(), typs.begin(), typs.end() );
+  for( unsigned j=0; j<d_arg_types.size(); j++ ){
+    Node si_v = NodeManager::currentNM()->mkBoundVar( d_arg_types[j] );
+    d_si_vars.push_back( si_v );
+  }
+}
+
+
+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 = TermDb::getQuantSimplify( 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;
+      if( processConjunct( cr, visited, args, terms, subs ) ){
+        for( unsigned j=0; j<terms.size(); j++ ){
+          si_terms.push_back( subs[j] );
+          si_subs.push_back( d_func_fo_var[subs[j].getOperator()] );
+        }
+        std::map< Node, Node > subs_map;
+        std::map< Node, Node > subs_map_rev;
+        std::vector< Node > funcs;
+        //normalize the invocations
+        if( !terms.empty() ){
+          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 );
+        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;
+        TermDb::getBoundVars( cr, bvs );
+        if( bvs.size()>d_si_vars.size() ){
+          Trace("si-prt") << "...not ground single invocation." << std::endl;
+          singleInvocation = false;
+        }else{
+          Trace("si-prt") << "...ground single invocation : success." << std::endl;
+        }
+      }else{
+        Trace("si-prt") << "...not single invocation." << std::endl;
+        singleInvocation = false;
+      }
+      Trace("si-prt") << "..... got si=" << singleInvocation << ", result : " << cr << std::endl;
+      d_conjuncts[2].push_back( cr );
+      if( singleInvocation ){
+        //replace with single invocation formulation
+        cr = cr.substitute( si_terms.begin(), si_terms.end(), si_subs.begin(), si_subs.end() );
+        Trace("si-prt") << "..... si version=" << cr << std::endl;
+        d_conjuncts[0].push_back( cr );
+      }else{
+        d_conjuncts[1].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 = TermDb::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;
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      if( !processConjunct( n[i], visited, args, terms, subs ) ){
+        ret = false;
+      }
+    }
+    if( ret ){
+      if( n.getKind()==APPLY_UF ){
+        if( std::find( terms.begin(), terms.end(), n )==terms.end() ){
+          Node f = n.getOperator();
+          //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 ){
+      ret = true;
+      std::vector< Node > children;
+      children.push_back( f );
+      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 ){
+        d_func_inv[f] = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+        std::stringstream ss;
+        ss << "F_" << f;
+        Node v = NodeManager::currentNM()->mkBoundVar( ss.str(), tn.getRangeType() );
+        d_func_fo_var[f] = v;
+        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] ) );
+}
+
+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<3; i++ ){
+    Trace(c) << ( i==0 ? "Single invocation" : ( i==1 ? "Non-single invocation" : "All" ) );
+    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;
+}
+
 }
\ 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 e814df110..0bdf246f0 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -42,11 +42,13 @@ public:
 };
 
 
+class SingleInvocationPartition;
 
 class CegConjectureSingleInv
 {
   friend class CegqiOutputSingleInv;
 private:
+  SingleInvocationPartition * d_sip;
   QuantifiersEngine * d_qe;
   CegConjecture * d_parent;
   CegConjectureSingleInvSol * d_sol;
@@ -63,6 +65,8 @@ private:
   //for recognizing templates for invariant synthesis
   int extractInvariantPolarity( Node n, Node inv, std::vector< Node >& curr_disj, bool pol );
   Node substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars );
+  // partially single invocation
+  Node removeDeepEmbedding( Node n, std::vector< Node >& progs, std::vector< TypeNode >& types, int& type_valid, std::map< Node, Node >& visited );
   //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 );
@@ -76,15 +80,16 @@ private:
   std::map< Node, Node > d_single_inv_app_map;
   //list of skolems for each argument of programs
   std::vector< Node > d_single_inv_arg_sk;
-  //list of skolems for each program
+  //list of variables/skolems for each program
+  std::vector< Node > d_single_inv_var;
   std::vector< Node > d_single_inv_sk;
   std::map< Node, int > d_single_inv_sk_index;
-  //list of skolems for each program
-  std::vector< Node > d_single_inv_var;
+  //program to solution index
+  std::map< Node, unsigned > d_prog_to_sol_index;
   //lemmas produced
   inst::InstMatchTrie d_inst_match_trie;
   inst::CDInstMatchTrie * d_c_inst_match_trie;
-  //original conjecture 
+  //original conjecture
   Node d_orig_conjecture;
   // solution
   std::vector< Node > d_varList;
@@ -108,12 +113,14 @@ public:
   CegConjectureSingleInv( QuantifiersEngine * qe, CegConjecture * p );
   // original conjecture
   Node d_quant;
-  // single invocation version of quant
+  // single invocation version of quantified formula
   Node d_single_inv;
   // transition relation version per program
   std::map< Node, Node > d_trans_pre;
   std::map< Node, Node > d_trans_post;
   std::map< Node, std::vector< Node > > d_prog_templ_vars;
+  //the non-single invocation portion of the quantified formula
+  std::map< Node, Node > d_nsi_op_map;
 public:
   //get the single invocation lemma(s)
   void getSingleInvLemma( Node guard, std::vector< Node >& lems );
@@ -135,6 +142,41 @@ public:
   void preregisterConjecture( Node q );
 };
 
+// partitions any formulas given to it into single invocation/non-single invocation
+// 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 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 );
+public:
+  void init( std::vector< TypeNode >& typs );
+  //inputs
+  void process( Node n );
+  std::vector< TypeNode > d_arg_types;
+  
+  //outputs (everything is with bound var)
+  std::map< Node, bool > d_funcs;
+  std::map< Node, Node > d_func_inv;
+  std::map< Node, Node > d_func_fo_var;
+  std::vector< Node > d_func_vars;
+  std::vector< Node > d_si_vars;
+  // si, nsi, all
+  std::vector< Node > d_conjuncts[3];
+  
+  bool isAntiSkolemizableType( Node f );
+  
+  Node getConjunct( int index );
+  Node getSingleInvocation() { return getConjunct( 0 ); }
+  Node getNonSingleInvocation() { return getConjunct( 1 ); }
+  Node getFullSpecification() { return getConjunct( 2 ); }
+  
+  void debugPrint( const char * c );
+};
+
+
 }
 }
 }
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index cdefcf8e9..be6f71c39 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -207,6 +207,8 @@ option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMo
   if and how to apply fairness for cegqi
 option cegqiSingleInv --cegqi-si bool :default false :read-write
   process single invocation synthesis conjectures
+option cegqiSingleInvPartial --cegqi-si-partial bool :default false
+  combined techniques for synthesis conjectures that are partially single invocation 
 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
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index d289e3938..fc1f052c3 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -75,7 +75,7 @@ bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) {
           for( std::map< Node, Node >::iterator it = msum2.begin(); it != msum2.end(); ++it ){
             std::map< Node, Node >::iterator it2 = msum.find( it->first );
             if( it2!=msum.end() ){
-              Node r = NodeManager::currentNM()->mkNode( MINUS, it2->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it2->second, 
+              Node r = NodeManager::currentNM()->mkNode( MINUS, it2->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it2->second,
                                                                 it->second.isNull() ? NodeManager::currentNM()->mkConst( Rational(1) ) : it->second );
               msum[it->first] = Rewriter::rewrite( r );
             }else{
@@ -155,6 +155,31 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Nod
   return ires;
 }
 
+Node QuantArith::solveEqualityFor( Node lit, Node v ) {
+  Assert( lit.getKind()==EQUAL || lit.getKind()==IFF );
+  //first look directly at sides
+  TypeNode tn = lit[0].getType();
+  for( unsigned r=0; r<2; r++ ){
+    if( lit[r]==v ){
+      return lit[1-r];
+    }
+  }
+  if( tn.isInteger() || tn.isReal() ){
+    if( quantifiers::TermDb::containsTerm( lit, v ) ){
+      std::map< Node, Node > msum;
+      if( QuantArith::getMonomialSumLit( lit, msum ) ){
+        Node val, veqc;
+        if( QuantArith::isolate( v, msum, veqc, val, EQUAL )!=0 ){
+          if( veqc.isNull() ){
+            return val;
+          }
+        }
+      }
+    }
+  }
+  return Node::null();
+}
+
 Node QuantArith::negate( Node t ) {
   Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t );
   tt = Rewriter::rewrite( tt );
@@ -184,33 +209,6 @@ void QuantArith::debugPrintMonomialSum( std::map< Node, Node >& msum, const char
   Trace(c) << std::endl;
 }
 
-bool QuantArith::solveEqualityFor( Node lit, Node v, Node & veq ) {
-  Assert( lit.getKind()==EQUAL || lit.getKind()==IFF );
-  //first look directly at sides
-  TypeNode tn = lit[0].getType();
-  for( unsigned r=0; r<2; r++ ){
-    if( lit[r]==v ){
-      Node olitr = lit[r==0 ? 1 : 0];
-      veq = tn.isBoolean() ? lit[r].iffNode( olitr ) : lit[r].eqNode( olitr );
-      return true;
-    }
-  }
-  if( tn.isInteger() || tn.isReal() ){
-    std::map< Node, Node > msum;
-    if( QuantArith::getMonomialSumLit( lit, msum ) ){
-      if( QuantArith::isolate( v, msum, veq, EQUAL ) ){
-        if( veq[0]!=v ){
-          Assert( veq[1]==v );
-          veq = v.eqNode( veq[0] );
-        }
-        return true;
-      }
-    }
-  }
-  return false;
-}
-
-
 
 void QuantRelevance::registerQuantifier( Node f ){
   //compute symbols in f
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index f65163415..566a09923 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -39,10 +39,10 @@ public:
   //return 1 : solved on LHS, return -1 : solved on RHS, return 0: failed
   static int isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff = false );
   static int isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k );
+  static Node solveEqualityFor( Node lit, Node v );
   static Node negate( Node t );
   static Node offset( Node t, int i );
   static void debugPrintMonomialSum( std::map< Node, Node >& msum, const char * c );
-  static bool solveEqualityFor( Node lit, Node v, Node & veq );
 };
 
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 79e62a6cd..724f16947 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -674,6 +674,47 @@ void TermDb::makeInstantiationConstantsFor( Node q ){
   }
 }
 
+void TermDb::getBoundVars2( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ) {
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    if( n.getKind()==BOUND_VARIABLE ){
+      if( std::find( vars.begin(), vars.end(), n )==vars.end() ) {
+        vars.push_back( n );
+      }
+    }
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      getBoundVars2( n[i], vars, visited );
+    }
+  }
+}
+
+Node TermDb::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) {
+  std::map< Node, Node >::iterator it = visited.find( n );
+  if( it!=visited.end() ){
+    return it->second;
+  }else{
+    Node ret = n;
+    if( n.getKind()==FORALL ){
+      ret = getRemoveQuantifiers2( n[1], visited );
+    }else if( n.getNumChildren()>0 ){
+      std::vector< Node > children;
+      bool childrenChanged = false;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node ni = getRemoveQuantifiers2( n[i], visited );
+        childrenChanged = childrenChanged || ni!=n[i];
+        children.push_back( ni );
+      }
+      if( childrenChanged ){
+        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+          children.insert( children.begin(), n.getOperator() );
+        }
+        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }
+    }
+    visited[n] = ret;
+    return ret;
+  }
+}
 
 Node TermDb::getInstConstAttr( Node n ) {
   if (!n.hasAttribute(InstConstantAttribute()) ){
@@ -722,6 +763,30 @@ bool TermDb::hasBoundVarAttr( Node n ) {
   return !getBoundVarAttr(n).isNull();
 }
 
+void TermDb::getBoundVars( Node n, std::vector< Node >& vars ) {
+  std::map< Node, bool > visited;
+  return getBoundVars2( n, vars, visited );
+}
+
+//remove quantifiers
+Node TermDb::getRemoveQuantifiers( Node n ) {
+  std::map< Node, Node > visited;
+  return getRemoveQuantifiers2( n, visited );
+}
+
+//quantified simplify 
+Node TermDb::getQuantSimplify( Node n ) {
+  std::vector< Node > bvs;
+  getBoundVars( n, bvs );
+  if( bvs.empty() ) {
+    return Rewriter::rewrite( n );
+  }else{
+    Node q = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs ), n );
+    q = Rewriter::rewrite( q );
+    return getRemoveQuantifiers( q );
+  }
+}
+
 /** get the i^th instantiation constant of q */
 Node TermDb::getInstantiationConstant( Node q, int i ) const {
   std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 8ce6aeaf0..86b0efbf3 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -267,7 +267,19 @@ public:
   static bool hasInstConstAttr( Node n );
   static Node getBoundVarAttr( Node n );
   static bool hasBoundVarAttr( Node n );
-
+  
+private:
+  /** get bound vars */
+  static void getBoundVars2( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited );
+  /** get bound vars */
+  static Node getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited );
+public:
+  //get the bound variables in this node
+  static void getBoundVars( Node n, std::vector< Node >& vars );
+  //remove quantifiers
+  static Node getRemoveQuantifiers( Node n );
+  //quantified simplify (treat free variables in n as quantified and run rewriter)
+  static Node getQuantSimplify( Node n );
 
 //for skolem
 private:
@@ -387,7 +399,7 @@ private:
   static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited );
 //general utilities
 public:
-  /** simple check for contains term */
+  /** simple check for whether n contains t as subterm */
   static bool containsTerm( Node n, Node t );
   /** simple check for contains term, true if contains at least one term in t */
   static bool containsTerms( Node n, std::vector< Node >& t );