`LRASolver` is not modular enough

Currently much of the preprocessing and validation logic for inequalities is split between LRASolver.from_encoded_cnf in the logic module and various helper functions in assumptions.lra_satask. This makes it a lot harder to change the way preprocessing and validation happens because you have to simultaneously think about two files in different modules.

In my opinion, the logic module should not depend on the assumptions module at all. And it shouldn't ever have to process sympy expressions as that should be the responsibility of the assumptions module. In particular, these imports in logic.algorithms.lra_theory.py should be removed and the code should be refactored to work without them:

from sympy.assumptions import Predicate
from sympy.assumptions.assume import AppliedPredicate
from sympy.assumptions.ask import Q
from sympy.core import Dummy
from sympy.core.mul import Mul
from sympy.core.add import Add
from sympy.core.relational import Eq, Ge, Gt, Le, Lt

Information about inequalities still needs to be passed down to LRASolver somehow. I think some new object should be defined in lra_theory.py that contains the least amount of information possible should be used. In particular, I think it only needs three parameters:

• terms, an array of tuples each with a symbol or expression and a coefficient
• constant, the constant coefficient
• strict, whether it was a strict inequality (e.g. 0 > x) or a non strict inequality (e.g. 0 >= x) Whether it was a less than or a greater than inequality doesn't need to be conveyed as greater than inequalities can be converted to less than inequalities.

Actually, I think we might need to handle equalities and disequalities as a special case. I think disequalities might be forbidden but I forget why. There was something confusing about how equalities and disequalities need to be handled.