5

Z3 Pythonでは、1） x = Const("x",IntSort()) と2）の違いは何x = Int("x") ですか？is_constは両方に対してtrueを返し、両方ともArithRefです。私は、1）定数を定義するのに適切であると思いました。たとえば、xは3.14であり、2）変数を作成することです。

x = 3.14のようなconst変数を作成する正しい方法はありますか（式x == 3.14を生成する以外）

4

1 に答える 1

7

Const("x", IntSort())との間に違いはありませんInt("x")。Int("x")前者のシンタックスシュガーと見なす必要があります。この関数Constは通常、ユーザー定義のソートの定数を定義するために使用されます。例：

S, (a, b, c) = EnumSort('S', ('a', 'b', 'c'))
x = Const("x", S)

Z3では、ユニバーサル変数と実存変数に「変数」という用語を使用します。数量詞のない数式には変数は含まれず、定数のみが含まれます。式では、、とx + 1 > 0言いx、1定数です。xは未解釈の定数であり、解釈された定数であると言い1ます。つまり、の意味は固定されていますが、式を充足可能にするために1、Z3は自由に解釈を割り当てることができます。x解釈された定数を作成したいだけの場合は3.14、を使用できますRealVal('3.14')。次の例では、xはZ3式ではなく、Z3式を指すPython変数です3.14。Z3式/式xを作成するときの省略形として使用できます。3.14Python変数zZ3式を指していますy。最後にz > x、Z3式を返しますy > 3.14。Z3Pyの初心者は通常、Python変数をZ3式と混同します。違いが明確になった後、すべてが理にかなっています。

x = RealVal('3.14')
z = Real('y')
print z > x
于 2012-09-16T17:29:07.980 に答える