%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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) ).