問題タブ [z3]

Z3バージョン3.1を使用しているときに.NETAPI関数.parseSmtlib2String（String）を使用しているときにset-logicを使用するにはどうすればよいですか？

私はいつもZ3Error-Exceptionで終わります。

その場合は必要ありませんか？

Z3 を使用して、線形整数演算、解釈されない関数、ブール変数に対する量指定子を含むロジックの充足可能性をチェックしています。Z3 は、充足可能な問題のモデルを提供しません。これは、量指定子 (または、私が選択したロジック: AUFLIA) によるものだと思います。

すべてのブール変数を自分でインスタンス化する以外に、Z3 にそのような問題のモデルを提供させる方法はありますか?

前の議論のフォローアップ：Z3：実存的なモデル値の抽出

違いはありますか？

と

Z3に関する限り？つまり、後者のQBVFソルバーを自動的に取得できますか？

また、実験の結果、私が発行した場合、次のことがわかりました。

電話の後(check-sat)、それはうまくいきます（これは素晴らしいです）。私も言うことができればもっと良いでしょう：

残念ながら、そのクエリに対して、Z3はそれがであると文句を言いますinvalid function application。evalそのように機能を使う方法はありますか？

ありがとう！

レオナルド：迅速な返信ありがとうございます！とても有難い。

次のスクリプトをZ3にフィードすると、次のようになります。

s1Z3は、恒等関数が与えられているモデルを正常に構築します。ただし、evalを呼び出すと、Z3がタイムアウトします。設定する必要のある特定のオプションはありますか？

また、次の行を削除すると、次のことに気付きました。

次に、Z3が応答しunknownます。QBVFは決定可能であるため、オプションを設定する必要があるのは少し驚きでした。すべてのQBVF問題でMBQIを設定する必要があるのtrueは事実ですか、それともこのインスタンスに特別な何かがありますか？

ありがとう..

Cygwin と JDK 1.7.0 を使用して Win XP で Scala^Z3 をコンパイルしようとしましたが、期待どおりに動作しませんでした。

私は次のことを行いました: - SBT 0.7.4 を使用 - github から現在の Scala^Z3 リビジョンを使用 - Cygwin とその gcc を使用 - JDK 1.7.0 (javac) を使用

「sbt update」が成功しました。「sbt package」は、次のような未定義の参照を示すいくつかのエラーになります。

\psuter-ScalaZ3-35cb691\src\c/z3_Z3Wrapper.c:10: `_Z3_mk_config' への未定義の参照

まったく機能させるために、 ....\PSuterScalaZ3\psuter-ScalaZ3-35cb691\project\build\scalaz3.scala 行 74 を次のように変更しました。

lazy val gcc : ManagedTask = if(isUnix || is32bit) {

ホームページには、Windows でも動作するはずであると記載されています。まったくですか？コンパイル済みの jar はありますか?

ここで z3.jar を見ました: http://lara.epfl.ch/~psuter/jniz3/z3.jar これも Linux バージョンですね。私にも合わなかったので…

Scala^Z3 は非常に優れたコードです (動作させることができれば ;))

Z3はAUFBVをサポートしますか？

次のスクリプトの場合：

オンラインのZ3デモは電話に満足しているようですが、その後、種類とset-logicについて不平を言います。（ちなみに、オンラインデモは、論理名に関係なく、などの偽の名前であっても、呼び出しに満足しているようです。）BitVecArrayset-logic(set-logic blarg)

SMT-LibのWebサイトにはUFBVもAUFBVも記載されていませんが、数量詞のない対応物（QF_UFBVおよびQF_AUFBV）を考えると、Z3がAUFBVもサポートすることを期待していました。

言うまでもなく、アレイは実際には非常に重要な役割を果たします。有限性の議論を考えると、AUFBVロジックは決定可能であり続けるべきだと思います。Z3がそれをサポートするのを見るのは本当に素晴らしいでしょう。

ありがとう！

レオナルド：http：//goedel.cs.uiowa.edu/smtlib/papers/smt-lib-reference-v2.0-r10​​.12.21.pdfによると、セクション3.7.1=>は、正しく関連付けられており、=連鎖可能です。ただし、Z3のオンラインバージョンはそのような使用をサポートしていないようです。この動作を実現するために設定する必要のあるオプションはありますか？

ありがとう..

私はZ3を初めて使用するので、愚かなことを聞​​いてすみません。

一部のフィールドが関数になるようにレコードを定義しようとしています。私はこれを試しました：

(declare-datatypes (DOM RAN) ((PFun (mk-pfun (dom (DOM) Bool) (law (DOM) RAN)))))

dom と ran は、タイプが関数である 2 つのフィールドであることを意図しています (dom は DOM から Bool への関数、law は DOM から RAN への関数)。関数の型を括弧で囲んでも試しました：

(declare-datatypes (DOM RAN) ((PFun (mk-pfun (dom ((DOM) Bool)) (law ((DOM) RAN))))))

これらはどれも機能しません。

チュートリアルを検索しましたが、この例はありません。

手伝って頂けますか？

ご回答ありがとうございます。

頑張れ、マキシ

2つのSMT問題インスタンスがあります。最初はここにあります：

Z3は、私のそれほど優れていないマシンで約2分でこの問題のモデルを返します。これは素晴らしいです。私もこれを持っています：

Z3を完了せずに、この問題でz3を一晩実行しました。これらのファイルの内容を確認すると、最初のインスタンスによって返されたモデルを「拒否」する追加のアサーションがあることを除いて、2番目のファイルが最初のファイルと同じであることがわかります。（私が何を意味するかを確認するために、それらの間で「差分」を行うことができます。）この問題には複数の満足のいくモデルがあることを偶然知っており、z3を使用してすべての満足のいくモデルを見つけようとしています。

これは完全に予想されることかもしれませんが、2番目の問題が最初の問題と比較してZ3にとってはるかに難しい問題である理由を知りたいと思いました。Z3がより簡単な時間を持てるように、2番目の問題を定式化するためのより良い方法はありますか？

ありがとう..

Z3 には、自動参照カウントと手動の 2 つのモードがあります。

手動参照カウントの仕組みを理解しています。例に感謝します。

しかし、自動参照カウントの場合、Z3 はどのようにして AST ノードを削除するかを知るのでしょうか? Z3_ast は C 言語の構造体であるため => Z3_ast が作成された後、Z3 の外部で Z3_ast のすべての割り当てと使用法を追跡することは不可能です。

または、Z3 は Z3 内のみの参照を追跡しますか? たとえば、ast1 = ast2 の場合、ref カウンターの更新は行われません。