path: root/lib/spack/spack/solver/concretize.lp

% Copyright 2013-2023 Lawrence Livermore National Security, LLC and other
% Spack Project Developers. See the top-level COPYRIGHT file for details.
%
% SPDX-License-Identifier: (Apache-2.0 OR MIT)

%=============================================================================
% This logic program implements Spack's concretizer
%=============================================================================

% ID of the nodes in the "root" link-run sub-DAG
#const min_dupe_id = 0.

#const link_run = 0.
#const direct_link_run =1.
#const direct_build = 2.

% Allow clingo to create nodes
{ attr("node", node(0..X-1, Package))         } :- max_dupes(Package, X), not virtual(Package).
{ attr("virtual_node", node(0..X-1, Package)) } :- max_dupes(Package, X), virtual(Package).

% Integrity constraints on DAG nodes
:- attr("root", PackageNode), not attr("node", PackageNode).
:- attr("version", PackageNode, _), not attr("node", PackageNode), not attr("virtual_node", PackageNode).
:- attr("node_version_satisfies", PackageNode), not attr("node", PackageNode).
:- attr("hash", PackageNode, _), not attr("node", PackageNode).
:- attr("node_platform", PackageNode, _), not attr("node", PackageNode).
:- attr("node_os", PackageNode, _), not attr("node", PackageNode).
:- attr("node_target", PackageNode, _), not attr("node", PackageNode).
:- attr("node_compiler_version", PackageNode, _, _), not attr("node", PackageNode).
:- attr("variant_value", PackageNode, _, _), not attr("node", PackageNode).
:- attr("node_flag_compiler_default", PackageNode), not attr("node", PackageNode).
:- attr("node_flag", PackageNode, _, _), not attr("node", PackageNode).
:- attr("node_flag_source", PackageNode, _, _), not attr("node", PackageNode).
:- attr("no_flags", PackageNode, _), not attr("node", PackageNode).
:- attr("external_spec_selected", PackageNode, _), not attr("node", PackageNode).
:- attr("depends_on", ParentNode, _, _), not attr("node", ParentNode).
:- attr("depends_on", _, ChildNode, _), not attr("node", ChildNode).
:- attr("node_flag_source", ParentNode, _, _), not attr("node", ParentNode).
:- attr("node_flag_source", _, _, ChildNode), not attr("node", ChildNode).

:- attr("virtual_node", VirtualNode), not provider(_, VirtualNode).
:- provider(_, VirtualNode), not attr("virtual_node", VirtualNode).
:- provider(PackageNode, _), not attr("node", PackageNode).

:- attr("root", node(ID, PackageNode)), ID > min_dupe_id.

% Nodes in the "root" unification set cannot depend on non-root nodes if the dependency is "link" or "run"
:- attr("depends_on", node(min_dupe_id, Package), node(ID, _), "link"), ID != min_dupe_id, unification_set("root", node(min_dupe_id, Package)).
:- attr("depends_on", node(min_dupe_id, Package), node(ID, _), "run"),  ID != min_dupe_id, unification_set("root", node(min_dupe_id, Package)).

% Rules on "unification sets", i.e. on sets of nodes allowing a single configuration of any given package
unify(SetID, PackageName) :- unification_set(SetID, node(_, PackageName)).
:- 2 { unification_set(SetID, node(_, PackageName)) }, unify(SetID, PackageName).

unification_set("root", PackageNode) :- attr("root", PackageNode).
unification_set(SetID, ChildNode) :- attr("depends_on", ParentNode, ChildNode, Type), Type != "build", unification_set(SetID, ParentNode).

unification_set(("build", node(X, Child)), node(X, Child))
  :- attr("depends_on", ParentNode, node(X, Child), Type),
     Type == "build",
     multiple_unification_sets(Child),
     unification_set(SetID, ParentNode).

unification_set("generic_build", node(X, Child))
  :- attr("depends_on", ParentNode, node(X, Child), Type),
     Type == "build",
     not multiple_unification_sets(Child),
     unification_set(_, ParentNode).

unification_set(SetID, VirtualNode)
  :- provider(PackageNode, VirtualNode),
     unification_set(SetID, PackageNode).

% Do not allow split dependencies, for now. This ensures that we don't construct graphs where e.g.
% a python extension depends on setuptools@63.4 as a run dependency, but uses e.g. setuptools@68
% as a build dependency.
%
% We'll need to relax the rule before we get to actual cross-compilation
:- depends_on(ParentNode, node(X, Dependency)), depends_on(ParentNode, node(Y, Dependency)), X < Y.


#defined multiple_unification_sets/1.

%----
% Rules to break symmetry and speed-up searches
%----

% In the "root" unification set only ID = 0 are allowed
:- unification_set("root", node(ID, _)), ID != 0.

% In the "root" unification set we allow only packages from the link-run possible subDAG
:- unification_set("root", node(_, Package)), not possible_in_link_run(Package), not virtual(Package).

% Each node must belong to at least one unification set
:- attr("node", PackageNode), not unification_set(_, PackageNode).

% Cannot have a node with an ID, if lower ID of the same package are not used
:- attr("node", node(ID1, Package)),
   not attr("node", node(ID2, Package)),
   max_dupes(Package, X), ID1=0..X-1, ID2=0..X-1, ID2 < ID1.

:- attr("virtual_node", node(ID1, Package)),
   not attr("virtual_node", node(ID2, Package)),
   max_dupes(Package, X), ID1=0..X-1, ID2=0..X-1, ID2 < ID1.

%-----------------------------------------------------------------------------
% Map literal input specs to facts that drive the solve
%-----------------------------------------------------------------------------

% TODO: literals, at the moment, can only influence the "root" unification set. This needs to be extended later.

% Node attributes that have multiple node arguments (usually, only the first argument is a node)
multiple_nodes_attribute("node_flag_source").
multiple_nodes_attribute("depends_on").
multiple_nodes_attribute("virtual_on_edge").
multiple_nodes_attribute("provider_set").

% Map constraint on the literal ID to facts on the node
attr(Name, node(min_dupe_id, A1))             :- literal(LiteralID, Name, A1), solve_literal(LiteralID).
attr(Name, node(min_dupe_id, A1), A2)         :- literal(LiteralID, Name, A1, A2), solve_literal(LiteralID), not multiple_nodes_attribute(Name).
attr(Name, node(min_dupe_id, A1), A2, A3)     :- literal(LiteralID, Name, A1, A2, A3), solve_literal(LiteralID), not multiple_nodes_attribute(Name).
attr(Name, node(min_dupe_id, A1), A2, A3, A4) :- literal(LiteralID, Name, A1, A2, A3, A4), solve_literal(LiteralID).

% Special cases where nodes occur in arguments other than A1
attr("node_flag_source", node(min_dupe_id, A1), A2, node(min_dupe_id, A3)) :- literal(LiteralID, "node_flag_source", A1, A2, A3), solve_literal(LiteralID).
attr("depends_on",       node(min_dupe_id, A1), node(min_dupe_id, A2), A3) :- literal(LiteralID, "depends_on",       A1, A2, A3), solve_literal(LiteralID).

attr("virtual_node", node(min_dupe_id, Virtual))                              :- literal(LiteralID, "provider_set", _,        Virtual), solve_literal(LiteralID).
attr("provider_set", node(min_dupe_id, Provider), node(min_dupe_id, Virtual)) :- literal(LiteralID, "provider_set", Provider, Virtual), solve_literal(LiteralID).
provider(node(min_dupe_id, Provider), node(min_dupe_id, Virtual))             :- literal(LiteralID, "provider_set", Provider, Virtual), solve_literal(LiteralID).

% Discriminate between "roots" that have been explicitly requested, and roots that are deduced from "virtual roots"
explicitly_requested_root(node(min_dupe_id, A1)) :- literal(LiteralID, "root", A1), solve_literal(LiteralID).

#defined concretize_everything/0.
#defined literal/1.
#defined literal/3.
#defined literal/4.
#defined literal/5.
#defined literal/6.

% Attributes for node packages which must have a single value
attr_single_value("version").
attr_single_value("node_platform").
attr_single_value("node_os").
attr_single_value("node_target").

% Error when no attribute is selected
error(100, no_value_error, Attribute, Package)
  :- attr("node", node(ID, Package)),
     attr_single_value(Attribute),
     not attr(Attribute, node(ID, Package), _).

% Error when multiple attr need to be selected
error(100, multiple_values_error, Attribute, Package)
  :- attr("node", node(ID, Package)),
     attr_single_value(Attribute),
     2 { attr(Attribute, node(ID, Package), Value) }.

%-----------------------------------------------------------------------------
% Version semantics
%-----------------------------------------------------------------------------

% Versions are declared with a weight and an origin, which indicates where the
% version was declared (e.g. "package_py" or "external").
pkg_fact(Package, version_declared(Version, Weight)) :- pkg_fact(Package, version_declared(Version, Weight, _)).

% We can't emit the same version **with the same weight** from two different sources
:- pkg_fact(Package, version_declared(Version, Weight, Origin1)),
   pkg_fact(Package, version_declared(Version, Weight, Origin2)),
   Origin1 < Origin2,
   internal_error("Two versions with identical weights").

