From b94e22b28419a13978cf2c86b3b7700bbb9d2601 Mon Sep 17 00:00:00 2001 From: Massimiliano Culpo Date: Thu, 22 Jun 2023 10:26:54 +0200 Subject: ASP-based solver: do not optimize on known dimensions All the solution modes we use imply that we have to solve for all the literals, except for "when possible". Here we remove a minimization on the number of literals not solved, and emit directly a fact when a literal *has* to be solved. --- lib/spack/spack/solver/asp.py | 6 ++++-- lib/spack/spack/solver/concretize.lp | 34 +++++++++------------------------ lib/spack/spack/solver/heuristic.lp | 3 --- lib/spack/spack/solver/when_possible.lp | 20 +++++++++++++++++++ 4 files changed, 33 insertions(+), 30 deletions(-) create mode 100644 lib/spack/spack/solver/when_possible.lp (limited to 'lib') diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py index 56bf7b6a39..b602cdb6d4 100644 --- a/lib/spack/spack/solver/asp.py +++ b/lib/spack/spack/solver/asp.py @@ -779,6 +779,8 @@ class PyclingoDriver: self.control.load(os.path.join(parent_dir, "heuristic.lp")) self.control.load(os.path.join(parent_dir, "os_compatibility.lp")) self.control.load(os.path.join(parent_dir, "display.lp")) + if not setup.concretize_everything: + self.control.load(os.path.join(parent_dir, "when_possible.lp")) timer.stop("load") # Grounding is the first step in the solve -- it turns our facts @@ -2360,8 +2362,8 @@ class SpackSolverSetup: fn.literal(idx, "variant_default_value_from_cli", *clause.args[1:]) ) - if self.concretize_everything: - self.gen.fact(fn.concretize_everything()) + if self.concretize_everything: + self.gen.fact(fn.solve_literal(idx)) def _get_versioned_specs_from_pkg_requirements(self): """If package requirements mention versions that are not mentioned diff --git a/lib/spack/spack/solver/concretize.lp b/lib/spack/spack/solver/concretize.lp index 3268f581f7..ad5418b4be 100644 --- a/lib/spack/spack/solver/concretize.lp +++ b/lib/spack/spack/solver/concretize.lp @@ -7,10 +7,6 @@ % This logic program implements Spack's concretizer %============================================================================= -%----------------------------------------------------------------------------- -% Map literal input specs to facts that drive the solve -%----------------------------------------------------------------------------- - #const root_node_id = 0. #const link_run = 0. @@ -78,21 +74,9 @@ unification_set(SetID, VirtualNode) :- provider(PackageNode, VirtualNode), unifi not attr("virtual_node", node(ID2, Package)), max_nodes(Package, X), ID1=0..X-1, ID2=0..X-1, ID2 < ID1. -% 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). - -% If concretize_everything() is a fact, then we cannot have unsolved specs -:- literal_not_solved(ID), concretize_everything. - -% Make a problem with "zero literals solved" unsat. This is to trigger -% looking for solutions to the ASP problem with "errors", which results -% in better reporting for users. See #30669 for details. -1 { literal_solved(ID) : literal(ID) }. - -opt_criterion(300, "number of input specs not concretized"). -#minimize{ 0@300: #true }. -#minimize { 1@300,ID : literal_not_solved(ID) }. +%----------------------------------------------------------------------------- +% 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. @@ -100,14 +84,14 @@ special_case("node_flag_source"). special_case("depends_on"). % 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). -attr(Name, node(root_node_id, A1), A2, A3) :- literal(LiteralID, Name, A1, A2, A3), literal_solved(LiteralID), not special_case(Name). -attr(Name, node(root_node_id, A1), A2, A3, A4) :- literal(LiteralID, Name, A1, A2, A3, A4), literal_solved(LiteralID). +attr(Name, node(root_node_id, A1)) :- literal(LiteralID, Name, A1), solve_literal(LiteralID). +attr(Name, node(root_node_id, A1), A2) :- literal(LiteralID, Name, A1, A2), solve_literal(LiteralID). +attr(Name, node(root_node_id, A1), A2, A3) :- literal(LiteralID, Name, A1, A2, A3), solve_literal(LiteralID), not special_case(Name). +attr(Name, node(root_node_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(root_node_id, A1), A2, node(root_node_id, A3)) :- literal(LiteralID, "node_flag_source", A1, A2, A3), literal_solved(LiteralID). -attr("depends_on", node(root_node_id, A1), node(root_node_id, A2), A3) :- literal(LiteralID, "depends_on", A1, A2, A3), literal_solved(LiteralID). +attr("node_flag_source", node(root_node_id, A1), A2, node(root_node_id, A3)) :- literal(LiteralID, "node_flag_source", A1, A2, A3), solve_literal(LiteralID). +attr("depends_on", node(root_node_id, A1), node(root_node_id, A2), A3) :- literal(LiteralID, "depends_on", A1, A2, A3), solve_literal(LiteralID). #defined concretize_everything/0. #defined literal/1. diff --git a/lib/spack/spack/solver/heuristic.lp b/lib/spack/spack/solver/heuristic.lp index 7d923219aa..cd5d94978f 100644 --- a/lib/spack/spack/solver/heuristic.lp +++ b/lib/spack/spack/solver/heuristic.lp @@ -6,9 +6,6 @@ %----------------- % Domain heuristic %----------------- -#heuristic literal_solved(ID) : literal(ID). [1, sign] -#heuristic literal_solved(ID) : literal(ID). [50, init] - #heuristic attr("hash", node(0, Package), Hash) : literal(_, "root", Package). [45, init] #heuristic attr("root", node(0, Package)) : literal(_, "root", Package). [45, true] #heuristic attr("node", node(0, Package)) : literal(_, "root", Package). [45, true] diff --git a/lib/spack/spack/solver/when_possible.lp b/lib/spack/spack/solver/when_possible.lp new file mode 100644 index 0000000000..7a8ddfef1c --- /dev/null +++ b/lib/spack/spack/solver/when_possible.lp @@ -0,0 +1,20 @@ +% 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) + +% Give clingo the choice to solve an input spec or not +{ solve_literal(ID) } :- literal(ID). +literal_not_solved(ID) :- not solve_literal(ID), literal(ID). + +% Make a problem with "zero literals solved" unsat. This is to trigger +% looking for solutions to the ASP problem with "errors", which results +% in better reporting for users. See #30669 for details. +1 { solve_literal(ID) : literal(ID) }. + +opt_criterion(300, "number of input specs not concretized"). +#minimize{ 0@300: #true }. +#minimize { 1@300,ID : literal_not_solved(ID) }. + +#heuristic literal_solved(ID) : literal(ID). [1, sign] +#heuristic literal_solved(ID) : literal(ID). [50, init] -- cgit v1.2.3-60-g2f50