Sympy: How to find longest expression that all N expressions have in common

Question

I have N expressions in Sympy and I need to find the longest expression that all N expressions have in common (like the longest expression is in/contained in all that N expressions)

from sympy import Symbol
from sympy.logic.boolalg import And, Not, Or
a = Symbol("a")
b = Symbol("b")

expr0 = And(And(a, b), c)
expr1 = Not(And(a, b))
expr2 = Or(Not(a), Not(b))
#?? now how to find that all expressions contains And(a,b) ?  

Why I need it? I have some expressions and I need to build If-then-else block for them:

expr0 causes operation Op0
expr1 causes operation Op1
expr2 causes operation Op2

and the result should be:
And(a,b) is longest expression which all of expr have in common
so I will be able to build if then else block like this

If (And(a, b)) {
    if(c)
        Op0;
}else{
    op1;
    op2;
}

So this is why i need to find the longest expression that all N expressions have in common. To optimalize this If-then-else blocks.

Answer 1

SymPy objects have the .has( ... ) method:

>>> expr1.has(expr0)
True

>>> expr2.has(expr0)
False

Regarding the rest of Python (i.e. not SymPy), you should better define what you mean by shared expression. Logical operations are usually supposed to return a value, not to build an expression.

EDIT

OK, from the discussion I understand that you want to look for a common subexpression between two expressions (so, not testing whether a subexpression is a common one).

Furthermore, you'd like to logically match equivalent expressions, that is, expressions that look differently but are logically equivalent should be matched as equivalent. This makes everything a bit more complicated, but I propose you an easy solution.

SymPy has the satisfiable( ) function, which finds solutions to logical expressions. If you pass the parameter all_models=True, this function will return all solutions that satisfy that logical condition:

In [5]: list(satisfiable(expr2, all_models=True))
Out[5]: [{b: False, a: False}, {b: False, a: True}, {b: True, a: False}]

The function preorder_traversal allows us to visit the whole expression tree (that is, easily create a for-loop to visit all subexpressions). So we can construct a double for-loop to perform the search on the subexpressions of expr1, check their satisfiability, perform a second for loop on the other expression (expr2 in this example), and compare the satisfiabilities of the two subexpressions:

for e1 in preorder_traversal(expr1):
    s1 = list(satisfiable(e1 ,all_models =True ))
    for e2 in preorder_traversal (expr2):
        s2 = list (satisfiable (e2 ,all_models =True ))
        if s1 == s2:
            print("Logically equiv subexpr found: ", e1, " and ", e2)

If you put here your expr1 and expr2, you'll get:

('Logically equiv subexpr found: ', Not(And(a, b)), ' and ', Or(Not(a), Not(b)))
('Logically equiv subexpr found: ', b, ' and ', b)
('Logically equiv subexpr found: ', a, ' and ', a)

I think you can easily adapt this code to your needs.

EDIT 2

To handle cases in which the tree splits into more than two subexpressions (that is, cases like And(a, b, c, d) or Xor(a, b, c, d, e)), you could generate subsets like this (code is not tested this time):

# get a function to generate all subsets of a tuple,
# let's say `subsets( )`

for e1 in preorder_traversal(expr1):
    for es1 in subsets(e1.args):
        s1 = list(satisfiable(e1.func(*es1), all_models=True))
        # NOW do the same with the `e2` for-loop,
        # then compare `s1` and `s2` as usual.

This code would appear like a series of 4 nested for-loops, but it can be rearranged defining some helper functions, to make it look nicer.

It can be further generalized to compare more than two expressions, again better reorganize the code a bit first.

EDIT 3

I thought a bit overnight, I think you can further improve this algorithm by sifting the first expression only with satisfiable( ), once you get the boolean solutions for your symbols, just replace them in the other expressions to see which part are compatible.