% We cannot use a version declared for an installed package if we end up building it
:- pkg_fact(Package, version_declared(Version, Weight, "installed")),
   attr("version", node(ID, Package), Version),
   version_weight(node(ID, Package), Weight),
   not attr("hash", node(ID, Package), _),
   internal_error("Reuse version weight used for built package").

% versions are declared w/priority -- declared with priority implies declared
pkg_fact(Package, version_declared(Version)) :- pkg_fact(Package, version_declared(Version, _)).

% If something is a package, it has only one version and that must be a
% declared version.
% We allow clingo to choose any version(s), and infer an error if there
% is not precisely one version chosen. Error facts are heavily optimized
% against to ensure they cannot be inferred when a non-error solution is
% possible
{ attr("version", node(ID, Package), Version) : pkg_fact(Package, version_declared(Version)) }
 :- attr("node", node(ID, Package)).

% A virtual package may or may not have a version, but never has more than one
error(100, "Cannot select a single version for virtual '{0}'", Virtual)
  :- attr("virtual_node", node(ID, Virtual)),
     2 { attr("version", node(ID, Virtual), Version) }.

% If we select a deprecated version, mark the package as deprecated
attr("deprecated", node(ID, Package), Version) :-
     attr("version", node(ID, Package), Version),
     pkg_fact(Package, deprecated_version(Version)).

error(100, "Package '{0}' needs the deprecated version '{1}', and this is not allowed", Package, Version)
  :- deprecated_versions_not_allowed(),
     attr("version", node(ID, Package), Version),
     not external(node(ID, Package)),
     not concrete(node(ID, Package)),
     pkg_fact(Package, deprecated_version(Version)).

possible_version_weight(node(ID, Package), Weight)
 :- attr("version", node(ID, Package), Version),
    pkg_fact(Package, version_declared(Version, Weight)).

% we can't use the weight for an external version if we don't use the
% corresponding external spec.
:- attr("version", node(ID, Package), Version),
   version_weight(node(ID, Package), Weight),
   pkg_fact(Package, version_declared(Version, Weight, "external")),
   not external(node(ID, Package)),
   internal_error("External weight used for built package").

% we can't use a weight from an installed spec if we are building it
% and vice-versa
:- attr("version", node(ID, Package), Version),
   version_weight(node(ID, Package), Weight),
   pkg_fact(Package, version_declared(Version, Weight, "installed")),
   build(node(ID, Package)),
   internal_error("Reuse version weight used for build package").

:- attr("version", node(ID, Package), Version),
   version_weight(node(ID, Package), Weight),
   not pkg_fact(Package, version_declared(Version, Weight, "installed")),
   not build(node(ID, Package)),
   internal_error("Build version weight used for reused package").

1 { version_weight(node(ID, Package), Weight) : pkg_fact(Package, version_declared(Version, Weight)) } 1
  :- attr("version", node(ID, Package), Version),
     attr("node", node(ID, Package)).

% node_version_satisfies implies that exactly one of the satisfying versions
% is the package's version, and vice versa.
% While this choice rule appears redundant with the initial choice rule for
% versions, virtual nodes with version constraints require this rule to be
% able to choose versions
{ attr("version", node(ID, Package), Version) : pkg_fact(Package, version_satisfies(Constraint, Version)) }
  :- attr("node_version_satisfies", node(ID, Package), Constraint).

% If there is at least a version that satisfy the constraint, impose a lower
% bound on the choice rule to avoid false positives with the error below
1 { attr("version", node(ID, Package), Version) : pkg_fact(Package, version_satisfies(Constraint, Version)) }
  :- attr("node_version_satisfies", node(ID, Package), Constraint),
     pkg_fact(Package, version_satisfies(Constraint, _)).

% More specific error message if the version cannot satisfy some constraint
% Otherwise covered by `no_version_error` and `versions_conflict_error`.
error(10, "Cannot satisfy '{0}@{1}'", Package, Constraint)
  :- attr("node_version_satisfies", node(ID, Package), Constraint),
     attr("version", node(ID, Package), Version),
     not pkg_fact(Package, version_satisfies(Constraint, Version)).

attr("node_version_satisfies", node(ID, Package), Constraint)
  :- attr("version", node(ID, Package), Version),
     pkg_fact(Package, version_satisfies(Constraint, Version)).

#defined version_satisfies/3.
#defined deprecated_versions_not_allowed/0.
#defined deprecated_version/2.

%-----------------------------------------------------------------------------
% Spec conditions and imposed constraints
%
% Given Spack directives like these:
%    depends_on("foo@1.0+bar", when="@2.0+variant")
%    provides("mpi@2:", when="@1.9:")
%
% The conditions are `@2.0+variant` and `@1.9:`, and the imposed constraints
% are `@1.0+bar` on `foo` and `@2:` on `mpi`.
%-----------------------------------------------------------------------------
% conditions are specified with `condition_requirement` and hold when
% corresponding spec attributes hold.

% A "condition_set(PackageNode, _)" is the set of nodes on which PackageNode can require / impose conditions
% Currently, for a given node, this is the link-run sub-DAG of PackageNode and its direct build dependencies
condition_set(PackageNode, PackageNode, direct_link_run) :- attr("node", PackageNode).

condition_set(PackageNode, PackageNode, direct_link_run) :- provider(PackageNode, VirtualNode).
condition_set(PackageNode, VirtualNode, direct_link_run) :- provider(PackageNode, VirtualNode).

condition_set(PackageNode, DependencyNode, direct_build) :- condition_set(PackageNode, PackageNode, direct_link_run), attr("depends_on", PackageNode, DependencyNode, "build").
condition_set(PackageNode, DependencyNode, direct_link_run) :- condition_set(PackageNode, PackageNode, direct_link_run), attr("depends_on", PackageNode, DependencyNode, Type), Type != "build".

condition_set(ID, VirtualNode, Type) :- condition_set(ID, PackageNode, Type), provider(PackageNode, VirtualNode).

condition_set(ID, PackageNode) :- condition_set(ID, PackageNode, _).

condition_set(VirtualNode, X) :- provider(PackageNode, VirtualNode), condition_set(PackageNode, X).

condition_packages(ID, A1) :- condition_requirement(ID, _, A1).
condition_packages(ID, A1) :- condition_requirement(ID, _, A1, _).
condition_packages(ID, A1) :- condition_requirement(ID, _, A1, _, _).
condition_packages(ID, A1) :- condition_requirement(ID, _, A1, _, _, _).

trigger_node(ID, node(PackageID, Package), node(PackageID, Package)) :- pkg_fact(Package, trigger_id(ID)), attr("node", node(PackageID, Package)).
trigger_node(ID, node(PackageID, Package), node(VirtualID, Virtual)) :- pkg_fact(Virtual, trigger_id(ID)), provider(node(PackageID, Package), node(VirtualID, Virtual)).

condition_nodes(TriggerID, PackageNode, node(X, A1))
  :- condition_packages(TriggerID, A1),
     condition_set(PackageNode, node(X, A1)),
     trigger_node(TriggerID, PackageNode, _).

cannot_hold(TriggerID, PackageNode)
  :- condition_packages(TriggerID, A1),
     not condition_set(PackageNode, node(_, A1)),
     trigger_node(TriggerID, PackageNode, _).

trigger_condition_holds(ID, RequestorNode) :-
  trigger_node(ID, PackageNode, RequestorNode);
  attr(Name, node(X, A1))             : condition_requirement(ID, Name, A1),             condition_nodes(ID, PackageNode, node(X, A1));
  attr(Name, node(X, A1), A2)         : condition_requirement(ID, Name, A1, A2),         condition_nodes(ID, PackageNode, node(X, A1));
  attr(Name, node(X, A1), A2, A3)     : condition_requirement(ID, Name, A1, A2, A3),     condition_nodes(ID, PackageNode, node(X, A1)), not multiple_nodes_attribute(Name);
  attr(Name, node(X, A1), A2, A3, A4) : condition_requirement(ID, Name, A1, A2, A3, A4), condition_nodes(ID, PackageNode, node(X, A1));
  % Special cases
  attr("node_flag_source", node(X, A1), A2, node(Y, A3)) : condition_requirement(ID, "node_flag_source", A1, A2, A3), condition_nodes(ID, PackageNode, node(X, A1)), condition_nodes(ID, PackageNode, node(Y, A3));
  not cannot_hold(ID, PackageNode).

condition_holds(ConditionID, node(X, Package))
  :- pkg_fact(Package, condition_trigger(ConditionID, TriggerID)),
     trigger_condition_holds(TriggerID, node(X, Package)).

trigger_and_effect(Package, TriggerID, EffectID)
  :- pkg_fact(Package, condition_trigger(ID, TriggerID)),
     pkg_fact(Package, condition_effect(ID, EffectID)).

% condition_holds(ID, node(ID, Package)) implies all imposed_constraints, unless do_not_impose(ID, node(ID, Package))
% is derived. This allows imposed constraints to be canceled in special cases.
impose(EffectID, node(X, Package))
  :- trigger_and_effect(Package, TriggerID, EffectID),
     trigger_node(TriggerID, _, node(X, Package)),
     trigger_condition_holds(TriggerID, node(X, Package)),
     not do_not_impose(EffectID, node(X, Package)).

