z3 - 量指定子を含む数式の場合、z3 がタイムアウトします

Question

次の例でタイムアウトが発生しています。 http://rise4fun.com/Z3/zbOcW

これを機能させるためのトリックはありますか (たとえば、問題を再構成するか、トリガーを使用することによって)?

Answer 1

この例では、マクロ ファインダーが便利です (意味のある forall 量指定子を使用することが多いと思います)。次のようにして有効にできます。

(set-option :macro-finder true)

すぐに取得できる更新された例を次に示しますsat(rise4fun リンク: http://rise4fun.com/Z3/Ux7gN ):

(set-option :macro-finder true)

(declare-const a (Array Int Bool))
(declare-const sz Int)
(declare-const n Int)
(declare-const d Int)
(declare-const r Bool)
(declare-const x Int)
(declare-const y Int)

;;ttff
(declare-fun ttff (Int Int Int) Bool)
  (assert
  (forall ((x1 Int) (y1 Int) (n1 Int))
  (= (ttff x1 y1 n1)
  (and
  (forall ((i Int))
  (=> (and (<= x1 i) (< i y1))
  (= (select a i) true)))
  (forall ((i Int))
  (=> (and (<= y1 i) (< i n1))
  (= (select a i) false)))))))

;; A1
  (assert (and (<= 0 n) (<= n sz)))

;; A2
  (assert (< 0 d))

;; A3
  (assert (and (and (<= 0 x) (<= x y)) (<= y n)))

;; A4
  (assert (ttff x y n))

;; A6
  (assert
  (=> (< 0 y)
  (= (select a (- y 1)) true)))

;; A7
  (assert
  (=> (< 0 x)
  (= (select a (- x 1)) false)))

;;G
(assert
  (not
  (iff
  (and (<= (* 2 d) (+ n 1)) (ttff (- (+ n 1) (* 2 d)) (- (+ n 1) d) (+ n 1)))
  (and (= (- (+ n 1) y) d) (<= d (- y x))))))
(check-sat)
(get-model)