当我使用 Z3_parse_smtlib2_file 解析 Z3 中提供的示例文件时出现解析错误答案

【问题标题】：parse error when i use Z3_parse_smtlib2_file to parse example files provided in Z3当我使用 Z3_parse_smtlib2_file 解析 Z3 中提供的示例文件时出现解析错误
【发布时间】：2012-09-18 08:26:28
【问题描述】：

我使用的是 Z3 4.1，我想在我的程序中解析 smt lib2 格式的输入。

所以我首先尝试使用Z3_parse_smtlib2_file 来解析Z3 中提供的示例（位于文件夹Z3-4.1/examples/smtlib 下）。但是我发现很多解析错误，然后我的程序立即退出。我认为输入格式应该是正确的。我尝试使用以下代码解析 Z3.2.smt2：

(set-option :auto-config true)
(set-option :produce-models true)

(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (> a 10))
(assert (< (f a true) 100))
(check-sat)

结果如下：

smt2parser_example
(error "line 1 column 26: error setting ':auto-config', option value cannot be modified after initialization")
Error code: 4
BUG: incorrect use of Z3.

API 是这样调用的：

fs = Z3_parse_smtlib2_file(ctx, fname, 0, 0, 0, 0, 0, 0);

问题出在哪里？输入文件应该没问题。问题出在 Z3_parse_smtlib2_file 的参数上吗？

【问题讨论】：

标签： api z3 parse-error

【解决方案1】：

如错误消息所示，一旦 Z3 上下文初始化，就无法修改 auto-config 选项。只有少数选项是可变的，可以在创建上下文后更改，并且自动配置不在其中。当行

(set-option :auto-config true)

从它正确解析的输入文件中删除。如果您的应用程序需要设置任何选项，最好将它们直接传递给上下文构造函数，即将config（C++ 中）或Z3_config（C 中）对象传递给它。

【讨论】：

克里斯托夫，你是对的。当我删除“(set-option :auto-config true)”行时，解析器 API 运行良好。但是我遇到了一个新问题。当我在输入文件末尾添加新行“（get-model）”时，Z3_parse_smtlib2_file 会产生错误。错误信息为：smt2parser_example (error "line 9 column 10: model is not available") 错误代码：4 BUG：Z3使用不正确。
确实，我也是这样。 :produce-models 选项在这里被忽略，它应该在构造上下文时设置。通常，解析函数 Z3_parse_smtlib* 主要用于解析公式。通过将 SMT2 脚本传递给 Z3 二进制文件，可以直接在命令行上执行它们。