smt

0熱

1答えて

に私がZ3/SMTLibのAPIについて質問があります。液体タイプツールが必要キーSMTサブルーチンは、次のクエリです：現在 INPUT: A "background" formula P , A list of "goal" formulas Qs = [Q1,...,Qn] OUTPUT: Largest Qs' \subset Qs s.t. forall Q in Qs'

1熱

2答えて

Z3はこのプログラムを検証できるはずですか？

私はZ3の初心者です。最近、いくつかの問題を確認するためにz3を使用しています。ここに私が試した一つの問題である：（X & Y < 0）は含意X/Y> = 0、以下、私が書いたプログラムは、次のとおり (declare-const x Int) (declare-const y Int) (define-fun assumption() Bool (and (< x 0) (< y

1熱

1答えて

SMT式用のより小さいモデルを得る

私は座っている可能性のある数式を持っているとしましょう。 SMTソルバーにそのような小さなソリューションを提供する方法はありますか？例： A +私はSMTソルバーは私に10の代わりに NOTE 100 乾杯のソリューションを提供したいという例では1> 10 ：私は持っています3年前にz3の作者がz3でその機能を実装していたと回答したsimilar questionを見ただけです。それが既に実装さ

2熱

1答えて

SMTソルバーを使用して関数を構成する方法を見つける方法はありますか？

私はSMTソルバーの初心者です。プログラム合成のバリエーションとして使用しようとしています。とにかく、何が問題になるのかは、与えられた入力に対して要求された出力を与える一連の適用された操作（以前に定義された関数の構成）を見つけることです。 SMTソルバーを使用して、特定の出力に到達するために関数を作成する順番を調べる方法はありますか？あなたが私のための読書資料を持っているなら、私は読んで嬉しいです

1熱

1答えて

Z3の検索時間は式の順序に影響されますか？

多くのプログラミング言語では、分岐効率は、句が提供される順序に依存します。例えば、Pythonで、 if p or q : はすぐpがtrueと評価されたので、一般的に最初の計算が光句を提供することをお勧めしてif文に分岐します。私はZ3の充足可能性チェックにも同じことが当てはまるのだろうかと思います。言い換えると、And(P, Q)とAnd(Q, P)のチェックの間に違いがありますか？ただし

1熱

1答えて

最大化/最小化Z3 SMT C++ API

C++ APIを使用して、指定されたシンボリック変数の最適化を得るにはどうすればよいですかSymVar_0？私はthis postを見ましたが、それを使用する方法についてはっきりしません。 (set-logic QF_AUFBV)(declare-fun SymVar_0() (_ BitVec 32))(declare-fun SymVar_1() (_ BitVec 8))(declare-

0熱

1答えて

QF_AUFBVモードでZ3が遅い

QF_AUFBVモードでSMT-COMP 2015 benchmark resultsをチェックしていて、衝撃的です。 Same thing for 2014. それによると、Z3は他のSMTソルバーよりも桁違いに遅いです。私の理解では、Z3はCVC4ほど高速です。何か不足していますか？よろしく

0熱

1答えて

CVC4最小化/最大化モデル最適化

ビットベクトルas Z3 doesの結果モデルを最大化または最小化するオプションはありますか？ありがとうございました。

1熱

1答えて

Z3の関数をJava実装で定義していますか？

これは私がやろうとしていることです。のは、私はこれに似た表現で（結合し、そのJava）のZ3を使用してopの値を見つけたいとしましょう： ((exists (op Int)) (= (foo op) 2) だから私はopに機能fooを呼びたいです変数を調べ、関数が返すopの値を調べる。2. Javaで関数fooを定義し、Z3がこれらの関数定義にアクセスする方法があると考えた。私はこのようにしたい

0熱

1答えて

少数の加算とシフトで定数を掛けること

addition, subtraction and shiftを使用して2つの数を掛けることは可能です。この手順の重要な部分は、このような操作の最小限の（最適な）シーケンスを見つけることです。ブルートフォースを使用してシーケンスを見つけると、指数関数的に成長するので、さまざまな経験則が使用されます。おそらく最もよく知られているのは、Robert Bernsteinの論文Multiplication