Решатель z3: z3-SMT на платформе Mac

Мне нужно поработать над решателем Z3 SMT для моей магистерской диссертации. Я уже проверил учебные пособия для Z3-SMT, которые основаны на входных данных SMT-Lib. Но я смог установить только z3-Py, для которого нужно знание Python. Я хотел знать, есть ли возможность установить z3 с использованием внешнего интерфейса SMT на Mac OSX. Если да, то не могли бы вы помочь это сделать?


z3 z3py
person Lena    schedule 01.11.2013    source источник
comment
Из z3.codeplex.com: Поддерживаемые платформы: Windows, OSX, Linux и FreeBSD. Там прямо сказано, что он будет работать на OSX.   -  person Scott Solmer    schedule 01.11.2013
comment
@ Okuma.Scott, я следовал инструкциям на сайте, но получил следующий результат: Z3Py успешно собран. Итак, как я понял z3 с помощью python был установлен. У меня нет никаких знаний о python, и я хочу знать, есть ли способ установить z3 с помощью SMT Lib.   -  person Lena    schedule 01.11.2013
comment
Согласно Википедии, SMT-LIB можно использовать с C/C++, .NET, OCaml, Python и Java. . Но информация, доступная на http://www.smtlib.org/, очень минимальна. Если Википедия права, она выглядит обнадеживающей.   -  person Scott Solmer    schedule 01.11.2013
comment
Википедия берет информацию из здесь Можно также вызывать Z3 процедурно, используя API ANSI C, API для общеязыковой среды выполнения, управляемой .NET, или API OCaml.   -  person Scott Solmer    schedule 01.11.2013
comment
Спасибо вам, ребята. Я применил то, что предложил @Taylor, и теперь это работает.   -  person Lena    schedule 03.11.2013

Ответы (1)


arrow_upward
0
arrow_downward

Самый простой способ запустить сценарии SMT-LIB — использовать интерфейсrise4fun: http://rise4fun.com/Z3.

Тем не менее, вам может понадобиться запустить Z3 в автономном режиме для больших проблем или в других программах. Похоже, вы уже установили Z3, так как у вас работает z3py. Если вам удалось установить z3py, вы также можете запустить Z3, так как z3py зависит от Z3 (технически это библиотека z3, но у вас, вероятно, установлены и библиотека, и исполняемый файл, если вы получили исходный код из codeplex и скомпилировали его). Инструкции по компиляции и установке для всех платформ см. по адресу: https://z3.codeplex.com/SourceControl/latest#README

После установки вы можете запустить исполняемый файл z3 в файле SMT-LIB2 с именем test.smt, используя ./z3 -smt2 test.smt (или просто z3 -smt2 test.smt, если вы поместите его в путь).

person Taylor T. Johnson    schedule 01.11.2013