0

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);
Toby Mao
  • 105
  • 1
  • 1
  • 10
  • 1
    Welcome to Stack Overflow. Please take the time to read [The Tour](http://stackoverflow.com/tour) and refer to the material from the [Help Center](http://stackoverflow.com/help/asking) what and how you can ask here. – πάντα ῥεῖ May 28 '17 at 13:35
  • Hm.. I just noted you used "C++ API" in the title. Are you doing the trying to convert and sum it up in C++ or in the script? – quetzalcoatl May 28 '17 at 13:49

4 Answers4

2

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.

alias
  • 28,120
  • 2
  • 23
  • 40
0
#include <iostream>
using namespace std;

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

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.

quetzalcoatl
  • 32,194
  • 8
  • 68
  • 107
  • @TobyMao: nope, I wrote it from memory. but it should be pretty straightforward if you configure the rules by C++ API (check how to define uninterpreted functions - see **Levent**'s answer), or should be totally not needed if you configure the rules by script text - just add it into the script.. – quetzalcoatl May 28 '17 at 21:56
0

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

Yann TM
  • 1,942
  • 13
  • 22