Z3Py Fixedpoint computation too weak

Question

I am using z3py APIs to compute a set of inductive annotations. I am mapping my constraints to a conjuction of generalized Horn clauses. Among the constraints, there are a couple of relations (l6 and iwc1) which need to be inferred. The variables involved (incr1, t1 and wc1) are all integers. I want the inferred predicates to be interval relations. The predicate l6(incr, t1) should capture the fact that incr = 0 and t1 >= 0. I am framing this as the following rule:

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

The inferred predicate l6 is:

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

Again, iwc1 is a predicate involving the variable wc1, and it tries to capture the fact that wc1 == incr + t1 where the values of incr and t1 are over-approximated by l6. In other words,

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

Since wc1 == incr + t1, and l6 infers that incr = 0 and t1>=0, I expected iwc1 to be wc1>=0. Instead, the inferred predicate is True. Why is iwc1 turning out to be so weak?

The complete program is available in this online z3py code.

If, instead, I modify the rule for iwc1 as follows:

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

then, I get the following error:

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

The program with the altered rule for iwc1 is available here. Z3Py is complaining that the variable incr is not bounded. Where am I making a mistake?

Answer 1

You have specified using the Datalog engine. It requires that variables in the body are bound in predicates.