1

与えられc == a + 4たt == c + b、もしb == -4、そしてt == a。私は反対のことをしようとしています。つまり、上記の 2 つの方程式 と が与えられた場合t == a、b

これは関連する質問aとかなり似ていますが、今回はとを切り替えるだけbで、コードが異なる結果を返すことに本当に混乱しています。

上記のリンクに投稿されたコードに続いて、以下のコードがあります（類似、唯一a、b切り替え）：

#!/usr/bin/python
from z3 import *

a, b, c, t = BitVecs('a b c t', 32)

g = True
g = And(g, c == (a + 4))
g = And(g, t == (c + b))

s = Solver()
s.add(ForAll([t, a, c], Implies(t == a, g)))
if s.check() == sat:
    print s.model()[b]
else:
    print 'Unsat'

ただし、Ubuntu では、上記のコードを実行すると予期しない結果Unsatが返されますが、値-4 (または0xfffffffc )は返されません。

なぜこれが間違っているのですか？

本当にありがとう。

4

1 に答える 1

1

Z3は実際に戻ってきてunknownいます。このメソッドは、 、またはをcheck返します。これは、式が実際に未飽和であることを示すカスタム戦術です。satunsatunknown

#!/usr/bin/python
from z3 import *
a, b, c, t = BitVecs('a b c t', 32)

g = True
g = And(g, c == (a + 4))
g = And(g, t == (c + b))

s = Goal()
s.add(ForAll([t, a, c], Implies(t == a, g)))

T = Then("simplify", "der", "distribute-forall")
# print the simplified formula. Note that it is unsat
print T(s)

# Create a solver using the tactic above and qe

s = Then("simplify", "der", "distribute-forall", "qe", "smt").solver()
s.add(ForAll([t, a, c], Implies(t == a, g)))
print s.check()

更新 式は次の形式です

forall t, a, c: t == a ==> c == (a + 4) and t == (c + b).

この式は、次と論理的に同等です。

forall a, c: c == (a + 4) and a == (c + b).

これは論理的に同等です

(forall a, c: c == (a + 4)) and (forall a, c: a == (c + b)).

どちらの部分式も、論理的には false と同等です。これが、式が満たされない理由です。

あなたが書いたコメントは、わずかに異なる式を作成したと信じていることを示唆しています

forall t, a, c: t == a ==> c == (a + 4) ==> t == (c + b).

この式はsatです。この数式を作成するには、置換する必要があります

g = True
g = And(g, c == (a + 4))
g = And(g, t == (c + b))

と

g = Implies(c == (a + 4), t == (c + b))

更新された例は、こちらから入手できます。

于 2013-07-05T19:31:30.437 に答える