View source with raw comments or as raw
    1/*  $Id$
    2
    3    Part of CLP(Q) (Constraint Logic Programming over Rationals)
    4
    5    Author:        Leslie De Koninck
    6    E-mail:        Leslie.DeKoninck@cs.kuleuven.be
    7    WWW:           http://www.swi-prolog.org
    8		   http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09
    9    Copyright (C): 2006, K.U. Leuven and
   10		   1992-1995, Austrian Research Institute for
   11		              Artificial Intelligence (OFAI),
   12			      Vienna, Austria
   13
   14    This software is based on CLP(Q,R) by Christian Holzbaur for SICStus
   15    Prolog and distributed under the license details below with permission from
   16    all mentioned authors.
   17
   18    This program is free software; you can redistribute it and/or
   19    modify it under the terms of the GNU General Public License
   20    as published by the Free Software Foundation; either version 2
   21    of the License, or (at your option) any later version.
   22
   23    This program is distributed in the hope that it will be useful,
   24    but WITHOUT ANY WARRANTY; without even the implied warranty of
   25    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   26    GNU General Public License for more details.
   27
   28    You should have received a copy of the GNU Lesser General Public
   29    License along with this library; if not, write to the Free Software
   30    Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
   31
   32    As a special exception, if you link this library with other files,
   33    compiled with a Free Software compiler, to produce an executable, this
   34    library does not by itself cause the resulting executable to be covered
   35    by the GNU General Public License. This exception does not however
   36    invalidate any other reasons why the executable file might be covered by
   37    the GNU General Public License.
   38*/
   39
   40:- module(bb_q,
   41	[
   42	    bb_inf/3,
   43	    bb_inf/4,
   44	    vertex_value/2
   45	]).   46:- use_module(library(error), [type_error/2]).   47:- use_module(bv_q,
   48	[
   49	    deref/2,
   50	    deref_var/2,
   51	    determine_active_dec/1,
   52	    inf/2,
   53	    iterate_dec/2,
   54	    sup/2,
   55	    var_with_def_assign/2
   56	]).   57:- use_module(nf_q,
   58	[
   59	    {}/1,
   60	    entailed/1,
   61	    nf/2,
   62	    nf_constant/2,
   63	    repair/2,
   64	    wait_linear/3
   65	]).   66
   67% bb_inf(Ints,Term,Inf)
   68%
   69% Finds the infimum of Term where the variables Ints are to be integers.
   70% The infimum is stored in Inf.
   71
   72bb_inf(Is,Term,Inf) :-
   73	bb_inf(Is,Term,Inf,_).
   74
   75bb_inf(Is,Term,Inf,Vertex) :-
   76	wait_linear(Term,Nf,bb_inf_internal(Is,Nf,Inf,Vertex)).
   77
   78% ---------------------------------------------------------------------
   79
   80% bb_inf_internal(Is,Lin,Inf,Vertex)
   81%
   82% Finds an infimum <Inf> for linear expression in normal form <Lin>, where
   83% all variables in <Is> are to be integers.
   84
   85% The incumbent must survive the backtracking that drives the search, but
   86% it must not survive the call itself.  It is therefore kept in a mutable
   87% term that is local to this call rather than in a global variable, which
   88% would clobber a global of the same name in the calling program and would
   89% make nested calls interfere.
   90
   91bb_inf_internal(Is,Lin,Inf,Vertex) :-
   92	State = state(none),
   93	(   bb_intern(Is,IsNf),
   94	    repair(Lin,LinR),	% bb_narrow ...
   95	    deref(LinR,Lind),
   96	    var_with_def_assign(Dep,Lind),
   97	    determine_active_dec(Lind),
   98	    bb_loop(Dep,IsNf,State),
   99	    fail
  100	;   arg(1,State,InfVal-Vertex),
  101	    {Inf =:= InfVal}
  102	).
  103
  104% bb_loop(Opt,Is,State)
  105%
  106% Minimizes the value of Opt where variables Is have to be integer values.
  107
  108bb_loop(Opt,Is,State) :-
  109	bb_reoptimize(Opt,Inf),
  110	bb_better_bound(State,Inf),
  111	vertex_value(Is,Ivs),
  112	(   bb_first_nonint(Is,Ivs,Viol,Floor,Ceiling)
  113	->  bb_branch(Viol,Floor,Ceiling),
  114	    bb_loop(Opt,Is,State)
  115	;   nb_setarg(1,State,Inf-Ivs) % new provisional optimum
  116	).
  117
  118% bb_reoptimize(Obj,Inf)
  119%
  120% Minimizes the value of Obj and puts the result in Inf.
  121% This new minimization is necessary as making a bound integer may yield a
  122% different optimum. The added inequalities may also have led to binding.
  123
  124bb_reoptimize(Obj,Inf) :-
  125	(   var(Obj)
  126	->  iterate_dec(Obj,Inf)
  127	;   Inf = Obj
  128	).
  129
  130% bb_better_bound(State,Inf)
  131%
  132% Checks if the new infimum Inf is better than the previous one (if such exists).
  133
  134bb_better_bound(State,Inf) :-
  135	arg(1,State,Best),
  136	(   Best = Inc-_
  137	->  Inf < Inc
  138	;   true
  139	).
  140
  141% bb_branch(V,U,L)
  142%
  143% Stores that V =< U or V >= L, can be used for different strategies within
  144% bb_loop/3.
  145
  146bb_branch(V,U,_) :- {V =< U}.
  147bb_branch(V,_,L) :- {V >= L}.
  148
  149% vertex_value(Vars,Values)
  150%
  151% Returns in <Values> the current values of the variables in <Vars>.
  152
  153vertex_value([],[]).
  154vertex_value([X|Xs],[V|Vs]) :-
  155	rhs_value(X,V),
  156	vertex_value(Xs,Vs).
  157
  158% rhs_value(X,Value)
  159%
  160% Returns in <Value> the current value of variable <X>.
  161
  162rhs_value(Xn,Value) :-
  163	(   nonvar(Xn)
  164	->  Value = Xn
  165	;   var(Xn)
  166	->  deref_var(Xn,Xd),
  167	    Xd = [I,R|_],
  168	    Value is R+I
  169	).
  170
  171% bb_first_nonint(Ints,Rhss,Eps,Viol,Floor,Ceiling)
  172%
  173% Finds the first variable in Ints which doesn't have an active integer bound.
  174% Rhss contain the Rhs (R + I) values corresponding to the variables.
  175% The first variable that hasn't got an active integer bound, is returned in
  176% Viol. The floor and ceiling of its actual bound is returned in Floor and Ceiling.
  177
  178bb_first_nonint([I|Is],[Rhs|Rhss],Viol,F,C) :-
  179	(   integer(Rhs)
  180	->  bb_first_nonint(Is,Rhss,Viol,F,C)
  181	;   Viol = I,
  182	    F is floor(Rhs),
  183	    C is ceiling(Rhs)
  184	).
  185
  186% bb_intern([X|Xs],[Xi|Xis])
  187%
  188% Turns the elements of the first list into integers into the second
  189% list via bb_intern/3.
  190
  191bb_intern([],[]).
  192bb_intern([X|Xs],[Xi|Xis]) :-
  193	nf(X,Xnf),
  194	bb_intern(Xnf,Xi,X),
  195	bb_intern(Xs,Xis).
  196
  197
  198% bb_intern(Nf,X,Term)
  199%
  200% Makes sure that Term which is normalized into Nf, is integer.
  201% X contains the possibly changed Term. If Term is a variable,
  202% then its bounds are hightened or lowered to the next integer.
  203% Otherwise, it is checked it Term is integer.
  204
  205bb_intern([],X,_) :-
  206	!,
  207	X = 0.
  208bb_intern([v(I,[])],X,_) :-
  209	!,
  210	integer(I),
  211	X = I.
  212bb_intern([v(1,[V^1])],X,_) :-
  213	!,
  214	V = X,
  215	bb_narrow_lower(X),
  216	bb_narrow_upper(X).
  217bb_intern(_,_,Term) :-
  218	type_error(var, Term).
  219
  220% bb_narrow_lower(X)
  221%
  222% Narrows the lower bound so that it is an integer bound.
  223% We do this by finding the infimum of X and asserting that X
  224% is larger than the first integer larger or equal to the infimum
  225% (second integer if X is to be strict larger than the first integer).
  226
  227bb_narrow_lower(X) :-
  228	(   inf(X,Inf)
  229	->  Bound is ceiling(Inf),
  230	    (   entailed(X > Bound)
  231	    ->  {X >= Bound+1}
  232	    ;   {X >= Bound}
  233	    )
  234	;   true
  235	).
  236
  237% bb_narrow_upper(X)
  238%
  239% See bb_narrow_lower/1. This predicate handles the upper bound.
  240
  241bb_narrow_upper(X) :-
  242	(   sup(X,Sup)
  243	->  Bound is floor(Sup),
  244	    (   entailed(X < Bound)
  245	    ->  {X =< Bound-1}
  246	    ;   {X =< Bound}
  247	    )
  248	;   true
  249	).
  250
  251		 /*******************************
  252		 *	       SANDBOX		*
  253		 *******************************/
  254:- multifile
  255	sandbox:safe_primitive/1.  256
  257sandbox:safe_primitive(bb_q:bb_inf(_,_,_)).
  258sandbox:safe_primitive(bb_q:bb_inf(_,_,_,_))