Automatically simplify redundant arithmetic relations

Question

I am looking for a way to automatically determine, e.g., that (a < 12) & (a < 3) & (c >= 4) is the same as (a < 3) & (c >= 4). I looked into Matlab's symbolic toolbox and SymPy in Python, but these are apparently only capable of simplifying purely Boolean logic (e.g., simplify(a & b | b & a) -> ans=(a & b))

Is there a way of using these symbolic math tools like described above?

Edit

As noted in the comment to @user12750353's answer, I would like to also simplify systems of relations that are concatenated with a Boolean OR, e.g., ((a < 12) & (a < 3) & (c >= 4)) | (a < 1).

Answer 1

SymPy sets can be used to do univariate simplification, e.g. ((x < 3) & (x < 5)).as_set() -> Interval.open(-oo, 3) and sets can be converted back to relationals. The following converts a complex expression to cnf form, separates args with respect to free symbols and simplifies those that are univariate while leaving multivariate arguments unchanged.

def f(eq):
    from collections import defaultdict
    from sympy import to_cnf, ordered
    cnf = to_cnf(eq)
    args = defaultdict(list)
    for a in cnf.args:
        args[tuple(ordered(a.free_symbols))].append(a)
    _args = []
    for k in args:
        if len(k) == 1:
            _args.append(cnf.func(*args[k]).as_set().as_relational(k[0]))
        else:
            _args.append(cnf.func(*args[k]))
    return cnf.func(*_args)

For example:

>>> from sympy.abc import a, c
>>> f((a < 1) | ((c >= 4) & (a < 3) & (a < 12)))
(a < 3) & ((c >= 4) | (a < 1))

Answer 2

You can take a look in sympy inequality solvers for some options.

I could apply reduce_inequalities to your problem

from sympy.abc import a, c
import sympy.solvers.inequalities as neq
t = neq.reduce_inequalities([a < 12, a < 3, c >= 4])

And it results (4 <= c) & (-oo < a) & (a < 3) & (c < oo)

It also works with some more complex examples

as long as you have one variable per inequality.