docs: def compute_(self):
          """
              Main core-guided loop, which iteratively calls a SAT
              oracle, extracts a new unsatisfiable core and processes
              it. The loop finishes as soon as a satisfiable formula is
              obtained. If specified in the command line, the method
              additionally calls :meth:`adapt_am1` to detect and adapt
              intrinsic AtMost1 constraints before executing the loop.
  
              :rtype: bool
          """
  
          # trying to adapt (simplify) the formula
          # by detecting and using atmost1 constraints
          if self.adapt:
              self.adapt_am1()
  
          # main solving loop
          while not self.oracle.solve(assumptions=self.sels + self.sums):
              self.get_core()
  
              if not self.core:
                  # core is empty, i.e. hard part is unsatisfiable
                  return False
  
              self.process_core()
  
              if self.verbose > 1:
                  print('c cost: {0}; core sz: {1}; soft sz: {2}'.format(self.cost,
                      len(self.core), len(self.sels) + len(self.sums)))
  
          return True