imposed_packages(ID, A1) :- imposed_constraint(ID, _, A1).
imposed_packages(ID, A1) :- imposed_constraint(ID, _, A1, _).
imposed_packages(ID, A1) :- imposed_constraint(ID, _, A1, _, _).
imposed_packages(ID, A1) :- imposed_constraint(ID, _, A1, _, _, _).
imposed_packages(ID, A1) :- imposed_constraint(ID, "depends_on", _, A1, _).

imposed_nodes(EffectID, node(NodeID, Package), node(X, A1))
  :- pkg_fact(Package, condition_trigger(ID, TriggerID)),
     pkg_fact(Package, condition_effect(ID, EffectID)),
     imposed_packages(EffectID, A1),
     condition_set(node(NodeID, Package), node(X, A1)),
     trigger_node(TriggerID, _, node(NodeID, Package)).

imposed_nodes(ConditionID, PackageNode, node(X, A1))
  :- imposed_packages(ConditionID, A1),
     condition_set(PackageNode, node(X, A1)),
     attr("hash", PackageNode, ConditionID).

:- imposed_packages(ID, A1), impose(ID, PackageNode), not condition_set(PackageNode, node(_, A1)).
:- imposed_packages(ID, A1), impose(ID, PackageNode), not imposed_nodes(ID, PackageNode, node(_, A1)).

% Conditions that hold impose may impose constraints on other specs
attr(Name, node(X, A1))             :- impose(ID, PackageNode), imposed_constraint(ID, Name, A1),             imposed_nodes(ID, PackageNode, node(X, A1)).
attr(Name, node(X, A1), A2)         :- impose(ID, PackageNode), imposed_constraint(ID, Name, A1, A2),         imposed_nodes(ID, PackageNode, node(X, A1)).
attr(Name, node(X, A1), A2, A3)     :- impose(ID, PackageNode), imposed_constraint(ID, Name, A1, A2, A3),     imposed_nodes(ID, PackageNode, node(X, A1)), not multiple_nodes_attribute(Name).
attr(Name, node(X, A1), A2, A3, A4) :- impose(ID, PackageNode), imposed_constraint(ID, Name, A1, A2, A3, A4), imposed_nodes(ID, PackageNode, node(X, A1)).

% For node flag sources we need to look at the condition_set of the source, since it is the dependent
% of the package on which I want to impose the constraint
attr("node_flag_source", node(X, A1), A2, node(Y, A3))
  :- impose(ID, node(X, A1)),
     imposed_constraint(ID, "node_flag_source", A1, A2, A3),
     condition_set(node(Y, A3), node(X, A1)).

% Here we can't use the condition set because it's a recursive definition, that doesn't define the
% node index, and leads to unsatisfiability. Hence we say that one and only one node index must
% satisfy the dependency.
1 { attr("depends_on", node(X, A1), node(0..Y-1, A2), A3) : max_dupes(A2, Y) } 1
  :- impose(ID, node(X, A1)),
     imposed_constraint(ID, "depends_on", A1, A2, A3).

% Reconstruct virtual dependencies for reused specs
attr("virtual_on_edge", node(X, A1), node(Y, A2), Virtual)
  :- impose(ID, node(X, A1)),
     depends_on(node(X, A1), node(Y, A2)),
     imposed_constraint(ID, "virtual_on_edge", A1, A2, Virtual),
     not build(node(X, A1)).

virtual_condition_holds(node(Y, A2), Virtual)
  :- impose(ID, node(X, A1)),
     attr("virtual_on_edge", node(X, A1), node(Y, A2), Virtual),
     not build(node(X, A1)).

% we cannot have additional variant values when we are working with concrete specs
:- attr("node", node(ID, Package)),
   attr("hash", node(ID, Package), Hash),
   attr("variant_value", node(ID, Package), Variant, Value),
   not imposed_constraint(Hash, "variant_value", Package, Variant, Value),
   internal_error("imposed hash without imposing all variant values").

% we cannot have additional flag values when we are working with concrete specs
:- attr("node", node(ID, Package)),
   attr("hash", node(ID, Package), Hash),
   attr("node_flag", node(ID, Package), FlagType, Flag),
   not imposed_constraint(Hash, "node_flag", Package, FlagType, Flag),
   internal_error("imposed hash without imposing all flag values").

#defined condition/2.
#defined condition_requirement/3.
#defined condition_requirement/4.
#defined condition_requirement/5.
#defined condition_requirement/6.
#defined imposed_constraint/3.
#defined imposed_constraint/4.
#defined imposed_constraint/5.
#defined imposed_constraint/6.

%-----------------------------------------------------------------------------
% Concrete specs
%-----------------------------------------------------------------------------
% if a package is assigned a hash, it's concrete.
concrete(PackageNode) :- attr("hash", PackageNode, _), attr("node", PackageNode).

%-----------------------------------------------------------------------------
% Dependency semantics
%-----------------------------------------------------------------------------
% Dependencies of any type imply that one package "depends on" another
depends_on(PackageNode, DependencyNode) :- attr("depends_on", PackageNode, DependencyNode, _).

% a dependency holds if its condition holds and if it is not external or
% concrete. We chop off dependencies for externals, and dependencies of
% concrete specs don't need to be resolved -- they arise from the concrete
% specs themselves.
dependency_holds(node(NodeID, Package), Dependency, Type) :-
  pkg_fact(Package, dependency_condition(ID, Dependency)),
  dependency_type(ID, Type),
  build(node(NodeID, Package)),
  not external(node(NodeID, Package)),
  condition_holds(ID, node(NodeID, Package)).

% We cut off dependencies of externals (as we don't really know them).
% Don't impose constraints on dependencies that don't exist.
do_not_impose(EffectID, node(NodeID, Package)) :-
  not dependency_holds(node(NodeID, Package), Dependency, _),
  attr("node", node(NodeID, Package)),
  pkg_fact(Package, dependency_condition(ID, Dependency)),
  pkg_fact(Package, condition_effect(ID, EffectID)).

% If a dependency holds on a package node, there must be one and only one dependency node satisfying it
1 { attr("depends_on", PackageNode, node(0..Y-1, Dependency), Type) : max_dupes(Dependency, Y) } 1
  :- dependency_holds(PackageNode, Dependency, Type),
     not virtual(Dependency).

% all nodes in the graph must be reachable from some root
% this ensures a user can't say `zlib ^libiconv` (neither of which have any
% dependencies) and get a two-node unconnected graph
needed(PackageNode) :- attr("root", PackageNode).
needed(DependencyNode) :- needed(PackageNode), depends_on(PackageNode, DependencyNode).
error(10, "'{0}' is not a valid dependency for any package in the DAG", Package)
  :- attr("node", node(ID, Package)),
     not needed(node(ID, Package)).

#defined dependency_type/2.

%-----------------------------------------------------------------------------
% Conflicts
%-----------------------------------------------------------------------------
error(1, Msg)
  :- attr("node", node(ID, Package)),
     pkg_fact(Package, conflict(TriggerID, ConstraintID, Msg)),
     % node(ID1, TriggerPackage) is node(ID2, Package) in most, but not all, cases
     condition_holds(TriggerID, node(ID1, TriggerPackage)),
     condition_holds(ConstraintID, node(ID2, Package)),
     unification_set(X, node(ID2, Package)),
     unification_set(X, node(ID1, TriggerPackage)),
     not external(node(ID, Package)),  % ignore conflicts for externals
     not attr("hash", node(ID, Package), _).  % ignore conflicts for installed packages

%-----------------------------------------------------------------------------
% Virtual dependencies
%-----------------------------------------------------------------------------

% If the provider is set from the command line, its weight is 0
possible_provider_weight(ProviderNode, VirtualNode, 0, "Set on the command line")
  :- attr("provider_set", ProviderNode, VirtualNode).

% Enforces all virtuals to be provided, if multiple of them are provided together
error(100, "Package '{0}' needs to provide both '{1}' and '{2}' together, but provides only '{1}'", Package, Virtual1, Virtual2)
:- condition_holds(ID, node(X, Package)),
   pkg_fact(Package, provided_together(ID, SetID, Virtual1)),
   pkg_fact(Package, provided_together(ID, SetID, Virtual2)),
   Virtual1 != Virtual2,
   attr("virtual_on_incoming_edges", node(X, Package), Virtual1),
   not attr("virtual_on_incoming_edges", node(X, Package), Virtual2),
   attr("virtual_node", node(_, Virtual1)),
   attr("virtual_node", node(_, Virtual2)).

% if a package depends on a virtual, it's not external and we have a
% provider for that virtual then it depends on the provider
node_depends_on_virtual(PackageNode, Virtual, Type)
  :- dependency_holds(PackageNode, Virtual, Type),
     virtual(Virtual),
     not external(PackageNode).

node_depends_on_virtual(PackageNode, Virtual) :- node_depends_on_virtual(PackageNode, Virtual, Type).

1 { attr("depends_on", PackageNode, ProviderNode, Type) : provider(ProviderNode, node(VirtualID, Virtual)) } 1
  :- node_depends_on_virtual(PackageNode, Virtual, Type).

attr("virtual_on_edge", PackageNode, ProviderNode, Virtual)
  :- dependency_holds(PackageNode, Virtual, Type),
     attr("depends_on", PackageNode, ProviderNode, Type),
     provider(ProviderNode, node(_, Virtual)),
     not external(PackageNode).

