How can I make a predefined Python function work with Z3py?

Question

As a beginner in Z3, I am wondering if there is a way to make Z3Py work with a predefined Python function. Following is a small example which explains my question.

from z3 import *

def f(x):
    if x > 0:
        print " > 0"
        return 1
    else:
        print " <= 0"
        return 0

a=Int('a')
s=Solver()
s.insert(f(a) == 0)

t = s.check()
print t
print a
m = s.model()
print m

f(x) is a function defined in python. When x <= 0, f(x) returns 0. I add a constraint s.insert(f(a) == 0) and hope that Z3 can find a appropriate value for variable "a" (e.g. -3). But these codes are not working correctly. How should I change it?

(Please note that I need f(x) defined outside Z3, and then is called by Z3. )

What I am trying to do is calling a predefined function provided by a graph library without translating it to Z3. I am using the NetworkX library, and some codes are given as following:

import networkx as nx

G1=nx.Graph()
G1.add_edge(0,1)

G2=nx.Graph()
G2.add_edge(0,1)
G2.add_edge(1,2)

print(nx.is_isomorphic(G1, G2))
#False

I need Z3 to help me find a vertex in G2 such that after removing this vertex, G2 is isomorphic to G1. e.g.

G2.remove_node(0)
print(nx.is_isomorphic(G1, G2))
#True

Answer 1

I think this will be tough if f is a general function (e.g., what if it's recursive?), although if you assume it has some structure (e.g., if then else), you might be able to write a simple translator. The issue is that Z3's functions are mathematical in nature and not directly equivalent to Python functions (see http://en.wikipedia.org/wiki/Uninterpreted_function ). If possible for your purpose, I would propose to go the opposite direction: define your function f in terms of Z3 constructs, then evaluate it within your program (e.g., using this method: Z3/Python getting python values from model ). If that won't work for you, please include some additional details on how you need to use the function. Here's a minimal example (rise4fun link: http://rise4fun.com/Z3Py/pslw ):

def f(x):
    return If(x > 0, 1, 0)

a=Int('a')
s=Solver()
P = (f(a) == 0)
s.add(P)

t = s.check()
print t
print a
m = s.model()
print m

res = simplify(f(m[a])) # evaluate f at the assignment to a found by Z3

print "is_int_value(res):", is_int_value(res)

print res.as_long() == 0 # Python 0

print f(1)
print simplify(f(1)) # Z3 value of 1, need to convert as above