Search code examples
optimizationz3z3py

Z3 ArithRef type: is there a way to show value once model evaluated?

Using Z3Py, once a model has been checked for an optimization problem, is there a way to convert ArithRef expressions into values?

Such as

y = If(x > 5, 0, 0.5 * x)

Once values have been found for x, can I get the evaluated value for y, without having to calculate again based on the given values for x?

Many thanks.

Solution

  • You need to evaluate, but it can be done by the model for you automatically:

    from z3 import *

x = Real('x')
y = If(x > 5, 0, 0.5 * x)

s = Solver()

r = s.check()

if r == sat:
    m = s.model();
    print("x =", m.eval(x, model_completion=True))
    print("y =", m.eval(y, model_completion=True))
else:
    print("Solver said:", r)

    This prints:

    x = 0
y = 0

    Note that we used the parameter model_completion=True since there are no constraints to force x (and consequently y) to any value in this model. If you have sufficient constraints added, you wouldn't need that parameter. (Of course, having it does not hurt.)