Z3 求解器类型错误：“ArithRef”对象无法解释为整数

Question

我正在尝试使用 Z3py 运行下面的代码，主要问题是我想使用求解器找到我的函数的参数。我想在我的函数中使用参数作为整数和实数。

x = Real('x') #declare a real symbolic variable
k = Int('k') #declare an integer symbolic variable


s = Solver() #initialize the solver

#this is the function that takes x and k and does some calculations with them
def f(x, k):
    for i in range(k):
        x = x*1.099-1
    return x

x0 = 10

s.add(Exists((x,k),  And(f(x0,k)<0))) #here i want to find if there exists such x and k as my arguments to function k that makes the output negative

s.check()

但是，此代码会导致 TypeError:'ArithRef' 对象无法解释为整数。我知道我不能按原样使用 k，但我找不到让它工作的方法。

这可能吗？预先感谢您！

我也尝试写这个：

x = Real('x') #declare a real symbolic variable
k = Int('k') #declare an integer symbolic variable


s = Solver() #initialize the solver

#this is the function that takes x and k and does some calculations with them
def f(x, k):
    for i in range(k):
        x = x*1.099-1
    return x

x0 = 10

s.add(Exists((x,k),  And(f(x0,k)<0))) #here i want to find if there exists such x and k as my arguments to function k that makes the output negative

s.check()

这会导致 ArgumentError: argument 2: : 类型错误

Answer 1

虽然 z3py 允许混合/匹配 Python 和 z3 构造，但它不允许以符号方式使用任意 Python 表达式。 （这将是一件非常困难的事情。）

特别是，符号变量不支持对

range

的调用。

请注意，

k

上的循环会产生一个非线性问题（将变量相乘），这对于 SMT 求解器来说已经很困难了。

您最好的选择是对

k

进行增量搜索。比如：

from z3 import *

x = Real('x')

def f(x, k):
    for i in range(k):
        x = x*1.099-1
    return x

for k in range(10):
    print(f"Trying k: {k}")

    s = Solver()
    s.add(x > 0)
    s.add(And(f(x, k) < 0))

    r = s.check()
    if(r == sat):
        print(s.model())
        break
    else:
        print(f"Solver said: {r}")

打印：

Trying k: 0
Solver said: unsat
Trying k: 1
[x = 500/1099]

您可能想断言一些其他约束以使这更有趣。 （例如，您有一个

Exists(x)

，未使用；但您也有

x0 = 10

。不太清楚您要表达的内容。）