smt

1熱

1答えて

.netと一緒にZ3（バージョン4.5.0.1）を使用したいのですが、SMTLIBファイルを使用できるかどうか疑問です。 using(Context context = new Context(new Dictionary<string, string>() { { "model", "true" } })) { context.ParseSMTLIB2String(Resources.

0熱

1答えて

SMT入力用にcvc4のユーザ定義シンボルのオーバーロードを有効にするオプションはありますか？

1.2からSMT-LIB言語のバージョンでは、ユーザー定義シンボルのオーバーロードが許可されていました。標準のバージョン2.0以降、オーバーロードは理論のシンボルに制限されています。しかし、SMTソルバーの中には、ユーザー定義のシンボルが過負荷になることがあります。私の使用例では便利です。証拠の義務は、過負荷で自動的に生成されます。 cvc4をSMTソルバーの私のポートフォリオに追加しましたが、

1熱

1答えて

数式を解くときにZ3にどこから始めるべきかを教えてください。

私は現在、Z3に与えられたアサーションに多数の不等式と等価が含まれている状況を扱っています。それらは、等価で使用される変数に値を割り当てることによって式を解くことが最も効率的であるように、互いに依存している。 Z3のヒューリスティックスを変更して、ソルバがこれらの公式で常に「開始」するようにする方法はありますか？私の推測では、最初に言及した同値を含む目標を処理する戦術を使用することでしょう。その

0熱

2答えて

SMT/SATソルバーとモデルチェッカー

最近、私は正式な検証技術を研究し始めました。文献では、モデルチェッカーとソルバーが何らかの意味で使用されています。しかし、モデルチェッカーとソルバーはどうつながっていますか？ p.s.いくつかの論文やリンクが提案されていれば幸いです。

3熱

1答えて

は、私がZ3と次のような問題を解決しようとしていますZ3

で `exists`スコープの変数へのアクセス： 4つの演算子（+、-、*、/）の設定した、で置換することができた事業者を決めますそれを真にするための式に従う： (((((1 <op1> 2) <op2> 3) <op3> 4) <op4> 5) <op5> 6) = 35 すべての有効な回答を印刷する必要があります。ここではサンプルプログラムは、Z3言語である： (declare-datat

0熱

1答えて

z3でBitVecでどのような値を表現できますか？

私はBitVecがz3でどのように機能するのか分かりません。この範囲内と外の値があるので、私は、これは「UNSAT」であることをことを期待 >>> import z3 >>> s = z3.Solver() >>> a = z3.BitVec("a", 32) >>> s.add(z3.ForAll(a, z3.Not(z3.And(a > 2147483647, a < 214748467

1熱

1答えて

既存のSMTソルバを使用して、QF_UF公式の等価ブール式を得ることは可能ですか？

熱心なSMTソルバでは、SMT式は、同等のブール式としてエンコードされ、SATソルバに供給されます。通常、QF_UFの式では、未知の関数はAckermannの減少またはブライアントの減少によって減少し、等値グラフの手法によって等価ブール式が構築されます。ソルバの低レベルの実装をハックすることなく、QF_UFの公式で同等のブール式を得るために既存のSMTソルバを呼び出すことが可能かどうかを知りたい

1熱

1答えて

Z3pyの式でZeroExt（n、a）を正しく使うには？

私はバイナリで隠されたkeygenアルゴリズムのパスワードを調べようとしています。だから、私は、アセンブリから式を抽出し、それを解決するために、小さなPythonスクリプトで（正しく、うまくいけば）翻訳： Traceback (most recent call last): File "./alt.py", line 13, in <module> state[i+1] = (

0熱

1答えて

CVC4の誘導データ型のアサーション

私はCVC4で少し実験を試みています。私は次の出力 sat ((x R) (y R)) sat ((x R) (y R)) を取得しています。この使用CVC4を実行すると、私は、この出力により、この動作によって混乱しています (set-option :produce-models true) (set-option :produce-assignments true) (set-lo