1/*
    2
    3    Part of CLP(Q,R) (Constraint Logic Programming over Rationals and Reals)
    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(clpcd_redund,
   41	[
   42	    redundancy_vars/2,
   43	    systems/3
   44	]).   45
   46:- use_module(library(clpcd/domain_ops)).   47:- use_module(library(clpcd/bv)).   48:- use_module(library(clpcd/nf)).   49:- use_module(library(clpcd/solve)).   50
   51%
   52% redundancy removal (semantic definition)
   53%
   54% done:
   55%	+) deal with active bounds
   56%	+) indep t_[lu] -> t_none invalidates invariants (fixed)
   57%
   58
   59% systems(Vars,SystemsIn,SystemsOut)
   60%
   61% Returns in SystemsOut the different classes to which variables in Vars
   62% belong. Every class only appears once in SystemsOut.
   63
   64systems([],Si,Si).
   65systems([V|Vs],Si,So) :-
   66	(   var(V),
   67	    get_attr(V,clpcd_itf,Att),
   68	    arg(6,Att,class(C)),
   69	    not_memq(Si,C)
   70	->  systems(Vs,[C|Si],So)
   71	;   systems(Vs,Si,So)
   72	).
   73
   74% not_memq(Lst,El)
   75%
   76% Succeeds if El is not a member of Lst (does not use unification).
   77
   78not_memq([],_).
   79not_memq([Y|Ys],X) :-
   80	X \== Y,
   81	not_memq(Ys,X).
   82
   83% redundancy_vars(Vs, CLP)
   84%
   85% Does the same thing as redundancy_vs/2 but has some extra timing facilities that
   86% may be used.
   87
   88redundancy_vars(Vs, CLP) :-
   89	!,
   90	redundancy_vs(Vs, CLP).
   91redundancy_vars(Vs, CLP) :-
   92	statistics(runtime,[Start|_]),
   93	redundancy_vs(Vs, CLP),
   94	statistics(runtime,[End|_]),
   95	Duration is End-Start,
   96	format(user_error,"% Redundancy elimination took ~d msec~n",Duration).
   97
   98
   99% redundancy_vs(Vs, CLP)
  100%
  101% Removes redundant bounds from the variables in Vs via redundant/3
  102
  103redundancy_vs(Vs, _) :-
  104	var(Vs),
  105	!.
  106redundancy_vs([], _).
  107redundancy_vs([V|Vs], CLP) :-
  108	(   get_attr(V,clpcd_itf,Att),
  109	    arg(2,Att,type(Type)),
  110	    arg(3,Att,strictness(Strict)),
  111	    redundant(Type,CLP,V,Strict)
  112	->  redundancy_vs(Vs, CLP)
  113	;   redundancy_vs(Vs, CLP)
  114	).
  115
  116% redundant(Type,CLP,Var,Strict)
  117%
  118% Removes redundant bounds from variable Var with type Type and strictness Strict.
  119% A redundant bound is one that is satisfied anyway (so adding the inverse of the bound
  120% makes the system infeasible. This predicate can either fail or succeed but a success
  121% doesn't necessarily mean a redundant bound.
  122
  123redundant(t_l(L),CLP,X,Strict) :-
  124	get_attr(X,clpcd_itf,Att),
  125	arg(1,Att,CLP),
  126	detach_bounds(CLP,X),	% drop temporarily
  127	% if not redundant, backtracking will restore bound
  128	negate_l(Strict,CLP,L,X),
  129	red_t_l.	% negate_l didn't fail, redundant bound
  130redundant(t_u(U),CLP,X,Strict) :-
  131	get_attr(X,clpcd_itf,Att),
  132	arg(1,Att,CLP),
  133	detach_bounds(CLP,X),
  134	negate_u(Strict,CLP,U,X),
  135	red_t_u.
  136redundant(t_lu(L,U),CLP,X,Strict) :-
  137	strictness_parts(Strict,Sl,Su),
  138	(   get_attr(X,clpcd_itf,Att),
  139	    arg(1,Att,CLP),
  140	    setarg(2,Att,type(t_u(U))),
  141	    setarg(3,Att,strictness(Su)),
  142	    negate_l(Strict,CLP,L,X)
  143	->  red_t_l,
  144	    (   redundant(t_u(U),CLP,X,Strict)
  145	    ->  true
  146	    ;   true
  147	    )
  148	;   get_attr(X,clpcd_itf,Att),
  149	    arg(1,Att,CLP),
  150	    setarg(2,Att,type(t_l(L))),
  151	    setarg(3,Att,strictness(Sl)),
  152	    negate_u(Strict,CLP,U,X)
  153	->  red_t_u
  154	;   true
  155	).
  156redundant(t_L(L),CLP,X,Strict) :-
  157	get_attr(X,clpcd_itf,Att),
  158	arg(1,Att,CLP),
  159	eval_d(CLP, -L, Bound),
  160	intro_at(CLP, X, Bound, t_none),	% drop temporarily
  161	detach_bounds(CLP,X),
  162	negate_l(Strict,CLP,L,X),
  163	red_t_L.
  164redundant(t_U(U),CLP,X,Strict) :-
  165	get_attr(X,clpcd_itf,Att),
  166	arg(1,Att,CLP),
  167	eval_d(CLP, -U, Bound),
  168	intro_at(CLP, X, Bound, t_none),	% drop temporarily
  169	detach_bounds(CLP,X),
  170	negate_u(Strict,CLP,U,X),
  171	red_t_U.
  172redundant(t_Lu(L,U),CLP,X,Strict) :-
  173	strictness_parts(Strict,Sl,Su),
  174	(   eval_d(CLP, -L, Bound),
  175	    get_attr(X,clpcd_itf,Att),
  176	    arg(1,Att,CLP),
  177	    intro_at(CLP, X, Bound, t_u(U)),
  178	    get_attr(X,clpcd_itf,Att2), % changed?
  179	    setarg(3,Att2,strictness(Su)),
  180	    negate_l(Strict,CLP,L,X)
  181	->  red_t_l,
  182	    (   redundant(t_u(U),CLP,X,Strict)
  183	    ->  true
  184	    ;   true
  185	    )
  186	;   get_attr(X,clpcd_itf,Att),
  187	    arg(1,Att,CLP),
  188	    setarg(2,Att,type(t_L(L))),
  189	    setarg(3,Att,strictness(Sl)),
  190	    negate_u(Strict,CLP,U,X)
  191	->  red_t_u
  192	;   true
  193	).
  194redundant(t_lU(L,U),CLP,X,Strict) :-
  195	strictness_parts(Strict,Sl,Su),
  196	(   get_attr(X,clpcd_itf,Att),
  197	    arg(1,Att,CLP),
  198	    setarg(2,Att,type(t_U(U))),
  199	    setarg(3,Att,strictness(Su)),
  200	    negate_l(Strict,CLP,L,X)
  201	->  red_t_l,
  202	    (   redundant(t_U(U),CLP,X,Strict)
  203	    ->  true
  204	    ;   true
  205	    )
  206	;   get_attr(X,clpcd_itf,Att),
  207	    arg(1,Att,CLP),
  208	    eval_d(CLP, -U, Bound),
  209	    intro_at(CLP, X, Bound, t_l(L)),
  210	    get_attr(X,clpcd_itf,Att2), % changed?
  211	    setarg(3,Att2,strictness(Sl)),
  212	    negate_u(Strict,CLP,U,X)
  213	->  red_t_u
  214	;   true
  215	).
  216
  217% strictness_parts(Strict,Lower,Upper)
  218%
  219% Splits strictness Strict into two parts: one related to the lowerbound and
  220% one related to the upperbound.
  221
  222strictness_parts(Strict,Lower,Upper) :-
  223	Lower is Strict /\ 2,
  224	Upper is Strict /\ 1.
  225
  226% negate_l(Strict,Lowerbound,X)
  227%
  228% Fails if X does not necessarily satisfy the lowerbound and strictness
  229% In other words: if adding the inverse of the lowerbound (X < L or X =< L)
  230% does not result in a failure, this predicate fails.
  231
  232negate_l(0,CLP,L,X) :-
  233	add_constraint(L > X, CLP),
  234	!,
  235	fail.
  236negate_l(1,CLP,L,X) :-
  237	add_constraint(L > X, CLP),
  238	!,
  239	fail.
  240negate_l(2,CLP,L,X) :-
  241	add_constraint(L >= X, CLP),
  242	!,
  243	fail.
  244negate_l(3,CLP,L,X) :-
  245	add_constraint(L >= X, CLP),
  246	!,
  247	fail.
  248negate_l(_,_,_,_).
  249
  250% negate_u(Strict,Upperbound,X)
  251%
  252% Fails if X does not necessarily satisfy the upperbound and strictness
  253% In other words: if adding the inverse of the upperbound (X > U or X >= U)
  254% does not result in a failure, this predicate fails.
  255
  256negate_u(0,CLP,U,X) :-
  257	add_constraint(U < X, CLP),
  258	!,
  259	fail.
  260negate_u(1,CLP,U,X) :-
  261	add_constraint(U =< X, CLP),
  262	!,
  263	fail.
  264negate_u(2,CLP,U,X) :-
  265        add_constraint(U < X, CLP),
  266	!,
  267	fail.
  268negate_u(3,CLP,U,X) :-
  269	add_constraint(U =< X, CLP),
  270	!,
  271	fail.
  272negate_u(_,_,_,_).
  273
  274% Profiling: these predicates are called during redundant and can be used
  275% to count the number of redundant bounds.
  276
  277red_t_l.
  278red_t_u.
  279red_t_L.
  280red_t_U