Z3条件语句 [英] Z3 Conditional Statement

问题描述

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

How to write a conditional statement in Z3.

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

我正在尝试通过Microsoft Research在Z3 Solver中实现这一目标，但到目前为止还算不上成功

I am trying to achieve this in Z3 Solver by Microsoft Research but so far no luck

推荐答案

查找SSA表单: https://en.wikipedia.org/wiki/Static_single_assignment_form

本质上，您必须将程序更改为类似于以下内容的

Essentially, you'll have to change your program to look something like:

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

一旦采用了这种所谓的静态单分配形式，您现在就可以直接或多或少地直接翻译每行；对 value_N 的最新赋值是 value 的最终值.

Once it is in this so called static single assignment form, you can now translate each line more or less directly; with the latest assignment to value_N being the final value of value.

循环将是有问题的:通常的策略是将它们展开到一定数量(有边界的模型检查)，并希望这足以满足要求.如果您发现最后一次展开还不够，则可以在该点生成一个未解释的值；否则，请执行以下操作.这可能会导致您的证明因虚假的反例而失败；但这是您最好的选择，而无需一个涉及归纳和循环不变式正确处理的方案.

Loops will be problematic: The usual strategy is to unroll them up to a certain count (bounded model checking), and hope that this suffices. If you detect that the last unrolling isn't sufficient, then you can generate an uninterpreted value at that point; which might cause your proofs to fail with spurious counter-examples; but that's the best you can do without a scheme that involves proper handling of induction and loop-invariants.

请注意，该研究领域称为符号执行"，具有悠久的历史，仍在进行积极的研究.您可能需要阅读以下内容: https://en.wikipedia.org/wiki/Symbolic_execution

Note that this field of study is called "symbolic execution" and has a long history, with active research still being conducted. You might want to read through this: https://en.wikipedia.org/wiki/Symbolic_execution

这篇关于Z3条件语句的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！