我正在尝试使用以下方法通过Z3的Java API读取常见的SMTLib2文件:

BoolExpr parseSMTLIB2String (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)

问题在于,它似乎仅读取断言,而忽略其余断言。因此,不能基于文件中定义的排序添加新的断言。排序是未知的,并且断言的添加失败。

有什么办法可以让我错过吗?

如果没有,看来我应该直接生成SMTLib2格式,而不要使用API​​。

感谢您的考虑。

最佳答案

没错,此函数返回一个表达式,该表达式是文件中所有断言的结合,而忽略了(几乎)所有其他文件内容。没有读取SMT2命令的功能,这通常是在Z3之外完成的。

就是说,parseSMTLIB2String带有参数sorts,可以通过稍后在SMT2文件中引用的排序填充该参数。可以使用它,以使SMT2文件和基础结构的其余部分引用相同的种类。

09-30 17:13
查看更多