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
295 lines
7.1 KiB
Prolog
295 lines
7.1 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: fourmotz.pl %
|
|
% Author: Christian Holzbaur christian@ai.univie.ac.at %
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
|
|
%
|
|
% TODO -) remove syntactic redundancy first ?!!
|
|
% -) avoid the construction of the crossproduct list
|
|
% +) consider strictness in crossproduct generation !!!
|
|
%
|
|
|
|
fm_elim( Vs, Target, Pivots) :-
|
|
prefilter( Vs, Vsf),
|
|
fm_elim_int( Vsf, Target, Pivots).
|
|
|
|
prefilter( [], []).
|
|
prefilter( [V|Vs], Res) :-
|
|
( get_atts( V, -target),
|
|
occurs( V) ->
|
|
Res = [V|Tail],
|
|
put_atts( V, keep_indep),
|
|
prefilter( Vs, Tail)
|
|
;
|
|
prefilter( Vs, Res)
|
|
).
|
|
|
|
%
|
|
% the target variables are marked with an attribute, and we get a list
|
|
% of them as an argument too
|
|
%
|
|
fm_elim_int( [], _, Pivots) :- % done
|
|
unkeep( Pivots).
|
|
fm_elim_int( Vs, Target, Pivots) :-
|
|
Vs = [_|_],
|
|
( best( Vs, Best, Rest) ->
|
|
occurences( Best, Occ),
|
|
elim_min( Best, Occ, Target, Pivots, NewPivots)
|
|
; % give up
|
|
NewPivots=Pivots, Rest = []
|
|
),
|
|
fm_elim_int( Rest, Target, NewPivots).
|
|
|
|
%
|
|
% Find the variable with the smallest netto increase on the
|
|
% size of the ineq. system after its elimination
|
|
%
|
|
best( Vs, Best, Rest) :-
|
|
findall( Delta-N, fm_cp_filter( Vs, Delta, N), Deltas),
|
|
keysort( Deltas, [_-N|_]),
|
|
select_nth( Vs, N, Best, Rest).
|
|
|
|
fm_cp_filter( Vs, Delta, N) :-
|
|
length( Vs, Len),
|
|
mem( Vs,X,Vst),
|
|
get_atts( X, [-target,lin(Lin)]),
|
|
indep( Lin, X),
|
|
occurences( X, Occ),
|
|
Occ = [_|_],
|
|
% crossproduct( Occ, New, []),
|
|
% length( New, CpLnew),
|
|
cp_card( Occ, 0,Lnew),
|
|
length( Occ, Locc),
|
|
Delta is Lnew-Locc,
|
|
length( Vst, Vstl),
|
|
N is Len-Vstl.
|
|
|
|
mem( [X|Xs], X, Xs).
|
|
mem( [_|Ys], X, Xs) :- mem( Ys, X, Xs).
|
|
|
|
select_nth( List, N, Nth, Others) :-
|
|
select_nth( List, 1,N, Nth, Others).
|
|
|
|
select_nth( [X|Xs], N,N, X, Xs) :- !.
|
|
select_nth( [Y|Ys], M,N, X, [Y|Xs]) :-
|
|
M1 is M+1,
|
|
select_nth( Ys, M1,N, X, Xs).
|
|
|
|
%
|
|
% fm_detach + reverse_pivot introduce indep t_none, which
|
|
% invalidates the invariants
|
|
%
|
|
elim_min( V, Occ, Target, Pivots, NewPivots) :-
|
|
crossproduct( Occ, New, []),
|
|
activate_crossproduct( New),
|
|
reverse_pivot( Pivots),
|
|
fm_detach( Occ),
|
|
% length( Occ, Locc), length( New, Lnew), print( fm(-Locc,+Lnew)), nl,
|
|
allvars( V, All),
|
|
redundancy_vars( All), % only for New \== []
|
|
make_target_indep( Target, NewPivots),
|
|
drop_dep( All).
|
|
|
|
%
|
|
% restore NF by reverse pivoting
|
|
%
|
|
reverse_pivot( []).
|
|
reverse_pivot( [I:D|Ps]) :-
|
|
get_atts( D, type(Dt)),
|
|
put_atts( D, -keep), % no longer
|
|
pivot( D, I, Dt),
|
|
reverse_pivot( Ps).
|
|
|
|
unkeep( []).
|
|
unkeep( [_:D|Ps]) :-
|
|
put_atts( D, -keep),
|
|
drop_dep_one( D),
|
|
unkeep( Ps).
|
|
|
|
|
|
%
|
|
% All we drop are bounds
|
|
%
|
|
fm_detach( []).
|
|
fm_detach( [V:_|Vs]) :-
|
|
detach_bounds( V),
|
|
fm_detach( Vs).
|
|
|
|
%
|
|
% Todo: maybe bulk_basis_add
|
|
%
|
|
activate_crossproduct( []).
|
|
activate_crossproduct( [lez(Strict,Lin)|News]) :-
|
|
arith_eval( 0, Z),
|
|
var_with_def_intern( t_u(Z), Var, Lin, Strict),
|
|
basis_add( Var, _),
|
|
activate_crossproduct( News).
|
|
|
|
% ------------------------------------------------------------------------------
|
|
|
|
crossproduct( []) --> [].
|
|
crossproduct( [A|As]) -->
|
|
crossproduct( As, A),
|
|
crossproduct( As).
|
|
|
|
crossproduct( [], _) --> [].
|
|
crossproduct( [B:Kb|Bs], A:Ka) -->
|
|
{
|
|
get_atts( A, [type(Ta),lin(LinA),strictness(Sa)]),
|
|
get_atts( B, [type(Tb),lin(LinB),strictness(Sb)]),
|
|
arith_eval( -Kb/Ka, K),
|
|
add_linear_f1( LinA, K, LinB, Lin)
|
|
},
|
|
( { arith_eval( K > 0) } -> % signs were opposite
|
|
{ Strict is Sa \/ Sb },
|
|
cross_lower( Ta, Tb, K, Lin, Strict),
|
|
cross_upper( Ta, Tb, K, Lin, Strict)
|
|
; % La =< A =< Ua -> -Ua =< -A =< -La
|
|
{
|
|
flip( Ta, Taf),
|
|
flip_strict( Sa, Saf),
|
|
Strict is Saf \/ Sb
|
|
},
|
|
cross_lower( Taf, Tb, K, Lin, Strict),
|
|
cross_upper( Taf, Tb, K, Lin, Strict)
|
|
),
|
|
crossproduct( Bs, A:Ka).
|
|
|
|
cross_lower( Ta, Tb, K, Lin, Strict) -->
|
|
{
|
|
lower( Ta, La),
|
|
lower( Tb, Lb),
|
|
!,
|
|
arith_eval(K*La+Lb,L),
|
|
normalize_scalar( L, Ln),
|
|
arith_eval( -1, Mone),
|
|
add_linear_f1( Lin, Mone, Ln, Lhs),
|
|
Sl is Strict >> 1 % normalize to upper bound
|
|
},
|
|
[ lez(Sl,Lhs) ].
|
|
cross_lower( _, _, _, _, _) --> [].
|
|
|
|
cross_upper( Ta, Tb, K, Lin, Strict) -->
|
|
{
|
|
upper( Ta, Ua),
|
|
upper( Tb, Ub),
|
|
!,
|
|
arith_eval(-(K*Ua+Ub),U),
|
|
normalize_scalar( U, Un),
|
|
add_linear_11( Un, Lin, Lhs),
|
|
Su is Strict /\ 2'01 % normalize to upper bound
|
|
},
|
|
[ lez(Su,Lhs) ].
|
|
cross_upper( _, _, _, _, _) --> [].
|
|
|
|
lower( t_l(L), L).
|
|
lower( t_lu(L,_), L).
|
|
lower( t_L(L), L).
|
|
lower( t_Lu(L,_), L).
|
|
lower( t_lU(L,_), L).
|
|
|
|
upper( t_u(U), U).
|
|
upper( t_lu(_,U), U).
|
|
upper( t_U(U), U).
|
|
upper( t_Lu(_,U), U).
|
|
upper( t_lU(_,U), U).
|
|
|
|
flip( t_l(X), t_u(X)).
|
|
flip( t_u(X), t_l(X)).
|
|
flip( t_lu(X,Y),t_lu(Y,X)).
|
|
flip( t_L(X), t_u(X)).
|
|
flip( t_U(X), t_l(X)).
|
|
flip( t_lU(X,Y),t_lu(Y,X)).
|
|
flip( t_Lu(X,Y),t_lu(Y,X)).
|
|
|
|
flip_strict( 2'00, 2'00).
|
|
flip_strict( 2'01, 2'10).
|
|
flip_strict( 2'10, 2'01).
|
|
flip_strict( 2'11, 2'11).
|
|
|
|
cp_card( [], Ci,Ci).
|
|
cp_card( [A|As], Ci,Co) :-
|
|
cp_card( As, A, Ci,Cii),
|
|
cp_card( As, Cii,Co).
|
|
|
|
cp_card( [], _, Ci,Ci).
|
|
cp_card( [B:Kb|Bs], A:Ka, Ci,Co) :-
|
|
get_atts( A, type(Ta)),
|
|
get_atts( B, type(Tb)),
|
|
arith_eval( -Kb/Ka, K),
|
|
( arith_eval( K > 0) -> % signs were opposite
|
|
cp_card_lower( Ta, Tb, Ci,Cii),
|
|
cp_card_upper( Ta, Tb, Cii,Ciii)
|
|
;
|
|
flip( Ta, Taf),
|
|
cp_card_lower( Taf, Tb, Ci,Cii),
|
|
cp_card_upper( Taf, Tb, Cii,Ciii)
|
|
),
|
|
cp_card( Bs, A:Ka, Ciii,Co).
|
|
|
|
cp_card_lower( Ta, Tb, Si,So) :-
|
|
lower( Ta, _),
|
|
lower( Tb, _),
|
|
!,
|
|
So is Si+1.
|
|
cp_card_lower( _, _, Si,Si).
|
|
|
|
cp_card_upper( Ta, Tb, Si,So) :-
|
|
upper( Ta, _),
|
|
upper( Tb, _),
|
|
!,
|
|
So is Si+1.
|
|
cp_card_upper( _, _, Si,Si).
|
|
|
|
% ------------------------------------------------------------------------------
|
|
|
|
|
|
|
|
occurences( V, Occ) :-
|
|
allvars( V, All),
|
|
occurences( All, V, Occ).
|
|
|
|
occurences( De, _, []) :- var( De), !.
|
|
occurences( [D|De], V, Occ) :-
|
|
( get_atts( D, [lin(Lin),type(Type)]),
|
|
occ_type_filter( Type),
|
|
nf_coeff_of( Lin, V, K) ->
|
|
Occ = [D:K|Occt],
|
|
occurences( De, V, Occt)
|
|
;
|
|
occurences( De, V, Occ)
|
|
).
|
|
|
|
occ_type_filter( t_l(_)).
|
|
occ_type_filter( t_u(_)).
|
|
occ_type_filter( t_lu(_,_)).
|
|
occ_type_filter( t_L(_)).
|
|
occ_type_filter( t_U(_)).
|
|
occ_type_filter( t_lU(_,_)).
|
|
occ_type_filter( t_Lu(_,_)).
|
|
|
|
%
|
|
% occurs( V) :- occurences( V, Occ), Occ = [_|_].
|
|
%
|
|
occurs( V) :-
|
|
allvars( V, All),
|
|
occurs( All, V).
|
|
|
|
occurs( De, _) :- var( De), !, fail.
|
|
occurs( [D|De], V) :-
|
|
( get_atts( D, [lin(Lin),type(Type)]),
|
|
occ_type_filter( Type),
|
|
nf_coeff_of( Lin, V, _) ->
|
|
true
|
|
;
|
|
occurs( De, V)
|
|
).
|