Added arithemtical lex constraint.

The arithmetical lex constraint seems slower than the existing
lex decomposition, but it doesn't have a bug for in saying that
g=2; k=12; b=16 is UNSAT as far as I'm aware. It times out after
1 hr, whereas the with the old lex constraint, it said UNSAT
after 1.5 min.
Pass Hall parameter in test script.
Updates.