我正在使用 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 + t1incr 和 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 没有界限。我在哪里犯错？