package examples.dijkstra;

import runtime.primitive.LogicalInt;
import util.arithmetics.primitives.intUtil;

public handler dijkstra {
	solver FibHeapHandler;

	public constraint edge(int,int,int), dijkstra(int);
	private constraint scan(int,int), relabel(int,int);
	local constraint distance(int,int);

	rules {
		local LogicalInt QN, QW;

		start_scanning @ dijkstra(A) <=> scan(A,0).

		stop_scanning @ scan(0,A) <=> true.
		label_neighb  @ 
			scan(N,L), edge(N,N2,W) ==> relabel(N2, intUtil.add(L,W)).
		scan_next @ 
			scan(N,L) <=> distance(N,L), extract_min(QN,QW), scan(QN,QW).

		scanned 	@ distance(N,_) \ relabel(N,_) <=> true.
		not_scanned	@ relabel(N,L) <=> decr_or_ins(N,L).
    }
}