Условное заявление Z3

Question

Как написать условное утверждение в Z3.

eg: 
if (a%2==0){
value=1
}

Я пытаюсь добиться этого в Z3 Solver от Microsoft Research, но пока не повезло

Answer 1

Посмотрите форму SSA: https://en.wikipedia.org/wiki/Static_single_assignment_form

По сути, вам придется изменить свою программу, чтобы она выглядела примерно так:

value_0 = 0
value_1 = (a%2 == 0) ? 1 : value_0

Как только он находится в этой так называемой статической форме одного назначения, теперь вы можете переводить каждую строку более или менее напрямую; с последним назначением value_N будучи окончательным значением value,

Циклы будут проблематичными: обычная стратегия состоит в том, чтобы развернуть их до определенного количества (проверка ограниченной модели) и надеяться, что этого достаточно. Если вы обнаружите, что последней развертки недостаточно, вы можете создать неинтерпретированное значение в этой точке; что может привести к сбою ваших доказательств с поддельными контрпримерами; но это лучшее, что вы можете сделать без схемы, которая включает в себя правильную обработку индукции и инвариантов цикла.

Обратите внимание, что эта область исследований называется "символическим исполнением" и имеет долгую историю, при этом активные исследования все еще проводятся. Вы можете прочитать это: https://en.wikipedia.org/wiki/Symbolic_execution