Исключение квантификаторов z3 в синтаксисе SMTLIB

Question

У меня есть следующий пример устранения квантификаторов с использованием z3py ниже. Однако я хотел бы переписать его с использованием синтаксиса SMTLIB (код ниже кода Python). Каким-то образом я не получил такой же вывод, как то, что я получил от Python, которые являются формулами. Интересно, кто-нибудь может указать мне на проблему.

from z3 import * a, five = Ints('a five') cmp = Bool('cmp')
j = Goal() j.add(Exists([five, cmp], And(five == a, cmp == (five < 1000), False == cmp)))
t = Tactic('qe') print(t(j)) # output [[1000 <= a]]

(declare-fun five () Int) (declare-fun a () Int) (declare-fun cmp () Bool) (assert (exists ((five Int) (cmp Bool)) (and (= five a) (= cmp (< five 1000)) (= cmp false) ))) (apply (then qe smt))

результат (цели (цель: точность, точность: глубина 1))

Answer 1

Я задал вопрос слишком быстро. После дополнительного поиска ( устранение квантификатора - дополнительные вопросы) я нашел решение ниже.

(declare-fun five () Int) (declare-fun a () Int) (declare-fun cmp () Bool) (assert (exists ((five Int) (cmp Bool)) (and (= five a) (= cmp (< five 1000)) (= cmp false) ))) (apply (using-params qe :qe-nonlinear true))