Z3Py定点计算太弱

Question

我正在使用z3py API来计算一组归纳注释。我正在将我的约束映射到广义Horn子句的组合中。在这些约束中，有几个关系（l6和iwc1）需要推断。所涉及的变量（incr1、t1和wc1）都是整数。我希望推断出的谓词是区间关系。谓词l6（incr，t1）应该捕获incr=0和t1>=0这一事实。我将其定义为以下规则：

fp.rule(l6(incr,t1), [incr==0, t1>=0])

推断出的谓词l6是：

And(0 <= Var(0), Var(0) <= 0, 0 <= Var(1))

同样，iwc1是一个涉及变量wc1的谓词，它试图捕捉wc1 == incr + t1的事实，其中incr和t1的值被l6过度近似。换句话说，

fp.rule(iwc1(wc1), And(wc1==(incr+t1), l6(incr,t1)))

由于wc1 == incr + t1和l6推断incr＝0和t1>＝0，所以我期望iwc1是wc1>＝0。相反，推断出的谓词是True。为什么iwc1变得如此虚弱？

完整的程序可以在这个在线z3py代码中获得。

相反，如果我修改iwc1的规则如下：

fp.rule(iwc1(wc1), And(wc1==incr+t1, incr==0, t1>=0))

然后，我得到以下错误：

z3types.Z3Exception: 'rule with unbound variable #2 in interpreted tail: iwc1(#0) :- n (= #2 0),n (= #0 (+ #2 #1)),n (>= #1 0).n'

修改了iwc1规则的程序在这里可用。Z3Py抱怨变量incr没有界。我在哪里犯错误？

Answer 1

您已经使用Datalog引擎进行了指定。它要求变量在主体中被绑定在谓词中。