attr("virtual_on_incoming_edges", ProviderNode, Virtual)
  :- attr("virtual_on_edge", _, ProviderNode, Virtual).

% dependencies on virtuals also imply that the virtual is a virtual node
1 { attr("virtual_node", node(0..X-1, Virtual)) : max_dupes(Virtual, X) }
  :- node_depends_on_virtual(PackageNode, Virtual).

% If there's a virtual node, we must select one and only one provider.
% The provider must be selected among the possible providers.

error(100, "'{0}' cannot be a provider for the '{1}' virtual", Package, Virtual)
  :-  attr("provider_set", node(min_dupe_id, Package), node(min_dupe_id, Virtual)),
      not virtual_condition_holds( node(min_dupe_id, Package), Virtual).

error(100, "Cannot find valid provider for virtual {0}", Virtual)
  :- attr("virtual_node", node(X, Virtual)),
     not provider(_, node(X, Virtual)).

error(100, "Cannot select a single provider for virtual '{0}'", Virtual)
  :- attr("virtual_node", node(X, Virtual)),
     2 { provider(P, node(X, Virtual)) }.

% virtual roots imply virtual nodes, and that one provider is a root
attr("virtual_node", VirtualNode) :- attr("virtual_root", VirtualNode).

% If we asked for a virtual root and we have a provider for that,
% then the provider is the root package.
attr("root", PackageNode) :- attr("virtual_root", VirtualNode), provider(PackageNode, VirtualNode).

% The provider is selected among the nodes for which the virtual condition holds
1 { provider(PackageNode, node(X, Virtual)) :
    attr("node", PackageNode), virtual_condition_holds(PackageNode, Virtual) } 1
  :- attr("virtual_node", node(X, Virtual)).

% The provider provides the virtual if some provider condition holds.
virtual_condition_holds(node(ProviderID, Provider), Virtual) :- virtual_condition_holds(ID, node(ProviderID, Provider), Virtual).
virtual_condition_holds(ID, node(ProviderID, Provider), Virtual) :-
   pkg_fact(Provider, provider_condition(ID, Virtual)),
   condition_holds(ID, node(ProviderID, Provider)),
   virtual(Virtual).

% If a "provider" condition holds, but this package is not a provider, do not impose the "provider" condition
do_not_impose(EffectID, node(X, Package))
  :- virtual_condition_holds(ID, node(X, Package), Virtual),
     pkg_fact(Package, condition_effect(ID, EffectID)),
     not provider(node(X, Package), node(_, Virtual)).

% Choose the provider among root specs, if possible
:- provider(ProviderNode, node(min_dupe_id, Virtual)),
   virtual_condition_holds(_, PossibleProvider, Virtual),
   PossibleProvider != ProviderNode,
   explicitly_requested_root(PossibleProvider),
   not explicitly_requested_root(ProviderNode).

% A package cannot be the actual provider for a virtual if it does not
% fulfill the conditions to provide that virtual
:- provider(PackageNode, node(VirtualID, Virtual)),
   not virtual_condition_holds(PackageNode, Virtual),
   internal_error("Virtual when provides not respected").

#defined provided_together/4.

%-----------------------------------------------------------------------------
% Virtual dependency weights
%-----------------------------------------------------------------------------

% A provider may have different possible weights depending on whether it's an external
% or not, or on preferences expressed in packages.yaml etc. This rule ensures that
% we select the weight, among the possible ones, that minimizes the overall objective function.
1 { provider_weight(DependencyNode, VirtualNode, Weight) :
    possible_provider_weight(DependencyNode, VirtualNode, Weight, _) } 1
 :- provider(DependencyNode, VirtualNode), internal_error("Package provider weights must be unique").

% A provider that is an external can use a weight of 0
possible_provider_weight(DependencyNode, VirtualNode, 0, "external")
  :- provider(DependencyNode, VirtualNode),
     external(DependencyNode).

% A provider mentioned in packages.yaml can use a weight
% according to its priority in the list of providers
possible_provider_weight(node(DependencyID, Dependency), node(VirtualID, Virtual), Weight, "packages_yaml")
  :- provider(node(DependencyID, Dependency), node(VirtualID, Virtual)),
     depends_on(node(ID, Package), node(DependencyID, Dependency)),
     pkg_fact(Package, provider_preference(Virtual, Dependency, Weight)).

% A provider mentioned in the default configuration can use a weight
% according to its priority in the list of providers
possible_provider_weight(node(DependencyID, Dependency), node(VirtualID, Virtual), Weight, "default")
  :- provider(node(DependencyID, Dependency), node(VirtualID, Virtual)),
     default_provider_preference(Virtual, Dependency, Weight).

% Any provider can use 100 as a weight, which is very high and discourage its use
possible_provider_weight(node(DependencyID, Dependency), VirtualNode, 100, "fallback") :- provider(node(DependencyID, Dependency), VirtualNode).

% do not warn if generated program contains none of these.
#defined virtual/1.
#defined virtual_condition_holds/2.
#defined external/1.
#defined buildable_false/1.
#defined default_provider_preference/3.

%-----------------------------------------------------------------------------
% External semantics
%-----------------------------------------------------------------------------

% if a package is external its version must be one of the external versions
{ external_version(node(ID, Package), Version, Weight):
    pkg_fact(Package, version_declared(Version, Weight, "external")) }
    :- external(node(ID, Package)).

error(100, "Attempted to use external for '{0}' which does not satisfy any configured external spec", Package)
  :- external(node(ID, Package)),
     not external_version(node(ID, Package), _, _).

error(100, "Attempted to use external for '{0}' which does not satisfy any configured external spec", Package)
  :- external(node(ID, Package)),
     2 { external_version(node(ID, Package), Version, Weight) }.

version_weight(PackageNode, Weight) :- external_version(PackageNode, Version, Weight).
attr("version", PackageNode, Version) :- external_version(PackageNode, Version, Weight).

% if a package is not buildable, only externals or hashed specs are allowed
external(node(ID, Package))
  :- buildable_false(Package),
     attr("node", node(ID, Package)),
     not attr("hash", node(ID, Package), _).

% a package is a real_node if it is not external
real_node(PackageNode) :- attr("node", PackageNode), not external(PackageNode).

% a package is external if we are using an external spec for it
external(PackageNode) :- attr("external_spec_selected", PackageNode, _).

% we can't use the weight for an external version if we don't use the
% corresponding external spec.
:- attr("version",  node(ID, Package), Version),
   version_weight(node(ID, Package), Weight),
   pkg_fact(Package, version_declared(Version, Weight, "external")),
   not external(node(ID, Package)),
   internal_error("External weight used for internal spec").

% determine if an external spec has been selected
attr("external_spec_selected", node(ID, Package), LocalIndex) :-
    external_conditions_hold(node(ID, Package), LocalIndex),
    attr("node", node(ID, Package)),
    not attr("hash", node(ID, Package), _).

external_conditions_hold(node(PackageID, Package), LocalIndex) :-
    pkg_fact(Package, possible_external(ID, LocalIndex)), condition_holds(ID, node(PackageID, Package)).

% it cannot happen that a spec is external, but none of the external specs
% conditions hold.
error(100, "Attempted to use external for '{0}' which does not satisfy any configured external spec", Package)
 :- external(node(ID, Package)),
    not external_conditions_hold(node(ID, Package), _).

%-----------------------------------------------------------------------------
% Config required semantics
%-----------------------------------------------------------------------------

package_in_dag(Node) :-  attr("node", Node).
package_in_dag(Node) :-  attr("virtual_node", Node).

activate_requirement(node(ID, Package), X) :-
  package_in_dag(node(ID, Package)),
  requirement_group(Package, X),
  not requirement_conditional(Package, X, _).

activate_requirement(node(ID, Package), X) :-
  package_in_dag(node(ID, Package)),
  requirement_group(Package, X),
  condition_holds(Y, node(ID, Package)),
  requirement_conditional(Package, X, Y).

requirement_group_satisfied(node(ID, Package), X) :-
  1 { condition_holds(Y, node(ID, Package)) : requirement_group_member(Y, Package, X) } 1,
  requirement_policy(Package, X, "one_of"),
  activate_requirement(node(ID, Package), X),
  requirement_group(Package, X).

requirement_weight(node(ID, Package), Group, W) :-
  condition_holds(Y, node(ID, Package)),
  requirement_has_weight(Y, W),
  requirement_group_member(Y, Package, Group),
  requirement_policy(Package, Group, "one_of"),
  requirement_group_satisfied(node(ID, Package), Group).

requirement_group_satisfied(node(ID, Package), X) :-
  1 { condition_holds(Y, node(ID, Package)) : requirement_group_member(Y, Package, X) } ,
  requirement_policy(Package, X, "any_of"),
  activate_requirement(node(ID, Package), X),
  requirement_group(Package, X).

% TODO: the following two choice rules allow the solver to add compiler
% flags if their only source is from a requirement. This is overly-specific
% and should use a more-generic approach like in https://github.com/spack/spack/pull/37180

{ attr("node_flag", node(ID, Package), FlagType, FlagValue) } :-
  requirement_group_member(ConditionID, Package, RequirementID),
  activate_requirement(node(ID, Package), RequirementID),
  pkg_fact(Package, condition_effect(ConditionID, EffectID)),
  imposed_constraint(EffectID, "node_flag_set", Package, FlagType, FlagValue).

