Question
Is there a way to use sympy to simplify (in the usual vaguely defined sense) a logical target expression based on some logical constraint expressions? Both the target expression and the constraints can have an arbitrary form in a set of symbols A,B,C... and the operands >>,&,|,~.
E.g. say I would expect
how_to_do_this( (C & A) | (C & B), [A >> B, ] )
-> (B & C)
Note that there might be multiple constraints. Besides the general case, also the special case of having only simple implications as constraints would be of interest.
First thoughts
A hackish approach I could think of would be to simply add the constraints, as
sp.simplify("A >> B & (C & A) | (C & B)")
-> B & C
However, for the same constraint A >> B with different target expressions, this would "contaminate" the target expression with the information of the constraint, e.g.
sp.simplify("A >> B & (C & D)")
-> C & D & (B | ~A)
which is unwanted, as the constraint belongs to a different logical context. Here the approach fails, as I'd simply expect the result (C & D) because the constraint just can't be used to simplify anything.
More formally, in this approach the constraints become part of the target expression, and thus something that it has to ensure.
Second thoughts
A different perspective, which however is almost the equivalent problem, would be to reformulate this with algebraic expressions, e.g.
how_to_do_this(x+2*y, [x+y==5])
-> y+5
however, note that the explicit approach "solve x+y=5 for x=5-y and substitue it into x+2*y" is not a general enough solution here, as e.g. the constraint A>>B cannot be "solved for" A (or B) in this sense, nor could a more complicated logical condition. The algorithm should rather "group out" x+y and replace it by 5, i.e. x+2*y=y+(x+y)=y+5. If such a mechanism is known for algebraic expressions, it should also be applicable to logic expressions: "group out A >> B and replace it by True".
These however are just ideas.
In SymPy 1.12 (which at the time of writing is not yet released) the simplify_logic function has a dontcare parameter which can be used for this.
The dontcare parameter is used like this:
In [29]: simplify_logic((C & A) | (C & B), dontcare = ~(A >> B))
Out[29]: B ∧ C
In [32]: simplify_logic(C & D, dontcare = ~(A >> B))
Out[32]: C ∧ D
The idea here is that you "don't care" about the case where A >> B is false because you know A >> B to be true:
https://en.wikipedia.org/wiki/Don%27t-care_term
For the algebraic approach that you suggest you would want to use something like resultants or Groebner bases. What you expect to get out is ambiguous unless you specify which symbols to eliminate or in what order they should be eliminated:
In [2]: resultant(x + 2*y, x + y - 5, x)
Out[2]: -y - 5
In [3]: resultant(x + 2*y, x + y - 5, y)
Out[3]: x - 10
In [5]: groebner([x + 2*y, x + y - 5], x, y)
Out[5]: GroebnerBasis([x - 10, y + 5], x, y, domain=ℤ, order=lex)
In [6]: groebner([x + 2*y, x + y - 5], y, x)
Out[6]: GroebnerBasis([y + 5, x - 10], y, x, domain=ℤ, order=lex)