如何在Z3中编写条件语句。
eg:
if (a%2==0){
value=1
}
我正试图在 Microsoft Research 的 Z3 Solver 中实现这一目标，但到目前为止还没有成功
【问题讨论】：
标签： conditional z3 solver
查找 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
【讨论】：