Calculate boolean sum

[ptr1120]

Hello,

I am having boolean variables and need to calculate the sum of them in a term, but I receive an ARITHTERM_REQUIRED error:

term_t terms[3];

type_t bool_type = yices_bool_type();
terms[0] = new_var(bool_type, "x");
terms[1] = new_var(bool_type, "y");
terms[2] = new_var(bool_type, "z");

term_t bool_sum = yices_sum(3, terms);
error_code_t e = yices_error_code(); // ARITHTERM_REQUIRED

term_t cardinality_term = yices_and2(yices_arith_gt_atom(bool_sum, yices_int32(0)), yices_arith_lt_atom(bool_sum, yices_int32(2)));

Is there any idea or workaround for archiving this?

Best regards Peter

[BrunoDutertre]

You have to convert your Booleans to integers ( false->0 and true->1), which can be done with if-then-else.

[ptr1120]

Thank you. I have several constraints (omitted in the above example) with boolean operators (and, or, implies,...) among these variables, which I think would create a new problem when using integers in boolean terms. Also having the case were much more than these 3 boolean variables need to be summed up, so creating all combinations for the cardinality term is also not an option.

[BrunoDutertre]

If you want to keep everything purely Boolean then you can't use yices_sum.

But if you're willing to use yices_sum, there's no combinatorial blow up. Here's the pattern:

    zero = yices_zero();
    one = yices_int32(1);
    for (i=0; i<n; i++) {
      aux[i] = yices_ite(term[i], one, zero);
    }
    term_t bool_sum = yices_sum(n, aux);

[ptr1120]

Thank you. Lastly I need to restrict this sum of booleans in order to restrict it to be in a certain range (see cardinality term), this is what I meant with the combinatorial approach. And yes I need boolean variables due to the fact that these variables are used in several other boolean constraints. Would it be complicated for me to provide a PR for a seperate sum operation with boolean support or is there a bigger technical restriction why this ist not allowed in the current sum operation?

[BrunoDutertre]

The code above just shows you how to build a "sum of Booleans" without changing anything to the Yices API. I'm not sure what's the problem with this. You can still assert constraints on the bool_sum term, and you can still use the Boolean variables term[I] in any other constraint that you have.

This said, there are ways of encoding cardinality constraints on a set of Boolean variables without converting to integers. Check these papers for example (there are many more on this topic).

https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.83.9527&rep=rep1&type=pdf

https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.458.7676&rep=rep1&type=pdf

[ptr1120]

Ok, now I understood that my boolean variables are used in your example (I thought I have to convert my boolean completely into integer). This way it works, thank you.