python - 在Z3 python中修改变量

Question

我正在编写某种模拟某些规则的应用程序。我发现 Z3py 的定点对我有帮助。我的应用程序大纲如下：(fp = Fixedpoint())

1. 声明一些整数变量，例如：a, b, c = Ints('ab c') 并注册到定点 - fp.(a, b, c)

2. 遵循某些变量（事实）的性质，增加或减少其他一些变量。例如：如果 (a>0 and b>0) 那么 c=c+1

3. 查询目标变量是否满足某些条件，例如 query(target>0)

我不知道如何使用规则来指定 2。有人可以告诉我这可能吗？

Answer 1

我采用了您概述的示例并创建了一个示例：

• http://rise4fun.com/Z3Py/kD1P

我希望这有帮助。

Z3 打印 UNSAT 因为查询不可访问。然后它显示一个不变量，证明查询不可访问。

更详细

要声明具有三个参数的属性，请执行以下操作：

P = Function('P', IntSort(), IntSort(), IntSort(), BoolSort())

为定点引擎注册它：

fp.register_relation(P)

添加您想到的任何规则：

fp.rule(P(-1,1,-10))
fp.rule(P(a,b,c+1), [a > 0, b > 0, P(a,b,c)])
fp.rule(P(a+1,b,c-1), [a <= 0, b < 0, P(a,b,c)])

第一条规则说明了最初的属性。第二条规则说如果 a > 0, b > 0，c 可以递增。

最后询问是否可以访问某些属性：

print fp.query(P(a,b,c),c > 0 )