問題タブ [z3]

Z3 は、再帰関数を含む式の充足可能性をチェックできないことを知っています。しかし、 Z3は境界のあるデータ構造を超えてそのような数式を処理できるのだろうか。たとえば、私はZ3 プログラムlastで最大 2 つの長さのリストと、リストの最後の要素を返すという関数を定義しました。ただし、Z3 は、 を含む数式の充足可能性を確認するように求められたときに終了しませんlast。

Z3 で制限付きリストに対して再帰関数を使用する方法はありますか?

Z3 を使用して部分文字列について推論しようとしていますが、直感的でない動作に遭遇しました。Z3 は、「xy」が「xy」内にあるかどうかを判断するように求められると「sat」を返しますが、「x」が「x」にあるか、「x」が「xy」にあるかを尋ねられると「unknown」を返します。

この動作を説明するために、次のコードにコメントを付けました。

問題が設定されたので、部分文字列を見つけようとします。

findMeXY代わりにinを検索するとxy、ソルバーは予想どおり 'sat' を返します。ソルバーは「xy」についてこのクエリを処理できるため、「x」についても処理できるはずです。さらに、 で検索するfindMeX='x'と'xy='xy'、「不明」が返されます。

SMTソルバー内でこの問題を表現するための説明、またはおそらく代替モデルを提案できる人はいますか?

I am using Z3 version 3.0. I want to assign a value to a bitvector variable, like below. But Z3 reports error "invalid function application, sort mismatch on argument at position 2 in line 3".

It seems wrong with my constant #x0a? how can i fix this?

Thanks

Microsoft Z3 を使用するための Silverlight 4 アプリを入手できた人はいますか?

ネイティブのWindows dllを使用しているように見えるため、動作していないようです。

WCF RIA サービスを使用し、Azure でホストされている Silverlight アプリがあります。

Web アプリは Microsoft Z3 dll を参照します。

この dll の 32 ビット バージョンを参照すると、64 ビット バージョンが必要なため、Azure はそれをホストできません。64 ビット バージョンを参照すると、RIA サービスがコンパイルされません。

Azure で 32 ビット dll を使用する方法を見つけるか、RIA サービス用の 63 ビット dll を参照する方法を見つける必要があります。

どのアプローチが最適で、どのように行うかについてのヒントはありますか?

ありがとう

サム

Z3 の QBVF ソルバーをいじっていて、存在するアサーションから値を抽出できるかどうか疑問に思っています。つまり、私が次のものを持っているとしましょう：

これは基本的に、「最小」の 16 ビット符号なし値があることを示しています。次に、私は言うことができます：

Z3-3.0 は喜んでこう答えます。

これは本当にクールです。しかし、私がやりたいのは、get-value を介してそのモデルの一部を抽出できるようにすることです。当然のことながら、次のいずれも機能していないようです

いずれの場合も、Z3 は当然、そのような定数はないと不平を言います。(check-sat)呼び出しへの応答によって証明されるように、Z3 がその情報を持っていることは明らかです。get-valueまたは他のメカニズムを介して、存在する値に自動的にアクセスする方法はありますか?

ありがとう..

Particularly, does it use DPLL(T)? Does it use under/over approximations? Does it handle linear arithmetic on a word level? What about non-linear arithmetic?

I found only a superficial mention of "simplifications similar to those in MathSAT/Boolector" in paper Efficiently Solving Quantified Bit-Vector Formulas.

It is extremely interesting what methods helped Z3 to get the first place in QF_BV section of smtcomp.

Windows7でz3ocamlバインディングが機能していません。これが私が従ったプロセスです。

1. インストールされたObjectiveCamlバージョン3.11.0（Microsoftツールチェーン）
2. インストールされたcamlidl-1.05（Microsoft Visual Studio 2008 + cygwinを使用して構築）
3. インストールされたz3-3.0
4. 「build.cmd」を実行してz3ocamlバインディングをビルドしました。ビルドは成功しました。
5. 「build.cmd」によって生成されたファイルをz3/ocamlからObjectiveCaml/libにコピーしました

6. ocamlインタラクティブを起動し、「z3.cma」をロードしました

   /li>

誰かが私にいくつかのヒントを教えてもらえますか？

編集1： 「Z3-3.0 \ examples\ocaml」で例を作成します。

build.cmdからの抜粋

VisualStudio2008コマンドプロンプトでbuild.cmdを実行すると次のエラーが発生しました

を削除すると-ccopt "%XCFLAGS%"、正常に動作します。生成されたexeも期待どおりに実行されます。（PATHにflexdllがあることに注意してください）。なぜこれが起こっているのか考えていますか？

Z3 2.xには、シンボル宣言がポップされないという機能（おそらくバグ）がありました。たとえば、次のコードはZ32.xで受け入れられます。

Z3 3.xは、このコード（「不明な定数」）を受け入れなくなりました。

古い動作を復元する方法はありますか？または、宣言（および宣言のみ、仮定ではない）がグローバルになるように、つまりポップされないように、スコープ内でシンボルを宣言する方法はありますか？

-st コマンド オプションを指定して Z3 3.1 を実行すると、奇妙な統計結果が得られます。Ctrl-C を押すと、Z3 は total_time < time を報告します。それ以外の場合、Z3 が終了するまで待つ場合: total_time > time。

1. 「合計時間」と「時間」は何を測定しますか?
2. それはバグですか（マイナーですが）（上記の違い）？

ありがとう！