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

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

Спасибо.

источник

2012-02-16 user1213045

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

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

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

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

источник

2012-02-16 06:47:00

Есть ли какие-либо другие опции, которые мне нужно установить иначе, чем значения по умолчанию в Z3 3.2, чтобы заставить его работать как Z3 2.8? – user1213045

Имейте в виду, что невозможно смоделировать точное поведение Z3 2.8. Многие изменения (новые алгоритмы, новые функции, алгоритмы и т. Д.) Были сделаны с Z3 2.8. Вы наблюдаете большое несоответствие производительности в своих тестах? –

Да. На данный момент трудно понять, где происходит узкое место производительности. Но на выходе видно замедление в 2x или более. Я хочу предотвратить возможности, в которых новая версия Z3 пытается решить, в то время как старый просто отказывается сказать «неизвестно». Например, как в случае MBQI = false. Я просто пытаюсь понять, есть ли другие параметры INI, которые должны быть изменены из значений по умолчанию в новом Z3, чтобы обеспечить максимально приближенное к 2.8 поведение. Спасибо. – user1213045

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

ответ

Смежные вопросы