java - Z3 Java API。阅读 SMTLib2 并扩展它

Question

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

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

问题是它似乎只读取断言而忽略其余部分。因此，不能根据文件中定义的类别添加新的断言。排序未知，添加断言失败。

有什么我想念的方法吗？

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

感谢您的考虑。

Answer 1

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

就是说，parseSMTLIB2String 采用参数 sorts，它可以由稍后在 SMT2 文件中引用的排序填充。这可以用于使 SMT2 文件和您的基础结构的其余部分引用相同的类型。