问Z3条件语句
EN

Stack Overflow用户

提问于 2017-06-02 02:18:04

回答 1查看 743关注 0票数 0

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

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

我正试图在微软研究院的Z3解算器中实现这一点，但到目前为止还没有成功

发布于 2017-06-03 00:09:10

从本质上讲，您必须将您的程序更改为如下所示：

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

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

循环将是有问题的:通常的策略是将它们展开到特定的计数(有界模型检查)，并希望这就足够了。如果您检测到最后一次展开不够充分，那么您可以在该点生成一个未解释的值；这可能会导致您的证明因错误的反例而失败；但这是在没有涉及正确处理归纳和循环不变量的方案的情况下所能做的最好的事情。

请注意，这一研究领域被称为“符号执行”，具有悠久的历史，目前仍在进行积极的研究。你可能想通读一下：https://en.wikipedia.org/wiki/Symbolic_execution

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/44314486

复制

相似问题

问Z3条件语句EN