Z3 Python中如何向函数调用传值并验证stf[N]是否存储4

问题根源与解决方法 #

你代码里的核心问题是赋值逻辑写反了，你原本想实现N=stm[n]，但实际写的stf = Store(stf,stf[N],stm[n])的作用是往stf数组的stf[N]索引位置写入stm[n]的值，全程没有对N加任何约束，N仍然是自由符号变量，所以你仅添加stf[N]==stm[n]得到SAT结果没有实际意义：Z3可以任意给N赋值，只要满足stf[N]刚好等于stm[n]即可，无法证明N等于n，也无法证明stf[N]存储的是4。

修正与验证方案 #

Z3中验证属性必然成立的标准方法是反证法：给求解器添加你要验证的属性的否定条件，如果s.check()返回unsat，就说明该属性在当前约束下永远成立。

完整示例代码

from z3 import *

if __name__ == '__main__':
    # 基础变量声明
    stm = Array('stm', IntSort(), IntSort())
    n = Int('n')
    stm = Store(stm, n, 4) # 固定stm[n] = 4
    stf = Array('stf', IntSort(), IntSort())
    N = Int('N')

    s = Solver()
    # 补充你原本缺失的约束：N = stm[n]
    s.add(N == stm[n])
    # 给stf数组的N索引位置写入stm[n]的值
    stf = Store(stf, N, stm[n])

    # 验证1：N是否必然等于n
    s.push() # 保存当前求解器上下文
    s.add(N != n)
    print("验证N等于n的结果：", s.check()) 
    # 输出为unsat，说明不存在N不等于n的合法解，即N必然等于n
    s.pop() # 恢复上下文，用于下一个验证

    # 验证2：stf[N]是否必然存储4
    s.add(Select(stf, N) != 4)
    print("验证stf[N]等于4的结果：", s.check())
    # 输出为unsat，说明stf[N]必然存储的是4

结果说明 #

• 如果验证N != n返回unsat，即可证明所有合法解中N都等于n
• 如果验证Select(stf, N) !=4返回unsat，即可证明stf[N]一定存储了4
• 如果你需要查看具体的合法解，可以删除否定断言后调用print(s.model())打印变量赋值

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