1/*  Part of SWI-Prolog
    2
    3    Author:        Tom Schrijvers
    4    E-mail:        tom.schrijvers@cs.kuleuven.ac.be
    5    WWW:           http://www.swi-prolog.org
    6    Copyright (c)  2004-2013, K.U.Leuven
    7    All rights reserved.
    8
    9    Redistribution and use in source and binary forms, with or without
   10    modification, are permitted provided that the following conditions
   11    are met:
   12
   13    1. Redistributions of source code must retain the above copyright
   14       notice, this list of conditions and the following disclaimer.
   15
   16    2. Redistributions in binary form must reproduce the above copyright
   17       notice, this list of conditions and the following disclaimer in
   18       the documentation and/or other materials provided with the
   19       distribution.
   20
   21    THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
   22    "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
   23    LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
   24    FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
   25    COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
   26    INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
   27    BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
   28    LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
   29    CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
   30    LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
   31    ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
   32    POSSIBILITY OF SUCH DAMAGE.
   33*/
   34
   35%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   36%
   37% Simple integer solver that keeps track of upper and lower bounds
   38%
   39% Author:	Tom Schrijvers
   40% E-mail:	tom.schrijvers@cs.kuleuven.ac.be
   41% Copyright:	2004, K.U.Leuven
   42%
   43%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   44%
   45% Todo:
   46%	- reduce redundant propagation work
   47%	- other labelling functions
   48%	- abs, mod, ...
   49%
   50%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   51
   52:- module(bounds,
   53	[
   54		op(760,yfx,(#<=>)),
   55		op(750,xfy,(#=>)),
   56		op(750,yfx,(#<=)),
   57		op(740,yfx,(#\/)),
   58		op(730,yfx,(#\)),
   59		op(720,yfx,(#/\)),
   60		op(710, fy,(#\)),
   61		op(700,xfx,(#>)),
   62		op(700,xfx,(#<)),
   63		op(700,xfx,(#>=)),
   64		op(700,xfx,(#=<)),
   65		op(700,xfx,(#=)),
   66		op(700,xfx,(#\=)),
   67		op(700,xfx,(in)),
   68		op(550,xfx,(..)),
   69		(#>)/2,
   70		(#<)/2,
   71		(#>=)/2,
   72		(#=<)/2,
   73		(#=)/2,
   74		(#\=)/2,
   75		(#<=>)/2,
   76		(#=>)/2,
   77		(#<=)/2,
   78		(#/\)/2,
   79		(#\/)/2,
   80		(#\)/2,
   81		(#\)/1,
   82		(in)/2,
   83		label/1,
   84		labeling/2,
   85		all_different/1,
   86		sum/3,
   87		lex_chain/1,
   88		indomain/1,
   89		check/1,
   90		tuples_in/2,
   91		serialized/2
   92	]).   93
   94:- use_module(library('clp/clp_events')).   95
   96/** <module> Simple integer solver that keeps track of upper and lower bounds
   97
   98@deprecated	No longer maintained.  Please use clpfd.pl
   99@author		Tom Schrijvers
  100*/
  101
  102%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  103% exported predicates
  104X #>= Y :-
  105	parse_expression(X,RX),
  106	parse_expression(Y,RY),
  107	geq(RX,RY,yes).
  108X #=< Y :-
  109	parse_expression(X,RX),
  110	parse_expression(Y,RY),
  111	leq(RX,RY,yes).
  112X #= Y :-
  113	parse_expression(X,RX),
  114	parse_expression(Y,RX).
  115X #\= Y :-
  116	parse_expression(X,RX),
  117	parse_expression(Y,RY),
  118	neq(RX,RY,yes).
  119X #> Y :-
  120	Z #= Y + 1,
  121	X #>= Z.
  122X #< Y :-
  123	Y #> X.
  124X in L .. U :-
  125	( is_list(X) ->
  126		domains(X,L,U)
  127	;
  128		domain(X,L,U)
  129	).
  130
  131L #<=> R :-
  132	reify(L,B),
  133	reify(R,B).
  134L #=> R :-
  135	reify(L,BL),
  136	reify(R,BR),
  137	myimpl(BL,BR).
  138R #<= L :-
  139	reify(L,BL),
  140	reify(R,BR),
  141	myimpl(BL,BR).
  142L #/\ R :-
  143	call(L),
  144	call(R).
  145L #\/ R :-
  146	reify(L,BL),
  147	reify(R,BR),
  148	myor(BL,BR,1).
  149L #\ R :-
  150	reify(L,BL),
  151	reify(R,BR),
  152	myxor(BL,BR,1).
  153
  154#\ C :-
  155	reify(C,B),
  156	mynot(B,1).
  157%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  158reify(B,R) :-
  159	var(B), !,
  160	R = B.
  161reify(B,R) :-
  162	number(B), !,
  163	R = B.
  164reify(X #>= Y,B) :-
  165	parse_expression(X,XR),
  166	parse_expression(Y,YR),
  167	reified_geq(XR,YR,B).
  168reify(X #> Y,B) :-
  169	parse_expression(X,XR),
  170	Z #= Y + 1,
  171	reified_geq(XR,Z,B).
  172reify(X #=< Y,B) :-
  173	parse_expression(X,XR),
  174	parse_expression(Y,YR),
  175	reified_geq(YR,XR,B).
  176reify(X #< Y,B) :-
  177	reify(Y #> X,B).
  178reify(X #= Y,B) :-
  179	parse_expression(X,XR),
  180	parse_expression(Y,YR),
  181	reified_eq(XR,YR,B).
  182reify(X #\= Y,B) :-
  183	parse_expression(X,XR),
  184	parse_expression(Y,YR),
  185	reified_neq(XR,YR,B).
  186reify((X #/\ Y),B) :-
  187	reify(X,BX),
  188	reify(Y,BY),
  189	myand(BX,BY,B).
  190reify((X #\/ Y),B) :-
  191	reify(X,BX),
  192	reify(Y,BY),
  193	myor(BX,BY,B).
  194reify((X #\ Y),B) :-
  195	reify(X,BX),
  196	reify(Y,BY),
  197	myxor(BX,BY,B).
  198reify(#\ C, B) :-
  199	reify(C,BC),
  200	mynot(BC,B).
  201
  202%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  203check(X #= Y) :-
  204	parse_expression(X,XR),
  205	parse_expression(Y,YR),
  206	check_eq(XR,YR).
  207
  208check(X #=< Y) :-
  209	parse_expression(X,XR),
  210	parse_expression(Y,YR),
  211	check_leq(XR,YR).
  212
  213check(X #>= Y) :-
  214	parse_expression(X,XR),
  215	parse_expression(Y,YR),
  216	check_leq(YR,XR).
  217
  218check(X #< Y) :-
  219	parse_expression(X,XR),
  220	parse_expression(Y,YR),
  221	check_lt(XR,YR).
  222
  223check(X #> Y) :-
  224	parse_expression(X,XR),
  225	parse_expression(Y,YR),
  226	check_lt(YR,XR).
  227
  228
  229%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  230parse_expression(Expr,Result) :-
  231	( var(Expr) ->
  232		Result = Expr
  233	; number(Expr) ->
  234		Result = Expr
  235	; Expr = (L + R) ->
  236		parse_expression(L,RL),
  237		parse_expression(R,RR),
  238		myplus(RL,RR,Result,yes)
  239	; Expr = (L * R) ->
  240		parse_expression(L,RL),
  241		parse_expression(R,RR),
  242		mytimes(RL,RR,Result,yes)
  243	; Expr = (L - R) ->
  244		parse_expression(L,RL),
  245		parse_expression(R,RR),
  246		mytimes(-1,RR,RRR,yes),
  247		myplus(RL,RRR,Result,yes)
  248	; Expr = (- E) ->
  249		parse_expression(E,RE),
  250		mytimes(-1,RE,Result,yes)
  251	; Expr = max(L,R) ->
  252		parse_expression(L,RL),
  253		parse_expression(R,RR),
  254		mymax(RL,RR,Result,yes)
  255	; Expr = min(L,R) ->
  256		parse_expression(L,RL),
  257		parse_expression(R,RR),
  258		mymin(RL,RR,Result,yes)
  259	; Expr = L mod R ->
  260		parse_expression(L,RL),
  261		parse_expression(R,RR),
  262		mymod(RL,RR,Result,yes)
  263	; Expr = abs(E) ->
  264		parse_expression(E,RE),
  265		myabs(RE,Result,yes)
  266	; Expr = (L / R) ->
  267		parse_expression(L,RL),
  268		parse_expression(R,RR),
  269		mydiv(RL,RR,Result,yes)
  270	).
  271
  272%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  273indomain(Var) :-
  274	( var(Var) ->
  275		bounds(Var,L,U),
  276		between(L,U,Var)
  277	;
  278		true
  279	).
  280
  281label(Vs) :- labeling([], Vs).
  282
  283labeling(Options, Vars) :-
  284	label(Options, leftmost, none, Vars).
  285
  286label([Option|Options], Selection, Optimisation, Vars) :-
  287	( selection(Option) ->
  288		label(Options, Option, Optimisation, Vars)
  289	; optimization(Option) ->
  290		label(Options, Selection, Option, Vars)
  291	;
  292		label(Options, Selection, Optimisation, Vars)
  293	).
  294label([], Selection, Optimisation, Vars) :-
  295	( Optimisation == none ->
  296		label(Vars, Selection)
  297	;
  298		optimize(Vars, Selection, Optimisation)
  299	).
  300
  301
  302label([],_) :- !.
  303label(Vars,Selection) :-
  304	select_var(Selection,Vars,Var,RVars),
  305	indomain(Var),
  306	label(RVars,Selection).
  307
  308selection(ff).
  309selection(min).
  310selection(max).
  311selection(leftmost).
  312
  313optimization(min(_)).
  314optimization(max(_)).
  315
  316select_var(leftmost,[Var|Vars],Var,Vars).
  317select_var(min,[V|Vs],Var,RVars) :-
  318		find_min(Vs,V,Var),
  319		delete_eq([V|Vs],Var,RVars).
  320select_var(max,[V|Vs],Var,RVars) :-
  321		find_max(Vs,V,Var),
  322		delete_eq([V|Vs],Var,RVars).
  323select_var(ff,[V|Vs],Var,RVars) :-
  324		find_ff(Vs,V,Var),
  325		delete_eq([V|Vs],Var,RVars).
  326
  327find_min([],Var,Var).
  328find_min([V|Vs],CM,Min) :-
  329	( min_lt(V,CM) ->
  330		find_min(Vs,V,Min)
  331	;
  332		find_min(Vs,CM,Min)
  333	).
  334
  335find_max([],Var,Var).
  336find_max([V|Vs],CM,Max) :-
  337	( max_gt(V,CM) ->
  338		find_max(Vs,V,Max)
  339	;
  340		find_max(Vs,CM,Max)
  341	).
  342
  343find_ff([],Var,Var).
  344find_ff([V|Vs],CM,FF) :-
  345	( ff_lt(V,CM) ->
  346		find_ff(Vs,V,FF)
  347	;
  348		find_ff(Vs,CM,FF)
  349	).
  350
  351ff_lt(X,Y) :-
  352	bounds(X,LX,UX),
  353	bounds(Y,LY,UY),
  354	UX - LX < UY - LY.
  355
  356min_lt(X,Y) :-
  357	bounds(X,LX,_),
  358	bounds(Y,LY,_),
  359	LX < LY.
  360
  361max_gt(X,Y) :-
  362	bounds(X,_,UX),
  363	bounds(Y,_,UY),
  364	UX > UY.
  365
  366bounds(X,L,U) :-
  367	( var(X) ->
  368		get(X,L,U,_)
  369	;
  370		X = L,
  371		X = U
  372	).
  373
  374delete_eq([],_,[]).
  375delete_eq([X|Xs],Y,List) :-
  376	( X == Y ->
  377		List = Xs
  378	;
  379		List = [X|Tail],
  380		delete_eq(Xs,Y,Tail)
  381	).
  382
  383optimize(Vars, Selection, Opt) :-
  384	copy_term(Vars-Opt, Vars1-Opt1),
  385	once(label(Vars1, Selection)),
  386	functor(Opt1, Direction, _),
  387	maplist(arg(1), [Opt,Opt1], [Expr,Expr1]),
  388	optimize(Direction, Selection, Vars1, Vars, Expr1, Expr).
  389
  390optimize(Direction, Selection, Vars0, Vars, Expr0, Expr) :-
  391	Val0 is Expr0,
  392	copy_term(Vars-Expr, Vars1-Expr1),
  393	( Direction == min ->
  394		Tighten = (Expr1 #< Val0)
  395	; % max
  396		Tighten = (Expr1 #> Val0)
  397	),
  398	( Tighten, label(Vars1, Selection) ->
  399		optimize(Direction, Selection, Vars1, Vars, Expr1, Expr)
  400	;
  401		Vars = Vars0,
  402		Expr = Expr0
  403	).
  404
  405%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  406all_different([]).
  407all_different([X|Xs]) :-
  408	different(Xs,X),
  409	all_different(Xs).
  410
  411different([],_).
  412different([Y|Ys],X) :-
  413	neq(X,Y,yes),
  414	different(Ys,X).
  415%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  416sum(Xs,Op,Value) :-
  417	sum1(Xs,0,Op,Value).
  418
  419sum1([],Sum,Op,Value) :-
  420	call(Op,Sum,Value).
  421sum1([X|Xs],Acc,Op,Value) :-
  422	NAcc #= Acc + X,
  423	sum1(Xs,NAcc,Op,Value).
  424
  425%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  426% contributed by Markus Triska
  427
  428lex_le([],[]).
  429lex_le([V1|V1s], [V2|V2s]) :-
  430      V1 #=< V2,
  431      ( integer(V1) ->
  432              ( integer(V2) ->
  433                      (V1 == V2 ->
  434                              lex_le(V1s,V2s)
  435                      ;
  436                              true
  437                      )
  438              ;
  439                      freeze(V2,lex_le([V1|V1s],[V2|V2s]))
  440              )
  441      ;
  442              freeze(V1,lex_le([V1|V1s],[V2|V2s]))
  443      ).
  444
  445lex_chain([]).
  446lex_chain([L|Ls]) :-
  447	lex_chain_lag(Ls, L).
  448
  449lex_chain_lag([], _).
  450lex_chain_lag([L|Ls], Prev) :-
  451	lex_le(Prev, L),
  452	lex_chain_lag(Ls, L).
  453
  454%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  455domain(X,L,U) :-
  456	( var(X) ->
  457		get(X,XL,XU,Exp),
  458		NL is max(L,XL),
  459		NU is min(U,XU),
  460		put(X,NL,NU,Exp)
  461	; % nonvar(X) ->
  462		X >= L,
  463		X =< U
  464	).
  465
  466domains([],_,_).
  467domains([V|Vs],L,U) :-
  468	domain(V,L,U),
  469	domains(Vs,L,U).
  470
  471%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  472leq(X,Y,New) :-
  473	geq(Y,X,New).
  474
  475%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  476geq(X,Y,New) :-
  477	( X == Y ->
  478		true
  479	; nonvar(X) ->
  480		( nonvar(Y) ->
  481			X >= Y
  482		;
  483			get(Y,YL,YU,Exp) ->
  484			NYU is min(X,YU),
  485			put(Y,YL,NYU,Exp)
  486		)
  487	; nonvar(Y) ->
  488		get(X,XL,XU,Exp) ->
  489		NXL is max(Y,XL),
  490		put(X,NXL,XU,Exp)
  491	;
  492		get(X,XL,XU,ExpX),
  493		get(Y,YL,YU,ExpY),
  494		XU >= YL,
  495		( XL > YU ->
  496			true
  497		; XU == YL ->
  498			X = Y
  499		; member(leq(Z,State),ExpX),
  500	          Y == Z ->
  501			set_passive(State),
  502			X = Y
  503		;
  504			( New == yes ->
  505				active_state(State),
  506				put(Y,YL,YU,[leq(X,State)|ExpY]),
  507				ExpX1 = [geq(Y,State)|ExpX]
  508			;
  509				ExpX1 = ExpX
  510			),
  511			NXL is max(XL,YL),
  512			put(X,NXL,XU,ExpX1),
  513			( get(Y,YL2,YU2,ExpY2) ->
  514				NYU is min(YU2,XU),
  515				put(Y,YL2,NYU,ExpY2)
  516			;
  517				true
  518			)
  519		)
  520	).
  521
  522%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  523neq(X,Y,New) :-
  524	X \== Y,
  525	( nonvar(X) ->
  526		( nonvar(Y) ->
  527			true
  528		;
  529			get(Y,L,U,Exp),
  530			( L == X ->
  531				NL is L + 1,
  532				put(Y,NL,U,Exp)
  533			; U == X ->
  534				NU is U - 1,
  535				put(Y,L,NU,Exp)
  536		        ; L > X ->
  537		                true
  538		        ; U < X ->
  539		                true
  540		        ;
  541				( New == yes ->
  542					active_state(State),
  543					put(Y,L,U,[neq(X,State)|Exp])
  544				;
  545					true
  546				)
  547			)
  548		)
  549	; nonvar(Y) ->
  550		neq(Y,X,New)
  551	;
  552		get(X,XL,XU,XExp),
  553		get(Y,YL,YU,YExp),
  554		( XL > YU ->
  555			true
  556		; YL > XU ->
  557			true
  558		;
  559			( New == yes ->
  560				active_state(State),
  561				put(X,XL,XU,[neq(Y,State)|XExp]),
  562				put(Y,YL,YU,[neq(X,State)|YExp])
  563			;
  564				true
  565			)
  566		)
  567	).
  568
  569%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  570myplus(X,Y,Z,New) :-
  571	( nonvar(X) ->
  572		( nonvar(Y) ->
  573			Z is X + Y
  574		; nonvar(Z) ->
  575			Y is Z - X
  576		;
  577			get(Z,ZL,ZU,ZExp),
  578			get(Y,YL,YU,YExp),
  579			( New == yes ->
  580				ZExp1 = [myplus2(Y,X)|ZExp],
  581				YExp1 = [myplus(X,Z)|YExp],
  582				put(Y,YL,YU,YExp1)
  583			;
  584				ZExp1 = ZExp
  585			),
  586			NZL is max(ZL,X+YL),
  587			NZU is min(ZU,X+YU),
  588			put(Z,NZL,NZU,ZExp1),
  589			( get(Y,YL2,YU2,YExp2) ->	% JW: YL2 and YU2?
  590				NYL is max(YL2,NZL-X),
  591				NYU is min(YU2,NZU-X),
  592				put(Y,NYL,NYU,YExp2)
  593			;
  594				Z is X + Y
  595			)
  596		)
  597	; nonvar(Y) ->
  598		myplus(Y,X,Z,New)
  599	; nonvar(Z) ->
  600		get(X,XL,XU,XExp),
  601		get(Y,YL,YU,YExp),
  602		( New == yes ->
  603			XExp1 = [myplus(Y,Z)|XExp],
  604			YExp1 = [myplus(X,Z)|YExp],
  605			put(Y,YL,YU,YExp1)
  606		;
  607			XExp1 = XExp
  608		),
  609		NXL is max(XL,Z-YU),
  610		NXU is min(XU,Z-YL),
  611		put(X,NXL,NXU,XExp1),
  612		( get(Y,YL2,YU2,YExp2) ->
  613			NYL is max(YL2,Z-NXU),
  614			NYU is min(YU2,Z-NXL),
  615			put(Y,NYL,NYU,YExp2)
  616		;
  617			X is Z - Y
  618		)
  619	;
  620		get(X,XL,XU,XExp),
  621		get(Y,YL,YU,YExp),
  622		get(Z,ZL,ZU,ZExp),
  623		( New == yes ->
  624			XExp1 = [myplus(Y,Z)|XExp],
  625			YExp1 = [myplus(X,Z)|YExp],
  626			ZExp1 = [myplus2(X,Y)|ZExp],
  627			put(Y,YL,YU,YExp1),
  628			put(Z,ZL,ZU,ZExp1)
  629		;
  630			XExp1 = XExp
  631		),
  632		NXL is max(XL,ZL-YU),
  633		NXU is min(XU,ZU-YL),
  634		put(X,NXL,NXU,XExp1),
  635		( get(Y,YL2,YU2,YExp2) ->
  636			NYL is max(YL2,ZL-NXU),
  637			NYU is min(YU2,ZU-NXL),
  638			put(Y,NYL,NYU,YExp2)
  639		;
  640			NYL = Y,
  641			NYU = Y
  642		),
  643		( get(Z,ZL2,ZU2,ZExp2) ->
  644			NZL is max(ZL2,NXL+NYL),
  645			NZU is min(ZU2,NXU+NYU),
  646			put(Z,NZL,NZU,ZExp2)
  647		;
  648			true
  649		)
  650	).
  651
  652%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  653% X * Y = Z
  654
  655div(X,Y,Z) :-
  656	( max_inf(X) ->
  657		( Y >= 0 ->
  658			Z = X
  659		;
  660			min_inf(Z)
  661		)
  662	; min_inf(X) ->
  663		( Y >= 0 ->
  664			Z = X
  665		;
  666			max_inf(Z)
  667		)
  668	; Y \== 0 ->
  669		Z is X / Y
  670	; X >= 0 ->
  671		max_inf(Z)
  672	; X < 0 ->
  673		min_inf(Z)
  674	).
  675
  676mytimes(X,Y,Z,New) :-
  677	( nonvar(X) ->
  678		(nonvar(Y) ->
  679			Z is X * Y
  680		; X == 0 ->
  681			Z = 0
  682		;  nonvar(Z) ->
  683			0 is Z mod X,
  684			Y is Z / X
  685		;
  686			get(Y,YL,YU,YExp),
  687			get(Z,ZL,ZU,ZExp),
  688			NZL is max(ZL,min(X * YL,X*YU)),
  689			NZU is min(ZU,max(X * YU,X*YL)),
  690			( New == yes ->
  691				YExp1 = [mytimes(X,Z)|YExp],
  692				put(Y,YL,YU,YExp1),
  693				put(Z,NZL,NZU,[mytimes2(X,Y)|ZExp])
  694			;
  695				put(Z,NZL,NZU,ZExp)
  696			),
  697			( get(Y,YL2,YU2,YExp2) ->
  698				min_divide(ZL,ZU,X,X,NYLT),
  699				max_divide(ZL,ZU,X,X,NYUT),
  700				NYL is max(YL2,ceiling(NYLT)),
  701				NYU is min(YU2,floor(NYUT)),
  702				put(Y,NYL,NYU,YExp2)
  703			;
  704				Z is X * Y
  705			)
  706		)
  707	; nonvar(Y) ->
  708		mytimes(Y,X,Z,New)
  709	; nonvar(Z) ->
  710		get(X,XL,XU,XExp),
  711		get(Y,YL,YU,YExp),
  712		min_divide(Z,Z,YL,YU,TNXL),
  713		max_divide(Z,Z,YL,YU,TNXU),
  714		NXL is max(XL,ceiling(TNXL)),
  715		NXU is min(XU,floor(TNXU)),
  716		( New == yes ->
  717			YExp1 = [mytimes(X,Z)|YExp],
  718			put(Y,YL,YU,YExp1),
  719			put(X,NXL,NXU,[mytimes(Y,Z)|XExp])
  720		;
  721			put(X,NXL,NXU,XExp)
  722		),
  723		( get(Y,YL2,YU2,YExp2) ->
  724			min_divide(Z,Z,NXL,NXU,NYLT),
  725			max_divide(Z,Z,NXL,NXU,NYUT),
  726			NYL is max(YL2,ceiling(NYLT)),
  727			NYU is min(YU2,floor(NYUT)),
  728			put(Y,NYL,NYU,YExp2)
  729		;
  730			( Y \== 0 ->
  731				0 is Z mod Y,
  732				X is Z / Y
  733			;
  734				Z = 0
  735			)
  736		)
  737	;
  738		get(X,XL,XU,XExp),
  739		get(Y,YL,YU,YExp),
  740		get(Z,ZL,ZU,ZExp),
  741		min_divide(ZL,ZU,YL,YU,TXL),
  742		NXL is max(XL,ceiling(TXL)),
  743		max_divide(ZL,ZU,YL,YU,TXU),
  744		NXU is min(XU,floor(TXU)),
  745		( New == yes ->
  746			put(Y,YL,YU,[mytimes(X,Z)|YExp]),
  747			put(Z,ZL,ZU,[mytimes2(X,Y)|ZExp]),
  748			put(X,NXL,NXU,[mytimes(Y,Z)|XExp])
  749		;
  750			put(X,NXL,NXU,XExp)
  751		),
  752		( get(Y,YL2,YU2,YExp2) ->
  753			min_divide(ZL,ZU,XL,XU,TYL),
  754			NYL is max(YL2,ceiling(TYL)),
  755			max_divide(ZL,ZU,XL,XU,TYU),
  756			NYU is min(YU2,floor(TYU)),
  757			put(Y,NYL,NYU,YExp2)
  758		;
  759			NYL = Y,
  760			NYU = Y
  761		),
  762		( get(Z,ZL2,ZU2,ZExp2) ->
  763			min_times(NXL,NXU,NYL,NYU,TZL),
  764			NZL is max(ZL2,TZL),
  765			max_times(NXL,NXU,NYL,NYU,TZU),
  766			NZU is min(ZU2,TZU),
  767			put(Z,NZL,NZU,ZExp2)
  768		;
  769
  770			true
  771		)
  772	).
  773
  774max_times(L1,U1,L2,U2,Max) :-
  775	Max is max(max(L1*L2,L1*U2),max(U1*L2,U1*U2)).
  776min_times(L1,U1,L2,U2,Min) :-
  777	Min is min(min(L1*L2,L1*U2),min(U1*L2,U1*U2)).
  778max_divide(L1,U1,L2,U2,Max) :-
  779	( L2 =< 0 , U2 >= 0 ->
  780		max_inf(Max)
  781	;	div(L1,L2,DLL),
  782		div(L1,U2,DLU),
  783	        div(U1,L2,DUL),
  784		div(U1,U2,DUU),
  785		Max is max(max(DLL,DLU),max(DUL,DUU))
  786	).
  787min_divide(L1,U1,L2,U2,Min) :-
  788	( L2 =< 0 , U2 >= 0 ->
  789		min_inf(Min)
  790	;	div(L1,L2,DLL),
  791		div(L1,U2,DLU),
  792	        div(U1,L2,DUL),
  793		div(U1,U2,DUU),
  794		Min is min(min(DLL,DLU),min(DUL,DUU))
  795	).
  796
  797
  798mydiv(X,Y,Z,New) :-
  799	( Y == 0 -> fail ; true	),
  800	( nonvar(X) ->
  801		( nonvar(Y) ->
  802			Z is X // Y
  803		;
  804			get(Y,YL,YU,YExp),
  805			( New == yes ->
  806				put(Y,YL,YU,[mydiv3(X,Z)|YExp])
  807			;
  808				true
  809			),
  810			( nonvar(Z) ->
  811				% TODO: cover this
  812				true
  813			;
  814				get(Z,ZL,ZU,ZExp),
  815				( YL =< 0, YU >= 0 ->
  816					NZL is max(-abs(X),ZL),
  817					NZU is min(abs(X),ZU)
  818				; X >= 0, YL > 0 ->
  819					NZL is max(X // YU, ZL),
  820					NZU is min(X // YL, ZU)
  821				;	% TODO: cover more cases
  822					NZL = ZL,
  823					NZU = ZU
  824				),
  825				( New == yes ->
  826					put(Z,NZL,NZU,[mydiv2(X,Y)|ZExp])
  827				;
  828					put(Z,NZL,NZU,ZExp)
  829				)
  830			)
  831		)
  832	; nonvar(Y) ->
  833		get(X,XL,XU,XExp),
  834		( nonvar(Z) ->
  835			(Z >= 0, Y >= 0 ->
  836				NXL is max(Z*Y,XL),
  837				NXU is min((Z+1)*Y - 1,XU)
  838			;
  839				% TODO: cover more cases
  840				NXL = XL,
  841				NXU = XU
  842			),
  843			( New == yes ->
  844				put(X,NXL,NXU,[mydiv(Y,Z)|XExp])
  845			;
  846				put(X,NXL,NXU,XExp)
  847			)
  848		;
  849			get(Z,ZL,ZU,ZExp),
  850			( XL >= 0, Y >= 0 ->
  851				NZL is max(XL // Y,ZL),
  852				NZU is min(XU // Y,ZU),
  853				NXL is max(Y*NZL, XL),
  854				NXU is min((NZU+1)*Y - 1, XU)
  855			; % TODO: cover more cases
  856				NZL is max(-max(abs(XL),abs(XU)),ZL),
  857				NZU is min(max(abs(XL),abs(XU)),ZU),
  858				NXL = XL,
  859				NXU = XU
  860			),
  861			( New == yes ->
  862				put(X,NXL,NXU,[mydiv(Y,Z)|XExp]),
  863				put(Z,NZL,NZU,[mydiv2(X,Y)|ZExp])
  864			;
  865				put(X,NXL,NXU,XExp),
  866				( nonvar(Z) -> true ; put(Z,NZL,NZU,ZExp) )
  867			)
  868		)
  869	; nonvar(Z) ->
  870		get(X,XL,XU,XExp),
  871		get(Y,YL,YU,YExp),
  872		(YL >= 0, XL >= 0 ->
  873			NXL is max(YL*Z,XL),
  874			NXU is min(YU*(Z + 1) - 1,XU)
  875		; % TODO: cover more cases
  876			NXL = XL,
  877			NXU = XU
  878		),
  879		( New == yes ->
  880			put(X,NXL,NXU,[mydiv(Y,Z)|XExp]),
  881			put(Y,YL,YU,[mydiv3(X,Z)|YExp])
  882		;
  883			put(X,NXL,NXU,XExp)
  884		)
  885	;
  886		get(X,XL,XU,XExp),
  887		get(Y,YL,YU,YExp),
  888		get(Z,ZL,ZU,ZExp),
  889		( New == yes ->
  890			put(Y,YL,YU,[mydiv3(X,Z)|YExp]),
  891			put(Z,ZL,ZU,[mydiv2(X,Y)|ZExp]),
  892			put(X,XL,XU,[mydiv(Y,Z)|XExp])
  893		;
  894			true
  895		)
  896	).
  897
  898
  899%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  900mymax(X,Y,Z,New) :-
  901	( nonvar(X) ->
  902		( nonvar(Y) ->
  903			Z is max(X,Y)
  904		; nonvar(Z) ->
  905			( Z == X ->
  906				geq(X,Y,yes)
  907			; Z > X ->
  908				Y = Z
  909			%; Z < X
  910			%	fail
  911			)
  912		;
  913			get(Y,YL,YU,YExp),
  914			get(Z,ZL,ZU,ZExp),
  915			( YL >= X ->
  916				Z = Y
  917			; X >= YU ->
  918				Z = X
  919			; X < ZL ->
  920				Y = Z
  921			;
  922				( New == yes ->
  923					put(Y,YL,YU,[mymax(X,Z)|YExp])
  924				;
  925					true
  926				),
  927				NZL is max(ZL,X),
  928				NZU is min(ZU,YU),
  929				( New == yes ->
  930					put(Z,NZL,NZU,[mymax2(X,Y)|ZExp])
  931				;
  932					put(Z,NZL,NZU,ZExp)
  933				),
  934				( get(Y,YL2,YU2,YExp2) ->
  935					NYU is min(YU2,NZU),
  936					put(Y,YL2,NYU,YExp2)
  937				;
  938					true
  939				)
  940			)
  941		)
  942	; nonvar(Y) ->
  943		mymax(Y,X,Z,New)
  944	; nonvar(Z) ->
  945		get(X,XL,XU,XExp),
  946		get(Y,YL,YU,YExp),
  947		( XU < Z ->
  948			Y = Z
  949		; % XU >= Z ->
  950		  YU < Z ->
  951			X = Z
  952		; % YU >= Z
  953		  XL > YU ->
  954			Z = X
  955		; YL > XU ->
  956			Z = Y
  957		;
  958			( New == yes ->
  959				put(Y,YL,YU,[mymax(X,Z)|YExp]),
  960				put(X,XL,Z,[mymax(Y,Z)|XExp])
  961			;
  962				put(X,XL,Z,XExp)
  963			),
  964			( get(Y,YL2,YU2,YExp2) ->
  965				NYU is min(YU2,Z),
  966				put(Y,YL2,NYU,YExp2)
  967			;
  968				true
  969			)
  970		)
  971	; X == Y ->
  972		Z = X
  973	; Z == X ->
  974		geq(X,Y,yes)
  975	; Z == Y ->
  976		geq(Y,X,yes)
  977	;
  978		get(X,XL,XU,XExp),
  979		get(Y,YL,YU,YExp),
  980		get(Z,ZL,ZU,ZExp),
  981		NZL is max(ZL,max(XL,YL)),
  982		NZU is min(ZU,max(XU,YU)),
  983		( New == yes ->
  984			put(X,XL,XU,[mymax(Y,Z)|XExp]),
  985			put(Y,YL,YU,[mymax(X,Z)|YExp]),
  986			put(Z,NZL,NZU,[mymax2(X,Y)|ZExp])
  987		;
  988			put(Z,NZL,NZU,ZExp)
  989		),
  990		( get(X,XL2,XU2,XExp2) ->
  991			( XU2 < NZL ->
  992				Y = Z
  993			; YU  < NZL ->
  994				X = Z
  995			; YU < XL2 ->
  996				X = Z
  997			; XU2 < YL ->
  998				Y = Z
  999			;
 1000				NXU is min(XU2,NZU),
 1001				put(X,XL2,NXU,XExp2),
 1002				( get(Y,YL2,YU2,YExp2) ->
 1003					NYU is min(YU2,NZU),
 1004					put(Y,YL2,NYU,YExp2)
 1005				;
 1006					mymax(Y,X,Z,no)
 1007				)
 1008			)
 1009		;
 1010			mymax(X,Y,Z,no)
 1011		)
 1012	).
 1013
 1014mymin(X,Y,Z,New) :-
 1015	( nonvar(X) ->
 1016		( nonvar(Y) ->
 1017			Z is min(X,Y)
 1018		; nonvar(Z) ->
 1019			( Z == X ->
 1020				leq(X,Y,yes)
 1021			; Z < X ->
 1022				Y = Z
 1023			%; Z > X
 1024			%	fail
 1025			)
 1026		;
 1027			get(Y,YL,YU,YExp),
 1028			get(Z,ZL,ZU,ZExp),
 1029			( YL >= X ->
 1030				Z = X
 1031			; X >= YU ->
 1032				Z = Y
 1033			; X > ZU ->
 1034				Y = Z
 1035			;
 1036				( New == yes ->
 1037					put(Y,YL,YU,[mymin(X,Z)|YExp])
 1038				;
 1039					true
 1040				),
 1041				NZL is max(ZL,YL),
 1042				NZU is min(ZU,X),
 1043				( New == yes ->
 1044					put(Z,NZL,NZU,[mymin2(X,Y)|ZExp])
 1045				;
 1046					put(Z,NZL,NZU,ZExp)
 1047				),
 1048				( get(Y,YL2,YU2,YExp2) ->
 1049					NYL is max(YL2,NZL),
 1050					put(Y,NYL,YU2,YExp2)
 1051				;
 1052					true
 1053				)
 1054			)
 1055		)
 1056	; nonvar(Y) ->
 1057		mymin(Y,X,Z,New)
 1058	; nonvar(Z) ->
 1059		get(X,XL,XU,XExp),
 1060		get(Y,YL,YU,YExp),
 1061		( XL > Z ->
 1062			Y = Z
 1063		; % XL =< Z ->
 1064		  YL > Z ->
 1065			X = Z
 1066		; % YL =< Z
 1067		  XU =< YL ->
 1068			Z = X
 1069		; YU =< XL ->
 1070			Z = Y
 1071		;
 1072			( New == yes ->
 1073				put(Y,YL,YU,[mymin(X,Z)|YExp]),
 1074				put(X,Z,XU,[mymin(Y,Z)|XExp])
 1075			;
 1076				put(X,Z,XU,XExp)
 1077			),
 1078			( get(Y,YL2,YU2,YExp2) ->
 1079				NYL is max(YL2,Z),
 1080				put(Y,NYL,YU2,YExp2)
 1081			;
 1082				true
 1083			)
 1084		)
 1085	; X == Y ->
 1086		Z = X
 1087	; Z == X ->
 1088		leq(X,Y,yes)
 1089	; Z == Y ->
 1090		leq(Y,X,yes)
 1091	;
 1092		get(X,XL,XU,XExp),
 1093		get(Y,YL,YU,YExp),
 1094		get(Z,ZL,ZU,ZExp),
 1095		NZL is max(ZL,min(XL,YL)),
 1096		NZU is min(ZU,min(XU,YU)),
 1097		( New == yes ->
 1098			put(X,XL,XU,[mymin(Y,Z)|XExp]),
 1099			put(Y,YL,YU,[mymin(X,Z)|YExp]),
 1100			put(Z,NZL,NZU,[mymin2(X,Y)|ZExp])
 1101		;
 1102			put(Z,NZL,NZU,ZExp)
 1103		),
 1104		( get(X,XL2,XU2,XExp2) ->
 1105			( XL2 > NZU ->
 1106				Y = Z
 1107			; YL  > NZU ->
 1108				X = Z
 1109			; YU < XL2 ->
 1110				Y = Z
 1111			; XU2 < YL ->
 1112				X = Z
 1113			;
 1114				NXL is max(XL2,NZL),
 1115				put(X,NXL,XU2,XExp2),
 1116				( get(Y,YL2,YU2,YExp2) ->
 1117					NYL is max(YL2,NZL),
 1118					put(Y,NYL,YU2,YExp2)
 1119				;
 1120					mymin(Y,X,Z,no)
 1121				)
 1122			)
 1123		;
 1124			mymin(X,Y,Z,no)
 1125		)
 1126	).
 1127
 1128myabs(X,Y,New) :-
 1129	( nonvar(X) ->
 1130		Y is abs(X)
 1131	; nonvar(Y) ->
 1132		Y >= 0,
 1133		get(X,LX,UX,ExpX),
 1134		( UX < Y ->
 1135			X is (-Y)
 1136		; LX > (-Y) ->
 1137			X = Y
 1138		;
 1139			NLX is (-Y),
 1140			( New == yes ->
 1141				put(X,NLX,Y,[myabs(Y)|ExpX])
 1142			;
 1143				put(X,NLX,Y,ExpX)
 1144			)
 1145		)
 1146	;
 1147		get(X,LX,UX,ExpX),
 1148		get(Y,LY,UY,ExpY),
 1149		UY > 0,
 1150		( New == yes ->
 1151			put(X,LX,UX,[myabs(Y)|ExpX])
 1152		;
 1153			true
 1154		),
 1155		( LX =< 0, UX >= 0 ->
 1156			NLY is max(0,LY)
 1157		;
 1158			NLY is max(min(abs(LX),abs(UX)),max(LY,0))
 1159		),
 1160		NUY is min(UY,max(abs(LX),abs(UX))),
 1161		( New == yes ->
 1162			put(Y,NLY,NUY,[myabs2(X)|ExpY])
 1163		;
 1164			put(Y,NLY,NUY,ExpY)
 1165		),
 1166		( var(X) ->
 1167			get(X,LX2,UX2,ExpX2),
 1168			( LX2 == LX, UX2 == UX ->
 1169				( NLY == 0 ->
 1170					NLX is max(LX,(-NUY)),
 1171					NUX is min(UX,NUY)
 1172				; LX > (-NLY)  ->
 1173					NLX is max(LX,NLY),
 1174					NUX is min(UX,NUY)
 1175				;
 1176					NLX is max((-NUY),LX),
 1177					( UX < NLY ->
 1178						NUX is min((-NLY),UX)
 1179					;
 1180						NUX is min(NUY,UX)
 1181					)
 1182				),
 1183				put(X,NLX,NUX,ExpX2)
 1184			;
 1185				true
 1186			)
 1187		;
 1188			true
 1189		)
 1190	).
 1191
 1192mymod(X,Y,Z,New) :- % Z is X mod Y
 1193	( nonvar(X) ->
 1194		( nonvar(Y) ->
 1195			Z is X mod Y
 1196		; nonvar(Z) ->
 1197			get(Y,YL,YU,YExp),
 1198			( Z > 0 ->
 1199				( X == Z ->
 1200					no_overlap(-X,X,YL,YU,NYL,NYU),
 1201					( New == yes ->
 1202						put(Y,NYL,NYU,[mymod2(X,Z)|YExp])
 1203					;
 1204						put(Y,NYL,NYU,YExp)
 1205					)
 1206				; % Z < X
 1207					no_overlap(-Z,Z,YL,YU,YL1,YU1),
 1208					in_between(-X,X,YL1,YU1,NYL,NYU),
 1209					( New == yes ->
 1210						put(Y,NYL,NYU,[mymod2(X,Z)|YExp])
 1211					;
 1212						put(Y,NYL,NYU,YExp)
 1213					)
 1214				)
 1215			; Z < 0 ->
 1216				( X == Z ->
 1217					no_overlap(X,-X,YL,YU,NYL,NYU),
 1218					( New == yes ->
 1219						put(Y,NYL,NYU,[mymod2(X,Z)|YExp])
 1220					;
 1221						put(Y,NYL,NYU,YExp)
 1222					)
 1223				; % Z < X
 1224					no_overlap(Z,-Z,YL,YU,YL1,YU1),
 1225					in_between(X,-X,YL1,YU1,NYL,NYU),
 1226					( New == yes ->
 1227						put(Y,NYL,NYU,[mymod2(X,Z)|YExp])
 1228					;
 1229						put(Y,NYL,NYU,YExp)
 1230					)
 1231				)
 1232			; % Z == 0
 1233				( X == 0 ->
 1234					no_overlap(0,0,YL,YU,NYL,NYU),% Y \== 0
 1235					( New == yes ->
 1236						put(Y,NYL,NYU,[mymod2(X,Z)|YExp])
 1237					;
 1238						put(Y,NYL,NYU,YExp)
 1239					)
 1240				; % X \== 0
 1241					PX is abs(X),
 1242					in_between(-PX,PX,YL,YU,NYL,NYU),% |Y| < |X|
 1243					( New == yes ->
 1244						put(Y,NYL,NYU,[mymod2(X,Z)|YExp])
 1245					;
 1246						put(Y,NYL,NYU,YExp)
 1247					)
 1248				)
 1249			)
 1250		; % var(Y), var(Z)
 1251			( New == yes ->
 1252				get(Y,YL,YU,YExp),
 1253				get(Z,ZL,ZU,ZExp),
 1254				put(Y,YL,YU,[mymod2(X,Z)|YExp]),
 1255				put(Z,ZL,ZU,[mymod3(X,Y)|ZExp])
 1256			;
 1257				true
 1258			)
 1259		)
 1260	; nonvar(Y) ->
 1261		Y \== 0,
 1262		( nonvar(Z) ->
 1263			get(X,XL,XU,XExp),
 1264			( Z > 0 ->
 1265				NXL is max(XL,1),
 1266				( New == yes ->
 1267					put(X,NXL,XU,[mymod1(Y,Z)|XExp])
 1268				;
 1269					put(X,NXL,XU,XExp)
 1270				)
 1271			; Z < 0 ->
 1272				NXU is min(XU,-1),
 1273				( New == yes ->
 1274					put(X,XL,NXU,[mymod1(Y,Z)|XExp])
 1275				;
 1276					put(X,XL,NXU,XExp)
 1277				)
 1278			;
 1279				( New == yes ->
 1280					put(X,XL,XU,[mymod1(Y,Z)|XExp])
 1281				;
 1282					put(X,XL,XU,XExp)
 1283				)
 1284			)
 1285		;
 1286			( New == yes ->
 1287				get(X,XL,XU,XExp),
 1288				get(Z,ZL,ZU,ZExp),
 1289				put(X,XL,XU,[mymod1(Y,Z)|XExp]),
 1290				put(Z,ZL,ZU,[mymod3(X,Y)|ZExp])
 1291			;
 1292				true
 1293			)
 1294		)
 1295	; nonvar(Z) ->
 1296		( New == yes ->
 1297			get(X,XL,XU,XExp),
 1298			get(Y,YL,YU,YExp),
 1299			put(X,XL,XU,[mymod1(Y,Z)|XExp]),
 1300			put(Y,YL,YU,[mymod2(X,Z)|YExp])
 1301		;
 1302			true
 1303		)
 1304	;
 1305		( New == yes ->
 1306			get(X,XL,XU,XExp),
 1307			get(Y,YL,YU,YExp),
 1308			get(Z,ZL,ZU,ZExp),
 1309			put(X,XL,XU,[mymod1(Y,Z)|XExp]),
 1310			put(Y,YL,YU,[mymod2(X,Z)|YExp]),
 1311			put(Z,ZL,ZU,[mymod3(X,Y)|ZExp])
 1312		;
 1313			true
 1314		)
 1315	).
 1316
 1317no_overlap(XL,XU,YL,YU,NYL,NYU) :-
 1318	( XL =< YL ->
 1319		NYL is XU + 1,
 1320		NYU = YU
 1321	; YU =< XU ->
 1322		NYU is XL - 1,
 1323		NYL is YL
 1324	;
 1325		NYL = YL,
 1326		NYU = YU
 1327	).
 1328in_between(XL,XU,YL,YU,NYL,NYU) :-
 1329	( XL >= YL ->
 1330		NYL is XL + 1
 1331	;
 1332		NYL = YL
 1333	),
 1334	( XU =< YU ->
 1335		NYU is XU -1
 1336	;
 1337		NYU = YU
 1338	).
 1339
 1340%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1341% TODO
 1342%	trigger reified constraints when geq is added
 1343reified_geq(X,Y,B) :-
 1344	( var(B) ->
 1345		( nonvar(X) ->
 1346			( nonvar(Y) ->
 1347				( X >= Y ->
 1348					B = 1
 1349				;
 1350					B = 0
 1351				)
 1352			;
 1353				get(Y,L,U,Expr),
 1354				( X >= U ->
 1355					B = 1
 1356				; X < L ->
 1357					B = 0
 1358				;
 1359					put(Y,L,U,[reified_leq(X,B)|Expr]),
 1360					get(B,BL,BU,BExpr),
 1361					put(B,BL,BU,[reified_geq2(X,Y)|BExpr]),
 1362					B in 0..1
 1363				)
 1364			)
 1365		; nonvar(Y) ->
 1366			get(X,L,U,Expr),
 1367			( L >= Y ->
 1368			B = 1
 1369			; U < Y ->
 1370				B = 0
 1371			;
 1372				put(X,L,U,[reified_geq(Y,B)|Expr]),
 1373				get(B,BL,BU,BExpr),
 1374				put(B,BL,BU,[reified_geq2(X,Y)|BExpr]),
 1375				B in 0..1
 1376			)
 1377		;
 1378			get(X,XL,XU,XExpr),
 1379			get(Y,YL,YU,YExpr),
 1380			( XL >= YU ->
 1381				B = 1
 1382			; XU < YL ->
 1383				B = 0
 1384			; member(geq(Z,_State),XExpr),
 1385			  Z == Y ->
 1386				B = 1
 1387			;
 1388				put(X,XL,XU,[reified_geq(Y,B)|XExpr]),
 1389				put(Y,YL,YU,[reified_leq(X,B)|YExpr]),
 1390				get(B,BL,BU,BExpr),
 1391				put(B,BL,BU,[reified_geq2(X,Y)|BExpr]),
 1392				B in 0..1
 1393			)
 1394		)
 1395	; B == 1 ->
 1396		X #>= Y
 1397	; B == 0 ->
 1398		X #< Y
 1399	).
 1400
 1401check_leq(X,Y) :-
 1402	( nonvar(X) ->
 1403		( nonvar(Y) ->
 1404			X =< Y
 1405		;
 1406			bounds(Y,L,_),
 1407			X =< L
 1408		)
 1409	;
 1410		( nonvar(Y) ->
 1411			bounds(X,_,U),
 1412			U =< Y
 1413		;
 1414			bounds(X,_,UX),
 1415			bounds(Y,LY,_),
 1416			UX =< LY
 1417		)
 1418	).
 1419
 1420check_lt(X,Y) :-
 1421	( nonvar(X) ->
 1422		( nonvar(Y) ->
 1423			X < Y
 1424		;
 1425			bounds(Y,L,_),
 1426			X < L
 1427		)
 1428	;
 1429		( nonvar(Y) ->
 1430			bounds(X,_,U),
 1431			U < Y
 1432		;
 1433			bounds(X,_,UX),
 1434			bounds(Y,LY,_),
 1435			UX < LY
 1436		)
 1437	).
 1438
 1439%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1440reified_eq(X,Y,B) :-
 1441	( var(B) ->
 1442		( nonvar(X) ->
 1443			( nonvar(Y) ->
 1444				( X == Y ->
 1445					B = 1
 1446				;
 1447					B = 0
 1448				)
 1449			;
 1450				get(Y,L,U,Expr),
 1451				( L > X ->
 1452					B = 0
 1453				; U < X ->
 1454					B = 0
 1455				;
 1456					put(Y,L,U,[reified_eq(X,B)|Expr]),
 1457					get(B,BL,BU,BExpr),
 1458					put(B,BL,BU,[reified_eq2(X,Y)|BExpr]),
 1459					B in 0..1
 1460				)
 1461			)
 1462		; nonvar(Y) ->
 1463			reified_eq(Y,X,B)
 1464		; X == Y ->
 1465			B = 1
 1466		;
 1467			get(X,XL,XU,XExpr),
 1468			get(Y,YL,YU,YExpr),
 1469			( XL > YU ->
 1470				B = 0
 1471			; YL > XU ->
 1472				B = 0
 1473			; member(neq(Z,_),XExpr),
 1474			  Z == Y ->
 1475				B = 0
 1476			;
 1477				put(X,XL,XU,[reified_eq(Y,B)|XExpr]),
 1478				put(Y,YL,YU,[reified_eq(X,B)|YExpr]),
 1479				get(B,BL,BU,BExpr),
 1480				put(B,BL,BU,[reified_eq2(X,Y)|BExpr]),
 1481				B in 0..1
 1482			)
 1483		)
 1484	; B == 1 ->
 1485		X #= Y
 1486	; B == 0 ->
 1487		X #\= Y
 1488	).
 1489
 1490
 1491check_eq(X,Y) :-
 1492	X == Y.
 1493%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1494reified_neq(X,Y,B) :-
 1495	mynot(B,B1),
 1496	reified_eq(X,Y,B1).
 1497
 1498%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1499mynot(B1,B2) :-
 1500	( nonvar(B1) ->
 1501		( B1 == 1 ->
 1502			B2 = 0
 1503		; B1 == 0 ->
 1504			B2 = 1
 1505		)
 1506	; nonvar(B2) ->
 1507		mynot(B2,B1)
 1508	;
 1509		get(B1,L1,U1,Expr1),
 1510		get(B2,L2,U2,Expr2),
 1511		put(B2,L2,U2,[mynot(B1)|Expr2]),
 1512		put(B1,L1,U1,[mynot(B2)|Expr1]),
 1513		B1 in 0..1,
 1514		B2 in 0..1
 1515	).
 1516%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1517myimpl(B1,B2) :-
 1518	( nonvar(B1) ->
 1519		( B1 == 1 ->
 1520			B2 = 1
 1521		; B1 == 0 ->
 1522			B2 in 0..1
 1523		)
 1524	; nonvar(B2) ->
 1525		( B2 == 0 ->
 1526			B1 = 0
 1527		; B2 == 1 ->
 1528			B1 in 0..1
 1529		)
 1530	;
 1531		get(B1,L1,U1,Expr1),
 1532		get(B2,L2,U2,Expr2),
 1533		put(B1,L1,U1,[myimpl(B2)|Expr1]),
 1534		put(B2,L2,U2,[myimpl2(B1)|Expr2]),
 1535		B1 in 0..1,
 1536		B2 in 0..1
 1537	).
 1538%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1539myand(X,Y,Z) :-
 1540	( nonvar(X) ->
 1541		( X == 1 ->
 1542			Y in 0..1,
 1543			Y = Z
 1544		; X == 0 ->
 1545			Y in 0..1,
 1546			Z = 0
 1547		)
 1548	; nonvar(Y) ->
 1549		myand(Y,X,Z)
 1550	; nonvar(Z) ->
 1551		( Z == 1 ->
 1552			X = 1,
 1553			Y = 1
 1554		; Z == 0 ->
 1555			X in 0..1,
 1556			Y in 0..1,
 1557			X + Y #=< 1
 1558		)
 1559	;
 1560		get(X,LX,UX,ExpX),
 1561		get(Y,LY,UY,ExpY),
 1562		get(Z,LZ,UZ,ExpZ),
 1563		put(X,LX,UX,[myand(Y,Z)|ExpX]),
 1564		put(Y,LY,UY,[myand(X,Z)|ExpY]),
 1565		put(Z,LZ,UZ,[myand2(X,Y)|ExpZ]),
 1566		[X,Y,Z] in 0..1
 1567	).
 1568
 1569%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1570myor(X,Y,Z) :-
 1571	( nonvar(X) ->
 1572		( X == 0 ->
 1573			Y in 0..1,
 1574			Y = Z
 1575		; X == 1 ->
 1576			Y in 0..1,
 1577			Z = 1
 1578		)
 1579	; nonvar(Y) ->
 1580		myor(Y,X,Z)
 1581	; nonvar(Z) ->
 1582		( Z == 0 ->
 1583			X = 0,
 1584			Y = 0
 1585		; Z == 1 ->
 1586			X in 0..1,
 1587			Y in 0..1,
 1588			X + Y #>= 1
 1589		)
 1590	;
 1591		get(X,LX,UX,ExpX),
 1592		get(Y,LY,UY,ExpY),
 1593		get(Z,LZ,UZ,ExpZ),
 1594		put(X,LX,UX,[myor(Y,Z)|ExpX]),
 1595		put(Y,LY,UY,[myor(X,Z)|ExpY]),
 1596		put(Z,LZ,UZ,[myor2(X,Y)|ExpZ]),
 1597		[X,Y,Z] in 0..1
 1598	).
 1599
 1600%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1601myxor(X,Y,Z) :-
 1602	( nonvar(X) ->
 1603		( X == 0 ->
 1604			Y in 0..1,
 1605			Y = Z
 1606		; X == 1 ->
 1607			mynot(Y,Z)
 1608		)
 1609	; nonvar(Y) ->
 1610		myxor(Y,X,Z)
 1611	; nonvar(Z) ->
 1612		( Z == 0 ->
 1613			X = Y,
 1614			[X,Y] in 0..1
 1615		; Z == 1 ->
 1616			X in 0..1,
 1617			Y in 0..1,
 1618			X + Y #= 1
 1619		)
 1620	;
 1621		get(X,LX,UX,ExpX),
 1622		get(Y,LY,UY,ExpY),
 1623		get(Z,LZ,UZ,ExpZ),
 1624		put(X,LX,UX,[myxor(Y,Z)|ExpX]),
 1625		put(Y,LY,UY,[myxor(X,Z)|ExpY]),
 1626		put(Z,LZ,UZ,[myxor2(X,Y)|ExpZ]),
 1627		[X,Y,Z] in 0..1
 1628	).
 1629
 1630
 1631%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1632get(X,L,U,Exp) :-
 1633	( get_attr(X,bounds,Attr) ->
 1634		Attr = bounds(L,U,Exp)
 1635	; var(X) ->
 1636		min_inf(L),
 1637		max_inf(U),
 1638		Exp = []
 1639	).
 1640
 1641put(X,L,U,Exp) :-
 1642	L =< U,
 1643	( L == U ->
 1644		X = L,
 1645		trigger_exps(Exp,X)
 1646	;
 1647		( get_attr(X,bounds,Attr) ->
 1648			put_attr(X,bounds,bounds(L,U,Exp)),
 1649			Attr = bounds(OldL,OldU,_),
 1650			( OldL == L, OldU == U ->
 1651				true
 1652			;
 1653				%format('\t~w in ~w .. ~w\n',[X,L,U]),
 1654				trigger_exps(Exp,X),
 1655				notify(X,bounds)
 1656			)
 1657		;
 1658			%format('\t~w in ~w .. ~w\n',[X,L,U]),
 1659			put_attr(X,bounds,bounds(L,U,Exp)),
 1660			notify(X,bounds)
 1661		)
 1662	).
 1663
 1664%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1665
 1666%	SWI-Prolog 5.7.x has unbounded arithmetic.  What to do?
 1667
 1668min_inf(Inf) :-
 1669	(   current_prolog_flag(min_integer,MInf)
 1670	->  Inf is MInf + 1
 1671	;   Inf = -9223372036854775807
 1672	).
 1673
 1674max_inf(Inf) :-
 1675	(   current_prolog_flag(max_integer,Inf)
 1676	->  true
 1677	;   Inf = 9223372036854775807
 1678	).
 1679
 1680%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1681attr_unify_hook(bounds(L,U,Exp),Other) :-
 1682	( get(Other,OL,OU,OExp) ->
 1683		NL is max(L,OL),
 1684		NU is min(U,OU),
 1685		append(Exp,OExp,NExp),
 1686		check_neqs(NExp,Other),
 1687		put(Other,NL,NU,NExp)
 1688	; % nonvar(Other) ->
 1689		Other >= L,
 1690		Other =< U,
 1691		trigger_exps(Exp,Other)
 1692	).
 1693
 1694check_neqs([],_).
 1695check_neqs([E|Es],X) :-
 1696	( E = neq(Y,_),
 1697	  X == Y ->
 1698		fail
 1699	;
 1700		check_neqs(Es,X)
 1701	).
 1702
 1703
 1704trigger_exps([],_).
 1705trigger_exps([E|Es],X) :-
 1706	trigger_exp(E,X),
 1707	trigger_exps(Es,X).
 1708
 1709trigger_exp(geq(Y,State),X) :-
 1710	( is_active(State) ->
 1711		geq(X,Y,no)
 1712	;
 1713		true
 1714	).
 1715trigger_exp(leq(Y,State),X) :-
 1716	( is_active(State) ->
 1717		leq(X,Y,no)
 1718	;
 1719		true
 1720	).
 1721trigger_exp(neq(Y,State),X) :-
 1722	( is_active(State) ->
 1723		neq(X,Y,no)
 1724	;
 1725		true
 1726	).
 1727trigger_exp(myplus(Y,Z),X) :-
 1728	myplus(X,Y,Z,no).
 1729trigger_exp(myplus2(A,B),X) :-
 1730	myplus(A,B,X,no).
 1731
 1732trigger_exp(mytimes(Y,Z),X) :-
 1733	mytimes(X,Y,Z,no).
 1734trigger_exp(mytimes2(A,B),X) :-
 1735	mytimes(A,B,X,no).
 1736
 1737trigger_exp(mymax(Y,Z),X) :-
 1738	mymax(X,Y,Z,no).
 1739trigger_exp(mymax2(X,Y),Z) :-
 1740	mymax(X,Y,Z,no).
 1741
 1742trigger_exp(mymin(Y,Z),X) :-
 1743	mymin(X,Y,Z,no).
 1744trigger_exp(mymin2(X,Y),Z) :-
 1745	mymin(X,Y,Z,no).
 1746
 1747trigger_exp(reified_leq(X,B),Y) :-
 1748	reified_geq(X,Y,B).
 1749trigger_exp(reified_geq(Y,B),X) :-
 1750	reified_geq(X,Y,B).
 1751trigger_exp(reified_geq2(X,Y),B) :-
 1752	reified_geq(X,Y,B).
 1753
 1754trigger_exp(reified_eq(Y,B),X) :-
 1755	reified_eq(X,Y,B).
 1756trigger_exp(reified_eq2(X,Y),B) :-
 1757	reified_eq(X,Y,B).
 1758
 1759trigger_exp(mynot(Y),X) :-
 1760	mynot(X,Y).
 1761
 1762trigger_exp(myimpl(Y),X) :-
 1763	myimpl(X,Y).
 1764trigger_exp(myimpl2(X),Y) :-
 1765	myimpl(X,Y).
 1766
 1767trigger_exp(myand(Y,Z),X) :-
 1768	myand(X,Y,Z).
 1769trigger_exp(myand2(X,Y),Z) :-
 1770	myand(X,Y,Z).
 1771
 1772trigger_exp(myor(Y,Z),X) :-
 1773	myor(X,Y,Z).
 1774trigger_exp(myor2(X,Y),Z) :-
 1775	myor(X,Y,Z).
 1776
 1777trigger_exp(myxor(Y,Z),X) :-
 1778	myxor(X,Y,Z).
 1779trigger_exp(myxor2(X,Y),Z) :-
 1780	myxor(X,Y,Z).
 1781
 1782trigger_exp(myabs(Y),X) :-
 1783	myabs(X,Y,no).
 1784trigger_exp(myabs2(X),Y) :-
 1785	myabs(X,Y,no).
 1786
 1787trigger_exp(mymod1(Y,Z),X) :-
 1788	mymod(X,Y,Z,no).
 1789trigger_exp(mymod2(X,Z),Y) :-
 1790	mymod(X,Y,Z,no).
 1791trigger_exp(mymod3(X,Y),Z) :-
 1792	mymod(X,Y,Z,no).
 1793
 1794trigger_exp(mydiv(Y,Z),X) :-
 1795	mydiv(X,Y,Z,no).
 1796trigger_exp(mydiv2(A,B),X) :-
 1797	mydiv(A,B,X,no).
 1798trigger_exp(mydiv3(A,B),X) :-
 1799	mydiv(A,X,B,no).
 1800
 1801trigger_exp(rel_tuple(Relation,Tuple), _) :-
 1802	( ground(Tuple) ->
 1803		memberchk(Tuple, Relation)
 1804	;
 1805		relation_unifiable(Relation, Tuple, Us),
 1806		Us \= [],
 1807		( Us = [Single] ->
 1808			Single = Tuple
 1809		;
 1810			( Us == Relation ->
 1811				true
 1812			;
 1813				tuple_domain(Tuple, Us)
 1814			)
 1815		)
 1816	).
 1817
 1818trigger_exp(serialized(Duration,Left,Right), X) :-
 1819	myserialized(Duration, Left, Right, X).
 1820
 1821
 1822memberchk_eq(X,[Y|Ys],Z) :-
 1823   (   X == Y ->
 1824       Z = Y
 1825   ;   memberchk_eq(X,Ys,Z)
 1826   ).
 1827
 1828
 1829%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1830
 1831tuples_in(Tuples, Relation) :-
 1832	ground(Relation),
 1833	bind_unique(Tuples, Relation),
 1834	approx_tuples_domain(Tuples, Relation),
 1835	tuples_freeze(Tuples, Relation).
 1836
 1837bind_unique([], _).
 1838bind_unique([Tuple|Ts], Relation) :-
 1839	relation_unifiable(Relation, Tuple, Us),
 1840	Us \= [],
 1841	( Us = [Single] ->
 1842		Single = Tuple
 1843	;
 1844		true
 1845	),
 1846	bind_unique(Ts, Relation).
 1847
 1848
 1849   % The following predicates find component-wise extrema in the relation.
 1850
 1851relation_mins_maxs(Relation, Mins, Maxs) :-
 1852	Relation = [R|_],
 1853	relation_mins_maxs(Relation, R, Mins, R, Maxs).
 1854
 1855relation_mins_maxs([], Mins, Mins, Maxs, Maxs).
 1856relation_mins_maxs([R|Rs], Mins0, Mins, Maxs0, Maxs) :-
 1857	components_mins_maxs(R, Mins0, Mins1, Maxs0, Maxs1),
 1858	relation_mins_maxs(Rs, Mins1, Mins, Maxs1, Maxs).
 1859
 1860components_mins_maxs([], [], [], [], []).
 1861components_mins_maxs([C|Cs], [Min0|Mins0], [Min|Mins], [Max0|Maxs0], [Max|Maxs]) :-
 1862	Min is min(Min0, C),
 1863	Max is max(Max0, C),
 1864	components_mins_maxs(Cs, Mins0, Mins, Maxs0, Maxs).
 1865
 1866
 1867   % Approximate the domains of each tuple variable for all tuples.
 1868   % Heuristics: Take component-wise mins/maxs of the relation.
 1869
 1870approx_tuples_domain(Tuples, Relation) :-
 1871	relation_mins_maxs(Relation, Mins, Maxs),
 1872	constrain_domains(Tuples, Mins, Maxs).
 1873
 1874constrain_domains([], _, _).
 1875constrain_domains([Tuple|Tuples], Mins, Maxs) :-
 1876	constrain_domain(Tuple, Mins, Maxs),
 1877	constrain_domains(Tuples, Mins, Maxs).
 1878
 1879constrain_domain([], [], []).
 1880constrain_domain([T|Ts], [Min|Mins], [Max|Maxs]) :-
 1881	T in Min..Max,
 1882	constrain_domain(Ts, Mins, Maxs).
 1883
 1884tuple_domain(Tuple, Relation) :-
 1885	relation_mins_maxs(Relation, Mins, Maxs),
 1886	constrain_domain(Tuple, Mins, Maxs).
 1887
 1888   % Set up the attributes for each tuple variable.
 1889   % Attributes are rel_tuple(Rel, Tuple) terms:
 1890   %    Rel: the relation of which Tuple must be an element
 1891   %    Tuple: the tuple to which this variable belongs
 1892   % Note that the variable is itself part of the Tuple of its attribute.
 1893
 1894tuple_freeze([],  _, _).
 1895tuple_freeze([T|Ts], Tuple, Relation) :-
 1896	( var(T) ->
 1897		get(T, L, U, Exp),
 1898		put(T, L, U, [rel_tuple(Relation,Tuple)|Exp])
 1899	;
 1900		true
 1901	),
 1902	tuple_freeze(Ts, Tuple, Relation).
 1903
 1904tuples_freeze([], _).
 1905tuples_freeze([Tuple|Tuples], Relation) :-
 1906	tuple_freeze(Tuple, Tuple, Relation),
 1907	tuples_freeze(Tuples, Relation).
 1908
 1909   % Find all tuples in the relation that can unify with Tuple, not
 1910   % taking into account attributes (like constraints), as that would
 1911   % trigger attr_unify_hook recursively.
 1912
 1913relation_unifiable([], _, []).
 1914relation_unifiable([R|Rs], Tuple, Us) :-
 1915	( unifiable(R, Tuple, _) ->
 1916		Us = [R|Rest]
 1917	;
 1918		Rest = Us
 1919	),
 1920	relation_unifiable(Rs, Tuple, Rest).
 1921
 1922%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 1923
 1924    % serialized/2; see Dorndorf et al. 2000, "Constraint Propagation
 1925    % Techniques for the Disjunctive Scheduling Problem"
 1926
 1927    % attribute: serialized(Duration, Left, Right)
 1928    %   Left and Right are lists of Start-Duration pairs representing
 1929    %   other tasks occupying the same resource
 1930
 1931    % Currently implements 2-b-consistency
 1932
 1933serialized(Starts, Durations) :-
 1934	pair_up(Starts, Durations, SDs),
 1935	serialize(SDs, []).
 1936
 1937
 1938pair_up([], [], []).
 1939pair_up([A|As], [B|Bs], [A-B|ABs]) :- pair_up(As, Bs, ABs).
 1940
 1941
 1942    % store attributes for serialized/2 constraint
 1943
 1944serialize([], _).
 1945serialize([Start-Duration|SDs], Left) :-
 1946	( var(Start) ->
 1947		get(Start, L, U, Exp),
 1948		put(Start, L, U, [serialized(Duration,Left,SDs)|Exp])
 1949	;
 1950		true
 1951	),
 1952	myserialized(Duration, Left, SDs, Start),
 1953	serialize(SDs, [Start-Duration|Left]).
 1954
 1955    % consistency check / propagation
 1956
 1957myserialized(Duration, Left, Right, Start) :-
 1958	myserialized(Left, Start, Duration),
 1959	myserialized(Right, Start, Duration).
 1960
 1961
 1962earliest_start_time(Start, EST) :-
 1963	( var(Start) ->
 1964		get(Start, EST, _, _)
 1965	;
 1966		EST = Start
 1967	).
 1968
 1969latest_start_time(Start, LST) :-
 1970	( var(Start) ->
 1971		get(Start, _, LST, _)
 1972	;
 1973		LST = Start
 1974	).
 1975
 1976
 1977myserialized([], _, _).
 1978myserialized([S_I-D_I|SDs], S_J, D_J) :-
 1979	( var(S_I) ->
 1980		serialize_lower_bound(S_I, D_I, Start, D_J),
 1981		( var(S_I) -> % STILL variable?
 1982			serialize_upper_bound(S_I, D_I, Start, D_J)
 1983		;
 1984			true
 1985		)
 1986	; var(S_J) ->
 1987		serialize_lower_bound(S_J, D_J, S, D_I),
 1988		( var(S_J) ->
 1989			serialize_upper_bound(S_J, D_J, S, D_I)
 1990		;
 1991			true
 1992		)
 1993	;
 1994		( S_I + D_I =< S_J ->
 1995			true
 1996		; S_J + D_J =< S_I ->
 1997			true
 1998		;
 1999			fail
 2000		)
 2001	),
 2002	myserialized(SDs, S_J, D_J).
 2003
 2004serialize_lower_bound(I, D_I, J, D_J) :-
 2005	get(I, EST_I, U, Exp),
 2006	latest_start_time(J, LST_J),
 2007	( EST_I + D_I > LST_J ->
 2008		earliest_start_time(J, EST_J),
 2009		EST is max(EST_I, EST_J+D_J),
 2010		put(I, EST, U, Exp)
 2011	;
 2012		true
 2013	).
 2014
 2015serialize_upper_bound(I, D_I, J, D_J) :-
 2016	get(I, L, LST_I, Exp),
 2017	earliest_start_time(J, EST_J),
 2018	( EST_J + D_J > LST_I ->
 2019		latest_start_time(J, LST_J),
 2020		LST is min(LST_I, LST_J-D_I),
 2021		put(I, L, LST, Exp)
 2022	;
 2023		true
 2024	).
 2025
 2026
 2027%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2028active_state(state(active)).
 2029is_active(state(active)).
 2030set_passive(State) :-
 2031	setarg(1,State,passive).
 2032
 2033%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 2034attr_portray_hook(bounds(L,U,_),_) :-
 2035	write(L..U)