0

これは私のPythonコードです:

s = z3.Solver()

f = z3.Function('f', z3.IntSort(), z3.IntSort())
g = z3.Function('g', z3.IntSort(), z3.IntSort())
h = z3.Function('h', z3.IntSort(), z3.IntSort())

a, b, c = z3.Ints('a b c')

imp_a = z3.And(f(a) == b, g(a) == c)
imp_b = h(c) == b
ax = z3.ForAll(a, z3.Implies(imp_a, imp_b))

l = [
    ax,
    f(1) == 5,
    g(1) == 2,
    h(2) != 5
]
s.add(l)

if s.check() == z3.sat:
    print s.model()
else:
    print 'Unsat'

このコードでは、Z3Py 構文で次の式を記述しました。

forall a, (f(a) == b and g(a) == c) => h(c) == b

このスクリプトを実行すると、モデルが見つかりますが、unsat. どうしてそれが可能でしょうか？何か不足していますか？

4

1 に答える 1

2

バインドするbのを忘れましたc:

ax = z3.ForAll([a,b,c], z3.Implies(imp_a, imp_b))

をバインドbしcた後、結果は になりunsatます。b、をバインドしない場合c、それらは自由定数として扱われ、式のモデルがあります。

于 2016-06-08T15:37:58.137 に答える