docs: def add_clause(self, clause, soft=False):
          """
              The method for adding a new hard of soft clause to the problem
              formula. Although the input formula is to be specified as an
              argument of the constructor of :class:`LBX`, adding clauses may be
              helpful when *enumerating* MCSes of the formula. This way, the
              clauses are added incrementally, i.e. *on the fly*.
  
              The clause to add can be any iterable over integer literals. The
              additional Boolean parameter ``soft`` can be set to ``True``
              meaning the the clause being added is soft (note that parameter
              ``soft`` is set to ``False`` by default).
  
              :param clause: a clause to add
              :param soft: whether or not the clause is soft
  
              :type clause: iterable(int)
              :type soft: bool
          """
  
          # first, map external literals to internal literals
          # introduce new variables if necessary
          cl = list(map(lambda l: self._map_extlit(l), clause))
  
          if not soft:
              # the clause is hard, and so we simply add it to the SAT oracle
              self.oracle.add_clause(cl)
          else:
              self.soft.append(cl)
  
              # soft clauses should be augmented with a selector
              sel = cl[0]
              if len(cl) > 1 or cl[0] < 0:
                  self.topv += 1
                  sel = self.topv
  
                  self.oracle.add_clause(cl + [-sel])
  
              self.sels.append(sel)