Блог

Я использую Z3 через его .Net Api. Я создаю модели, которые имеют значительно огромное количество ограничений. До сих пор я использовал соответствующие команды Z3 (в .Net Api) для построения моей модели построчно. Но теперь, когда модель увеличилась в размерах, время, необходимое для создания модели, очень велико. Я подумал, есть ли способ создать модель в виде текстового файла и ввести завершенную модель в решатель Z3 за один раз?

Ваш вопрос довольно загадочный, но все SMT-решатели поддерживают так называемый формат ввода SMTLib2: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

Итак, по крайней мере теоретически, вы можете записать свои ограничения в файл в формате SMTLib, как описано в приведенном выше документе, а затем вызвать z3 для этого файла.

Но это не обязательно будет быстрее, чем прямое использование API: на самом деле, я ожидаю, что вызов z3 через его API будет быстрее, поскольку он позволяет избежать этапа «запись в файл, чтение из файла»; но это может работать лучше в вашем конкретном случае использования, есливы можете повторно использовать некоторые из этих ограничений во многих вызовах.

Если вы используете python api, вы можете использовать эти две функции, если работаете с текстовыми файлами или строковым вводом:

parse_smt2_file() и parse_smt2_string() который вы можете найти здесь