2

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

psksvp
  • 139
  • 11

1 Answers1

2

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

psksvp
  • 139
  • 11