e5f4633c39
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
158 lines
4.0 KiB
Prolog
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.
|
|
|
|
|