{ attr("node_flag_source", node(NodeID1, Package1), FlagType, node(NodeID2, Package2)) } :-
  requirement_group_member(ConditionID, Package1, RequirementID),
  activate_requirement(node(NodeID1, Package1), RequirementID),
  pkg_fact(Package1, condition_effect(ConditionID, EffectID)),
  imposed_constraint(EffectID, "node_flag_source", Package1, FlagType, Package2),
  imposed_nodes(EffectID, node(NodeID2, Package2), node(NodeID1, Package1)).

requirement_weight(node(ID, Package), Group, W) :-
  W = #min {
    Z : requirement_has_weight(Y, Z), condition_holds(Y, node(ID, Package)), requirement_group_member(Y, Package, Group);
    % We need this to avoid an annoying warning during the solve
    %   concretize.lp:1151:5-11: info: tuple ignored:
    %   #sup@73
    10000
  },
  requirement_policy(Package, Group, "any_of"),
  requirement_group_satisfied(node(ID, Package), Group).

error(100, "cannot satisfy a requirement for package '{0}'.", Package) :-
  activate_requirement(node(ID, Package), X),
  requirement_group(Package, X),
  not requirement_message(Package, X, _),
  not requirement_group_satisfied(node(ID, Package), X).


error(10, Message) :-
  activate_requirement(node(ID, Package), X),
  requirement_group(Package, X),
  requirement_message(Package, X, Message),
  not requirement_group_satisfied(node(ID, Package), X).


#defined requirement_group/2.
#defined requirement_conditional/3.
#defined requirement_message/3.
#defined requirement_group_member/3.
#defined requirement_has_weight/2.
#defined requirement_policy/3.

%-----------------------------------------------------------------------------
% Variant semantics
%-----------------------------------------------------------------------------
% a variant is a variant of a package if it is a variant under some condition
% and that condition holds
node_has_variant(node(NodeID, Package), Variant) :-
  pkg_fact(Package, conditional_variant(ID, Variant)),
  condition_holds(ID, node(NodeID, Package)).

node_has_variant(node(ID, Package), Variant) :-
  pkg_fact(Package, variant(Variant)),
  attr("node", node(ID, Package)).

attr("variant_propagate", PackageNode, Variant, Value, Source) :-
  attr("node", PackageNode),
  depends_on(ParentNode, PackageNode),
  attr("variant_propagate", ParentNode, Variant, Value, Source),
  not attr("variant_set", PackageNode, Variant).

attr("variant_value", node(ID, Package), Variant, Value) :-
  attr("node", node(ID, Package)),
  node_has_variant(node(ID, Package), Variant),
  attr("variant_propagate", node(ID, Package), Variant, Value, _),
  pkg_fact(Package, variant_possible_value(Variant, Value)).

error(100, "{0} and {1} cannot both propagate variant '{2}' to package {3} with values '{4}' and '{5}'", Source1, Source2, Variant, Package, Value1, Value2) :-
  attr("variant_propagate", node(X, Package), Variant, Value1, Source1),
  attr("variant_propagate", node(X, Package), Variant, Value2, Source2),
  node_has_variant(node(X, Package), Variant),
  Value1 < Value2.

% a variant cannot be set if it is not a variant on the package
error(100, "Cannot set variant '{0}' for package '{1}' because the variant condition cannot be satisfied for the given spec", Variant, Package)
  :- attr("variant_set", node(X, Package), Variant),
     not node_has_variant(node(X, Package), Variant),
     build(node(X, Package)).

% a variant cannot take on a value if it is not a variant of the package
error(100, "Cannot set variant '{0}' for package '{1}' because the variant condition cannot be satisfied for the given spec", Variant, Package)
  :- attr("variant_value", node(X, Package), Variant, _),
     not node_has_variant(node(X, Package), Variant),
     build(node(X, Package)).

% if a variant is sticky and not set its value is the default value
attr("variant_value", node(ID, Package), Variant, Value) :-
  node_has_variant(node(ID, Package), Variant),
  not attr("variant_set", node(ID, Package), Variant),
  pkg_fact(Package, variant_sticky(Variant)),
  variant_default_value(Package, Variant, Value),
  build(node(ID, Package)).

% at most one variant value for single-valued variants.
{
  attr("variant_value", node(ID, Package), Variant, Value)
  : pkg_fact(Package, variant_possible_value(Variant, Value))
}
 :- attr("node", node(ID, Package)),
    node_has_variant(node(ID, Package), Variant),
    build(node(ID, Package)).


error(100, "'{0}' required multiple values for single-valued variant '{1}'", Package, Variant)
  :- attr("node", node(ID, Package)),
     node_has_variant(node(ID, Package), Variant),
     pkg_fact(Package, variant_single_value(Variant)),
     build(node(ID, Package)),
     2 { attr("variant_value", node(ID, Package), Variant, Value) }.

error(100, "No valid value for variant '{1}' of package '{0}'", Package, Variant)
  :- attr("node", node(X, Package)),
     node_has_variant(node(X, Package), Variant),
     build(node(X, Package)),
     not attr("variant_value", node(X, Package), Variant, _).

% if a variant is set to anything, it is considered 'set'.
attr("variant_set", PackageNode, Variant) :- attr("variant_set", PackageNode, Variant, _).

% A variant cannot have a value that is not also a possible value
% This only applies to packages we need to build -- concrete packages may
% have been built w/different variants from older/different package versions.
error(10, "'Spec({1}={2})' is not a valid value for '{0}' variant '{1}'", Package, Variant, Value)
 :- attr("variant_value", node(ID, Package), Variant, Value),
    not pkg_fact(Package, variant_possible_value(Variant, Value)),
    build(node(ID, Package)).

% Some multi valued variants accept multiple values from disjoint sets.
% Ensure that we respect that constraint and we don't pick values from more
% than one set at once
error(100, "{0} variant '{1}' cannot have values '{2}' and '{3}' as they come from disjoint value sets", Package, Variant, Value1, Value2)
  :- attr("variant_value", node(ID, Package), Variant, Value1),
     attr("variant_value", node(ID, Package), Variant, Value2),
     pkg_fact(Package, variant_value_from_disjoint_sets(Variant, Value1, Set1)),
     pkg_fact(Package, variant_value_from_disjoint_sets(Variant, Value2, Set2)),
     Set1 < Set2, % see[1]
     build(node(ID, Package)).

% variant_set is an explicitly set variant value. If it's not 'set',
% we revert to the default value. If it is set, we force the set value
attr("variant_value", PackageNode, Variant, Value)
 :- attr("node", PackageNode),
    node_has_variant(PackageNode, Variant),
    attr("variant_set", PackageNode, Variant, Value).

% The rules below allow us to prefer default values for variants
% whenever possible. If a variant is set in a spec, or if it is
% specified in an external, we score it as if it was a default value.
variant_not_default(node(ID, Package), Variant, Value)
 :- attr("variant_value", node(ID, Package), Variant, Value),
    not variant_default_value(Package, Variant, Value),
    % variants set explicitly on the CLI don't count as non-default
    not attr("variant_set", node(ID, Package), Variant, Value),
    % variant values forced by propagation don't count as non-default
    not attr("variant_propagate", node(ID, Package), Variant, Value, _),
    % variants set on externals that we could use don't count as non-default
    % this makes spack prefer to use an external over rebuilding with the
    % default configuration
    not external_with_variant_set(node(ID, Package), Variant, Value),
    attr("node", node(ID, Package)).


% A default variant value that is not used
variant_default_not_used(node(ID, Package), Variant, Value)
  :- variant_default_value(Package, Variant, Value),
     node_has_variant(node(ID, Package), Variant),
     not attr("variant_value", node(ID, Package), Variant, Value),
     not attr("variant_propagate", node(ID, Package), Variant, _, _),
     attr("node", node(ID, Package)).

% The variant is set in an external spec
external_with_variant_set(node(NodeID, Package), Variant, Value)
 :- attr("variant_value", node(NodeID, Package), Variant, Value),
    condition_requirement(ID, "variant_value", Package, Variant, Value),
    pkg_fact(Package, possible_external(ID, _)),
    external(node(NodeID, Package)),
    attr("node", node(NodeID, Package)).

