2
У меня есть очень простой пример программы Z3, который выглядит следующим образом:Выполнение сценария Z3 в командной строке
(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (> a 10))
(assert (< (f a true) 100))
(check-sat)
Эта типовая программа может быть выполнена в Z3 онлайн компилятором и нет никаких проблем. Но когда я хочу, чтобы выполнить ту же самую программу, используя командную строку с помощью следующей команды:
Z3 <script path>
Я получаю ошибку говоря:
ERROR: line 1 column 21: could not match expression to benchmark .
и эта ошибка повторяется для каждой строки в программе. Может ли кто-нибудь помочь мне увидеть, что я делаю неправильно?
Спасибо, что было здорово. Еще один вопрос, знаете ли вы, как я могу генерировать все различные варианты возможных ответов модели? –
См. Http://stackoverflow.com/questions/13395391/z3-finding-all-satisfying-models – dejvuth
Спасибо за ваш ответ, но это код в Z3 python. Я не могу использовать его в обычном синтаксисе Z3 –