CODEWITHSUNDEEP
z3
Zeinab Ganjei
Zeinab Ganjei

Reputation: 133

solving equation and quantifier elimination

I want to use z3 to find the result of the following expression after quantifier elimination. What is the correct syntax?

(declare-fun n () Int)
(declare-fun X () Int)
(declare-fun X_1_ () Int)
(declare-fun X_0_ () Int)

(assert (exists ((R__0 Int) (R__1 Int)(R_0_0 Int) (R_1_0 Int)) (and (>= n 3) 
     (= X  n)
    (=(+ X_0_  X_1_) X)
    (>= X_0_  0)
    (<= R_0_0  X_0_)
    (>= R_0_0  0)
    (<= R_0_0  R__0)
    (>= X_1_  0)
    (<= R_1_0  X_1_)
    (>=  R_1_0 0)
    (<=  R_1_0 R__0)
    (<= R__0  X)
    (<=  R__1 X)
    (= (+ R_1_0  R_0_0) R__0)
    (> (* 3 R__0)  (* 2 n))
    (>= R_0_0  R_1_0)
    (<=  (* 3 R_0_0) (* 2 n))
    (<= (* 3 R__1) (* 2 n)))))
    (apply (using-params qe :qe-nonlinear true))

Upvotes: 0

Views: 42

Answers (1)

alias
alias

Reputation: 30428

Use the qe_rec tactic. Changing your last line to:

(apply qe_rec)

produces:

(goals
(goal
  (>= X_1_ 0)
  (>= X_0_ 0)
  (= (+ X_0_ X_1_) X)
  (= X n)
  (>= n 3)
  (<= (+ (* (- 2) n) (* 3 X_1_)) 0)
  (>= (* 9 X_1_) 7)
  (<= (+ (* 2 n) (* (- 6) X_0_)) (- 1))
  :precision precise :depth 1)
)

Upvotes: 1

Related Questions