SMTLIB構文のz3限定子削除

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

私はあまりにも早く質問をしました。より多くの検索（Quantifier Elimination - More questions）の後、私は以下の解決策を見つけました。

(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))