%% ipkg_configuration_model.lp --- smodels program for ipkg
%                                  configuration 
% Author: Tommi Syrjänen <tommi.syrjanen@hut.fi>
%
% version 1.2 (23.11.2001)
%
% Usage:
%   lparse -d none ipkg_configuration_model.lp data.lp user.lp | smodels
%
% Where 'data.lp' is the package data file and 'user.lp' contains the
% user requirements.
%
% The output is a configuration where an atom in(P) is true if the
% package P is in the configuration. 
% #option -dn.

% Declare the version comparison function. 
function vc.

const size_limit = 32000. % in KB

use_size_limits. % Comment out when size limits are not used

% In ipkg, all packages are software packages
package(X) :- software(X).


%% A package may be in a configuration if it is justified
{ in(X) } :- package(X), justified(X).
{ in(X,Y) } :- available_version(X,Y), justified(X,Y).

% A chosen package increases the installed size by its size:
in_size(P, V, S) :-
    size(P, V, S),
    in(P, V).

% weight in_size(P, V, X) = X.

%%% CONSTRAINTS

%% Dependency
 :- depends(P1, V1, C),
    in(P1, V1),
    not satisfied(C).

%% Conflict
 :- conflicts(P1, V1, C),
   in(P1, V1),
   satisfied(C).

% It is an error if a required package is not in
 :- priority(P, required),
    not in(P),
    package(P).

% It is an error if user requirements are not followed:
 :- user_include(P),
    not in(P).

 :- user_include(P, V),
    not in(P, V).

 :- user_exclude(P),
    in(P).

 :- user_exclude(P, V),
    in(P, V).

% If a software package is in, exactly one version of it should be in
% the configuration:
 :- { in(P, V) : available_version(P, V) } 0,
     in(P),
     software(P).

 :- 2 { in(P, V) : available_version(P, V) },
     in(P),
     software(P).


% Combined sizes of the installed packages should not be too big
 :- size_limit [ in_size(P, V, S) : size(P, V, S) ],
    use_size_limits.

%%% VERSION CLAUSES

% When is a package in a version clause
in_clause(C, P, V) :-
    any_clause(C, P),
    available_version(P, V).

in_clause(C, P, V_2) :-
    op_clause(C, P, Op, V_1),
    available_version(P, V_2),
    vc(Op, V_2, V_1).

nonempty(C) :-
    in_clause(C, P, V).

% A version clause is satisfied if one of its packages is in
satisfied(C) :-
    in_clause(C, P, V),
    in(P, V).



%%% JUSTIFICATIONS

% High-priority packages are always justified.
high_priority(required).
high_priority(important). % <- comment out if not wanted
high_priority(standard).

justified(X) :-
    priority(X, Y),
    high_priority(Y).

% A justified package justifies all its available versions and vice
% versa:

justified(P, V) :-
    justified(P),
    available_version(P, V).

justified(P) :-
    justified(P, V),
    available_version(P, V).

% A selected package is justified
justified(P) :- user_include(P).
justified(P, V) :- user_include(P, V).


% An unsatisfied dependency justifies one package satisfying the
% dependency:
1 { justifies(P_1, V_1, P_2, V_2) : in_clause(C, P_2, V_2)
    } 1 :-
    in(P_1, V_1),
    depends(P_1, V_1, C),
    available_version(P_1, V_1).

1 { justifies(P_1, V_1, P_2, V_2) : in_clause(C, P_2, V_2)
    } 1 :-
    in(P_1, V_1),
    recommends(P_1, V_1, C),
    nonempty(C),
    available_version(P_1, V_1).


1 { justifies(P_1, V_1, P_2, V_2) : in_clause(C, P_2, V_2)
    } 1 :-
    in(P_1, V_1),
    suggests(P_1, V_1, C),
    nonempty(C),
    available_version(P_1, V_1).


justified(P_2, V_2) :-
    justifies(P_1, V_1, P_2, V_2),
    may_justify(P_1, V_1, P_2, V_2).

may_justify(P_1, V_1, P_2, V_2) :-
    depends(P_1, V_1, C),
    in_clause(C, P_2, V_2).

may_justify(P_1, V_1, P_2, V_2) :-
    recommends(P_1, V_1, C),
    in_clause(C, P_2, V_2).

may_justify(P_1, V_1, P_2, V_2) :-
    suggests(P_1, V_1, C),
    in_clause(C, P_2, V_2).


hide justified(_, _).
hide justified(_).