I'm new to Z3 and still couldn't find how I can express conditional new assignments based on the different possible evaluations. In If-then-else example in https://github.com/Z3Prover/z3/blob/master/examples/c/test_capi.c#L1846 I still need to make the assignment to true or false, and when I want to make it true or false based on possible evaluations of another variable. How can I do this?
In the evaluation example I want the value calculated to be used to affect the still not evaluated values that are going to be checked by assertion later. So if this is the way how I can return back the model UN-evaluated with the new (evaluation based) conditions to the context again? i.e. I want to do composite conditions without final evaluations. Is that possible?
The following line from ite_example():
ite = Z3_mk_ite(ctx, f, one, zero)
creates an expression that will evaluate to whatever the (symbolic) term one evaluates to, if f evaluates to true, or alternatively to whatever zero evaluates to, if f evalautes to false. In ite_example, f always evaluates to false, but it may be any other (symbolic) term of Boolean sort.
For example,
x = mk_int_var(ctx, "x");
y = mk_int_var(ctx, "y");
x_eq_y = Z3_mk_eq(ctx, x, y);
will create a term called x_eq_y, representing "x = y", which is of Boolean sort.