Я использую Z3 с SMT2 через C API / JNA / Scala и, кажется, работает довольно хорошо.

Я хочу попробовать пошаговое решение. Итак, сначала я перевожу это с помощьюZ3_parse_smtlib2_string:

(declare-fun x () Int)
(assert (>= x 0))
(check-sat)
(get-model)

Тогда я вернусьZ3_ast, положить его в решатель черезZ3_solver_assertпроверьте это с помощью Z3_solver_check и получите модель черезZ3_solver_get_model (если проверка вернулась удовлетворительно, что имеет место в этом примере). Пока проблем нет.

Но когда я хочу утверждать что-то дополнительно, как это:

(assert (= x 1))

Я застреваю в точке, гдеZ3_parse_smtlib2_string называется, потому что жалуется, что х неизвестная константа. Если я добавлю также добавитьdeclare-fun ко второму фрагменту я получаю неверную ошибку аргумента. Разве эта переменная уже не существует в среде? Нужно ли устанавливать дополнительные параметрыZ3_parse_smtlib2_string? Как я могу получить те из предварительно проанализированной формулы?

Также используя(set-option: global-decls true) не работает, как Z3 говорит мне, что этоoption value cannot be modified after initialization.

Кто-нибудь знает, как решить эту проблему?