smt

1熱

1答えて

CVC4：定量化機能を持つboolの機能を合成する設定ですか？私は現在、次の形式の式を解くためにCVC4を使用してい

：ここ exists f1, ..., fn . P(f1, ..., fn) /\ forall (b1...bk) . Q(f1,...fn,b1,...bk) 、f1...fnはBoolにBoolのいくつかの数の関数であり、 b1...bkはブール値です。私の問題は、SMTのUFフラグメントに正当に該当します。それは、量子はありますが、関数とブール値以外のソートはありません。 CVC4

-2熱

1答えて

Z3での「最小化」の仕組み

私はZ3のminimize関数をたくさん使っていますが、私はいくつかのスケーラビリティの問題（最小化する変数の数が増えると）について心配しています。 "最小化"の根底にあるアルゴリズムは何ですか？そして、物事をスピードアップする一般的な方法はありますか？

3熱

2答えて

Z3またはZ3に渡す前に一貫性のない方程式を検出できますか？

私は次の例でz3で作業していました。 f=Function('f',IntSort(),IntSort()) n=Int('n') c=Int('c') s=Solver() s.add(c>=0) s.add(f(0)==0) s.add(ForAll([n],Implies(n>=0, f(n+1)==f(n)+10/(n-c)))) 最後の式には一貫性がありません（n=cは不

1熱

1答えて

z3pyでZ3 EnumSortの値を抽出できません

現在、問題をZ3にエンコードしようとしています。「tristate」ブール型（つまり、true,falseおよびunknownのブール値）をモデル化したいと考えています。ここでが、私はそれをモデル化してきた方法です。 #!/usr/bin/env python import z3 from collections import OrderedDict TristateValues =

2熱

1答えて

Z3：線形代数を表現する

行列やベクトルを含む式の性質を証明したいと考えています（サイズは大きくなる可能性がありますが、サイズは固定されています）。 Iは、式の結果は、対角行列または三角行列である、またはそれは、正定であることを証明したい例えば ... そのために私は、エンコードよく知られた特性をたいと思いますし、以下のような線形代数からアイデンティティ、： ||x + y|| <= ||x|| + ||y|| (A *

1熱

1答えて

が部分的にZ3でZ3

でのConstを解釈、一方がそうのような完全に解釈constを宣言することができ：考える (define-fun y() Int 3) ; y == 3 ： (declare-const x Int) 同様に、一つはこのような完全解釈いずれかを定義することができ代数的データ型の場合、次のような完全に解釈されたタプルを持つことができます。 (declare-datatypes() ((It

0熱

1答えて

Z3：C APIを使用してすべての解決策を見つける

私はZ3ソルバーの新人で、Windows 10、VS2013コマンドプロンプトを使用しています。私はCを使用しようとしていますが、私はZ3ソルバーを使用して以下の問題を解決しようとしました。設定問題：a + 2*b + 3*c = 7を満たすa、b、cの可能な組み合わせは何ですか？は、だから私はZ3のCのコード例に基づいて、Cコードの下に作られた： void example(){

2熱

1答えて

EPR断片のプレノックス定量の順序は重要ですか？

1次論理の効果的命題（EPR）フラグメントは、しばしば∃X.∀Y.Φ(X,Y)という形式のプレノックスで数量化された式のセットとして定義されます。XとYは（おそらくは空の）可変シーケンスです。定量化の順序、つまり∃*∀*はEPRの決定可能性に関係しますか？定量化の順序が入れ替わった場合、決定性を失うか？特に、私は決定可能なロジックで集合モナドのバインド操作のセマンティクスをキャプチャすることに興

2熱

1答えて

Z3で完全に評価された結果は？

Z3は、しばしば、中間関数の束として定義されたモデルを返します。たとえば、次のようなことがよくあります（私の不適切な構文を許してください）。 (define-const myArray (Array Bool Int) (_ as-array f)) (define-fun f (x Bool) Int (f!10 (k!26 x))) ...などです。私は私のプログラム（ライブラリバイン