битвектор против целого числа в Z3

Я реализовал z3, используя фиксированную точку phi (Real, Real, Int, Int, Int, Int) и добавил некоторые правила в фиксированную точку. Это дало мне ответ, однако, когда я меняю тип Int на тип BitVector, он не может решить проблему и, наконец, «тайм-аут». Я думал, что будет быстрее использовать битвектор вместо int, однако это не так, почему?


z3
person Community    schedule 02.07.2012    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Я думаю, вы используете DL_ENGINE=1. Это вызывает механизм PDR, который в настоящее время предназначен только для чистых логических переменных и линейной вещественной арифметики (и часто также работает для линейной целочисленной арифметики).

person Nikolaj Bjorner    schedule 03.07.2012
comment
вы правы, я использую DL_ENGINE = 1, и когда я запускаю программу, она не показывает никаких ошибок, просто тайм-аут. Однако, когда я удаляю DL_ENGINE = 1, он показывает ошибку, в которой говорится, что в правило. Я использовал ctx.mkbound() для создания ограниченной переменной, я не понимаю, почему такая ошибка? - person ; 03.07.2012
comment
Кстати, есть ли подробное описание параметров INI, я не знаю, как их использовать. - person ; 03.07.2012

arrow_upward
2
arrow_downward

DL_ENGINE=0 запускает восходящий механизм регистрации данных. Он использует конечные таблицы, поэтому обрабатывает битовые векторы и логические значения в домене таблиц.
Два текущих варианта:

DL_ENGINE=0: use a Datalog engine for saturation. It works for finite domains.
DL_ENGINE=1: use a PDR engine.

Учебник на http://rise4fun.com/z3py/tutorial/fixedpoints иллюстрирует примеры использования этих двух опции.

person Nikolaj Bjorner    schedule 03.07.2012
comment
Спасибо, значит если есть Real, DL_ENGINE=0 для него не подходит, да? потому что Real не является конечной областью - person ; 03.07.2012