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

Я новичок в использовании 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), иначе это выдавало ошибку.

Спасибо.


z3
person user1213045    schedule 16.02.2012    source источник

Ответы (1)


arrow_upward
1
arrow_downward

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

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

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

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

person Leonardo de Moura    schedule 16.02.2012
comment
Есть ли какие-либо другие параметры, которые мне нужно установить иначе, чем значения по умолчанию в Z3 3.2, чтобы он работал как Z3 2.8? - person user1213045; 07.03.2012
comment
Имейте в виду, что невозможно точно смоделировать поведение Z3 2.8. Многие изменения (новые алгоритмы, новые функции, алгоритмы и т. д.) были внесены по сравнению с Z3 2.8. Вы наблюдаете большое несоответствие производительности в ваших тестах? - person Leonardo de Moura; 07.03.2012
comment
Да. На данный момент трудно понять, где происходит узкое место в производительности. Но на выходе наблюдается замедление в 2 раза и более. Я хочу предотвратить возможности, которые новая версия Z3 пытается решить, в то время как старая просто отказывается говорить неизвестно. Например: как в случае MBQI = false. Я просто пытаюсь понять, есть ли другие параметры INI, которые должны быть изменены со значений по умолчанию в новом Z3, чтобы обеспечить поведение как можно ближе к 2.8. Спасибо. - person user1213045; 09.03.2012