Z3条件语句

Question

如何在Z3中编写条件语句。

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

我想微软研究院来实现这Z3求解，但到目前为止没有运气

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