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)