将整数算术与布尔值混合 - Z3 证明器

Mixing integer arithmetic with boolean - Z3 prover

本文关键字：Z3 证明 混合 布尔值 整数      更新时间：2023-10-16

在阅读这个问题之前，请考虑它旨在与 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++ 文件中给出的示例，但我无法弄清楚它在混合整数算术和布尔值时是如何工作的。

假设你是 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<100(;

此处如果x大于 10 x>10结果true .同样，如果x小于 100 x<100结果true .如果两者都true，则右侧结果为 true，这将分配给y 。 ||表示或。

相关文章：