/* 
 * Inequality constraint solver in CHR(chr)
 * Author: Seiji OGAWA, 2011-03-31
 * 
 * Examples are taken from:
 *   http://dtai.cs.kuleuven.be/CHR/examples.shtml
 *
 * If you'd like to change parameter N, 
 * please change the 1st argument of query: start("N").
 *
 */

:- use_module(library(chr)).
:- chr_option(optimize, full).
:- chr_constraint leq(-, -), list/1, l/2, start/1, s/2, s/3, time/1.
%:- chr_trace.

reflexivity  @ leq(X,X) <=> true.
antisymmetry @ leq(X,Y), leq(Y,X) <=> X = Y.
idempotence  @ leq(X,Y) \ leq(X,Y) <=> true.
transitivity @ leq(X,Y), leq(Y,Z) ==> leq(X,Z).

start(N) <=>
  cputime(X),
  s(N, 0),
  list([]),
  cputime(Y),
  Z is Y - X,
  time(Z).

s(M, I), list(H) <=> M > I | I1 is I+1, s(M,I1), list([X|H]).
s(M,M),  list([X|R]) <=> l(X, [X|R]).
l(H, [X,Y|R]) <=> l(H, [Y|R]), leq(X, Y).
l(H, [R]) <=> leq(R, H).