This repository has been archived on 2023-08-20. You can view files and clone it, but cannot push or open issues or pull requests.
vsc e5f4633c39 This commit was generated by cvs2svn to compensate for changes in r4,
which included commits to RCS files with non-trunk default branches.


git-svn-id: https://yap.svn.sf.net/svnroot/yap/trunk@5 b08c6af1-5177-4d33-ba66-4b1c6b8b522a
2001-04-09 19:54:03 +00:00

158 lines
4.0 KiB
Prolog

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% clp(q,r) version 1.3.2 %
% %
% (c) Copyright 1992,1993,1994,1995 %
% Austrian Research Institute for Artificial Intelligence (OFAI) %
% Schottengasse 3 %
% A-1010 Vienna, Austria %
% %
% File: redund.pl %
% Author: Christian Holzbaur christian@ai.univie.ac.at %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% redundancy removal (semantic definition)
%
% done:
% +) deal with active bounds
% +) indep t_[lu] -> t_none invalidates invariants (fixed)
%
%
% O(n^2), use sort later
%
systems( [], Si, Si).
systems( [V|Vs], Si, So) :-
( var(V), get_atts( V, class(C)),
not_memq( Si, C) ->
systems( Vs, [C|Si], So)
;
systems( Vs, Si, So)
).
not_memq( [], _).
not_memq( [Y|Ys], X) :-
X \== Y,
not_memq( Ys, X).
redundancy_systems( []).
redundancy_systems( [S|Sys]) :-
class_allvars( S, All),
redundancy_vs( All),
redundancy_systems( Sys).
redundancy_vars( Vs) :- !, redundancy_vs( Vs).
redundancy_vars( Vs) :-
statistics( runtime, [Start|_]),
redundancy_vs( Vs),
statistics( runtime, [End|_]),
Duration is End-Start,
format( user_error, "% Redundancy elimination took ~d msec~n", Duration).
%
% remove redundant bounds from variables
%
redundancy_vs( Vs) :- var( Vs), !.
redundancy_vs( []).
redundancy_vs( [V|Vs]) :-
( get_atts( V, [type(Type),strictness(Strict)]),
redundant( Type, V, Strict) ->
redundancy_vs( Vs)
;
redundancy_vs( Vs)
).
redundant( t_l(L), X, Strict) :-
detach_bounds( X), % drop temporarily
negate_l( Strict, L, X),
red_t_l.
redundant( t_u(U), X, Strict) :-
detach_bounds( X),
negate_u( Strict, U, X),
red_t_u.
redundant( t_lu(L,U), X, Strict) :-
strictness_parts( Strict, Sl, Su),
( put_atts( X, [type(t_u(U)),strictness(Su)]),
negate_l( Strict, L, X) ->
red_t_l,
( redundant( t_u(U), X, Strict) -> true ; true )
; put_atts( X, [type(t_l(L)),strictness(Sl)]),
negate_u( Strict, U, X) ->
red_t_u
;
true
).
redundant( t_L(L), X, Strict) :-
arith_eval( -L, Bound),
intro_at( X, Bound, t_none), % drop temporarily
detach_bounds( X),
negate_l( Strict, L, X),
red_t_L.
redundant( t_U(U), X, Strict) :-
arith_eval( -U, Bound),
intro_at( X, Bound, t_none), % drop temporarily
detach_bounds( X),
negate_u( Strict, U, X),
red_t_U.
redundant( t_Lu(L,U), X, Strict) :-
strictness_parts( Strict, Sl, Su),
( arith_eval( -L, Bound),
intro_at( X, Bound, t_u(U)),
put_atts( X, strictness(Su)),
negate_l( Strict, L, X) ->
red_t_l,
( redundant( t_u(U), X, Strict) -> true ; true )
; put_atts( X, [type(t_L(L)),strictness(Sl)]),
negate_u( Strict, U, X) ->
red_t_u
;
true
).
redundant( t_lU(L,U), X, Strict) :-
strictness_parts( Strict, Sl, Su),
( put_atts( X, [type(t_U(U)),strictness(Su)]),
negate_l( Strict, L, X) ->
red_t_l,
( redundant( t_U(U), X, Strict) -> true ; true )
; arith_eval( -U, Bound),
intro_at( X, Bound, t_l(L)),
put_atts( X, strictness(Sl)),
negate_u( Strict, U, X) ->
red_t_u
;
true
).
strictness_parts( Strict, Lower, Upper) :-
Lower is Strict /\ 2'10,
Upper is Strict /\ 2'01.
%
% encapsulation via \+ (unfolded to avoid metacall)
%
/**/
negate_l( 2'00, L, X) :- { L > X }, !, fail.
negate_l( 2'01, L, X) :- { L > X }, !, fail.
negate_l( 2'10, L, X) :- { L >= X }, !, fail.
negate_l( 2'11, L, X) :- { L >= X }, !, fail.
negate_l( _, _, _).
negate_u( 2'00, U, X) :- { U < X }, !, fail.
negate_u( 2'01, U, X) :- { U =< X }, !, fail.
negate_u( 2'10, U, X) :- { U < X }, !, fail.
negate_u( 2'11, U, X) :- { U =< X }, !, fail.
negate_u( _, _, _).
/**/
%
% profiling
%
red_t_l.
red_t_u.
red_t_L.
red_t_U.