(Z3Py) какие-либо ограничения в объявлении функций?

Есть ли ограничения в объявлении функций?

Например, этот фрагмент кода возвращает 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 интерпретирует объявленную функцию? Он просто вызывает это несколько раз или здесь тоже есть какой-то скрытый механизм?


python z3
person Community    schedule 10.08.2012    source источник

Ответы (1)


arrow_upward
3
arrow_downward

В вызове функции one_op(unk_op, arg1, arg2) unk_op является выражением Z3. Тогда такие выражения, как op==1 и op==2 (в определении one_op), также являются символическими выражениями Z3. Поскольку op==1 не является логическим выражением Python False. Функция one_op всегда будет возвращать выражение Z3 arg1*arg2. Мы можем проверить это, выполнив print one_op(unk_op, arg1, arg2). Обратите внимание, что операторы if в определении one_op являются операторами Python.

Я считаю, что ваше истинное намерение - вернуть выражение 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]
person Leonardo de Moura    schedule 10.08.2012
comment
А, так функция должна возвращать выражение Z3, это как конструктор выражений! - person ; 10.08.2012