Z3 Java API。 SMTLib2を読んで、それをexending

Question

私は次のメソッドを使用してZ3ののJava APIによって共通SMTLib2ファイルを読み込むしようとしています：

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

問題は、唯一のアサーションを読み取り、残りを無視するようだということです。したがって、ファイルに定義されているソートに基づいて新しいアサーションを追加することはできません。ソートは不明であり、アサーションの追加は失敗します。

これを行う方法はありますか？

もしそうでなければ、APIを使用する代わりにSMTLib2形式を直接生成する必要があるようです。

ありがとうございました。

Answer 1

これは間違いなく、この関数は、（ほとんど）他のすべてのファイルの内容を無視して、ファイル内のすべてのアサーションの結合である式を返します。通常はZ3の外で行われるSMT2コマンドの読み込み機能はありません。

つまり、parseSMTLIB2Stringは、パラメータsortsを取ります。このパラメータは、後でSMT2ファイルで参照されるソートによって設定できます。これは、SMT2ファイルと残りのインフラストラクチャが同じソートを参照するように使用できます。