Z3,C++ API, How to convert bool sort to int sort

I am using Z3 in C++, and I have some bool-sort exprs.

What I want to do is to count the number of true-value exprs.

A very simple way is to convert those expr into int-sort and then add them up.

However I don't know how to convert bool to int.

Thanks!

SOLUTION:

As the cpp example file shows(function 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);

Solution

Pseudo-boolean functions

For counting booleans, and asserting how many are true etc. (mutex like conditions), pseudo-boolean functions are your friends:

https://github.com/Z3Prover/z3/blob/master/src/api/c%2B%2B/z3%2B%2B.h#L949-L953

These functions allow you to assert constraints that let you create cardinality conditions, which is what I suspect you are trying to do in the first place. These functions generate much better code for z3 to solve, compared to any other indirect encoding. Here's a discussion on it, based on the python interface: K-out-of-N constraint in Z3Py

Direct counting

You can also do a direct count of course, but you should prefer the above functions if they suit your need. If you really do want to get an integer, you'll have to use:

int_val: create a number expression
ite: if-then-else
sum: create a sum

Essentially creating the expression (pseudo-code):

 z = int_val(0);
 o = int_val(1);
 sum(ite(b1, o, z), ite(b2, o, z), ...)

But you should really stick to pseudo-booleans if at all possible.