将整数算术与布尔值混合 - Z3 证明者答案

【问题标题】：Mixing integer arithmetic with boolean - Z3 prover将整数算术与布尔值混合 - Z3 证明者
【发布时间】：2017-03-22 10:50:52
【问题描述】：

在阅读此问题之前，请考虑它旨在与 Z3 求解器工具一起使用并且它是 c++ api（所有内容都被重新定义，因此它不是正常的 c++ 语法）

谁能解释我如何将布尔逻辑与整数混合（编程明智）？示例：

y =  (x > 10 and x < 100) //y hsould be true or false (boolean)
z =  (y == true and k > 20 and k < 200)
m =  (z or w) //suppose w takes true of false (boolean)

我尝试了 c++ 文件中给出的示例，但我无法弄清楚在混合整数算术和布尔值时它是如何工作的。

【问题讨论】：

好吧，拿 x>10。如果 x 为 3，则表达式为假。所以这与算术无关，真的，但它们是逻辑表达式，将通过使用布尔算术的正确优先顺序来解决。
你有什么不明白的？ x > 10 的结果是 bool。
在 C++ 中，像 z or w 这样的表达式（对于那些好奇的人来说与 z || w 相同）是 true 或 false，它对应于整数值 1 和0。考虑到您之前在获取z 的结果时使用k 作为整数值（我假设），您确定要将z or w 的结果分配给k 吗？
@Someprogrammerdude 对不起，我编辑了它。
也许你最好展示你目前所写的实际程序，即使用 Z3 的 API 来构造求解器、项等的程序。

标签： c++ z3

【解决方案1】：

假设您是 C++ 的初学者，编写答案。

也许你正在寻找这个。

bool y,z,m,w;
int x, k; 
y = (x>10 && x<100);  
z = (y == true && k > 20 && k < 200);
m = (z || w);

让我们看看这条线是什么意思： y = (x>10 && x

这里如果x 大于 10 x>10 则结果 true。以同样的方式，如果x 小于 100 x<100 结果true。如果两者都是true，则右侧结果为true，将分配给y。 || 表示或。

【讨论】：