code: def split_core(self, minw):
          
  
          for clid in self.core:
              sel = self.sels[clid]
  
              if self.wght[clid] > minw:
                  self.topv += 1
  
                  cl_new = []
                  for l in self.soft[clid]:
                      if l != -sel:
                          cl_new.append(l)
                      else:
                          cl_new.append(-self.topv)
  
                  self.sels.append(self.topv)
                  self.vmap[self.topv] = len(self.soft)
  
                  self.soft.append(cl_new)
                  self.wght.append(self.wght[clid] - minw)
                  self.wght[clid] = minw
  
                  self.scpy.append(True)
docs: Split clauses in the core whenever necessary.
  
              Given a list of soft clauses in an unsatisfiable core, the method
              is used for splitting clauses whose weights are greater than the
              minimum weight of the core, i.e. the ``minw`` value computed in
              :func:`treat_core`. Each clause :math:`(c\\vee\\neg{s},w)`, s.t.
              :math:`w>minw` and :math:`s` is its selector literal, is split into
              clauses (1) clause :math:`(c\\vee\\neg{s}, minw)` and (2) a
              residual clause :math:`(c\\vee\\neg{s}',w-minw)`. Note that the
              residual clause has a fresh selector literal :math:`s'` different
              from :math:`s`.
  
              :param minw: minimum weight of the core
              :type minw: int