0

次のように、いくつかのブールフラグに基づいて実変数を再初期化する必要があります。の真理値を変更すると同時に、別の値location_nextで再初期化したいと思いx_nextます。どうやってやるの？

location, location_next = Bools('location location_next')
x, x_next = Reals('x x_next')
...
location_next == If(And(Not(location), x_next >= 12),
                    True,
                    If(And(location, x_next <= 0), False, location))
4

1 に答える 1

3

この関数If(Z3 API 内) を使用して、非ブール式を作成することもできます。すべてIf(c, t1, t2)の 、csort Boolean 、およびt1同じt2sort (type) を持つ必要がありSます。この場合、If(c, t1, t2)is は sort の Z3 式を生成しますS。以下に小さな例を示します。

x, y = Reals('x y')
print If(x > 0, x + 1, y - 1)

上記の例のリンクは次のとおりです: http://rise4fun.com/Z3Py/V4e

次の例では、 が と の場合に等しく、 が と の場合にに等しく、それ以外の場合に が等しいx_nextという式があります。x+1locationFalsex >= 12x-1locationTruex <= 0x

x_next == If(And(Not(location), x >= 12),
             x+1,
             If(And(location, x <= 0), x-1, x))
于 2012-08-08T14:39:59.693 に答える