Хотя я вижу, что в C ++ существует обход Z3 AST (обрисовано в общих чертах в этом вопросе ), я не могу найти его эквивалентный метод в Java API, есть ли способ, которым я могу пройтиZ3 AST в Java?
Спасибо!
Я думаю, что соответствующие функции находятся здесь: https://github.com/Z3Prover/z3/blob/master/src/api/java/Expr.java
(я не программист на Java, и я не использовал их сам; так что возьмите это с собой!)