Python - 如何将布尔对称树表达式解析为布尔 Z3Py 表达式

你走在正确的轨道上。从本质上讲，您需要将 SymPy “编译”为 Z3。这可以通过多种方式实现，但这不是一件便宜/容易的事情，因为您需要分析大量的 SymPy 代码。但是，看起来您的表达方式足够“简单”，因此您可以使用简单的翻译器。首先看看如何递归处理 SymPy 树： https://docs.sympy.org/latest/tutorials/intro-tutorial/manipulation.html#recursing-through-an-expression-tree

如果你赶时间，你可以使用Axel的程序，在另一个答案中给出。这是一个可能更惯用、更易于扩展和更强大的版本：

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!")