docs: def add_clause(self, clause, weight=None):
          """
              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:`RC2`, adding clauses may be helpful when
              *enumerating* MaxSAT solutions 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 integer parameter ``weight`` can
              be set to meaning the the clause being added is soft
              having the corresponding weight (note that parameter
              ``weight`` is set to ``None`` by default meaning that the
              clause is hard).
  
              :param clause: a clause to add
              :param weight: weight of the clause (if any)
  
              :type clause: iterable(int)
              :type weight: int
  
              .. code-block:: python
  
                  >>> from pysat.examples.rc2 import RC2
                  >>> from pysat.formula import WCNF
                  >>>
                  >>> wcnf = WCNF()
                  >>> wcnf.append([-1, -2])  # adding hard clauses
                  >>> wcnf.append([-1, -3])
                  >>>
                  >>> wcnf.append([1], weight=1)  # adding soft clauses
                  >>> wcnf.append([2], weight=1)
                  >>> wcnf.append([3], weight=1)
                  >>>
                  >>> with RC2(wcnf) as rc2:
                  ...     rc2.compute()  # solving the MaxSAT problem
                  [-1, 2, 3]
                  ...     print rc2.cost
                  1
                  ...     rc2.add_clause([-2, -3])  # adding one more hard clause
                  ...     rc2.compute()  # computing another model
                  [-1, -2, 3]
                  ...     print rc2.cost
                  2
          """
  
          # first, map external literals to internal literals
          # introduce new variables if necessary
          cl = list(map(lambda l: self._map_extlit(l), clause))
  
          if not weight:
              # the clause is hard, and so we simply add it to the SAT oracle
              self.oracle.add_clause(cl)
          else:
              # soft clauses should be augmented with a selector
              selv = cl[0]  # for a unit clause, no selector is needed
  
              if len(cl) > 1:
                  self.topv += 1
                  selv = self.topv
  
                  cl.append(-self.topv)
                  self.oracle.add_clause(cl)
  
              if selv not in self.wght:
                  # record selector and its weight
                  self.sels.append(selv)
                  self.wght[selv] = weight
                  self.smap[selv] = len(self.sels) - 1
              else:
                  # selector is not new; increment its weight
                  self.wght[selv] += weight
  
              self.sels_set.add(selv)