在Z3 python中修改变量

Question

我在写一些模拟某种规则的应用程序。我发现Z3py的固定点是我的帮助。我的应用程序的轮廓可以是如下： （FP =定点（））

1. 声明一些整数变量，例如：A，B，C =整数（ 'AB C'）和寄存器到定点 - FP（ a，b，c）

2. 按照某些变量的属性（事实），增加或减少一些其他变量。例如： if（a> 0 and b> 0）then c = c + 1

3. 查询目标变量是否满足某些条件，例如：查询（目标> 0）

我不知道如何使用规则来指定2.有人能告诉我，这是有可能做到这一点？

Answer 1

我把你介绍的例子，创建了一个例子：

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

我希望这有助于。

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

更详细

要使用三个参数声明属性做：

fp.register_relation(P) 

添加你心目中的规矩：

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

要为定点引擎注册吧：

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)]) 

第一条规则说明什么属性最初持有。 第二条规则说C能递增如果a> 0，B> 0

最后问，如果某些属性是可到达：

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