code: def atmost(cls, lits, bound=1, top_id=None, encoding=EncType.seqcounter):
          
  
          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 = [(lits, bound)], top_id
              return ret
  
          # saving default SIGINT handler
          def_sigint_handler = signal.signal(signal.SIGINT, signal.SIG_DFL)
  
          res = pycard.encode_atmost(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
docs: This method can be used for creating a CNF encoding of an AtMostK
              constraint, i.e. of :math:`\sum_{i=1}^{n}{x_i}\leq k`. The method
              shares the arguments and the return type with method
              :meth:`CardEnc.atleast`. Please, see it for details.