CODEWITHSUNDEEP
z3c-api
user3131978
user3131978

Reputation: 37

In Z3: how if then else based conditions be formulated (based on evaluations of variables)?

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?

Upvotes: 0

Views: 870

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

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.

Upvotes: 2

Related Questions