docs: def relax_core(self):
          """
              Relax and bound the core.
  
              After unsatisfiable core splitting, this method is called. If the
              core contains only one clause, i.e. this clause cannot be satisfied
              together with the hard clauses of the formula, the formula gets
              augmented with the negation of the clause (see
              :func:`remove_unit_core`).
  
              Otherwise (if the core contains more than one clause), every clause
              :math:`c` of the core is *relaxed*. This means a new *relaxation
              literal* is added to the clause, i.e. :math:`c\gets c\\vee r`,
              where :math:`r` is a fresh (unused) relaxation variable. After the
              clauses get relaxed, a new cardinality encoding is added to the
              formula enforcing the sum of the new relaxation variables to be not
              greater than 1, :math:`\sum_{c\in\phi}{r\leq 1}`, where
              :math:`\phi` denotes the unsatisfiable core.
          """
  
          if len(self.core) > 1:
              # relaxing
              rels = []
  
              for clid in self.core:
                  self.topv += 1
                  rels.append(self.topv)
                  self.soft[clid].append(self.topv)
  
              # creating a new cardinality constraint
              am1 = CardEnc.atmost(lits=rels, top_id=self.topv, encoding=self.cenc)
  
              for cl in am1.clauses:
                  self.hard.append(cl)
  
              # only if minicard
              # (for other solvers am1.atmosts should be empty)
              for am in am1.atmosts:
                  self.atm1.append(am)
  
              self.topv = am1.nv
  
          elif len(self.core) == 1:  # unit core => simply negate the clause
              self.remove_unit_core()