Fix cleanup and CNF vpool updating

[brossignol]

Hello, I propose a fix to test_clausification not passing after #167.

Currently on master vpool are not cleaned correctly after creating a CNF:

print(dict(Formula._vpool))
>>> {}

cnf = CNF(from_clauses=[[1, 2, 3]])
print(dict(Formula._vpool))
>>> {'default': IDPool(start_from=1, occupied=[[1, 3]])}

Formula.cleanup()
print(dict(Formula._vpool))
>>> {'default': IDPool(start_from=1, occupied=[[1, 3]])}

It is because Formula.cleanup only looks at context within _instances and not at context in ._vpool. It is possible to have a context in _vpool without being in _instances (ex: creating a CNF). It is also possible to have a context in _instances without being in _vpool (ex: creating Atom(int)). The bug didn't appear before because 'default' context was always in _instances with Atom(True/False), but the problem still existed for other contexts.

I propose to simply looks in both _vpool and _instances when cleaning all.

Additional fixes:

• In CNF the logic to update self.nv what duplicated (with different variation doing the same thing), I propose to centralize it into _compute_nv().
• CNF.append was not updating the _vpool occupy. I fix it. This will add some extra computation (not much) but I don't see a way around it.

[alexeyignatiev]

Thanks. I didn't update the pool when appending a new clause because this would surely affect the performance. The thing is there can be millions of clauses added by a user's encoder and in that case the user normally doesn't want to deal with the new Formula functionality but rather to encode everything on their own. In this case, updating the pool is a waste of time.

[alexeyignatiev]

This can be solved by adding a keyword argument update_vpool=False.

[alexeyignatiev]

@brossignol, I've now done this. Note that some of the tests started failing with this patch. (Some problem with _compute_nv()).

[alexeyignatiev]

Namely, the issue is that the function does not handle the case of an empty clause in the formula, which should be handled properly.

[alexeyignatiev]

This is fixed now.