Remove simplification specialized for sygus si solution reconstruction (#3147)

4 files changed, 6 insertions, 580 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 3fbb4eaee..e4f16de65 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -614,9 +614,9 @@ Node CegSingleInv::getSolution(unsigned sol_index,
   }
   d_orig_solution = s;
 
-  //simplify the solution
+  //simplify the solution using the extended rewriter
   Trace("csi-sol") << "Solution (pre-simplification): " << d_orig_solution << std::endl;
-  s = d_sol->simplifySolution( s, stn );
+  s = d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(s);
   Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl;
   return reconstructToSyntax( s, stn, reconstructed, rconsSygus );
 }
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index 074971622..b74caf49a 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -83,567 +83,6 @@ void CegSingleInvSol::debugTermSize(Node sol, int& t_size, int& num_ite)
   }
 }
 
-Node CegSingleInvSol::pullITEs(Node s)
-{
-  if( s.getKind()==ITE ){
-    bool success;
-    do {
-      success = false;
-      std::vector< Node > conj;
-      Node t;
-      Node rem;
-      if( pullITECondition( s, s, conj, t, rem, 0 ) ){
-        Assert( !conj.empty() );
-        Node cond = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
-        Trace("csi-sol-debug") << "For " << s << ", can pull " << cond << " -> " << t << " with remainder " << rem << std::endl;
-        t = pullITEs( t );
-        rem = pullITEs( rem );
-        Trace("csi-pull-ite") << "PI: Rewrite : " << s << std::endl;
-        Node prev = s;
-        s = NodeManager::currentNM()->mkNode( ITE, TermUtil::simpleNegate( cond ), t, rem );
-        Trace("csi-pull-ite") << "PI: Rewrite Now : " << s << std::endl;
-        Trace("csi-pull-ite") << "(= " << prev << " " << s << ")" << std::endl;
-        success = true;
-      }
-    }while( success );
-  }
-  return s;
-}
-
-// pull condition common to all ITE conditions in path of size > 1
-bool CegSingleInvSol::pullITECondition(Node root,
-                                       Node n_ite,
-                                       std::vector<Node>& conj,
-                                       Node& t,
-                                       Node& rem,
-                                       int depth)
-{
-  Assert( n_ite.getKind()==ITE );
-  std::vector< Node > curr_conj;
-  std::vector< Node > orig_conj;
-  bool isAnd;
-  if( n_ite[0].getKind()==AND || n_ite[0].getKind()==OR ){
-    isAnd = n_ite[0].getKind()==AND;
-    for( unsigned i=0; i<n_ite[0].getNumChildren(); i++ ){
-      Node cond = n_ite[0][i];
-      orig_conj.push_back( cond );
-      if( n_ite[0].getKind()==OR ){
-        cond = TermUtil::simpleNegate( cond );
-      }
-      curr_conj.push_back( cond );
-    }
-  }else{
-    Node neg = n_ite[0].negate();
-    if( std::find( conj.begin(), conj.end(), neg )!=conj.end() ){
-      //if negation of condition exists, use it
-      isAnd = false;
-      curr_conj.push_back( neg );
-    }else{
-      //otherwise, use condition
-      isAnd = true;
-      curr_conj.push_back( n_ite[0] );
-    }
-    orig_conj.push_back( n_ite[0] );
-  }
-  // take intersection with current conditions
-  std::vector< Node > new_conj;
-  std::vector< Node > prev_conj;
-  if( n_ite==root ){
-    new_conj.insert( new_conj.end(), curr_conj.begin(), curr_conj.end() );
-    Trace("csi-sol-debug") << "Pull ITE root " << n_ite << ", #conj = " << new_conj.size() << std::endl;
-  }else{
-    for( unsigned i=0; i<curr_conj.size(); i++ ){
-      if( std::find( conj.begin(), conj.end(), curr_conj[i] )!=conj.end() ){
-        new_conj.push_back( curr_conj[i] );
-      }
-    }
-    Trace("csi-sol-debug") << "Pull ITE " << n_ite << ", #conj = " << conj.size() << " intersect " << curr_conj.size() << " = " << new_conj.size() << std::endl;
-  }
-  //cannot go further
-  if( new_conj.empty() ){
-    return false;
-  }
-  //it is an intersection with current
-  conj.clear();
-  conj.insert( conj.end(), new_conj.begin(), new_conj.end() );
-  //recurse if possible
-  Node trec = n_ite[ isAnd ? 2 : 1 ];
-  Node tval = n_ite[ isAnd ? 1 : 2 ];
-  bool success = false;
-  if( trec.getKind()==ITE ){
-    prev_conj.insert( prev_conj.end(), conj.begin(), conj.end() );
-    success = pullITECondition( root, trec, conj, t, rem, depth+1 );
-  }
-  if( !success && depth>0 ){
-    t = trec;
-    rem = trec;
-    success = true;
-    if( trec.getKind()==ITE ){
-      //restore previous state
-      conj.clear();
-      conj.insert( conj.end(), prev_conj.begin(), prev_conj.end() );
-    }
-  }
-  if( success ){
-    //make remainder : strip out conditions in conj
-    Assert( !conj.empty() );
-    std::vector< Node > cond_c;
-    Assert( orig_conj.size()==curr_conj.size() );
-    for( unsigned i=0; i<curr_conj.size(); i++ ){
-      if( std::find( conj.begin(), conj.end(), curr_conj[i] )==conj.end() ){
-        cond_c.push_back( orig_conj[i] );
-      }
-    }
-    if( cond_c.empty() ){
-      rem = tval;
-    }else{
-      Node new_cond = cond_c.size()==1 ? cond_c[0] : NodeManager::currentNM()->mkNode( n_ite[0].getKind(), cond_c );
-      rem = NodeManager::currentNM()->mkNode( ITE, new_cond, isAnd ? tval : rem, isAnd ? rem : tval );
-    }
-    return true;
-  }else{
-    return false;
-  }
-}
-
-Node CegSingleInvSol::flattenITEs(Node n, bool rec)
-{
-  Assert( !n.isNull() );
-  if( n.getKind()==ITE ){
-    Trace("csi-sol-debug") << "Flatten ITE." << std::endl;
-    Node ret;
-    Node n0 = rec ? flattenITEs( n[0] ) : n[0];
-    Node n1 = rec ? flattenITEs( n[1] ) : n[1];
-    Node n2 = rec ? flattenITEs( n[2] ) : n[2];
-    Assert( !n0.isNull() );
-    Assert( !n1.isNull() );
-    Assert( !n2.isNull() );
-    if( n0.getKind()==NOT ){
-      ret = NodeManager::currentNM()->mkNode( ITE, n0[0], n2, n1 );
-    }else if( n0.getKind()==AND || n0.getKind()==OR ){
-      std::vector< Node > children;
-      for( unsigned i=1; i<n0.getNumChildren(); i++ ){
-        children.push_back( n0[i] );
-      }
-      Node rem = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( n0.getKind(), children );
-      if( n0.getKind()==AND ){
-        ret = NodeManager::currentNM()->mkNode( ITE, rem, NodeManager::currentNM()->mkNode( ITE, n0[0], n1, n2 ), n2 );
-      }else{
-        ret = NodeManager::currentNM()->mkNode( ITE, rem, n1, NodeManager::currentNM()->mkNode( ITE, n0[0], n1, n2 ) );
-      }
-    }else{
-      if( n0.getKind()==ITE ){
-        n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ),
-                                                   NodeManager::currentNM()->mkNode( AND, n0.negate(), n2 ) );
-      }else if( n0.getKind()==EQUAL && n0[0].getType().isBoolean() ){
-        n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ),
-                                                   NodeManager::currentNM()->mkNode( AND, n0.negate(), n1.negate() ) );
-      }else{
-        return NodeManager::currentNM()->mkNode( ITE, n0, n1, n2 );
-      }
-      ret = NodeManager::currentNM()->mkNode( ITE, n0, n1, n2 );
-    }
-    Assert( !ret.isNull() );
-    return flattenITEs( ret, false );
-  }else{
-    if( n.getNumChildren()>0 ){
-      std::vector< Node > children;
-      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-        children.push_back( n.getOperator() );
-      }
-      bool childChanged = false;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        Node nc = flattenITEs( n[i] );
-        children.push_back( nc );
-        childChanged = childChanged || nc!=n[i];
-      }
-      if( !childChanged ){
-        return n;
-      }else{
-        return NodeManager::currentNM()->mkNode( n.getKind(), children );
-      }
-    }else{
-      return n;
-    }
-  }
-}
-
-// assign is from literals to booleans
-// union_find is from args to values
-
-bool CegSingleInvSol::getAssign(bool pol,
-                                Node n,
-                                std::map<Node, bool>& assign,
-                                std::vector<Node>& new_assign,
-                                std::vector<Node>& vars,
-                                std::vector<Node>& new_vars,
-                                std::vector<Node>& new_subs)
-{
-  std::map< Node, bool >::iterator ita = assign.find( n );
-  if( ita!=assign.end() ){
-    Trace("csi-simp-debug") << "---already assigned, lookup " << pol << " " << ita->second << std::endl;
-    return pol==ita->second;
-  }else if( n.isConst() ){
-    return pol==(n==d_qe->getTermUtil()->d_true);
-  }else{
-    Trace("csi-simp-debug") << "---assign " << n << " " << pol << std::endl;
-    assign[n] = pol;
-    new_assign.push_back( n );
-    if( ( pol && n.getKind()==AND ) || ( !pol && n.getKind()==OR ) ){
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        if( !getAssign( pol, n[i], assign, new_assign, vars, new_vars, new_subs ) ){
-          return false;
-        }
-      }
-    }else if( n.getKind()==NOT ){
-      return getAssign( !pol, n[0], assign, new_assign, vars, new_vars, new_subs );
-    }else if( pol && n.getKind()==EQUAL ){
-      getAssignEquality( n, vars, new_vars, new_subs );
-    }
-  }
-  return true;
-}
-
-bool CegSingleInvSol::getAssignEquality(Node eq,
-                                        std::vector<Node>& vars,
-                                        std::vector<Node>& new_vars,
-                                        std::vector<Node>& new_subs)
-{
-  Assert( eq.getKind()==EQUAL );
-  //try to find valid argument
-  for( unsigned r=0; r<2; r++ ){
-    if( std::find( d_varList.begin(), d_varList.end(), eq[r] )!=d_varList.end() ){
-      Assert( std::find( vars.begin(), vars.end(), eq[r] )==vars.end() );
-      if( std::find( new_vars.begin(), new_vars.end(), eq[r] )==new_vars.end() ){
-        Node eqro = eq[r==0 ? 1 : 0 ];
-        if (!expr::hasSubterm(eqro, eq[r]))
-        {
-          Trace("csi-simp-debug")
-              << "---equality " << eq[r] << " = " << eqro << std::endl;
-          new_vars.push_back(eq[r]);
-          new_subs.push_back(eqro);
-          return true;
-        }
-      }
-    }
-  }
-  return false;
-}
-
-Node CegSingleInvSol::simplifySolution(Node sol, TypeNode stn)
-{
-  int tsize, itesize;
-  if( Trace.isOn("csi-sol") ){
-    tsize = 0;itesize = 0;
-    debugTermSize( sol, tsize, itesize );
-    Trace("csi-sol") << tsize << " " << itesize << " rewrite..." << std::endl;
-    Trace("csi-sol-debug") << "sol : " << sol << "..." << std::endl;
-  }
-  Node sol0 = Rewriter::rewrite( sol );
-  Trace("csi-sol") << "now : " << sol0 << std::endl;
-
-  Node curr_sol = sol0;
-  Node prev_sol;
-  do{
-    prev_sol = curr_sol;
-    //first, pull ITE conditions
-    if( Trace.isOn("csi-sol") ){
-      tsize = 0;itesize = 0;
-      debugTermSize( curr_sol, tsize, itesize );
-      Trace("csi-sol") << tsize << " " << itesize << " pull ITE..." << std::endl;
-      Trace("csi-sol-debug") << "sol : " << curr_sol << "..." << std::endl;
-    }
-    Node sol1 = pullITEs( curr_sol );
-    Trace("csi-sol") << "now : " << sol1 << std::endl;
-    //do standard rewriting
-    if( sol1!=curr_sol ){
-      if( Trace.isOn("csi-sol") ){
-        tsize = 0;itesize = 0;
-        debugTermSize( sol1, tsize, itesize );
-        Trace("csi-sol") << tsize << " " << itesize << " rewrite..." << std::endl;
-        Trace("csi-sol-debug") << "sol : " << sol1 << "..." << std::endl;
-      }
-      Node sol2 = Rewriter::rewrite( sol1 );
-      Trace("csi-sol") << "now : " << sol2 << std::endl;
-      curr_sol = sol2;
-    }
-    //now do branch analysis
-    if( Trace.isOn("csi-sol") ){
-      tsize = 0;itesize = 0;
-      debugTermSize( curr_sol, tsize, itesize );
-      Trace("csi-sol") << tsize << " " << itesize << " simplify solution..." << std::endl;
-      Trace("csi-sol-debug") << "sol : " << curr_sol << "..." << std::endl;
-    }
-    std::map< Node, bool > sassign;
-    std::vector< Node > svars;
-    std::vector< Node > ssubs;
-    Node sol3 = simplifySolutionNode( curr_sol, stn, sassign, svars, ssubs, 0 );
-    Trace("csi-sol") << "now : " << sol3 << std::endl;
-    if( sol3!=curr_sol ){
-      //do standard rewriting again
-      if( Trace.isOn("csi-sol" ) ){
-        tsize = 0;itesize = 0;
-        debugTermSize( sol3, tsize, itesize );
-        Trace("csi-sol") << tsize << " " << itesize << " rewrite..." << std::endl;
-      }
-      Node sol4 = Rewriter::rewrite( sol3 );
-      Trace("csi-sol") << "now : " << sol4 << std::endl;
-      curr_sol = sol4;
-    }
-  }while( curr_sol!=prev_sol );
-
-  return curr_sol;
-}
-
-Node CegSingleInvSol::simplifySolutionNode(Node sol,
-                                           TypeNode stn,
-                                           std::map<Node, bool>& assign,
-                                           std::vector<Node>& vars,
-                                           std::vector<Node>& subs,
-                                           int status)
-{
-  Assert( vars.size()==subs.size() );
-  std::map< Node, bool >::iterator ita = assign.find( sol );
-  if( ita!=assign.end() ){
-    //it is currently assigned a boolean value
-    return NodeManager::currentNM()->mkConst( ita->second );
-  }else{
-    d_qe->getTermDatabaseSygus()->registerSygusType( stn );
-    std::map< int, TypeNode > stnc;
-    if( !stn.isNull() ){
-      int karg = d_qe->getTermDatabaseSygus()->getKindConsNum( stn, sol.getKind() );
-      if( karg!=-1 ){
-        const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
-        if( dt[karg].getNumArgs()==sol.getNumChildren() ){
-          for( unsigned i=0; i<dt[karg].getNumArgs(); i++ ){
-            stnc[i] = d_qe->getTermDatabaseSygus()->getArgType( dt[karg], i );
-          }
-        }
-      }
-    }
-
-    if( sol.getKind()==ITE ){
-      Trace("csi-simp") << "Simplify ITE " << std::endl;
-      std::vector< Node > children;
-      for( unsigned r=1; r<=2; r++ ){
-        std::vector< Node > new_assign;
-        std::vector< Node > new_vars;
-        std::vector< Node > new_subs;
-        if( getAssign( r==1, sol[0], assign, new_assign, vars, new_vars, new_subs ) ){
-          Trace("csi-simp") << "- branch " << r << " led to " << new_assign.size() << " assignments, " << new_vars.size() << " equalities." << std::endl;
-          unsigned prev_size = vars.size();
-          Node nc = sol[r];
-          if( !new_vars.empty() ){
-            nc = nc.substitute( new_vars.begin(), new_vars.end(), new_subs.begin(), new_subs.end() );
-            vars.insert( vars.end(), new_vars.begin(), new_vars.end() );
-            subs.insert( subs.end(), new_subs.begin(), new_subs.end() );
-          }
-          nc = simplifySolutionNode( nc, stnc[r], assign, vars, subs, 0 );
-          children.push_back( nc );
-          //clean up substitution
-          if( !new_vars.empty() ){
-            vars.resize( prev_size );
-            subs.resize( prev_size );
-          }
-        }else{
-          Trace("csi-simp") << "- branch " << r << " of " << sol[0] << " is infeasible." << std::endl;
-        }
-        //clean up assignment
-        for( unsigned i=0; i<new_assign.size(); i++ ){
-          assign.erase( new_assign[i] );
-        }
-      }
-      if( children.size()==1 || ( children.size()==2 && children[0]==children[1] ) ){
-        return children[0];
-      }else{
-        Assert( children.size()==2 );
-        Node ncond = simplifySolutionNode( sol[0], stnc[0], assign, vars, subs, 0 );
-        Node ret = NodeManager::currentNM()->mkNode( ITE, ncond, children[0], children[1] );
-
-        //expand/flatten if necessary
-        Node orig_ret = ret;
-        if( !stnc[0].isNull() ){
-          d_qe->getTermDatabaseSygus()->registerSygusType( stnc[0] );
-          Node prev_ret;
-          while( !d_qe->getTermDatabaseSygus()->hasKind( stnc[0], ret[0].getKind() ) && ret!=prev_ret ){
-            prev_ret = ret;
-            Node exp_c = d_qe->getTermDatabaseSygus()->expandBuiltinTerm( ret[0] );
-            if( !exp_c.isNull() ){
-              Trace("csi-simp-debug") << "Pre expand to " << ret[0] << " to " << exp_c << std::endl;
-              ret = NodeManager::currentNM()->mkNode( ITE, exp_c, ret[1], ret[2] );
-            }
-            if( !d_qe->getTermDatabaseSygus()->hasKind( stnc[0], ret[0].getKind() ) ){
-              Trace("csi-simp-debug") << "Flatten based on " << ret[0] << "." << std::endl;
-              ret = flattenITEs( ret, false );
-            }
-          }
-        }
-        return ret;
-        /*
-        if( orig_ret!=ret ){
-          Trace("csi-simp") << "Try expanded ITE" << std::endl;
-          return ret;//simplifySolutionNode( ret, stn, assign, vars, subs, status );
-        }else{
-          return ret;
-        }
-        */
-      }
-    }else if( sol.getKind()==OR || sol.getKind()==AND ){
-      Trace("csi-simp") << "Simplify " << sol.getKind() << std::endl;
-      //collect new equalities
-      std::map< Node, bool > atoms;
-      std::vector< Node > inc;
-      std::vector< Node > children;
-      std::vector< Node > new_vars;
-      std::vector< Node > new_subs;
-      Node bc = sol.getKind()==OR ? d_qe->getTermUtil()->d_true : d_qe->getTermUtil()->d_false;
-      for( unsigned i=0; i<sol.getNumChildren(); i++ ){
-        bool do_exc = false;
-        Node c;
-        std::map< Node, bool >::iterator ita = assign.find( sol[i] );
-        if( ita==assign.end() ){
-          c = sol[i];
-        }else{
-          c = NodeManager::currentNM()->mkConst( ita->second );
-        }
-        Trace("csi-simp") << "  - child " << i << " : " << c << std::endl;
-        if( c.isConst() ){
-          if( c==bc ){
-            Trace("csi-simp") << "  ...singularity." << std::endl;
-            return bc;
-          }else{
-            do_exc = true;
-          }
-        }else{
-          Node atom = c.getKind()==NOT ? c[0] : c;
-          bool pol = c.getKind()!=NOT;
-          std::map< Node, bool >::iterator it = atoms.find( atom );
-          if( it==atoms.end() ){
-            atoms[atom] = pol;
-            if( status==0 && atom.getKind()==EQUAL ){
-              if( pol==( sol.getKind()==AND ) ){
-                Trace("csi-simp") << "  ...equality." << std::endl;
-                if( getAssignEquality( atom, vars, new_vars, new_subs ) ){
-                  children.push_back( sol[i] );
-                  do_exc = true;
-                }
-              }
-            }
-          }else{
-            //repeated atom
-            if( it->second!=pol ){
-              return NodeManager::currentNM()->mkConst( sol.getKind()==OR );
-            }else{
-              do_exc = true;
-            }
-          }
-        }
-        if( !do_exc ){
-          inc.push_back( sol[i] );
-        }else{
-          Trace("csi-simp") << "  ...exclude." << std::endl;
-        }
-      }
-      if( !new_vars.empty() ){
-        if( !inc.empty() ){
-          Node ret = inc.size()==1 ? inc[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc );
-          Trace("csi-simp") << "Base return is : " << ret << std::endl;
-          // apply substitution
-          ret = ret.substitute( new_vars.begin(), new_vars.end(), new_subs.begin(), new_subs.end() );
-          ret = Rewriter::rewrite( ret );
-          Trace("csi-simp") << "After substitution : " << ret << std::endl;
-          unsigned prev_size = vars.size();
-          vars.insert( vars.end(), new_vars.begin(), new_vars.end() );
-          subs.insert( subs.end(), new_subs.begin(), new_subs.end() );
-          ret = simplifySolutionNode( ret, TypeNode::null(), assign, vars, subs, 1 );
-          //clean up substitution
-          if( !vars.empty() ){
-            vars.resize( prev_size );
-            subs.resize( prev_size );
-          }
-          //Trace("csi-simp") << "After simplification : " << ret << std::endl;
-          if( ret.isConst() ){
-            if( ret==bc ){
-              return bc;
-            }
-          }else{
-            if( ret.getKind()==sol.getKind() ){
-              for( unsigned i=0; i<ret.getNumChildren(); i++ ){
-                children.push_back( ret[i] );
-              }
-            }else{
-              children.push_back( ret );
-            }
-          }
-        }
-      }else{
-        //recurse on children
-        for( unsigned i=0; i<inc.size(); i++ ){
-          Node retc = simplifySolutionNode( inc[i], TypeNode::null(), assign, vars, subs, 0 );
-          if( retc.isConst() ){
-            if( retc==bc ){
-              return bc;
-            }
-          }else{
-            children.push_back( retc );
-          }
-        }
-      }
-      // now, remove all equalities that are implied
-      std::vector< Node > final_children;
-      for( unsigned i=0; i<children.size(); i++ ){
-        bool red = false;
-        Node atom = children[i].getKind()==NOT ? children[i][0] : children[i];
-        bool pol = children[i].getKind()!=NOT;
-        if( status==0 && atom.getKind()==EQUAL ){
-          if( pol!=( sol.getKind()==AND ) ){
-            std::vector< Node > tmp_vars;
-            std::vector< Node > tmp_subs;
-            if( getAssignEquality( atom, vars, tmp_vars, tmp_subs ) ){
-              Trace("csi-simp-debug") << "Check if " << children[i] << " is redundant in " << sol << std::endl;
-              for( unsigned j=0; j<children.size(); j++ ){
-                if( j!=i && ( j>i || std::find( final_children.begin(), final_children.end(), children[j] )!=final_children.end() ) ){
-                  Node sj = children[j].substitute( tmp_vars.begin(), tmp_vars.end(), tmp_subs.begin(), tmp_subs.end() );
-                  sj = Rewriter::rewrite( sj );
-                  if( sj==( sol.getKind()==AND ? d_qe->getTermUtil()->d_false : d_qe->getTermUtil()->d_true ) ){
-                    Trace("csi-simp") << "--- " << children[i].negate() << " is implied by " << children[j].negate() << std::endl;
-                    red = true;
-                    break;
-                  }
-                }
-              }
-              if( !red ){
-                Trace("csi-simp-debug") << "...is not." << std::endl;
-              }
-            }
-          }
-        }
-        if( !red ){
-          final_children.push_back( children[i] );
-        }
-      }
-      return final_children.size()==0 ? NodeManager::currentNM()->mkConst( sol.getKind()==AND ) :
-             ( final_children.size()==1 ? final_children[0] : NodeManager::currentNM()->mkNode( sol.getKind(), final_children ) );
-    }else{
-      //generic simplification
-      std::vector< Node > children;
-      if( sol.getMetaKind() == kind::metakind::PARAMETERIZED ){
-        children.push_back( sol.getOperator() );
-      }
-      bool childChanged = false;
-      for( unsigned i=0; i<sol.getNumChildren(); i++ ){
-        Node nc = simplifySolutionNode( sol[i], stnc[i], assign, vars, subs, 0 );
-        childChanged = childChanged || nc!=sol[i];
-        children.push_back( nc );
-      }
-      if( childChanged ){
-        return NodeManager::currentNM()->mkNode( sol.getKind(), children );
-      }
-    }
-    return sol;
-  }
-}
-
 void CegSingleInvSol::preregisterConjecture(Node q)
 {
   Trace("csi-sol") << "Preregister conjecture : " << q << std::endl;
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
index 40117af6c..6a00bc467 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h
@@ -45,23 +45,9 @@ class CegSingleInvSol
 private:
   bool debugSolution( Node sol );
   void debugTermSize( Node sol, int& t_size, int& num_ite );
-  Node pullITEs( Node n );
-  bool pullITECondition( Node root, Node n, std::vector< Node >& conj, Node& t, Node& rem, int depth );
-  Node flattenITEs( Node n, bool rec = true );
-  bool getAssign( bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign,
-                  std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs );
-  bool getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs );
-  Node simplifySolutionNode( Node sol, TypeNode stn, std::map< Node, bool >& assign,
-                             std::vector< Node >& vars, std::vector< Node >& subs, int status );
 
  public:
   CegSingleInvSol(QuantifiersEngine* qe);
