使用Z3_parse_smtlib2_file解析Z3中提供的示例文件时出现解析错误
使用Z3_parse_smtlib2_file解析Z3中提供的示例文件时出现解析错误
提问于 2012-09-27 00:32:41
我使用的是SMT4.1，我想在我的程序中解析Z3 lib2格式的输入。
因此，我首先尝试使用Z3_parse_smtlib2_file来解析Z3中提供的示例(位于Z34.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);问题出在哪里？输入文件应该是OK的。问题出在Z3_parse_smtlib2_file中的参数中吗？
回答 1
Stack Overflow用户
发布于 2012-09-28 02:26:04
如错误消息所示，一旦初始化了Z3上下文，就不能修改自动配置选项。只有几个选项是可变的，并且可以在创建上下文后更改，并且自动配置不在其中。当线条
(set-option :auto-config true)从它正确解析的输入文件中删除。如果您的应用程序需要设置任何选项，最好将它们直接传递给上下文构造函数，即通过将config (在C++中)或Z3_config (在C中)对象传递给它。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/12606349
复制相关文章
相似问题
腾讯云开发者
