diff options
| author | Massimiliano Culpo <massimiliano.culpo@gmail.com> | 2023-06-19 14:34:05 +0200 |
|---|---|---|
| committer | Todd Gamblin <tgamblin@llnl.gov> | 2023-08-15 15:54:37 -0700 |
| commit | c050b99a06a3ad11c76962b08141e513ea69b6c1 (patch) | |
| tree | a1113a1a5859cf5329fc01f65744a93d914ec093 /lib | |
| parent | 60f82685ae5bf5cb45ab47ab1bf271d240f117ed (diff) | |
| download | spack-c050b99a06a3ad11c76962b08141e513ea69b6c1.tar.gz spack-c050b99a06a3ad11c76962b08141e513ea69b6c1.tar.bz2 spack-c050b99a06a3ad11c76962b08141e513ea69b6c1.tar.xz spack-c050b99a06a3ad11c76962b08141e513ea69b6c1.zip | |
Introduce unification sets
Unification sets are possibly overlapping sets of nodes that
might contain at most a single configuration for any package.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/spack/spack/solver/concretize.lp | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/lib/spack/spack/solver/concretize.lp b/lib/spack/spack/solver/concretize.lp index 30c3275ab9..77fa3d47be 100644 --- a/lib/spack/spack/solver/concretize.lp +++ b/lib/spack/spack/solver/concretize.lp @@ -14,7 +14,10 @@ #const root_node_id = 0. % Allow clingo to create nodes -{ attr("node", node(0..X-1, Package)) } :- max_nodes(Package, X). +{ attr("node", node(0..X-1, Package)) } :- max_nodes(Package, X), not virtual(Package). + +max_nodes(Package, 1) :- virtual(Package). +{ attr("virtual_node", node(0..X-1, Package)) } :- max_nodes(Package, X), virtual(Package). % Integrity constraints on DAG nodes :- attr("root", PackageNode), not attr("node", PackageNode). @@ -36,6 +39,12 @@ :- attr("node_flag_source", ParentNode, _, _), not attr("node", ParentNode). :- attr("node_flag_source", _, _, ChildNode), not attr("node", ChildNode). +% Rules on "unification sets", i.e. on sets of nodes allowing a single configuration of any given package +unification_set("root", PackageNode) :- attr("root", PackageNode). +unification_set(SetID, ChildNode) :- attr("depends_on", ParentNode, ChildNode, _), unification_set(SetID, ParentNode). +unify(SetID, PackageName) :- unification_set(SetID, node(_, PackageName)). +:- 2 { unification_set(SetID, node(_, PackageName)) }, unify(SetID, PackageName). + % Give clingo the choice to solve an input spec or not { literal_solved(ID) } :- literal(ID). literal_not_solved(ID) :- not literal_solved(ID), literal(ID). @@ -52,6 +61,8 @@ opt_criterion(300, "number of input specs not concretized"). #minimize{ 0@300: #true }. #minimize { 1@300,ID : literal_not_solved(ID) }. +% TODO: literals, at the moment, can only influence the "root" unification set. This needs to be extended later. + % Map constraint on the literal ID to facts on the node attr(Name, node(root_node_id, A1)) :- literal(LiteralID, Name, A1), literal_solved(LiteralID). attr(Name, node(root_node_id, A1), A2) :- literal(LiteralID, Name, A1, A2), literal_solved(LiteralID). @@ -209,8 +220,7 @@ condition_holds(ID, node(root_node_id, Package)) :- attr(Name, node(root_node_id, A1), A2, A3) : condition_requirement(ID, Name, A1, A2, A3), Name != "node_flag_source"; attr(Name, node(root_node_id, A1), A2, A3, A4) : condition_requirement(ID, Name, A1, A2, A3, A4); % Special cases - % FIXME (node transformation): is node_flag_source needed? - attr("node_flag_source", node(NodeID, Package), A2, node(ID, A3)) : condition_requirement(ID, "node_flag_source", Package, A2, A3). + attr("node_flag_source", node(root_node_id, Package), A2, node(root_node_id, A3)) : condition_requirement(ID, "node_flag_source", Package, A2, A3). % 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. @@ -225,8 +235,6 @@ attr(Name, node(root_node_id, A1), A2, A3, A4) :- impose(ID, node(NodeID, Packag % Special cases special_case(ID, Name, A1, A2, A3) :- imposed_constraint(ID, Name, A1, A2, A3), Name == "node_flag_source". special_case(ID, Name, A1, A2, A3) :- imposed_constraint(ID, Name, A1, A2, A3), Name == "depends_on". - -% FIXME (node transformation): is node_flag_source needed? attr("node_flag_source", node(NodeID, Package), A2, node(0, A3)) :- impose(ID, node(NodeID, Package)), imposed_constraint(ID, "node_flag_source", Package, A2, A3). attr("depends_on", node(NodeID, Package), node(0, A2), A3) :- impose(ID, node(NodeID, Package)), imposed_constraint(ID, "depends_on", Package, A2, A3). |