0

z3とmathsatを使用していくつかの実験を行う必要があります。私はすでにmathsatで実験を終えました。mathsatの入力ファイルを作成するには時間がかかり、z3の入力ファイルを再度作成したくありません。Mathsatは、「msat」ファイルからの「smt」ファイルの生成をサポートしています。変換コマンドを以下に示します。

/home/xdb/mathsat/mathsat-4.2.17-linux-x86_64/bin/mathsat -input=msat -output=smt -logic=QF_LRA /home/xdb/satcase/sample/sample.msat>>/home/xdb/satcase/sample/sample.smt

私の質問は、z3がこの「smt」ファイルを認識できるかどうかです。

4

1 に答える 1

0

Z3はSMT1.0および2.0ファイルを読み取ることができます。形式はhttp://www.smtlib.orgで定義されています。MathSATによって生成された数式が標準に準拠している場合は、問題はありません。生成されたファイルを読み取るためにZ3を使用しようとしましたか？それが機能しなかった場合、Z3によって生成されたエラーメッセージは何でしたか？

于 2013-01-04T14:38:49.333 に答える