Предложение If в Z3py без else

Как написать предложение If('condition', x, y) в Z3py, если у нас нет части else?

@TDG Выдает мне ошибку в Z3py, если я опускаю часть else

Mario 02.04.2022 18:09
Почему в Python есть оператор "pass"?
Почему в Python есть оператор "pass"?
Оператор pass в Python - это простая концепция, которую могут быстро освоить даже новички без опыта программирования.
Некоторые методы, о которых вы не знали, что они существуют в Python
Некоторые методы, о которых вы не знали, что они существуют в Python
Python - самый известный и самый простой в изучении язык в наши дни. Имея широкий спектр применения в области машинного обучения, Data Science,...
Основы Python Часть I
Основы Python Часть I
Вы когда-нибудь задумывались, почему в программах на Python вы видите приведенный ниже код?
LeetCode - 1579. Удаление максимального числа ребер для сохранения полной проходимости графа
LeetCode - 1579. Удаление максимального числа ребер для сохранения полной проходимости графа
Алиса и Боб имеют неориентированный граф из n узлов и трех типов ребер:
Оптимизация кода с помощью тернарного оператора Python
Оптимизация кода с помощью тернарного оператора Python
И последнее, что мы хотели бы показать вам, прежде чем двигаться дальше, это
Советы по эффективной веб-разработке с помощью Python
Советы по эффективной веб-разработке с помощью Python
Как веб-разработчик, Python может стать мощным инструментом для создания эффективных и масштабируемых веб-приложений.
0
1
36
2
Перейти к ответу Данный вопрос помечен как решенный

Ответы 2

Помните, что выражения 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. (Что, если это список?)

Чтобы удовлетворить ваши потребности в программировании, всегда лучше спросить о конкретных случаях, когда вам нужна эта конструкция; в противном случае ответы обязательно будут обобщениями. То есть, хотя описанное выше является общей стратегией, ваша конкретная проблема может иметь более простое решение. Но без дополнительных подробностей невозможно узнать, чего именно вы пытаетесь достичь.

Другие вопросы по теме