code: def _init(self, formula):
          
  
          self.oracle = Solver(name=self.solver, bootstrap_with=formula.hard,
                  incr=True, use_timer=True)
  
          for i, cl in enumerate(formula.soft):
              # TODO: if clause is unit, use its literal as selector
              # (ITotalizer must be extended to support PB constraints first)
              self.topv += 1
              selv = self.topv
              cl.append(self.topv)
              self.oracle.add_clause(cl)
              self.sels.append(selv)
  
          if self.verbose > 1:
              print('c formula: {0} vars, {1} hard, {2} soft'.format(formula.nv, len(formula.hard), len(formula.soft)))
docs: SAT oracle initialization. The method creates a new SAT oracle and
              feeds it with the formula's hard clauses. Afterwards, all soft
              clauses of the formula are augmented with selector literals and
              also added to the solver. The list of all introduced selectors is
              stored in variable ``self.sels``.
  
              :param formula: input MaxSAT formula
              :type formula: :class:`WCNF`