Причина тайм-аута?

Question

Я новичок в использовании Z3. Но я хочу понять, причина истечения времени ожидания в следующей программе, введенной в Z3:

(declare-fun ADDR (Int) Int)
(declare-fun STAR (Int Int) Int)
(declare-fun VAR (Int Int) Int)
(declare-const error Int)

(assert (forall ((x Int)) (= x (STAR (ADDR x) 0))) );causes a timeout?
(assert (forall ((x Int)) (>= (ADDR x) 4000)) )
(assert (not (= (VAR  error 0) 1)))
(check-sat)
(get-model)

Еще один вопрос, который у меня есть, есть ли что-то новое с forall в версии 3.2? Я должен был поставить дополнительные скобки (x Int), иначе это выдавало ошибку.

Спасибо.

Answer 1

Эта формула выполнима, и Z3 не может построить модель для нее.Вы можете избежать тайм-аута, если отключите поиск моделей для количественных формул.

(set-option :auto-config false)
(set-option :mbqi false)

Если вы сделаете это, Z3 вернет неизвестное и «модель-кандидат».Эта проблема обсуждается в руководстве Z3 .

Необходимы дополнительные скобки, поскольку Z3 3.x полностью совместим со стандартом SMT 2.0 .