如何在带有声明函数的 Z3 的 Python API 中正确使用 Solver() 命令

问题描述

我通过使用 Z3 的 Python API 的某些脚本得到了意想不到的结果.我认为我误解了某些过程或只是错误地使用了某些命令.例如，假设我有以下脚本:

I'm getting unexpected results with some script using Python API of Z3. I think that I'm misunderstanding some process or simply using some command wrong. For example, suppose I have the following script:

from z3 import *

x = Int('x')

def g(x):
    if x == 0:
       return 1
    elif x > 0:
       return x**(x+1)

s = Solver()
s.add(g(x) > x)
print s.check()
if s.check()== sat:
    m = s.model()
    m.evaluate(x, model_completion=True)
    print m

这将返回以下输出:

sat
[x = 0]

没关系，但是如果我将 s.add(g(x) > x) 替换为 s.add(x > 1, g(x) > x)，返回unsat.我期待这样的事情:

That it's OK, but if I substitute s.add(g(x) > x) by s.add(x > 1, g(x) > x), this returns unsat. I was expecting something like:

sat
[x = 2]

有人能帮我了解发生了什么吗?

Can anybody help me to understand what's going on?

推荐答案

Python 的 if-then-else 无法转换为 Z3 的 if-then-else.您必须使用如果"功能.请参阅此处:https://github.com/Z3Prover/z3/blob/master/src/api/python/z3.py#L1092

Python's if-then-else does not translate to Z3's if-then-else. You have to use the "If" function. See here: https://github.com/Z3Prover/z3/blob/master/src/api/python/z3.py#L1092

这篇关于如何在带有声明函数的 Z3 的 Python API 中正确使用 Solver() 命令的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！