I have the following example of quantifiers elimination using z3py below. However I would like to rewrite it using SMTLIB syntax (code below python code). Somehow I did not get the same output like what I got from python which are formulas. I wonder if anyone could point me out the problem.
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))
output (goals (goal :precision precise :depth 1) )
I asked the question too quickly. After more searching (Quantifier Elimination - More questions), I found a solution below.
(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))