code: def _compute(self):
          
  
          while True:
              if self.oracle.solve(assumptions=self.sels):
                  self.model = self.oracle.get_model()
                  self.model = filter(lambda l: abs(l) <= self.orig_nv, self.model)
                  return
              else:
                  self.treat_core()
  
                  if self.verbose > 1:
                      print('c cost: {0}; core sz: {1}'.format(self.cost, len(self.core)))
  
                  self.reinit()
docs: This method implements WMSU1 algorithm. The method is essentially a
              loop, which at each iteration calls the SAT oracle to decide
              whether the working formula is satisfiable. If it is, the method
              derives a model (stored in variable ``self.model``) and returns.
              Otherwise, a new unsatisfiable core of the formula is extracted
              and processed (see :func:`treat_core`), and the algorithm proceeds.