我正在尝试使用以下方法通过Z3的Java API读取常见的SMTLib2文件:
BoolExpr parseSMTLIB2String (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
问题在于,它似乎仅读取断言,而忽略其余断言。因此,不能基于文件中定义的排序添加新的断言。排序是未知的,并且断言的添加失败。
有什么办法可以让我错过吗?
如果没有,看来我应该直接生成SMTLib2格式,而不要使用API。
感谢您的考虑。
最佳答案
没错,此函数返回一个表达式,该表达式是文件中所有断言的结合,而忽略了(几乎)所有其他文件内容。没有读取SMT2命令的功能,这通常是在Z3之外完成的。
就是说,parseSMTLIB2String
带有参数sorts
,可以通过稍后在SMT2文件中引用的排序填充该参数。可以使用它,以使SMT2文件和基础结构的其余部分引用相同的种类。