All possible values for a record datatype in Z3?

Question

I am trying to define a record datatype in z3 consisting of six elements of different types. This is how I did it: (declare-datatypes () ((S (mk-pair (p1 (P1type)) (p2 (P2type)) (p3 (P3type)) (m1 (bool)) (m2 (bool)) (m3 (bool)) )))) But when I use (forall (x1 S)), the solver does not seem to consider all possible combinations of valuations for my datatype. I appreciate if you let me know if I am doing something wrong, or I should not expect z3 to consider all combinations of valuations for S. Thanks a lot, Fathiyeh

Answer 1

Here is a permalink to your example: http://rise4fun.com/Z3/0sl11

The model produces interpretations for the functions LS and thau. Both of these functions map values from S into Booleans. So they are predicates. The model says what are possible values for these predicates that satisfy the formulas. It does not have to formulate the predicates by listing each case explicitly. These predicates are typically written as a big if-then-else expression. The last else branch contains the default case for the values that are not explicitly handled in the if-branches.