% The default value for a variant in a package is what is prescribed:
%
% 1. On the command line
% 2. In packages.yaml (if there's no command line settings)
% 3. In the package.py file (if there are no settings in
%    packages.yaml and the command line)
%
variant_default_value(Package, Variant, Value)
 :- pkg_fact(Package, variant_default_value_from_package_py(Variant, Value)),
    not variant_default_value_from_packages_yaml(Package, Variant, _),
    not attr("variant_default_value_from_cli", node(min_dupe_id, Package), Variant, _).

variant_default_value(Package, Variant, Value)
 :- variant_default_value_from_packages_yaml(Package, Variant, Value),
    not attr("variant_default_value_from_cli", node(min_dupe_id, Package), Variant, _).

variant_default_value(Package, Variant, Value) :-
    attr("variant_default_value_from_cli", node(min_dupe_id, Package), Variant, Value).

% Treat 'none' in a special way - it cannot be combined with other
% values even if the variant is multi-valued
error(100, "{0} variant '{1}' cannot have values '{2}' and 'none'", Package, Variant, Value)
 :- attr("variant_value", node(X, Package), Variant, Value),
    attr("variant_value", node(X, Package), Variant, "none"),
    Value != "none",
    build(node(X, Package)).

% patches and dev_path are special variants -- they don't have to be
% declared in the package, so we just allow them to spring into existence
% when assigned a value.
auto_variant("dev_path").
auto_variant("patches").

node_has_variant(PackageNode, Variant)
  :- attr("variant_set", PackageNode, Variant, _), auto_variant(Variant).

pkg_fact(Package, variant_single_value("dev_path"))
  :- attr("variant_set", node(ID, Package), "dev_path", _).

% suppress warnings about this atom being unset.  It's only set if some
% spec or some package sets it, and without this, clingo will give
% warnings like 'info: atom does not occur in any rule head'.
#defined variant_default_value/3.
#defined variant_default_value_from_packages_yaml/3.

%-----------------------------------------------------------------------------
% Platform semantics
%-----------------------------------------------------------------------------

% if no platform is set, fall back to the default
error(100, "platform '{0}' is not allowed on the current host", Platform)
  :- attr("node_platform", _, Platform), not allowed_platform(Platform).

attr("node_platform", PackageNode, Platform)
 :- attr("node", PackageNode),
    not attr("node_platform_set", PackageNode),
    node_platform_default(Platform).

% setting platform on a node is a hard constraint
attr("node_platform", PackageNode, Platform)
 :- attr("node", PackageNode), attr("node_platform_set", PackageNode, Platform).

% platform is set if set to anything
attr("node_platform_set", PackageNode) :- attr("node_platform_set", PackageNode, _).

%-----------------------------------------------------------------------------
% OS semantics
%-----------------------------------------------------------------------------
% convert weighted OS declarations to simple one
os(OS) :- os(OS, _).

% one os per node
{ attr("node_os", PackageNode, OS) : os(OS) } :- attr("node", PackageNode).

% can't have a non-buildable OS on a node we need to build
error(100, "Cannot select '{0} os={1}' (operating system '{1}' is not buildable)", Package, OS)
 :- build(node(X, Package)),
    attr("node_os", node(X, Package), OS),
    not buildable_os(OS).

% can't have dependencies on incompatible OS's
error(100, "{0} and dependency {1} have incompatible operating systems 'os={2}' and 'os={3}'", Package, Dependency, PackageNodeOS, DependencyOS)
  :- depends_on(node(X, Package), node(Y, Dependency)),
     attr("node_os", node(X, Package), PackageNodeOS),
     attr("node_os", node(Y, Dependency), DependencyOS),
     not os_compatible(PackageNodeOS, DependencyOS),
     build(node(X, Package)).

% give OS choice weights according to os declarations
node_os_weight(PackageNode, Weight)
 :- attr("node", PackageNode),
    attr("node_os", PackageNode, OS),
    os(OS, Weight).

% match semantics for OS's
node_os_match(PackageNode, DependencyNode) :-
   depends_on(PackageNode, DependencyNode),
   attr("node_os", PackageNode, OS),
   attr("node_os", DependencyNode, OS).

node_os_mismatch(PackageNode, DependencyNode) :-
   depends_on(PackageNode, DependencyNode),
   not node_os_match(PackageNode, DependencyNode).

% every OS is compatible with itself. We can use `os_compatible` to declare
os_compatible(OS, OS) :- os(OS).

% Transitive compatibility among operating systems
os_compatible(OS1, OS3) :- os_compatible(OS1, OS2), os_compatible(OS2, OS3).

% We can select only operating systems compatible with the ones
% for which we can build software. We need a cardinality constraint
% since we might have more than one "buildable_os(OS)" fact.
:- not 1 { os_compatible(CurrentOS, ReusedOS) : buildable_os(CurrentOS) },
   attr("node_os", Package, ReusedOS),
   internal_error("Reused OS incompatible with build OS").

% If an OS is set explicitly respect the value
attr("node_os", PackageNode, OS) :- attr("node_os_set", PackageNode, OS), attr("node", PackageNode).

#defined os_compatible/2.

%-----------------------------------------------------------------------------
% Target semantics
%-----------------------------------------------------------------------------

% Each node has only one target chosen among the known targets
{ attr("node_target", PackageNode, Target) : target(Target) } :- attr("node", PackageNode).

% If a node must satisfy a target constraint, enforce it
error(10, "'{0} target={1}' cannot satisfy constraint 'target={2}'", Package, Target, Constraint)
  :- attr("node_target", node(X, Package), Target),
     attr("node_target_satisfies", node(X, Package), Constraint),
     not target_satisfies(Constraint, Target).

% If a node has a target and the target satisfies a constraint, then the target
% associated with the node satisfies the same constraint
attr("node_target_satisfies", PackageNode, Constraint)
  :- attr("node_target", PackageNode, Target), target_satisfies(Constraint, Target).

% If a node has a target, all of its dependencies must be compatible with that target
error(100, "Cannot find compatible targets for {0} and {1}", Package, Dependency)
  :- depends_on(node(X, Package), node(Y, Dependency)),
     attr("node_target", node(X, Package), Target),
     not node_target_compatible(node(Y, Dependency), Target).

% Intermediate step for performance reasons
% When the integrity constraint above was formulated including this logic
% we suffered a substantial performance penalty
node_target_compatible(PackageNode, Target)
 :- attr("node_target", PackageNode, MyTarget),
    target_compatible(Target, MyTarget).

#defined target_satisfies/2.

% can't use targets on node if the compiler for the node doesn't support them
error(100, "{0} compiler '{2}@{3}' incompatible with 'target={1}'", Package, Target, Compiler, Version)
  :- attr("node_target", node(X, Package), Target),
     node_compiler(node(X, Package), CompilerID),
     not compiler_supports_target(CompilerID, Target),
     compiler_name(CompilerID, Compiler),
     compiler_version(CompilerID, Version),
     build(node(X, Package)).

% if a target is set explicitly, respect it
attr("node_target", PackageNode, Target)
 :- attr("node", PackageNode), attr("node_target_set", PackageNode, Target).

% each node has the weight of its assigned target
node_target_weight(node(ID, Package), Weight)
 :- attr("node", node(ID, Package)),
    attr("node_target", node(ID, Package), Target),
    pkg_fact(Package, target_weight(Target, Weight)).

% compatibility rules for targets among nodes
node_target_match(ParentNode, DependencyNode)
  :- attr("depends_on", ParentNode, DependencyNode, Type), Type != "build",
     attr("node_target", ParentNode, Target),
     attr("node_target", DependencyNode, Target).

node_target_mismatch(ParentNode, DependencyNode)
  :- attr("depends_on", ParentNode, DependencyNode, Type), Type != "build",
     not node_target_match(ParentNode, DependencyNode).

% disallow reusing concrete specs that don't have a compatible target
error(100, "'{0} target={1}' is not compatible with this machine", Package, Target)
  :- attr("node", node(X, Package)),
     attr("node_target", node(X, Package), Target),
     not target(Target).

%-----------------------------------------------------------------------------
% Compiler semantics
%-----------------------------------------------------------------------------
% There must be only one compiler set per built node.
{ node_compiler(PackageNode, CompilerID) : compiler_id(CompilerID) } :-
    attr("node", PackageNode),
    build(PackageNode).

% Infer the compiler that matches a reused node
node_compiler(PackageNode, CompilerID)
  :- attr("node_compiler_version", PackageNode, CompilerName, CompilerVersion),
     attr("node", PackageNode),
     compiler_name(CompilerID, CompilerName),
     compiler_version(CompilerID, CompilerVersion),
     concrete(PackageNode).

% Expand the internal attribute into "attr("node_compiler_version")
attr("node_compiler_version", PackageNode, CompilerName, CompilerVersion)
  :- node_compiler(PackageNode, CompilerID),
     compiler_name(CompilerID, CompilerName),
     compiler_version(CompilerID, CompilerVersion),
     build(PackageNode).

attr("node_compiler", PackageNode, CompilerName)
  :- attr("node_compiler_version", PackageNode, CompilerName, CompilerVersion).

error(100, "No valid compiler version found for '{0}'", Package)
  :- attr("node", node(X, Package)),
     not node_compiler(node(X, Package), _).

% We can't have a compiler be enforced and select the version from another compiler
error(100, "Cannot select a single compiler for package {0}", Package)
 :- attr("node", node(X, Package)),
    2 { attr("node_compiler_version", node(X, Package), C, V) }.

% If the compiler of a node cannot be satisfied, raise
error(10, "No valid compiler for {0} satisfies '%{1}'", Package, Compiler)
  :- attr("node", node(X, Package)),
     attr("node_compiler_version_satisfies", node(X, Package), Compiler, ":"),
     not compiler_version_satisfies(Compiler, ":", _).

% If the compiler of a node must satisfy a constraint, then its version
% must be chosen among the ones that satisfy said constraint
error(100, "No valid version for '{0}' compiler '{1}' satisfies '@{2}'", Package, Compiler, Constraint)
  :- attr("node", node(X, Package)),
     attr("node_compiler_version_satisfies", node(X, Package), Compiler, Constraint),
		 not compiler_version_satisfies(Compiler, Constraint, _).

error(100, "No valid version for '{0}' compiler '{1}' satisfies '@{2}'", Package, Compiler, Constraint)
  :- attr("node", node(X, Package)),
     attr("node_compiler_version_satisfies", node(X, Package), Compiler, Constraint),
     not compiler_version_satisfies(Compiler, Constraint, ID),
     node_compiler(node(X, Package), ID).

% If the node is associated with a compiler and the compiler satisfy a constraint, then
% the compiler associated with the node satisfy the same constraint
attr("node_compiler_version_satisfies", PackageNode, Compiler, Constraint)
  :- node_compiler(PackageNode, CompilerID),
     compiler_name(CompilerID, Compiler),
     compiler_version_satisfies(Compiler, Constraint, CompilerID).

#defined compiler_version_satisfies/3.

% If the compiler version was set from the command line,
% respect it verbatim
:- attr("node_compiler_version_set", PackageNode, Compiler, Version),
   not attr("node_compiler_version", PackageNode, Compiler, Version).

:- attr("node_compiler_set", PackageNode, Compiler),
   not attr("node_compiler_version", PackageNode, Compiler, _).

% Cannot select a compiler if it is not supported on the OS
% Compilers that are explicitly marked as allowed
% are excluded from this check
error(100, "{0} compiler '%{1}@{2}' incompatible with 'os={3}'", Package, Compiler, Version, OS)
  :- attr("node_os", node(X, Package), OS),
     node_compiler(node(X, Package), CompilerID),
     compiler_name(CompilerID, Compiler),
     compiler_version(CompilerID, Version),
     not compiler_os(CompilerID, OS),
     not allow_compiler(Compiler, Version),
     build(node(X, Package)).

% If a package and one of its dependencies don't have the
% same compiler there's a mismatch.
compiler_match(PackageNode, DependencyNode)
  :- depends_on(PackageNode, DependencyNode),
     node_compiler(PackageNode, CompilerID),
     node_compiler(DependencyNode, CompilerID).

compiler_mismatch(PackageNode, DependencyNode)
  :- depends_on(PackageNode, DependencyNode),
     not attr("node_compiler_set", DependencyNode, _),
     not compiler_match(PackageNode, DependencyNode).

compiler_mismatch_required(PackageNode, DependencyNode)
  :- depends_on(PackageNode, DependencyNode),
     attr("node_compiler_set", DependencyNode, _),
     not compiler_match(PackageNode, DependencyNode).

#defined compiler_os/3.
#defined allow_compiler/2.

% compilers weighted by preference according to packages.yaml
compiler_weight(node(ID, Package), Weight)
 :- node_compiler(node(ID, Package), CompilerID),
    compiler_name(CompilerID, Compiler),
    compiler_version(CompilerID, V),
    pkg_fact(Package, node_compiler_preference(Compiler, V, Weight)).
compiler_weight(node(ID, Package), Weight)
 :- node_compiler(node(ID, Package), CompilerID),
    compiler_name(CompilerID, Compiler),
    compiler_version(CompilerID, V),
    not pkg_fact(Package, node_compiler_preference(Compiler, V, _)),
    default_compiler_preference(CompilerID, Weight).
compiler_weight(node(ID, Package), 100)
 :- node_compiler(node(ID, Package), CompilerID),
    compiler_name(CompilerID, Compiler),
    compiler_version(CompilerID, V),
    not pkg_fact(Package, node_compiler_preference(Compiler, V, _)),
    not default_compiler_preference(CompilerID, _).

% For the time being, be strict and reuse only if the compiler match one we have on the system
error(100, "Compiler {1}@{2} requested for {0} cannot be found. Set install_missing_compilers:true if intended.", Package, Compiler, Version)
 :- attr("node_compiler_version", node(ID, Package), Compiler, Version),
    not node_compiler(node(ID, Package), _).

#defined node_compiler_preference/4.
#defined default_compiler_preference/3.

%-----------------------------------------------------------------------------
% Compiler flags
%-----------------------------------------------------------------------------

% propagate flags when compiler match
can_inherit_flags(PackageNode, DependencyNode, FlagType)
  :- same_compiler(PackageNode, DependencyNode),
     not attr("node_flag_set", DependencyNode, FlagType, _),
     flag_type(FlagType).

same_compiler(PackageNode, DependencyNode)
  :- depends_on(PackageNode, DependencyNode),
     node_compiler(PackageNode, CompilerID),
     node_compiler(DependencyNode, CompilerID),
     compiler_id(CompilerID).

node_flag_inherited(DependencyNode, FlagType, Flag)
  :- attr("node_flag_set", PackageNode, FlagType, Flag),
     can_inherit_flags(PackageNode, DependencyNode, FlagType),
     attr("node_flag_propagate", PackageNode, FlagType).

% Ensure propagation
:- node_flag_inherited(PackageNode, FlagType, Flag),
   can_inherit_flags(PackageNode, DependencyNode, FlagType),
   attr("node_flag_propagate", PackageNode, FlagType).

error(100, "{0} and {1} cannot both propagate compiler flags '{2}' to {3}", Source1, Source2, Package, FlagType) :-
  depends_on(Source1, Package),
  depends_on(Source2, Package),
  attr("node_flag_propagate", Source1, FlagType),
  attr("node_flag_propagate", Source2, FlagType),
  can_inherit_flags(Source1, Package, FlagType),
  can_inherit_flags(Source2, Package, FlagType),
  Source1 < Source2.

% remember where flags came from
attr("node_flag_source", PackageNode, FlagType, PackageNode)
  :- attr("node_flag_set", PackageNode, FlagType, _).

attr("node_flag_source", DependencyNode, FlagType, Q)
  :- attr("node_flag_source", PackageNode, FlagType, Q),
     node_flag_inherited(DependencyNode, FlagType, _),
     attr("node_flag_propagate", PackageNode, FlagType).

% compiler flags from compilers.yaml are put on nodes if compiler matches
attr("node_flag", PackageNode, FlagType, Flag)
  :- compiler_flag(CompilerID, FlagType, Flag),
     node_compiler(PackageNode, CompilerID),
     flag_type(FlagType),
     compiler_id(CompilerID),
     compiler_name(CompilerID, CompilerName),
     compiler_version(CompilerID, Version).

attr("node_flag_compiler_default", PackageNode)
  :- not attr("node_flag_set", PackageNode, FlagType, _),
     compiler_flag(CompilerID, FlagType, Flag),
     node_compiler(PackageNode, CompilerID),
     flag_type(FlagType),
     compiler_id(CompilerID),
     compiler_name(CompilerID, CompilerName),
     compiler_version(CompilerID, Version).

% if a flag is set to something or inherited, it's included
attr("node_flag", PackageNode, FlagType, Flag) :- attr("node_flag_set", PackageNode, FlagType, Flag).
attr("node_flag", PackageNode, FlagType, Flag) :- node_flag_inherited(PackageNode, FlagType, Flag).

% if no node flags are set for a type, there are no flags.
attr("no_flags", PackageNode, FlagType)
  :- not attr("node_flag", PackageNode, FlagType, _),
     attr("node", PackageNode),
     flag_type(FlagType).

#defined compiler_flag/3.


%-----------------------------------------------------------------------------
% Installed packages
%-----------------------------------------------------------------------------
% the solver is free to choose at most one installed hash for each package
{ attr("hash", node(ID, Package), Hash) : installed_hash(Package, Hash) } 1
 :- attr("node", node(ID, Package)), internal_error("Package must resolve to at most one hash").

% you can't choose an installed hash for a dev spec
:- attr("hash", PackageNode, Hash), attr("variant_value", PackageNode, "dev_path", _).

% You can't install a hash, if it is not installed
:- attr("hash", node(ID, Package), Hash), not installed_hash(Package, Hash).
% This should be redundant given the constraint above
:- attr("node", PackageNode), 2 { attr("hash", PackageNode, Hash) }.

% if a hash is selected, we impose all the constraints that implies
impose(Hash, PackageNode) :- attr("hash", PackageNode, Hash).

% if we haven't selected a hash for a package, we'll be building it
build(PackageNode) :- not attr("hash", PackageNode, _), attr("node", PackageNode).

% Minimizing builds is tricky. We want a minimizing criterion

% because we want to reuse what is avaialble, but
% we also want things that are built to stick to *default preferences* from
% the package and from the user. We therefore treat built specs differently and apply
% a different set of optimization criteria to them. Spack's *first* priority is to
% reuse what it *can*, but if it builds something, the built specs will respect
% defaults and preferences.  This is implemented by bumping the priority of optimization
% criteria for built specs -- so that they take precedence over the otherwise
% topmost-priority criterion to reuse what is installed.
%
% The priority ranges are:
%   200+        Shifted priorities for build nodes; correspond to priorities 0 - 99.
%   100 - 199   Unshifted priorities. Currently only includes minimizing #builds.
%   0   -  99   Priorities for non-built nodes.
build_priority(PackageNode, 200) :- build(PackageNode), attr("node", PackageNode).
build_priority(PackageNode, 0)   :- not build(PackageNode), attr("node", PackageNode).

% don't assign versions from installed packages unless reuse is enabled
% NOTE: that "installed" means the declared version was only included because
% that package happens to be installed, NOT because it was asked for on the
% command line.  If the user specifies a hash, the origin will be "spec".
%
% TODO: There's a slight inconsistency with this: if the user concretizes
% and installs `foo ^bar`, for some build dependency `bar`, and then later
% does a `spack install --fresh foo ^bar/abcde` (i.e.,the hash of `bar`, it
% currently *won't* force versions for `bar`'s build dependencies -- `--fresh`
% will instead build the latest bar. When we actually include transitive
% build deps in the solve, consider using them as a preference to resolve this.
:- attr("version", node(ID, Package), Version),
   version_weight(node(ID, Package), Weight),
   pkg_fact(Package, version_declared(Version, Weight, "installed")),
   not optimize_for_reuse().

#defined installed_hash/2.

% This statement, which is a hidden feature of clingo, let us avoid cycles in the DAG
#edge (A, B) : depends_on(A, B).


%-----------------------------------------------------------------
% Optimization to avoid errors
%-----------------------------------------------------------------
% Some errors are handled as rules instead of constraints because
% it allows us to explain why something failed.
#minimize{ 0@1000: #true}.

#minimize{ Weight@1000,Msg: error(Weight, Msg) }.
#minimize{ Weight@1000,Msg,Arg1: error(Weight, Msg, Arg1) }.
#minimize{ Weight@1000,Msg,Arg1,Arg2: error(Weight, Msg, Arg1, Arg2) }.
#minimize{ Weight@1000,Msg,Arg1,Arg2,Arg3: error(Weight, Msg, Arg1, Arg2, Arg3) }.
#minimize{ Weight@1000,Msg,Arg1,Arg2,Arg3,Arg4: error(Weight, Msg, Arg1, Arg2, Arg3, Arg4) }.

%-----------------------------------------------------------------------------
% How to optimize the spec (high to low priority)
%-----------------------------------------------------------------------------
% Each criterion below has:
%   1. an opt_criterion(ID, Name) fact that describes the criterion, and
%   2. a `#minimize{ 0@2 : #true }.` statement that ensures the criterion
%      is displayed (clingo doesn't display sums over empty sets by default)

% Try hard to reuse installed packages (i.e., minimize the number built)
opt_criterion(110, "number of packages to build (vs. reuse)").
#minimize { 0@110: #true }.
#minimize { 1@110,PackageNode : build(PackageNode), optimize_for_reuse() }.

opt_criterion(100, "number of nodes from the same package").
#minimize { 0@100: #true }.
#minimize { ID@100,Package : attr("node", node(ID, Package)) }.
#minimize { ID@100,Package : attr("virtual_node", node(ID, Package)) }.
#defined optimize_for_reuse/0.

% A condition group specifies one or more specs that must be satisfied.
% Specs declared first are preferred, so we assign increasing weights and
% minimize the weights.
opt_criterion(75, "requirement weight").
#minimize{ 0@275: #true }.
#minimize{ 0@75: #true }.
#minimize {
    Weight@75+Priority,PackageNode,Group
    : requirement_weight(PackageNode, Group, Weight),
      build_priority(PackageNode, Priority)
}.

% Minimize the number of deprecated versions being used
opt_criterion(73, "deprecated versions used").
#minimize{ 0@273: #true }.
#minimize{ 0@73: #true }.
#minimize{
    1@73+Priority,PackageNode
    : attr("deprecated", PackageNode, _),
      build_priority(PackageNode, Priority)
}.

% Minimize the:
% 1. Version weight
% 2. Number of variants with a non default value, if not set
% for the root package.
opt_criterion(70, "version weight").
#minimize{ 0@270: #true }.
#minimize{ 0@70: #true }.
#minimize {
    Weight@70+Priority
    : attr("root", PackageNode),
      version_weight(PackageNode, Weight),
      build_priority(PackageNode, Priority)
}.

