Generate SMT define-fun from graph edges list

gen_edges_fun_smt.py

# the main function
def get_edges_as_smt(function_name:str, a1:str, a2:str, node_type:str, graph):
    or_components = []
    for s, d_list in graph.items():
        for d in d_list:
            or_components.append('(and (= {a1} {s}) (= {a2} {d}))'.format(a1=a1,a2=a2,s=node_type+str(s),d=node_type+str(d)))
    or_smt = '(or %s)' % (' '.join(or_components))
    return '(define-fun {function_name} (({a1} {node_type}) ({a2} {node_type})) Bool {body})'.format(
            a1=a1, a2=a2, node_type=node_type, function_name=function_name, body=or_smt)


graph = { 0: [1, 4],
          1: [0, 2],
          2: [1, 3],
          3: [4, 2],
          4: [0, 3] }


# for convenience printing the dot graph
print("digraph module {")
for src, dst_list in graph.items():
    for dst in dst_list:
        print("{src} -> {dst}".format_map(locals()))
print("}")


get_edges_as_smt('is_edge', 's', 'd', 'V', graph)