我如何以编程方式调用 Z3答案

【问题标题】：how do i invoke Z3 Programmatically我如何以编程方式调用 Z3
【发布时间】：2012-02-08 21:02:16
【问题描述】：

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

例如：

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

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

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

万分感谢！！！

【问题讨论】：

标签： z3

【解决方案1】：

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

【讨论】：

嘿，我尝试使用 Z3_parse_smtlib2_file API 读取输入 smt2 文件，然后使用检查 API。但是Z3给了我意想不到的结果。在使用检查 API 之前（完成解析后）我是否遗漏了什么？是否有 Z3_parse_smtlib2_file API 的完整示例？
函数 Z3_parse_smtlib2_file 返回一个指向包含 SMT 2.0 文件中所有断言的表达式的指针。断言未断言到 Z3 上下文中。用户负责调用 Z3_assert_cnstr。示例parser_example1 展示了如何做到这一点。这个例子是针对Z3_parse_smtlib_string的，但是思路是一样的。