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