def leq(cls, lits, weights=None, bound=1, top_id=None,
            encoding=EncType.best):
        """
            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`


        """

        return cls._encode(lits, weights, bound, top_id, encoding,
                comparator='<')