How to get all the output of the expression, only true, or only false, or both true and false?

[Flians]

Hi.

For a expression: f(X), X is the set of {true, false}. Each output of the expression is true or false. How to get all the output of the expression, only true, or only false, or both true and false?

Thank you.

[aytey]

The SMT solver is going to give you one satisfying assignment (== model) for your formula. This will included a concrete value for x (e.g., either true or false), depending on the choice the SMT solver makes internally.

If you're interested in knowing if the value can be true, false or both, then you will need to add additional assertions to the SMT solver to find this out.

For example: (assert x) (for the true case) and (assert (not x)) (for the false case). You should do this inside of push/pop, such that you can remove the true case to find the false case (and vice versa).

If you get sat for both true and false, then you will know that it is possible to get true and false for both. However, understand that you're going to get a potentially different model for the other parts of the formula, if you assert true/false on x.

I think the short answer is: SMT solvers do not support a "don't care" kind of value automatically. You need to interact with the solver via new assertions to find out if the term is a "don't care".

[Flians]

Thank you. I must use twice check() to determine the value of the output.