Как запустить файл smtLib с помощью Z3 в Ubuntu?

Например, у меня есть файл smtLib 'encoding.smt'. Теперь я хочу запустить этот файл с помощью z3 (автономный исполняемый файл) с заданным временем ожидания и выделением памяти на машине с Ubuntu. Нравиться :

$./z3 encoding.smt 240(sec) 6(GB)

Я скачал 32-битный zip-файл Ubuntu со страницы загрузки Z3. Что мне теперь делать? В папке «bin» есть приложение z3. Должен ли я изменить какую-либо переменную среды, если я хочу написать любой скрипт Z3py под Ubuntu?

Может ли кто-нибудь дать мне шаги для обоих (запуск файла .smt с помощью автономного Z3 с заданным тайм-аутом и памятью и запуск файла .smt из сценария z3py с заданным тайм-аутом) и память)

Спасибо за ваше предложение


z3 z3py
person user1770051    schedule 27.11.2013    source источник
comment
Я получил параметры тайм-аута, памяти z3 (исполняемого файла) с помощью команды справки $ ./z3 -h. Но может ли кто-нибудь сказать мне, как я могу установить параметры в сценарии Z3py? например -solver.set('время ожидания', 240) Solver.set('память', 6) !! Я не знаю, как установить эти параметры. Я видел сообщение о тайм-ауте, но как я могу установить ограничение памяти. Спасибо   -  person user1770051    schedule 27.11.2013

Ответы (1)


arrow_upward
0
arrow_downward

Эти параметры называются timeout и memory_max_size соответственно. В интерфейсе python их можно установить следующим образом:

set_option(timeout='60')
set_option(memory_max_size='1000')

Список опций (глобальных и модульных) можно получить, запустив z3 -p. Эти параметры также можно установить в командной строке, например,

z3 encoding.smt2 timeout=60 memory_max_size=1000
person Christoph Wintersteiger    schedule 13.12.2013