使用上下文和求解器提取 z3 查询

Question

从查询中提取值后，如here 所述， 我遇到了一些看起来像错误的东西。当我只有 context 和 solver 时，如何打印相关查询的人类可读格式？

我的意思是，假设就在执行此行之前，我想打印查询：

Z3_solver_check(ctx,solver)

我本可以使用这个 API：

Z3_ast_to_string(Z3_context c, Z3_ast a)

但是Z3_ast a在哪里？我的意思是它隐含在求解器的某个地方，但我怎样才能提取它呢？ 非常感谢任何帮助，谢谢！

Answer 1

您正在寻找Z3_solver_to_string。