在量化公式的情况下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)