What is output format of get_answer() method in z3 Fixed point API?

[duttasridhar]

Let us take the following example where it tries to find path between 2 vertices.

fp = Fixedpoint()
fp.set(engine='datalog')
fp.set('datalog.generate_explanations', True)
s = BitVecSort(3)
edge = Function('edge', s, s, BoolSort())
path = Function('path', s, s, BoolSort())
a,b,c = Consts('a b c',s)
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)])
v1 = BitVecVal(1,s)
v2 = BitVecVal(2,s)
v4 = BitVecVal(4,s)
fp.fact(edge(v1,v2))
fp.fact(edge(v2,v4))
print(fp.query(path(v1,v4)))
fp.get_answer()

The output it gives is

sat
ν0 = : query!109() :- path(#b001,#b100).(: path(#2,#0) :- path(#1,#0), edge(#2,#1).(: path(#1,#0) :- edge(#1,#0).(: edge(#b010,#b100).), : edge(#b001,#b010).))

What is the format of the output provided by the get_answer() above?

My requirement is to convert the above format into the actual path which is v1 --> v2 --> v4?

Thanks for the help!