Z3py使用Solver遇TypeError：ArithRef对象无法解析为整数

问题背景 #

尝试用Z3Py编写代码，期望通过求解器找到满足条件的整数参数k和实数参数x，使得函数计算结果为负。运行时先后出现两个错误：

• TypeError: 'ArithRef' object cannot be interpreted as an integer
• ArgumentError: argument 2: <class 'TypeError'>: wrong type

原代码逻辑：定义循环函数f，尝试通过Exists断言找参数，让f(x0, k)输出负数，但代码中直接用符号变量k作为range()的参数，导致错误。

错误原因 #

1. 符号变量无法用于Python内置循环：range()需要具体的整数值，而k是Z3的IntRef类型符号变量，在求解器得出具体值前，它不是可直接计算的整数，无法驱动Python的for循环。
2. 逻辑与API使用问题：原代码中Exists的参数逻辑混淆（传入固定值x0却要找x），且And包裹单个条件属于冗余写法。

解决方法 #

用Z3的符号化递归定义替代Python的for循环，让求解器能处理符号化的循环次数；同时修正约束逻辑，明确要寻找的参数条件。

场景1：寻找正整数k，使得f(10, k) < 0 #

from z3 import *

k = Int('k')
s = Solver()

# 递归定义符号化函数，处理循环次数为符号变量的情况
def f_sym(x, n):
    # 基准情况：循环次数为0时返回初始值x
    return If(n == 0, x, f_sym(x * 1.099 - 1, n - 1))

x0 = 10
# 添加约束：k必须是正整数，且计算结果小于0
s.add(k > 0)
s.add(f_sym(x0, k) < 0)

# 求解并输出结果
if s.check() == sat:
    print("找到解：", s.model())
else:
    print("无解")

场景2：寻找实数x和正整数k，使得f(x, k) < 0 #

from z3 import *

x = Real('x')
k = Int('k')
s = Solver()

def f_sym(x_val, n):
    return If(n == 0, x_val, f_sym(x_val * 1.099 - 1, n - 1))

# 添加约束：k为正整数，且计算结果小于0
s.add(k > 0)
s.add(f_sym(x, k) < 0)

if s.check() == sat:
    print("找到解：", s.model())
else:
    print("无解")

说明 #

• 用Z3的If实现递归函数，让求解器能理解符号化的循环逻辑，避免依赖Python运行时的整数循环。
• 直接通过s.add()添加约束即可实现存在性求解，无需显式使用Exists（复杂公式场景除外）。

内容的提问来源于stack exchange，提问作者Serra Dane