CODEWITHSUNDEEP
pythonz3linear-programmingz3py
dec
dec

Reputation: 11

Forall quantification over free variables of z3 optimizer

I'm trying to construct and solve a linear program using the Z3 SMT solver with the following form:

maximize x_1 + .. + x_n subject to:
    0 <= x_i <= 1 (for i in 1..n)
    a_1*x_1+..+a_n*x_n + b_1*z_1+..+b_m*z_m + c >= 0 (or in short g(X,Z) >= 0)

I'm using the z3py python library to do so but as I solve the linear program I get a model which has a valuation for every variable of the model, but instead I'd like to have the constraint of non-negativity (g(X,Z) >=0) to hold over all possible Z and have a valuation of the rest of the free variables, is there a way to achieve this with the z3-solver library?

The following is a relevant snippet of the code that I've used to create the optimizer:

...
lp = Optimize()
for i in range(n):
    lp.add(0 <= x_i)
    lp.add(x_i <= 1)
lp.add(a_1*x_1+..+a_n*x_n + b_1*z_1+..+b_m*z_m + c >= 0)
lp.maximize(x_1 + .. + x_n)
...

where every symbol is an ArithRef created with the Real function.

Upvotes: 0

Views: 56

Answers (0)

Related Questions