-  /** simplify solution
-   *
-   * Returns the simplified version of node sol whose syntax is restricted by
-   * the grammar corresponding to sygus datatype stn.
-   */
-  Node simplifySolution( Node sol, TypeNode stn );
   /** reconstruct solution
    *
    * Returns (if possible) a node that is equivalent to sol those syntax
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 19e5fa899..9a1e5d6dc 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1635,9 +1635,7 @@ set(regress_1_tests
   regress1/sygus-abduct-test-user.smt2
   regress1/sygus/VC22_a.sy
   regress1/sygus/abv.sy
-  regress1/sygus/array_search_2.sy
   regress1/sygus/array_search_5-Q-easy.sy
-  regress1/sygus/array_sum_2_5.sy
   regress1/sygus/bvudiv-by-2.sy
   regress1/sygus/car_3.lus.sy
   regress1/sygus/cegar1.sy
@@ -1652,7 +1650,6 @@ set(regress_1_tests
   regress1/sygus/constant-ite-bv.sy
   regress1/sygus/constant.sy
   regress1/sygus/crci-ssb-unk.sy
-  regress1/sygus/crcy-si-rcons.sy
   regress1/sygus/crcy-si.sy
   regress1/sygus/cube-nia.sy
   regress1/sygus/double.sy
@@ -2176,6 +2173,10 @@ set(regression_disabled_tests
   regress1/sygus/Base16_1.sy
   regress1/sygus/enum-test.sy
   regress1/sygus/inv_gen_fig8.sy
+  # rely on heuristic solution reconstruction TODO #3146 revisit
+  regress1/sygus/array_search_2.sy
+  regress1/sygus/array_sum_2_5.sy
+  regress1/sygus/crcy-si-rcons.sy
   regress2/arith/arith-int-098.cvc
   regress2/arith/miplib-opt1217--27.smt2
   regress2/arith/miplib-pp08a-3000.smt2