Z3 Java API。閱讀SMTLib2和exending它

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文件和其他基礎結構指向相同的類別。