z3 - 我如何以编程方式调用 Z3

Question

嗨，我是 Z3 SMT 求解器的新手。我知道您可以使用相关 API 以编程方式调用 Z3。但我想用 Z3 SMT 求解器做以下事情：

1. 如何以编程方式为 Z3 提供一个输入文件？
2. 我怎样才能逐步获得解决方案？

例如：

while ((check-sat) returns sat)
  get the assignments for all boolean vairables

最后，如何让Z3解完公式后将结果保存到一个输出文件中？

我可以查看任何想法或文件吗？

谢谢百万！！！

Answer 1

Z3 发行版包含几个（编程 API）示例。

• examples/c/test_capi.c：许多使用 C 接口的小例子。
• examples/dotnet/test_managed.cs：C# 中的类似示例
• examples/maxsat/maxsat.c：基于 Z3 API 的 MaxSAT 程序（C 语言）。
• examples/ocaml/test_mlapi.ml：ML 中的示例
• examples/theory/test_user_theory.c：展示如何实现外部理论（插件）的示例。