Нормальная форма формулы, возвращенная тактикой Z3

Question

Я использую тактику устранения квантификатора Z3 через Z3py и попробовал следующие примеры.

from z3 import *
x,y,xp,yp = Ints('x y xp yp')
t = Tactic('qe')

t(Exists((xp, yp), And(xp==x+1, yp==y+2, xp<=8, xp >=1, yp<=12, yp>=2)))
#returns: [[y <= 10, y >= 0, x <= 7, x >= 0]]

t(Exists((xp, yp), Implies(x<10 , And(xp==x+1, yp==y+2, xp<=8, xp >=1, yp<=12, yp>=2))))
#returns: [[Or(10 <= x, And(y <= 10, y >= 0, And(x <= 7, x >= 0)))]]

Я думаю, что полученные формулы находятся в DNF без квантификатора (что мне и нужно), но я не смог найти в документации API ничего, что гарантировало бы это. Кто-нибудь знает, если qe всегда возвращает формулы в DNF?

Где я могу (если вообще смогу) найти такие детали касательно тактики без необходимости копаться в исходном коде?

РЕДАКТИРОВАТЬ: Все формулы ограничены линейной целочисленной арифметики.

Answer 1

По своему замыслу тактика делает «лучшее усилие». То есть, хотя qe предназначен для устранения квантификаторов, он может в конечном итоге не сделать этого, возвращая стек цели без изменений.

Обратите внимание, что устранение квантификаторов - это не просто одна тактика, а целая коллекция, в зависимости от того, какие другие теории задействованы в вашем тесте. Смотрите каталог: https://github.com/Z3Prover/z3/tree/master/src/qe