我有一个用 Z3 用 C++ 编写的可满足性问题，我正在尝试将其转换为 SMT-LIB2，然后将其输入 CVC4 来解决。
当我Z3_solver为问题打印（使用Z3_solver_to_string()）时，我相信它是以Z3_PRINT_SMTLIB_FULL表格形式打印的，而不是Z3_PRINT_SMTLIB2_COMPLIANT（CVC4 抛出Parse Error: unexpected token '('）。
我在 API 中看到有一个方法调用Z3_set_ast_print_mode()来以正确的 SMT-LIB 形式获取 AST，但是有没有办法为该Z3_solver类型执行此操作？求解器是否适合在这里打印，或者我应该打印其中一个节点并将其发送到 CVC4？