def treat_core(self):
        """
            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`).
        """

        # 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()
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`).