code: def exhaust_core(self, tobj):
          
  
          # the first case is simpler
          if self.oracle.solve(assumptions=[-tobj.rhs[1]]):
              return 1
          else:
              self.cost += self.minw
  
          for i in range(2, len(self.rels)):
              # saving the previous bound
              self.tobj[-tobj.rhs[i - 1]] = tobj
              self.bnds[-tobj.rhs[i - 1]] = i - 1
  
              # increasing the bound
              self.update_sum(-tobj.rhs[i - 1])
  
              if self.oracle.solve(assumptions=[-tobj.rhs[i]]):
                  # the bound should be equal to i
                  return i
  
              # the cost should increase further
              self.cost += self.minw
  
          return None
docs: Exhaust core by increasing its bound as much as possible.
              Core exhaustion was originally referred to as *cover
              optimization* in [5]_.
  
              Given a totalizer object ``tobj`` representing a sum of
              some *relaxation* variables :math:`r\in R` that augment
              soft clauses :math:`\\mathcal{C}_r`, the idea is to
              increase the right-hand side of the sum (which is equal to
              1 by default) as much as possible, reaching a value
              :math:`k` s.t. formula
              :math:`\\mathcal{H}\wedge\\mathcal{C}_r\wedge(\sum_{r\in
              R}{r\leq k})` is still unsatisfiable while increasing it
              further makes the formula satisfiable (here
              :math:`\\mathcal{H}` denotes the hard part of the
              formula).
  
              The rationale is that calling an oracle incrementally on a
              series of slightly modified formulas focusing only on the
              recently computed unsatisfiable core and disregarding the
              rest of the formula may be practically effective.