Can Z3 call python function during decision making of variables?

Question

I am trying to solve a problem, for example I have a 4 point and each two point has a cost between them. Now I want to find a sequence of nodes which total cost would be less than a bound. I have written a code but it seems not working. The main problem is I have define a python function and trying to call it with in a constraint.

Here is my code: I have a function def getVal(n1,n2): where n1, n2 are Int Sort. The line Nodes = [ Int("n_%s" % (i)) for i in range(totalNodeNumber) ] defines 4 points as Int sort and when I am adding a constraint s.add(getVal(Nodes[0], Nodes[1]) + getVal(Nodes[1], Nodes[2]) < 100) then it calls getVal function immediately. But I want that, when Z3 will decide a value for Nodes[0], Nodes[1], Nodes[2], Nodes[3] then the function should be called for getting the cost between to points.

from z3 import *
import random

totalNodeNumber = 4
Nodes = [ Int("n_%s" % (i)) for i in range(totalNodeNumber) ]
def getVal(n1,n2):
    # I need n1 and n2 values those assigned by Z3
    cost = random.randint(1,20)
    print cost
    return IntVal(cost)

s = Solver()

#constraint: Each Nodes value should be distinct
nodes_index_distinct_constraint  = Distinct(Nodes)
s.add(nodes_index_distinct_constraint)

#constraint: Each Nodes value should be between 0 and totalNodeNumber
def get_node_index_value_constraint(i):
    return And(Nodes[i] >= 0, Nodes[i] < totalNodeNumber)
nodes_index_constraint  = [ get_node_index_value_constraint(i) for i in range(totalNodeNumber)]
s.add(nodes_index_constraint)

#constraint: Problem with this constraint
# Here is the problem it's just called python getVal function twice without assiging Nodes[0],Nodes[1],Nodes[2] values
# But I want to implement that - Z3 will call python function during his decission making of variables
s.add(getVal(Nodes[0], Nodes[1]) + getVal(Nodes[1], Nodes[2]) + getVal(Nodes[2], Nodes[3]) < 100)

if s.check() == sat:
    print "SAT"
    print "Model: "
    m = s.model()
    nodeIndex = [ m.evaluate(Nodes[i]) for i in range(totalNodeNumber) ]
    print nodeIndex
else:
    print "UNSAT"
    print "No solution found !!"

If this is not a right way to solve the problem then could you please tell me what would be other alternative way to solve it. Can I encode this kind of problem to find optimal sequence of way points using Z3 solver?

Nikolaj Bjorner Nikolaj Bjorner · Accepted Answer · 2013-08-01T20:00:58

I don't understand what problem you need to solve. Definitely, the way getVal is formulated does not make sense. It does not use the arguments n1, n2. If you want to examine values produced by a model, then you do this after Z3 returns from a call to check().

Can Z3 call python function during decision making of variables?

2 Answers