CODEWITHSUNDEEP
pythonz3smtz3py
aybb_2000
aybb_2000

Reputation: 29

How can I use value from the list as an index in z3 python SMT solver

.

this is the math formulation that I'm trying to recreate in Z3 SMT solver with python. My problem accrues on f_x_i

x = [Int(f"x{i}") for i in range(n)]
for i in range(0, n):
constraints.append(And(x[i] >= 0, x[i] <= m))

constraints.append(f_values[x[i]] >= e_values[i])

this the code that I'm trying to run and this is the error that I get:

onstraints.append(f_values[x[i]] >= e_values[i])
                   ~~~~~~~~^^^^^^
TypeError: list indices must be integers or slices, not ArithRef

How can I get the value of x[i] and use it as an index?

Upvotes: 0

Views: 26

Answers (0)

Related Questions