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)