code: def _map_extlit(self, l):
          
  
          v = abs(l)
  
          if v in self.vmap.e2i:
              return int(copysign(self.vmap.e2i[v], l))
          else:
              self.topv += 1
  
              self.vmap.e2i[v] = self.topv
              self.vmap.i2e[self.topv] = v
  
              return int(copysign(self.topv, l))
docs: Map an external variable to an internal one if necessary.
  
              This method is used when new clauses are added to the formula
              incrementally, which may result in introducing new variables
              clashing with the previously used *clause selectors*. The method
              makes sure no clash occurs, i.e. it maps the original variables
              used in the new problem clauses to the newly introduced auxiliary
              variables (see :func:`add_clause`).
  
              Given an integer literal, a fresh literal is returned. The returned
              integer has the same sign as the input literal.
  
              :param l: literal to map
              :type l: int
  
              :rtype: int