Помните, что выражения Z3 — это логические формулы первого порядка, а не операторы. Если x
и y
являются логическими значениями, If(b,x,y)
эквивалентно b && x || !b && y
. Исключение y
эквивалентно замене на true
, а также на b ==> x
, т.е. Implies(b, x)
в Z3py.
Думает сложнее, если x
и y
не логические, а, например. целые числа. В этом случае условное выражение по сути является тернарным оператором b ? x : y
. Поскольку функции (и, следовательно, операторы) в SMT тотальны, вы не можете просто опустить y
(что бы b ? x
оценивало, если b
было ложным?).
В этой ситуации вы можете работать с недоопределенной переменной: объявите новую переменную SMT z
и ограничьте ее Implies(b, z == x)
. Таким образом, z
известно как x
, если b
истинно, а если b
ложно, z
имеет некоторое неизвестное значение.
Все выражения в z3 производят значение; думайте об этом как о функциональном языке программирования, а не как об императивном. Итак, вы имеют предоставляете пункт else
.
Такого рода вещи обычно возникают при моделировании императивных языков в z3; что-то вроде:
foo = expr1
if cond:
foo = expr2
Правильный способ смоделировать это — использовать так называемый Форма SSA и «сохранить» старое значение, т. Е. Приведенное выше становится:
foo0 = expr1
foo1 = If(cond, expr2, foo0)
Обратите внимание, что каждое присвоение «одной и той же» переменной получает новое имя (foo0
, foo1
и т. д.), и когда значение не изменяется с помощью условного оператора, мы просто сохраняем его старое значение. Большинство систем символьного моделирования (таких как Кли или другие API более высокого уровня) делают это за вас «под капотом». Обратите внимание, что придумать правильное задание, хотя оно и может быть автоматизировано, может быть сложно, в зависимости от типа foo
. (Что, если это список?)
Чтобы удовлетворить ваши потребности в программировании, всегда лучше спросить о конкретных случаях, когда вам нужна эта конструкция; в противном случае ответы обязательно будут обобщениями. То есть, хотя описанное выше является общей стратегией, ваша конкретная проблема может иметь более простое решение. Но без дополнительных подробностей невозможно узнать, чего именно вы пытаетесь достичь.
@TDG Выдает мне ошибку в Z3py, если я опускаю часть else