[Python] Automatic python function writing using z3 constraints

I'm working on a project involving IP solving on using some matrice M. I am using the z3 solver in Python.

Sometime I need to check if a given input was valid according to M; hence no "solving" was required. I used to call z3 anyway and try if solver.check() was True or False.

def check_input_validity(input):
X = [Int("x%s" %(i)) for i in range(Nt-12)]

#an example of the constraints I used:
const1 = [(sum(layer3_m)-2)*(1-X) <= sum([layer3_m[j]*X[j] for j in range(Nt)]) for i in range(Nt)]

input_constraint = [X == int(input) for i in range(len(input))]

s = z3.Solver()
s.add(const1+input_constraint)
return s.check()


As M was always the same, I tried to hardcode the constraint of the IP in a single function taking only the input of the problem. So I just wrote a simple function:

def write_constraint():
X = [Int("x%s" %(i)) for i in range(Nt-12)]
const1 = [(sum(layer3_m)-2)*(1-X) <= sum([layer3_m[j]*X[j] for j in range(Nt)]) for i in range(Nt)]

output = ''
for clause in const1:
output+='('+clause+') and '

print output


Then I copied the output from the shell and pasted it in a function that now look like this:

def input_validity(k):
offset = 12
k = [int(x) for x in k]
return ( 2*(1 - k[12-offset]) <=0 +k[13-offset] +k[15-offset] +k[28-offset] +k[31-offset] ) and ( 2*(1 - k[13-offset]) <=0 (...)


which runs incredibly faster as the implementation of and in python is lazy so it stops evaluating when one clause is False (at least it's what I was taught, is it correct?)

Now I would like to use the same strategy for solving this same problem on some different M. I could do it by hand again, but it feels wrong.

Question: I feel it should be possible to write this exact function (input validity) automatically using the knowledge of M only. How can I do it?

Continue reading...