2017-08-28 20 views
2

私は次のメソッドを使用してZ3ののJava APIによって共通SMTLib2ファイルを読み込むしようとしています:Z3 Java API。 SMTLib2を読んで、それをexending

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

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

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

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

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

答えて

1

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

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

関連する問題