Python — как анализировать логические выражения дерева Sympy в логические выражения Z3Py

Вы на правильном пути. По сути, вам нужно «скомпилировать» SymPy в Z3. Этого можно добиться разными способами, но это недешево и не просто, поскольку вам нужно будет анализировать большие участки кода SymPy. Однако похоже, что ваши выражения достаточно «просты», поэтому вам может сойти с рук простой переводчик. Начните с изучения того, как рекурсивно обрабатывать деревья SymPy: https://docs.sympy.org/latest/tutorials/intro-tutorial/manipulation.html#recursing-through-an-expression-tree

Если вы спешите, вы можете использовать программу Акселя, приведенную в другом ответе. Вот версия, которая, вероятно, немного более идиоматична, ее легче расширять и она более надежна:

import sympy
import z3

# Sympy vs Z3. Add more correspondences as necessary!
table = { sympy.logic.boolalg.And    : z3.And
        , sympy.logic.boolalg.Or     : z3.Or
        , sympy.logic.boolalg.Not    : z3.Not
        , sympy.logic.boolalg.Implies: z3.Implies
        }

# Sympy vs Z3 Constants
constants = { sympy.logic.boolalg.BooleanTrue : z3.BoolVal(True)
            , sympy.logic.boolalg.BooleanFalse: z3.BoolVal(False)
            }

def compile_to_z3(exp):
    """Compile sympy expression to z3"""
    pexp = sympy.parsing.sympy_parser.parse_expr(exp)
    pvs  = {v: z3.Bool(str(v)) for v in pexp.atoms() if type(v) not in constants}

    def cvt(expr):
        if expr in pvs:
            return pvs[expr]

        texpr = type(expr)
        if texpr in constants:
            return constants[texpr]

        if texpr in table:
            return table[texpr](*map(cvt, expr.args))

        raise NameError("Unimplemented: " + str(expr))

    return cvt(pexp)

if __name__ == '__main__':
    z3.solve(compile_to_z3("false"))
    z3.solve(compile_to_z3("a & ~b | c"))
    z3.solve(compile_to_z3("false >> (a & ~b | c)"))

Это печатает:

no solution
[c = False, b = False, a = True]
[]

Вы можете добавить новые функции в table, чтобы расширить его по своему усмотрению.

Я не удержался и реализовал простейший преобразователь.

from sympy import symbols
from sympy.parsing.sympy_parser import parse_expr
from z3 import *

#  extract all variables and define a SymPy expression
def create_sympy_expression(expr):
    declare_sympy_symbols(expr)
    return parse_expr(expr)

#  assume all single-character operands as SymPy variables
dicz3sym = {}
def declare_sympy_symbols(expr):
    for c in expr:
        if 'a' <= c <= 'z':
            if not c in dicz3sym:
                dicz3sym[c] = z3.Bool(c)

def transform_sympy_to_z3(exp):
    params = [transform_sympy_to_z3(arg) for arg in exp.args]
    func = str(exp.func)
    if func == "And":
        return z3.And(params)
    elif func == "Not":
        return z3.Not(params[0])
    elif func == "Or":
        return z3.Or(params)
    elif exp.name in dicz3sym:
        return dicz3sym[exp.name]
    else:
        raise NameError("unknown/unimplemented operator: " + func)

if __name__ == '__main__':
    exp = create_sympy_expression("a & ~b | c")
    z3exp = transform_sympy_to_z3(exp)
    s = Solver()
    s.add(z3exp)
    if s.check() == sat:
        m = s.model()
        print("Solution found:")
        for v in dicz3sym:
            print(f"{v} = {m[dicz3sym[v]]}")
    else:
        print("No solution. Sorry!")