% http://www.cs.kuleuven.be/~dtai/events/ASP-competition/Benchmarks/ChannelRouting.shtml
% From B-Prolog's example suite.

solve(As):-
    extract_inputs(As,L,T,Nets),
    post_domain_constrs(Nets,L,T),
    not_overlap(Nets),
    extract_level_vars(Nets,Levels),
    labeling(Levels),!,
    sort(Nets,OrderedNets),
    extract_global_tracks(OrderedNets,Vars),
    labeling([ff],Vars),!,
    output(Nets).
solve(_):-
    format("UNSATISFIABLE~n").

extract_inputs([],_L,_T,Nets):-closetail(Nets).
extract_inputs([layers(L)|As],L1,T,Nets):-!,L1=L,
    extract_inputs(As,L,T,Nets).
extract_inputs([tracks(T)|As],L,T1,Nets):-!,T1=T,    
    extract_inputs(As,L,T,Nets).
extract_inputs([connect(Id,TB,TermNo)|As],L,T,Nets):-
    Term=term(TB,TermNo),
    Net=net(_Level,Id,_Layer,_Track,_GlobTrack,Terms),
    member(Net,Nets),
    member(Term,Terms),!,
    extract_inputs(As,L,T,Nets).

post_domain_constrs([],_L,_T).
post_domain_constrs([net(_Level,_Id,Layer,Track,GlobalTrack,Terms)|Nets],L,T):-
    Layer :: 1..L,
    Track :: 1..T,
    Max is L*T-1,
    GlobalTrack :: 0..Max,
    Layer #= GlobalTrack // T +1,
    Track #= GlobalTrack mod T + 1,
    closetail(Terms),
    post_domain_constrs(Nets,L,T).

not_overlap([_]):-!.
not_overlap([Net|Nets]):-
    Net=net(Level,_Id,_Layer,_Track,_GlobTrack,Terms),
    Level #>0, 
    (member(term(top,_),Terms)->true;Level #> 100),  
            % assign a large level to it if it connects to only bottom terminals
    not_overlap(Net,Nets),
    not_overlap(Nets).

not_overlap(_,[]).
not_overlap(Net1,[Net2|Nets]):-
    not_overlap_horizontally(Net1,Net2),
    not_overlap_vertically(Net1,Net2),    
    not_overlap(Net1,Nets).
    
not_overlap_horizontally(net(_,_,Layer1,Track1,GlobTrack1,Terms1),net(_,_,Layer2,Track2,GlobTrack2,Terms2)):-
    terminals_intersect(Terms1,Terms2),!,
    Layer1#=Layer2 #=> Track1#\=Track2,
    GlobTrack1 #\= GlobTrack2.
not_overlap_horizontally(_,_).

not_overlap_vertically(net(Level1,_,Layer1,Track1,GlobTrack1,Terms1),net(Level2,_,Layer2,Track2,GlobTrack2,Terms2)):-
    terminals_above(Terms1,Terms2),!,
    Level1 #< Level2,   % used as heuristics in labeling
    Layer1#=Layer2 #=> Track1#<Track2,
    Layer1 #=< Layer2 #=> GlobTrack1 #<GlobTrack2.
not_overlap_vertically(net(Level1,_,Layer1,Track1,GlobTrack1,Terms1),net(Level2,_,Layer2,Track2,GlobTrack2,Terms2)):-
    terminals_above(Terms2,Terms1),!,
    Level2 #< Level1,   % used as heuristics in labeling
    Layer1#=Layer2 #=> Track2#<Track1,
    Layer2 #=< Layer1 #=> GlobTrack2 #<GlobTrack1.
not_overlap_vertically(_,_).

nets_above(net(_,_,_,_,_,Terms1),net(_,_,_,_,_,Terms2)):-
    terminals_above(Terms1,Terms2),!.

terminals_intersect(Terms1,Terms2):-
    member(term(_,S1),Terms1),
    member(term(_,E1),Terms1),
    S1<E1,
    member(term(_,T),Terms2),
    T>=S1,T=<E1,!.
terminals_intersect(Terms1,Terms2):-
    member(term(_,S2),Terms2),
    member(term(_,E2),Terms2),
    S2<E2,
    member(term(_,T),Terms1),
    T>=S2,T=<E2,!.

terminals_above(Terms1,Terms2):-
    member(term(top,T),Terms1),
    member(term(bot,T),Terms2),!.

extract_level_vars([],[]).
extract_level_vars([net(Level,_,_,_,_,_)|Nets],[Level|Vars]):-
    extract_level_vars(Nets,Vars).

extract_global_tracks([],[]).
extract_global_tracks([net(_,_,_,_,GlobalTrack,_)|Nets],[GlobalTrack|Vars]):-
    extract_global_tracks(Nets,Vars).

output([]).
output([net(_,Id,Layer,Track,_,_)|Nets]):-
    write(pos(Id,Layer,Track)),write('. '),
    output(Nets).

test:-
    solve([layers(1), tracks(7), 
	   connect(n1,top,1), connect(n1,top,2),
	   connect(n2,bot,1), connect(n2,bot,3), connect(n2,top,4),
	   connect(n3,bot,2), connect(n3,top,5), connect(n3,top,7),
	   connect(n4,top,3), connect(n4,top,6), connect(n4,bot,7),
	   connect(n5,bot,5), connect(n5,top,9), connect(n5,top,11),
	   connect(n6,bot,6), connect(n6,top,8), connect(n6,bot,9),
	   connect(n7,bot,8), connect(n7,bot,12),
	   connect(n8,top,10), connect(n8,bot,11),
	   connect(n9,bot,10), connect(n9,top,12)]).