opt_criterion(65, "number of non-default variants (roots)").
#minimize{ 0@265: #true }.
#minimize{ 0@65: #true }.
#minimize {
    1@65+Priority,PackageNode,Variant,Value
    : variant_not_default(PackageNode, Variant, Value),
      attr("root", PackageNode),
      build_priority(PackageNode, Priority)
}.

opt_criterion(60, "preferred providers for roots").
#minimize{ 0@260: #true }.
#minimize{ 0@60: #true }.
#minimize{
    Weight@60+Priority,ProviderNode,Virtual
    : provider_weight(ProviderNode, Virtual, Weight),
      attr("root", ProviderNode),
      build_priority(ProviderNode, Priority)
}.

opt_criterion(55, "default values of variants not being used (roots)").
#minimize{ 0@255: #true }.
#minimize{ 0@55: #true }.
#minimize{
    1@55+Priority,PackageNode,Variant,Value
    : variant_default_not_used(PackageNode, Variant, Value),
      attr("root", PackageNode),
      build_priority(PackageNode, Priority)
}.

% Try to use default variants or variants that have been set
opt_criterion(50, "number of non-default variants (non-roots)").
#minimize{ 0@250: #true }.
#minimize{ 0@50: #true }.
#minimize {
    1@50+Priority,PackageNode,Variant,Value
    : variant_not_default(PackageNode, Variant, Value),
      not attr("root", PackageNode),
      build_priority(PackageNode, Priority)
}.

