code: def append(self, clause, is_atmost=False):
          
  
          if not is_atmost:
              self.nv = max([abs(l) for l in clause] + [self.nv])
              self.clauses.append(clause)
          else:
              self.nv = max([abs(l) for l in clause[0]] + [self.nv])
              self.atmosts.append(clause)
docs: Add a single clause or a single AtMostK constraint to CNF+ 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.
  
              :param clause: a new clause to add.
              :param is_atmost: if ``True``, the clause is AtMostK.
  
              :type clause: list(int)
              :type is_atmost: bool
  
              .. code-block:: python
  
                  >>> from pysat.formula import CNFPlus
                  >>> cnf = CNFPlus()
                  >>> cnf.append([-3, 4])
                  >>> cnf.append([[1, 2, 3], 1], is_atmost=True)
                  >>> print cnf.clauses
                  [[-3, 4]]
                  >>> print cnf.atmosts
                  [[1, 2, 3], 1]