Я использую API-интерфейсы z3py для вычисления набора индуктивных аннотаций. Я сопоставляю свои ограничения с конъюнкцией обобщенных предложений Хорна. Среди ограничений есть пара отношений (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 не ограничена. Где я делаю ошибку?
