我在 C++ 中使用 Z3，并且我有一些布尔排序表达式。
我要做的是统计真值表达式的数量。
一个非常简单的方法是将这些 expr 转换为 int-sort 然后将它们相加。
但是我不知道如何将 bool 转换为 int。
谢谢！
解决方案：
如 cpp 示例文件所示（函数 ite_example2()）：
expr b = c.bool_const("x");
expr x = c.int_val(1);
expr y = c.int_val(0);
expr conj = ite(b,x,y);
【问题讨论】：
标签： z3
对于计算布尔值和断言有多少是真的等等（类似互斥的条件），伪布尔函数是你的朋友：
https://github.com/Z3Prover/z3/blob/master/src/api/c%2B%2B/z3%2B%2B.h#L949-L953
这些函数允许您断言允许您创建基数条件的约束，这是我怀疑您首先尝试做的事情。与任何其他间接编码相比，这些函数为 z3 生成了更好的代码来解决。下面是关于它的讨论，基于python接口：K-out-of-N constraint in Z3Py
当然，您也可以直接计数，但如果它们适合您的需要，您应该更喜欢上述功能。如果你真的想得到一个整数，你必须使用：
本质上是创建表达式（伪代码）：
z = int_val(0);
o = int_val(1);
sum(ite(b1, o, z), ite(b2, o, z), ...)
但如果可能的话，你真的应该坚持使用伪布尔值。
【讨论】：
我使用 Z3 已经很长时间了，但我认为您应该能够定义一个有效地投影 true=>1 和 false=>0（或其他方式）的函数。
假设您正在执行 脚本，它看起来类似于
(declare-fun boolToIntDirect (Bool) Int)
(assert (= (boolToIntDirect false) 0))
(assert (= (boolToIntDirect true) 1))
(declare-fun boolToIntNegated (Bool) Int)
(assert (= (boolToIntNegated false) 1))
(assert (= (boolToIntNegated true) 0))
然后，如果您使用该函数构造一个表达式，它将进行转换，并且还会报告任何问题，例如获取非 bool 参数。
【讨论】：
#include <iostream>
using namespace std;
int main() {
int a = 6;
a += (int)true;
cout << a << "\n";
}
【讨论】：
a += (int)true; c 风格的演员表不是一个好主意和干净的方法。