code: def leq(cls, lits, weights=None, bound=1, top_id=None,
              encoding=EncType.best):
          
  
          return cls._encode(lits, weights, bound, top_id, encoding,
                  comparator='<')
docs: This method can be used for creating a CNF encoding of a LEQ
              (weighted AtMostK) constraint, i.e. of
              :math:`\sum_{i=1}^{n}{a_i\cdot x_i}\leq k`. The resulting set of
              clauses is returned as an object of class :class:`.formula.CNF`.
  
              The input list of literals can contain either integers or pairs
              ``(l, w)``, where ``l`` is an integer literal and ``w`` is an
              integer weight. The latter can be done only if no ``weights`` are
              specified separately. The type of encoding to use can be specified
              using the ``encoding`` parameter. By default, it is set to
              ``EncType.best``, i.e. it is up to the PBLib encoder to choose the
              encoding type.
  
              :param lits: a list of literals in the sum.
              :param weights: a list of weights
              :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 weights: iterable(int)
              :type bound: int
              :type top_id: integer or None
              :type encoding: integer
  
              :rtype: :class:`pysat.formula.CNF`