code: def append(self, clause, weight=None, is_atmost=False):
          
  
          if not is_atmost:
              self.nv = max([abs(l) for l in clause] + [self.nv])
  
              if weight:
                  self.soft.append(clause)
                  self.wght.append(weight)
              else:
                  self.hard.append(clause)
          else:
              self.nv = max([abs(l) for l in clause[0]] + [self.nv])
              self.atms.append(clause)
docs: Add a single clause or a single AtMostK constraint to WCNF+
              formula. This method additionally updates the number of variables,
              i.e.  variable ``self.nv``, used in the formula.
  
              If the clause is an AtMostK constraint, this should be set with the
              use of the additional default argument ``is_atmost``, which is set
              to ``False`` by default.
  
              If ``is_atmost`` is set to ``False``, the clause can be either hard
              or soft depending on the ``weight`` argument. If no weight is
              specified, the clause is considered hard. Otherwise, the clause is
              soft.
  
              :param clause: a new clause to add.
              :param weight: an integer weight of the clause.
              :param is_atmost: if ``True``, the clause is AtMostK.
  
              :type clause: list(int)
              :type weight: integer or None
              :type is_atmost: bool
  
              .. code-block:: python
  
                  >>> from pysat.formula import WCNFPlus
                  >>> cnf = WCNFPlus()
                  >>> cnf.append([-3, 4])
                  >>> cnf.append([[1, 2, 3], 1], is_atmost=True)
                  >>> cnf.append([-1, -2], weight=35)
                  >>> print cnf.hard
                  [[-3, 4]]
                  >>> print cnf.atms
                  [[1, 2, 3], 1]
                  >>> print cnf.soft
                  [[-1, -2]]
                  >>> print cnf.wght
                  [35]