問題タブ [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 - コードに関するSmtlibの問題
私はこの次のコードを持っています
コードは最初にunsat（check-sat）を返し、2番目にsat（check-sat）を返すはずですが、不明になります。
誰かが何が問題なのか教えてもらえますか？私はWindows7を使用していますが、cygwinを使用してjSMTLIBを使用しています
ありがとうサイフ
z3 - integer/bv 混合ベンチマークの健全性の問題?
次の SMT-Lib2 スクリプトがあります。
Z3 v3.2 を Mac で実行すると、次のようになります。
これは、s0 = -1 がモデルであることを示しています。ただし、s0 = -1 の場合、s3 = 1 および s5 = #b0 となり、アサーションが偽になります。実際、記載されているベンチマークは満足できないものであると確信しています。
Z3 の出力で気づいたことの 1 つは、カーディナリティ制約に対して与えられる定量化された式です。それは言います：
アサーションは接続詞で、かなり奇妙に聞こえます。それは分離ではないでしょうか？これが問題の根本的な原因であるかどうかはわかりませんが、怪しげに聞こえます。
arrays - Z3におけるSMTLIB配列理論の奇妙さ
SMTLIB配列を使用しているときに、Z3の理論の理解と私の理解の違いに気づきました。私は公式ウェブサイト[1]にあるSMTLIB配列理論[0]を使用しています。
私の問題は簡単な例で最もよく説明されていると思います。
最初の配列はインデックス1で2を返し、他のすべてのインデックスでは0を返し、2番目の配列はインデックス0で1を返し、インデックス1で2を返し、他のすべてのインデックスで0を返す必要があります。selectインデックス0で呼び出すと、これを確認できるようです。
Z3はsat両方に戻ります。
予想通り、この場合、Z3（重要な場合はlinux-amd64でバージョン3.2を使用しています）が応答unsatします。次に、これら2つのアレイを比較してみましょう。
Z3はsat、「これら2つの配列は同等に比較される」と解釈します。ただし、これらの配列は同等に比較されないと思います。私はこれをSMTLIB配列理論に基づいています。
したがって、平易な英語では、これは「2つの配列は、すべてのインデックスで等しい場合にのみ、等しいと比較される」という意味になります。誰かが私にこれを説明できますか？私は何かを見逃しているのですか、それとも理論を誤解していますか？この問題についてのご意見をお待ちしております。
よろしく、レオン
[0] http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2 [1] http://smtlib.org
command - stdin / smt2を介したcheck_assumptions？
SMT2標準（またはそのZ3拡張）は、API呼び出し「check_assumptions」と同等のコマンドを提供しますか？Josh Berdineによると、多くの場合、プッシュポップスコープよりもガードリテラルとcheck_assumptionsを使用する方が高速です。ただし、今のところstdioを介してZ3を使用し、(check-assumoptions p)yieldsのみを使用することに固執していますunsupported。
z3 - z3 で「良い」unsat-core を取得する (ロジック QF_BV)
Z3 SMT ソルバーを使用して、SMTLIB 2 言語を使用してロジック QF_BV で表現した問題を解決しています。
モデルは満足できないので、ソルバーに不飽和コアを生成させようとしています。
私のモデルは、assertステートメントを使用して指定するいくつかの「必須」の制約で構成されています。
unsat-core 生成で考慮したいアサーションは、(assert (! (EXPR) :named NAME))構文を使用して指定されています。
予想どおり、 Z3 は を返しますunsat。ただし、Z3 は常に、すべての名前付きアサーションで構成される「些細な」unsat-core をダンプするようです。
名前付きアサーションのサブセットが存在することを知っています。これは unsat-core です。このコアは、Yices SMT ソルバーを使用して見つけました。これにより、比較的小さな unsat-core が得られることがよくあります。Yices モデルは Z3 モデルと同じです (SMT2 から Yices 入力言語への行ごとの翻訳です)。
「良い」unsat-core を生成することはソルバー固有の機能ですか、それとも Z3 がより良いコアを提供できるようにするための一般的な提案/変更はありますか?
z3 - z3_dbg.dll はまだディストリビューションの一部ですか?
Z3 の最後のリリースでは、z3_dbg.dll を入手できませんでした。まだリリースされていますか？
アレクサンドル。
z3 - pull_nested_quantifiers オプションは Z3 での単純化で機能しますか?
数式内のネストされたすべての量指定子を最も外側のレベルに移動したいと考えています。次のコマンドが Z3 で機能することを期待していましたが、機能しません。
の目的は:pull-nested-quantifiers何ですか? SMT-LIB または Z3 API を使用してネストされた量指定子を取得するにはどうすればよいですか?
z3 - Z3 Context serialization/deserialization?
Is it possible to serialize/deserialize a Z3 context (from C#)? If not, is this feature planned ?
I think this feature is important for real world applications.
z3 - Z3: 実数モデル
このベンチマークの場合:
私は得ています：
これは既知の問題ですか? (これは Linux と Mac の両方で Z3 V3.2 を使用しています。)
z3 - 中間モデルの出力を無効にすることはできますか？
数量詞を含む式には、trans関数の宣言が含まれています。Z3はモデルを正常に検出し、印刷します。trans!1!4464ただし、モデル内のどこでも使用されていない、trans!7!4463..などの関数のモデルも出力します。それは何ですか？この出力を無効にするにはどうすればよいですか？
クエリは次のとおりです：http：//dl.dropbox.com/u/444947/asyn_arbiter_bound_16.smt2 そしてこれがZ3の出力です-http : //dl.dropbox.com/u/444947/asyn_arbiter_bound_16_result.txt