Unify Expression and NormalForm expression types

There doesn't seem to be any use for a Python implementation of a
set(frozenset(uniqid)) representation of a normal form expression.
It can never implement the full Function interface, and the Expression
implementation is already pretty fast for most stuff.

This commit adds normal form classes to expr.py. They use the familiar
Dimacs encoding of integer literals indexed as [-N..-1, 1..N].

The new usage model is to "encode" an expression into a normal form
To revert back, use the "decode" method.
Also, you may use the `expr2dimacscnf` convenience method to
automatically convert a CNF expression to the DimacsCNF class, which
helps interface with PicoSAT.
Get rid of nfexpr module