时间戳

首页 > 解决方案 > Z3Py如何在solve（）函数后获取值

python - Z3Py如何在solve（）函数后获取值

问题描述

有人可以解释如何在使用https://pypi.org/project/z3-solver/的 solve() 函数时访问方程变量的结果值。

x, y = BitVecs('x y', 32)
solve(x + y == 2, x > 0, y > 0)

我试过以下无济于事

m = solve(x + y == 2, x > 0, y > 0)
print(m.x)

请注意，在这种情况下，我们不想使用Solver

s = Solver()
s.add(And(x + y == 2, x > 0, y > 0))
s.check()
m = s.model()
print(m[x], m[y])

标签： pythonz3z3py

解决方案

似乎没有直接的方法。函数solve()打印找到的解决方案但不返回模型。

solve()文件z3.py中的定义：

def solve(*args, **keywords):
    """Solve the constraints `*args`.

    This is a simple function for creating demonstrations. It creates a solver,
    configure it using the options in `keywords`, adds the constraints
    in `args`, and invokes check.

    >>> a = Int('a')
    >>> solve(a > 0, a < 2)
    [a = 1]
    """
    s = Solver()
    s.set(**keywords)
    s.add(*args)
    if keywords.get('show', False):
        print(s)
    r = s.check()
    if r == unsat:
        print("no solution")
    elif r == unknown:
        print("failed to solve")
        try:
            print(s.model())
        except Z3Exception:
            return
    else:
        print(s.model())

所以，solve()只是一个包装函数。它创建一个Solver()并且不公开结果模型来访问变量。

推荐阅读