問題タブ [mathsat]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
z3 - z3はMathSATの出力ファイルを入力ファイルとして読み取ることができますか？
z3とmathsatを使用していくつかの実験を行う必要があります。私はすでにmathsatで実験を終えました。mathsatの入力ファイルを作成するには時間がかかり、z3の入力ファイルを再度作成したくありません。Mathsatは、「msat」ファイルからの「smt」ファイルの生成をサポートしています。変換コマンドを以下に示します。
私の質問は、z3がこの「smt」ファイルを認識できるかどうかです。
z3 - Alt-Ergo を使用して次の SMT-LIB コードを実行する方法
次の SMT-LIB コードは、Z3、MathSat、および CVC4 では問題なく実行されますが、Alt-Ergo では実行されません。どうなるか教えてください。よろしくお願いします。
z3 - Mathsat を使用して特定のインスタンスの解の数を決定する方法
Mathsat はコマンドcheck-allsatをサポートしていますが、Z3 はサポートしていません。次の例を検討してください。
このコードを mathsat で実行すると、すべての一貫した割り当てが取得されます。問題は、Mathsat を使用してそのような一貫した割り当ての数を決定する方法です。
z3 - SMT -LIB で Z3 と CVC4 を使用して、二面体群 D3 の定理を証明する方法
以前の投稿で、Z3 SMT-LIB を使用した二面体群 D3 の 1 つの定理が証明されました。この投稿では、次の SMT-LIB コードを使用して、Z3 と CVC4 の両方を使用してそのような定理を証明しようとします。
Z3 または CVC4 を使用してこのコードを実行すると、正しい結果が得られます。Z3オンラインでこのコードをここで実行してください
質問は次のとおりです。
Z3 の場合、メッセージ
unsupported ; :incrementalが生成されます。このメッセージは結果を変更しないようですが、なぜですか?CVC4 の場合、
unknownZ3 が生成する間にメッセージが生成されますsat。繰り返しますが、このメッセージは結果を変更しないようです。なぜですか?Mathsat を使用して SMT-LIB コードを実行する方法。
z3 - ソルバーの決定に応じて get-model または unsat-core を実行する
SMT-LIB 2.0 スクリプトで、ソルバーの最後の充足可能性の決定 (sat、unsat、...) にアクセスする可能性があるかどうか疑問に思います。たとえば、次のコード:
Z3 で実行:
MathSAT で実行すると、次のように返されます。
MathSAT 5 では、ブレークオン (get-model) するだけで、到達すらしません (get-unsat-core)。SMT-LIB 2.0 言語で、決定が SAT の場合に get-model を実行し、決定が UNSAT の場合に unsat-core を実行する方法はありますか? ソリューションは、たとえば次のようになります。
SMT-LIB 2.0 言語のドキュメントを検索しましたが、ヒントは見つかりませんでした。
編集:以下のコードも試しましたが、残念ながら機能しませんでした。