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