2

ForAllで数量詞を使用しようとしているので、すべてbの式で結果が得られます。以下のコードでこれを実装しました（Z3 python）：a * b == bba == 1

from z3 import *

a, b, a1 = BitVecs('a b a1', 32)

f = True
f = And(f, a1 == a * b)
f = And(f, a1 == b)

s = Solver()
s.add(ForAll(b, f))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat'

a = 1Z3 が出力で提供してくれると思っていましたが、そうではありませんでしたUnsat。問題がどこにあるかについて何か考えはありますか？

(ForAll を適切に使用していないと思われますが、修正方法がわかりません)

4

4 に答える 4

1

Z3 (とりわけ) に、 b のすべての値に対して b と等しい単一の a1 を見つけるように求めています。これは不可能です。あなたの問題はZ3ではなく、基本的なロジックにあります。

于 2013-06-16T17:31:18.097 に答える
1

これについてあなたはどう思いますか：

a, b, a1 = BitVecs('a b a1', 32)

f = True
f = And(f, a1 == a * b)
g= True
g = And(f, a1 == b)

s = Solver()
s.add(ForAll(b, ForAll(a1,f == g)))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat

出力：

a = 1

その他の形式:

a, b, a1 = BitVecs('a b a1', 32)

f = True
f = And(f, a1 == a * b)
g= True
g = And(g, a1 == b)

s = Solver()
s.add(ForAll(b, ForAll(a1,f == g)))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat'

出力：

a = 1
于 2013-06-16T13:44:53.193 に答える
0

これについてあなたはどう思いますか：

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

a1 = a*b
a2 = b


s = Solver()
s.add(ForAll(b, a1 == a2))

if s.check() == sat:
     print 'a =', s.model()[a]
else:
     print 'Unsat'

出力：

a = 1

他の方法：

a, b = BitVecs('a b', 32)
a1 = a*b
a2 = b
f = True
f = And(f, a1 == a2)


s = Solver()
s.add(ForAll(b, f))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat'

出力：

a = 1
于 2013-06-15T17:00:20.900 に答える