3

関数の宣言に制限はありますか?

たとえば、このコードは unsat を返します。

from z3 import *

def one_op (op, arg1, arg2):
    if op==1:
        return arg1*arg2
    if op==2:
        return arg1-arg2
    if op==3:
        return arg1+arg2

    return arg1+arg2 # default

s=Solver()

arg1, arg2, result, unk_op=Ints ('arg1 arg2 result unk_op')

s.add (unk_op>=1, unk_op<=3)

s.add (arg1==1)
s.add (arg2==2)
s.add (result==3)
s.add (one_op(unk_op, arg1, arg2)==result)

print s.check()

Z3Py は宣言された関数をどのように解釈しますか? それは時々それを呼び出すだけですか、それともいくつかの隠された機械がここにもありますか?

4

1 に答える 1

3

関数呼び出しone_op(unk_op, arg1, arg2)で、unk_opは Z3 式です。そして( の定義の)op==1などの式も Z3 記号式です。は Python のブール式ではないためです。関数は常に Z3 式を返します。を実行することで確認できます。の定義のステートメントは Python ステートメントであることに注意してください。op==2one_opop==1Falseone_oparg1*arg2print one_op(unk_op, arg1, arg2)ifone_op

あなたの本当の意図は、条件式を含む Z3 式を返すことだと思います。次のように定義することで、これを実現できますone_op。

def one_op (op, arg1, arg2):
    return  If(op==1,
               arg1*arg2,
               If(op==2,
                  arg1-arg2,
                  If(op==3,
                     arg1+arg2,
                     arg1+arg2)))

これで、コマンドIfは Z3 条件式を作成します。この定義を使用することで、満足のいく解決策を見つけることができます。完全な例を次に示します。

from z3 import *

def one_op (op, arg1, arg2):
    return  If(op==1,
               arg1*arg2,
               If(op==2,
                  arg1-arg2,
                  If(op==3,
                     arg1+arg2,
                     arg1+arg2)))

s=Solver()

arg1, arg2, result, unk_op=Ints ('arg1 arg2 result unk_op')

s.add (unk_op>=1, unk_op<=3)
s.add (arg1==1)
s.add (arg2==2)
s.add (result==3)
s.add (one_op(unk_op, arg1, arg2)==result)

print s.check()
print s.model()

結果は次のとおりです。

sat
[unk_op = 3, result = 3, arg2 = 2, arg1 = 1]
于 2012-08-10T16:36:34.027 に答える