問題タブ [z3]
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 と SMT-LIB を使用して、最大 2 つの値を取得します
smt-lib2 を使用して数式の最大値を取得するにはどうすればよいですか?
私はこのようなものが欲しい：
もちろん、'max' は smtlibv2 にはわかりません。では、どうすればこれを行うことができますか？
types - Z3の列挙型間のサブタイプ関係の表現
Z3の列挙型間のサブタイプ関係を表現するための最良の方法は何ですか？
具体的には、次のようなことをしたいと思います。
次に、新しいサブタイプを作成します。
そのため、動物タイプの4つの異なる定数があるという主張はSATですが、哺乳類タイプの4つの異なる定数があるという主張はUNSATです。
z3 - Z3 と smtlib を使用して、値が混在する構成/モデルを計算する
属性値を計算するにはどうすればよいですか? 次に例を示します。
これで私は2つのモデルを取得します:
今、私が欲しいのは次のようなものです：
したがって、属性の合計が 6 より大きいモデルを取得したいと思います。
たぶん、配列を操作することがこれを達成する方法です...
z3 - Z3のソフト/ハード制約
Z3でソフト制約とハード制約を表現するにはどうすればよいですか？APIから、仮定（ソフト制約）を設定できることはわかっていますが、コマンドラインツールを使用する場合はこれを表現できません。私はz3/smt2/siを使用してそれを呼んでいます
scala - scala^z3 を使用した z3 で可能な構成が多すぎます
これは主に論理的な問題だと思います...
私はこの smtlib 式を使用します:
この構造の用語はどれですか（少なくとも私の意見では）：
私の推測: resultSet は次のようになります。
しかし、これはscala^z3 ctx.checkAndGetAllModels()を使用しています:
ad と abcd が入っているのはなぜですか? 期待した結果だけを得ることができますか?
algorithm - SMTソルバーでブール式の最適解を見つけることは可能ですか?
編集の理由により、解決する大きなブール式があります。ここに画像を貼り付ける必要があります。
areaまた、 4 つの整数の次元を測定する関数が既にあります。area(c,d,e,f)=|c−d|×|e−f|
数式が満足できるかどうかを判断するだけ(a,b,c,d,e,f)ではなく、大きな数式を作成し、数式を満たす他の 6 タプルの次元以上の最適な 6 タプルをTRUE探しarea(c,d,e,f)ています。
言い換えれMax(area(c,d,e,f))ば、大きな公式の対象を見つけてください。
SMT ソルバーがこの問題に役立つかどうか疑問に思っています。Z3が をサポートしていることを学びquantifiers、ブール式が満足できるかどうかを判断できるようになりました。しかし問題はZ3、関数の最適解を見つけるのに役立つかどうかareaです。
誰にもアイデアはありますか？SMT ソルバー、Z3、またはその他のアルゴリズムについてのコメントをお待ちしております...
optimization - Z3 でコードを最適化する方法は? (PI_NON_NESTED_ARITH_WEIGHT 関連)
ブール式の最適化問題z3を解決することを目的としたコードがあります
量指定子と含意のためだと思いますが、このコードには多くのコストがかかります。オンラインでテストしたところ、2 つの警告が表示され、最終結果はunknown次のようになりました。
良い結果が得られないのがこれらの2つの警告であるかどうか、誰か教えてもらえますか? このコードを最適化して実行する方法はありますか?
scala - Scala^Z3 はパーサー エラーで実行中のスレッドを強制終了します
Scala^Z3 (Z3 3.2 およびそれに応じた Scala^Z3 Java ライブラリ) を使用すると、次のようなパーサー エラーが発生します。
実行されたスレッドは強制終了され、コードを try/catch などで囲んでもこれを止めることはできません。
この動作を停止する方法はありますか?
z3 - Z3は、declare-sort / define-sortによって導入されたソートを含むデータ型を処理できますか？
宣言ソートまたは定義ソートによって導入されたソートを含むデータ型を定義しようとしています。ただし、次の試行はエラーになります。
それを行う方法はありますか？
前もって感謝します。
z3 - Z3 (NET API) でモデル化/充足可能性をチェックするために必要なメモリと時間を見つける方法
いくつかの研究問題を解決するために、Z3 と Yices と一緒に 1 年足らず働いています。これらのソルバーを使用して、常にパフォーマンスを評価する必要があります。特に、モデリング/チェックに必要な時間とスペース (メモリ) (充足可能性) の 2 つです。Z3の場合、それらを直接見つける手がかりは見つかりませんでした。「統計」(Z3 NET API が提供する関数「DisplayStatistics」を使用) を試してみたところ、(例) 以下に示すような出力が見つかりました。
番号。競合: 122
番号。決定: 2245
番号。伝播: 27884 (バイナリ: 21129)
番号。再起動: 1
番号。最終チェック: 1
番号。分。点灯: 52
番号。追加された式: 3766
番号。mk ブール変数: 2782
番号。デル ブール変数: 658
番号。mk エノード: 1723
番号。削除ノード: 78
番号。mk 句: 3622
番号。デル節: 1517
番号。mk bin 節: 3067
番号。mk 点灯: 18935
番号。ta 競合: 28
番号。行を追加: 5091
番号。ピボット: 328
番号。下をアサート: 2597
番号。アサートアッパー：3416
番号。Diseq をアサート: 1353
番号。バインドされた小道具: 787
番号。固定式: 697
番号。オフセット式: 866
番号。疑似nl.: 34
番号。式 アダプター: 820
これらの値を解釈して、使用されたメモリ/時間を理解する方法がわかりません。実行時間を見つける方法がいくつかあります (Stopwatch などのタイマー クラスを使用)。しかし、スペースが必要な場合は、方法が見つかりませんでした。モデリングに必要なブール変数 (低レベル、SAT ソルバー) の数を取得できれば、非常にうまく機能します。
誰かが私に解決策を示すことができれば、それは素晴らしいことです。