Dependency graphs and topological sorting using Z3 SMT-solver

Topological sorting is an operation many programmers well familiar with: this is what "make" tool
do when it find an order of items to process.
Items not dependent of anything can be processed first.
The most dependent items at the end.

Dependency graph is a graph and topological sorting is such a "contortion" of the graph,
when you can see an order of items.

For example, let's create a sample graph in Wolfram Mathematica:

Each arrow shows that an item is needed by an item arrow pointing to, i.e., if "a -> b", then item "a" must be first
processed, because "b" needs it, or "b" depends on "a".

How would tsort sort the graph? I'm making the text file with input data:

7 1
7 0
5 1
3 0
3 4
1 2
1 6
1 4
0 6

And run tsort:

% tsort tst
3
5
7
0
1
4
6
2

Now I'll use Z3 SMT-solver for topological sort, which is overkill, but quite spectacular: all we need to do
is to add constraint for each edge (or "connection") in graph, if "a -> b", then "a" must be less then "b", where
each variable reflects ordering.

#!/usr/bin/env python
from z3 import*
TOTAL=8
order=[Int('%d'% i)for i inrange(TOTAL)]
s=Solver()
s.add(Distinct(order))for i inrange(TOTAL):
s.add(And(order[i]>=0, order[i]<TOTAL))
s.add(order[5]<order[1])
s.add(order[3]<order[4])
s.add(order[3]<order[0])
s.add(order[7]<order[0])
s.add(order[7]<order[1])
s.add(order[1]<order[2])
s.add(order[1]<order[4])
s.add(order[1]<order[6])
s.add(order[0]<order[6])print s.check()
m=s.model()
order_to_print=[None]*(TOTAL)for i inrange(TOTAL):
order_to_print[m[order[i]].as_long()]=i
print order_to_print