Z3: лучший способ моделировать?

Question

У меня два экземпляра проблем с SMT.Первое здесь:

http://gist.github.com/1232766

Z3 возвращает модель для этой проблемы приблизительно через 2 минуты на моей не очень большой машине, и это здорово .. У меня также есть эта:

http://gist.github.com/1232769

Я запустил z3 за одну ночь по этой проблеме без завершения Z3.Если вы проверите содержимое этих файлов, вы увидите, что второй файл идентичен первому, за исключением того, что у него есть дополнительное утверждение для «отклонения» модели, возвращенной первым экземпляром.(Вы можете сделать «разницу» между ними, чтобы понять, что я имею в виду.) Я случайно узнал, что у этой задачи есть несколько удовлетворяющих моделей, и я пытаюсь использовать z3, чтобы найти все удовлетворительные модели.Я понимаю, что этого вполне можно ожидать, но мне было любопытно узнать, почему вторая проблема гораздо сложнее для Z3 по сравнению с первой.Есть ли лучший способ сформулировать вторую проблему, чтобы Z3 было легче?

Спасибо ..

Answer 1

Трудно дать вам точный ответ, не зная больше о вашем заявлении. Как вы предположили, моделирование играет большую роль в используемой логике: AUFBV. Стратегия, используемая Z3, также оказывает большое влияние на общую производительность. Z3 оснащен несколькими встроенными стратегиями. Он имеет много параметров, которые могут быть использованы для влияния на поиск. Z3 также имеет язык спецификации стратегии. Это новая функция. Я не рекламирую его, потому что он работает, и язык, скорее всего, изменится в следующих версиях. Вы можете получить дополнительную информацию о языке стратегии, выполнив команды:

(help check-sat-using)
(help-strategy)

При этом в Z3 есть встроенная стратегия, которая, кажется, эффективна для вашей проблемы. Это стратегия, используемая для логики UFBV. Ваша проблема использует массивы, но их можно избежать, преобразовав table0 в функцию с двумя аргументами:

(declare-fun table0 ((_ BitVec 64) (_ BitVec 64)) (_ BitVec 8))

И заменяя каждый член формы (select (table0 s65) t) на (table0 s65 t), где t - произвольный термин. Наконец, вы также должны добавить команду (set-logic UFBV) в начале файла. С этим параметром мне удалось сгенерировать 4 разные модели для вашего запроса. Я не пытался генерировать больше, чем это. Каждый звонок занимает около 75 секунд.