% Minimize the weights of the providers, i.e. use as much as
% possible the most preferred providers
opt_criterion(45, "preferred providers (non-roots)").
#minimize{ 0@245: #true }.
#minimize{ 0@45: #true }.
#minimize{
    Weight@45+Priority,ProviderNode,Virtual
    : provider_weight(ProviderNode, Virtual, Weight),
      not attr("root", ProviderNode),
      build_priority(ProviderNode, Priority)
}.

% Try to minimize the number of compiler mismatches in the DAG.
opt_criterion(40, "compiler mismatches that are not from CLI").
#minimize{ 0@240: #true }.
#minimize{ 0@40: #true }.
#minimize{
    1@40+Priority,PackageNode,DependencyNode
    : compiler_mismatch(PackageNode, DependencyNode),
      build_priority(PackageNode, Priority)
}.

opt_criterion(39, "compiler mismatches that are not from CLI").
#minimize{ 0@239: #true }.
#minimize{ 0@39: #true }.
#minimize{
    1@39+Priority,PackageNode,DependencyNode
    : compiler_mismatch_required(PackageNode, DependencyNode),
      build_priority(PackageNode, Priority)
}.

% Try to minimize the number of compiler mismatches in the DAG.
opt_criterion(35, "OS mismatches").
#minimize{ 0@235: #true }.
#minimize{ 0@35: #true }.
#minimize{
    1@35+Priority,PackageNode,DependencyNode
    : node_os_mismatch(PackageNode, DependencyNode),
      build_priority(PackageNode, Priority)
}.

opt_criterion(30, "non-preferred OS's").
#minimize{ 0@230: #true }.
#minimize{ 0@30: #true }.
#minimize{
    Weight@30+Priority,PackageNode
    : node_os_weight(PackageNode, Weight),
      build_priority(PackageNode, Priority)
}.

% Choose more recent versions for nodes
opt_criterion(25, "version badness").
#minimize{ 0@225: #true }.
#minimize{ 0@25: #true }.
#minimize{
    Weight@25+Priority,PackageNode
    : version_weight(PackageNode, Weight),
      build_priority(PackageNode, Priority)
}.

% Try to use all the default values of variants
opt_criterion(20, "default values of variants not being used (non-roots)").
#minimize{ 0@220: #true }.
#minimize{ 0@20: #true }.
#minimize{
    1@20+Priority,PackageNode,Variant,Value
    : variant_default_not_used(PackageNode, Variant, Value),
      not attr("root", PackageNode),
      build_priority(PackageNode, Priority)
}.

% Try to use preferred compilers
opt_criterion(15, "non-preferred compilers").
#minimize{ 0@215: #true }.
#minimize{ 0@15: #true }.
#minimize{
    Weight@15+Priority,PackageNode
    : compiler_weight(PackageNode, Weight),
      build_priority(PackageNode, Priority)
}.

% Minimize the number of mismatches for targets in the DAG, try
% to select the preferred target.
opt_criterion(10, "target mismatches").
#minimize{ 0@210: #true }.
#minimize{ 0@10: #true }.
#minimize{
    1@10+Priority,PackageNode,Dependency
    : node_target_mismatch(PackageNode, Dependency),
      build_priority(PackageNode, Priority)
}.

opt_criterion(5, "non-preferred targets").
#minimize{ 0@205: #true }.
#minimize{ 0@5: #true }.
#minimize{
    Weight@5+Priority,PackageNode
    : node_target_weight(PackageNode, Weight),
      build_priority(PackageNode, Priority)
}.

% Choose more recent versions for nodes
opt_criterion(1, "edge wiring").
#minimize{ 0@201: #true }.
#minimize{ 0@1: #true }.
#minimize{
    Weight@1,ParentNode,PackageNode
    : version_weight(PackageNode, Weight),
      not attr("root", PackageNode),
      depends_on(ParentNode, PackageNode)
}.

%-----------
% Notes
%-----------

% [1] Clingo ensures a total ordering among all atoms. We rely on that total ordering
%     to reduce symmetry in the solution by checking `<` instead of `!=` in symmetric
%     cases. These choices are made without loss of generality.