docs: def atleast(cls, lits, bound=1, top_id=None, encoding=EncType.seqcounter):
          """
              This method can be used for creating a CNF encoding of an AtLeastK
              constraint, i.e. of :math:`\sum_{i=1}^{n}{x_i}\geq k`. The method
              takes 1 mandatory argument ``lits`` and 3 default arguments can be
              specified: ``bound``, ``top_id``, and ``encoding``.
  
              :param lits: a list of literals in the sum.
              :param bound: the value of bound :math:`k`.
              :param top_id: top variable identifier used so far.
              :param encoding: identifier of the encoding to use.
  
              :type lits: iterable(int)
              :type bound: int
              :type top_id: integer or None
              :type encoding: integer
  
              Parameter ``top_id`` serves to increase integer identifiers of
              auxiliary variables introduced during the encoding process. This is
              helpful when augmenting an existing CNF formula with the new
              cardinality encoding to make sure there is no collision between
              identifiers of the variables. If specified the identifiers of the
              first auxiliary variable will be ``top_id+1``.
  
              The default value of ``encoding`` is :attr:`Enctype.seqcounter`.
  
              The method *translates* the AtLeast constraint into an AtMost
              constraint by *negating* the literals of ``lits``, creating a new
              bound :math:`n-k` and invoking :meth:`CardEnc.atmost` with the
              modified list of literals and the new bound.
  
              :raises CardEnc.NoSuchEncodingError: if encoding does not exist.
  
              :rtype: a :class:`.CNFPlus` object where the new \
              clauses (or the new native atmost constraint) are stored.
          """
  
          if encoding < 0 or encoding > 9:
              raise(NoSuchEncodingError(encoding))
  
          if not top_id:
              top_id = max(map(lambda x: abs(x), lits))
  
          # we are going to return this formula
          ret = CNFPlus()
  
          # Minicard's native representation is handled separately
          if encoding == 9:
              ret.atmosts, ret.nv = [([-l for l in lits], len(lits) - bound)], top_id
              return ret
  
          # saving default SIGINT handler
          def_sigint_handler = signal.signal(signal.SIGINT, signal.SIG_DFL)
  
          res = pycard.encode_atleast(lits, bound, top_id, encoding)
  
          # recovering default SIGINT handler
          def_sigint_handler = signal.signal(signal.SIGINT, def_sigint_handler)
  
          if res:
              ret.clauses, ret.nv = res
  
          return ret