修改z3python中的变量

Question

我在写一些模拟规则的应用程序。我找到了Z3P的固定点。我的应用程序大纲如下： （fp=定点（））

1. 声明一些整数变量，例如：a，b，c=Ints（'a b c'），并注册到fixedpoint-fp。（a，b，c）

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

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

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

Answer 1

我以你概述的例子为例，创建了一个例子：

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

我希望这有帮助。在

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

更详细

要使用三个参数声明属性，请执行以下操作：

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

要将其注册为定点引擎，请执行以下操作：

^{pr2}$

添加您心中的任何规则：

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可以递增。在

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

^{4}$