code: def treat_core(self):
          
  
          # extracting the core
          self.core = [self.vmap[sel] for sel in self.oracle.get_core()]
          minw = min(map(lambda i: self.wght[i], self.core))
  
          # updating the cost
          self.cost += minw
  
          # splitting clauses in the core if necessary
          self.split_core(minw)
  
          # relaxing clauses in the core and adding a new atmost1 constraint
          self.relax_core()
docs: Now that the previous SAT call returned UNSAT, a new unsatisfiable
              core should be extracted and relaxed. Core extraction is done
              through a call to the :func:`pysat.solvers.Solver.get_core` method,
              which returns a subset of the selector literals deemed responsible
              for unsatisfiability.
  
              After the core is extracted, its *minimum weight* ``minw`` is
              computed, i.e. it is the minimum weight among the weights of all
              soft clauses involved in the core (see [5]_). Note that the cost of
              the MaxSAT solution is incremented by ``minw``.
  
              Clauses that have weight larger than ``minw`` are split (see
              :func:`split_core`). Afterwards, all clauses of the unsatisfiable
              core are relaxed (see :func:`relax_core`).