решение уравнения и устранение кванторов - PullRequest
Новая
       3

решение уравнения и устранение кванторов

0 голосов
/ 06 февраля 2020

Я хочу использовать z3, чтобы найти результат следующего выражения после исключения квантификатора. Какой правильный синтаксис? 

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

1 Ответ

1 голос
/ 06 февраля 2020

Используйте qe_rec tacti c. Изменение вашей последней строки на: 

(apply qe_rec)

производит: 

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