1

我正在使用 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 中的参数吗？

4

1 回答 1

1

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

(set-option :auto-config true)

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

于 2012-09-27T18:26:04.257 回答