Отображение объявлений, проанализированных из файла SMT-LIB2

Я использую Z3 с Java API. В моем файле SMT-LIB2 есть несколько переменных:

(declare-fun x0 () Int)
(declare-fun x1 () Bool)
; alot more

Я хочу получить все эти переменные и сохранить их в массиве Expr. Из примера, распределенного с z3, я нахожу API SMTLIBDecls которые обрабатывают объявления, анализируемые из файла SMT-LIB1, но для SMT-LIB2 подобного API нет. Как я могу получить декларации?

Благодарю.

1 ответ

В настоящее время для этой цели нет функции, но ее легко получить, пройдя выражения. Ранее это запрашивалось для C/C++, но ответ также относится к Java: Z3 4.3.1 C-API parse_smtlib2_string: откуда получить объявления?

Кроме того, эти сообщения могут также представлять интерес: перемещение дерева Z3_ast в C/C++. Как узнать, соответствует ли z3_ast предложению?

licensed under cc by-sa 3.0 with attribution.