docs: def _encode(cls, lits, weights=None, bound=1, top_id=None,
              encoding=EncType.best, comparator='<'):
          """
              This is the method that wraps the encoder of PyPBLib. Although the
              method can be invoked directly, a user is expected to call one of
              the following methods instead: :meth:`atmost`, :meth:`atleast`, or
              :meth:`equals`.
  
              The 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.
  
              :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.
              :param comparator: identifier of the comparison operator
  
              :type lits: iterable(int)
              :type weights: iterable(int)
              :type bound: int
              :type top_id: integer or None
              :type encoding: integer
              :type comparator: str
  
              :rtype: :class:`pysat.formula.CNF`
          """
  
          if encoding < 0 or encoding > 5:
              raise(NoSuchEncodingError(encoding))
  
          assert lits, 'No literals are provided.'
  
          # preparing weighted literals
          if weights:
              assert len(lits) == len(weights), 'Same number of literals and weights is expected.'
              wlits = [pblib.WeightedLit(l, w) for l, w in zip(lits, weights)]
          else:
              if all(map(lambda lw: (type(lw) in (list, tuple)) and len(lw) == 2, lits)):
                  # literals are already weighted
                  wlits = [pblib.WeightedLit(*wl) for wl in lits]
                  lits = zip(*lits)[0]  # unweighted literals for getting top_id
              elif all(map(lambda l: type(l) is int, lits)):
                  # no weights are provided => all weights are units
                  wlits = [pblib.WeightedLit(l, 1) for l in lits]
              else:
                  assert 0, 'Incorrect literals given.'
  
          if not top_id:
              top_id = max(map(lambda x: abs(x), lits))
  
          # pseudo-Boolean constraint and variable manager
          constr = pblib.PBConstraint(wlits, EncType._to_pbcmp[comparator], bound)
          varmgr = pblib.AuxVarManager(top_id + 1)
  
          # encoder configuration
          config = pblib.PBConfig()
          config.set_PB_Encoder(EncType._to_pbenc[encoding])
  
          # encoding
          result = pblib.VectorClauseDatabase(config)
          pb2cnf = pblib.Pb2cnf(config)
          pb2cnf.encode(constr, result, varmgr)
  
          # extracting clauses
          return CNF(from_clauses=result.get_clauses())