z3 times out in case of a formula with quantifiers

Question

I am getting timeout on the following example. http://rise4fun.com/Z3/zbOcW

Is there any trick to make this work (eg.by reformulating the problem or using triggers)?

Answer 1

For this example, the macro finder will be useful (I think often with forall quantifiers with implications), you can enable it with:

(set-option :macro-finder true)

Here's your updated example that gets sat quickly (rise4fun link: 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)