docs: def init(self, formula, incr=False):
          """
              Initialize the internal SAT oracle. The oracle is used
              incrementally and so it is initialized only once when
              constructing an object of class :class:`RC2`. Given an
              input :class:`.WCNF` formula, the method bootstraps the
              oracle with its hard clauses. It also augments the soft
              clauses with "fresh" selectors and adds them to the oracle
              afterwards.
  
              Optional input parameter ``incr`` (``False`` by default)
              regulates whether or not Glucose's incremental mode [6]_
              is turned on.
  
              :param formula: input formula
              :param incr: apply incremental mode of Glucose
  
              :type formula: :class:`.WCNF`
              :type incr: bool
          """
  
          # creating a solver object
          self.oracle = Solver(name=self.solver, bootstrap_with=formula.hard,
                  incr=incr, use_timer=True)
  
          # adding soft clauses to oracle
          for i, cl in enumerate(formula.soft):
              selv = cl[0]  # if clause is unit, selector variable is its literal
  
              if len(cl) > 1:
                  self.topv += 1
                  selv = self.topv
  
                  cl.append(-self.topv)
                  self.oracle.add_clause(cl)
  
              if selv not in self.wght:
                  # record selector and its weight
                  self.sels.append(selv)
                  self.wght[selv] = formula.wght[i]
                  self.smap[selv] = i
              else:
                  # selector is not new; increment its weight
                  self.wght[selv] += formula.wght[i]
  
          # storing the set of selectors
          self.sels_set = set(self.sels)
  
          # at this point internal and external variables are the same
          for v in range(1, formula.nv + 1):
              self.vmap.e2i[v] = v
              self.vmap.i2e[v] = v
  
          if self.verbose > 1:
              print('c formula: {0} vars, {1} hard, {2} soft'.format(formula.nv,
                  len(formula.hard), len(formula.soft)))