Finding path between two nodes

Question

I was wondering if there is a way to build a topology in z3py, if I am given with 6 nodes namely: n1, n2, n3, n4, n5, n6 and they have certain links among them e.g. l12 (which implies there is a link between node n1 and n2), l16, l23, l25, l34,l35, l36. I can define l_{i}{j} as a bool variable so that it may refer whether there exists any link between 2 nodes or node (for sure I will have to define all possible links in this way). The question is how to define the notion of a path in Z3py, so that I can figure out if there exists any path between 2 nodes or not (SAT or UNSAT if SAT which path?). I tried looking for z3py tutorial but it isnt available online anymore, I am new to z3 so kindly bear with me. I could only figure out the following modeling in python which is very naive. Is it possible to model a path as an uninterpreted function in z3py?

graph = {'n1': ['n2', 'n6'],
         'n2': ['n3', 'n5'],
         'n3': ['n4', 'n5','n6'],
         'n4': ['n3'],
         'n5': ['n2', 'n3'],
         'n6': ['n3','n1']}
def path_finder (graph, start, end, path=[]):
    path = path + [start]
    if start == end:
        return path
    if not graph.has_key(start):
        return None
    for node in graph[start]:
        if node not in path:
            newpath = path_finder (graph, node, end, path)
            if newpath: return newpath
    return None

print path_finder (graph, 'n1','n4')

Answer 1

I modified a Fixpoint example to accomplish path search

from z3 import *

#  cf. https://ericpony.github.io/z3py-tutorial/fixpoint-examples.htm

fp = Fixedpoint()
fp.set(engine='datalog')

#  3 bits are sufficient to model our 6 nodes
s = BitVecSort(3)
edge = Function('edge', s, s, BoolSort())
path = Function('path', s, s, BoolSort())
a = Const('a', s)
b = Const('b', s)
c = Const('c', s)

#  the rules:
#  a path can be a single edge or
#  a combination of a path and an edge
fp.register_relation(path,edge)
fp.declare_var(a, b, c)
fp.rule(path(a, b), edge(a, b))
fp.rule(path(a, c), [edge(a, b), path(b, c)])

n1 = BitVecVal(1, s)
n2 = BitVecVal(2, s)
n3 = BitVecVal(3, s)
n4 = BitVecVal(4, s)
n5 = BitVecVal(5, s)
n6 = BitVecVal(6, s)
n7 = BitVecVal(7, s)

graph = {n1: [n2, n6, n7],
         n2: [n3, n5],
         n3: [n4, n5, n6],
         n4: [n3],
         n5: [n2, n3],
         n6: [n3, n1]}

#  establish facts by enumerating the graph dictionary
for i, (source, nodes) in enumerate(graph.items()):
    for destination in nodes:
        fp.fact(edge(source, destination))

print("current set of rules:\n", fp)

print(fp.query(path(n1, n4)), "yes, we can reach n4 from n1\n")

print(fp.query(path(n7, n1)), "no, we cannot reach n1 from n7\n")