問題タブ [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 モデルの配列項の値
研究に z3 を使用していますが、次の問題があります。配列と未解釈の関数を含む充足可能な数式のモデルを分析しています。特定の配列エントリを検査したいと思います。
z3 ガイドの例では、そのような値にアクセスできます。
たとえば、次のような質問に対して
次のような答えが得られます
の値がmy_arrayで0あることを示します1。
しかし、私が得る答えは次のようになります
これはまったく役に立ちません。
また、モデルの開始時に、次のようなブロックを取得します。
私はこれの意味をよく理解していませんが、ガイドの簡単な例では同様のブロックが表示されないため、どういうわけかこれは私の問題に関連しているようです。z3のこの動作を引き起こす原因、または回避方法を知っている人はいますか?
いくつかの実験の後、望ましくない動作を示す「最小限の」例を見つけました。インデックス式で解釈されない関数を使用することと関係があるようです。
これに対する z3 の応答は次のとおりです。
z3 - モデルの並べ替えの不一致
z3 で QF_AUFLIA の式を分析しました。結果は でしたsat。によって返されたモデルには(get-model)、次の行が含まれていました。
SMTLIBv2 言語に関する私の理解によれば、このステートメントは形式が正しくありません。=同じ種類の引数にのみ適用する必要があります。ただし、2sortIntとsortfalseがありますBool。
この 2 行だけを z3 にフィードバックすると、次のように同意してくれます。
これはバグですか？
そうでない場合、どのように解釈すればよい(= 2 false)ですか?
z3 - Z3 バージョン 2.19 と 3.2 の間に SMTLIB-2 コード構文に関する違いはありますか?
Z3 V3.1 をインストールした後、次の SMT-LIB コードが機能しません。私の以前のバージョン（Z3 V2.19）ではかなり良かったです。
上記のコードをバージョン 3.1 で実行するには、何を変更する必要がありますか。
z3 - Z3における未解釈関数の表現について
簡単な質問があります。簡単なプログラム (Z3 NET API を使用) を作成し、次のような出力を得ました。
プログラム（一部）：
出力：
「else -> true」を false (つまり、「else -> false」) にできるかどうか疑問に思っています。
statistics - Z3 3.2 で統計情報を取得するには?
Z3 2.x では SMTLib2 コマンドを使用しました
Z3 実行の統計を取得します。Z3 3.2 を使用すると、
上記のために、そして
Z3 は次のように応答します。
統計情報を取得する新しい方法 (/st コマンド ライン オプション以外) は?
INIオプションページのリスト
は有効なオプションですが、Z3 3.2 は再び次のように応答します。
z3 - z3_astが句に対応するかどうかを確認するにはどうすればよいですか？
私はcapiでZ3を使用しています。Z3_ast与えられた変数が以下のような節に対応するかどうかを知ることは可能or_b1_b2ですか？
ありがとうございました
z3 - 入力ファイルで Z3 を呼び出す方法
以下を含むファイルがあります。
オンライン チュートリアルによると、このファイルに対して z3 を実行すると、次のように返されます。
だから私はこれが正当な Z3 入力であることを知っています。ただし、「z3 [option]」を実行すると、選択したオプションに関係なく、エラーメッセージが表示されるだけです。エラーメッセージはありません。入力ファイルで Z3 を正しく呼び出す方法を教えてもらえますか?
よろしく。
z3 - 任意の命題式の変数の上限/下限を決定する
任意の命題式 PHI (いくつかの変数に対する線形制約) が与えられた場合、各変数の (近似) 上限と下限を決定する最良の方法は何ですか?
一部の変数は制限されていない場合があります。この場合、アルゴリズムは、これらの変数に上限/下限がないと結論付ける必要があります。
例えば、PHI = (x=3 AND y>=1)。x の上限と下限は両方とも 3 です。y の下限は 1 で、y には上限がありません。
これは非常に単純な例ですが、一般的な解決策はありますか (おそらく SMT ソルバーを使用)?
optimization - z3 からの間違った結果
Z3 SMT Solver で次のことを証明しようとしています: ((x*x) + x) = ((~x * ~x) + ~x). これは正しいです。これは、C プログラミング言語のオーバーフロー セマンティックのためです。
今、私は次の smt-lib コードを書きました:
z3 からの出力は次のとおりです。
ここで私の質問: 結果が「unsat」になるのはなぜですか? コード内の simple コマンドは、myfun1 と myfun2 が同じ結果になるように有効な割り当てを取得できることを示しています。
私のコードに何か問題がありますか、それとも z3 のバグですか?
誰でも私を助けてください。どうも