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

Question

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);

Answer 1

#include <iostream>
using namespace std;

int main() {
    int a = 6;
    a += (int)true;
    cout << a << "\n";
}

Answer 2

It's been a long time I used Z3, but I think you should be able to define a function that will effectively project true=>1 and false=>0 (or the other way).

Assuming that you are doing it the script it would look similar to

(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))

Then, if you construct an expression using that function, it will do the conversion, and will also report any problems like i.e. getting non-bool argument.

Answer 3

There are built-in functions in Z3 for counting "k amongst N" and other variants.

They should usually be preferred as they offer better performance due to dedicated strategies.

((_ at-most k) x y z)

this means at most k of the Booleans x, y, z... are true.

See this other question for more details, and the comment by Nikolaj Bjorner on the answer for the SMT syntax of the variants.

K-out-of-N constraint in Z3Py