Skip to content

Commit 10129b4

Browse files
alalazoalalazo
committed
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.
1 parent d761d92 commit 10129b4

File tree

4 files changed

+33
-30
lines changed

4 files changed

+33
-30
lines changed

‎lib/spack/spack/solver/asp.py‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -780,6 +780,8 @@ def visit(node):
780780
self.control.load(os.path.join(parent_dir, "heuristic.lp"))
781781
self.control.load(os.path.join(parent_dir, "os_compatibility.lp"))
782782
self.control.load(os.path.join(parent_dir, "display.lp"))
783+
if not setup.concretize_everything:
784+
self.control.load(os.path.join(parent_dir, "when_possible.lp"))
783785
timer.stop("load")
784786

785787
# Grounding is the first step in the solve -- it turns our facts
@@ -2361,8 +2363,8 @@ def literal_specs(self, specs):
23612363
fn.literal(idx, "variant_default_value_from_cli", *clause.args[1:])
23622364
)
23632365

2364-
if self.concretize_everything:
2365-
self.gen.fact(fn.concretize_everything())
2366+
if self.concretize_everything:
2367+
self.gen.fact(fn.solve_literal(idx))
23662368

23672369
def _get_versioned_specs_from_pkg_requirements(self):
23682370
"""If package requirements mention versions that are not mentioned

‎lib/spack/spack/solver/concretize.lp‎

Lines changed: 9 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -7,10 +7,6 @@
77
% This logic program implements Spack's concretizer
88
%=============================================================================
99

10-
%-----------------------------------------------------------------------------
11-
% Map literal input specs to facts that drive the solve
12-
%-----------------------------------------------------------------------------
13-
1410
#const root_node_id = 0.
1511

1612
#const link_run = 0.
@@ -78,36 +74,24 @@ unification_set(SetID, VirtualNode) :- provider(PackageNode, VirtualNode), unifi
7874
not attr("virtual_node", node(ID2, Package)),
7975
max_nodes(Package, X), ID1=0..X-1, ID2=0..X-1, ID2 < ID1.
8076

81-
% Give clingo the choice to solve an input spec or not
82-
{ literal_solved(ID) } :- literal(ID).
83-
literal_not_solved(ID) :- not literal_solved(ID), literal(ID).
84-
85-
% If concretize_everything() is a fact, then we cannot have unsolved specs
86-
:- literal_not_solved(ID), concretize_everything.
87-
88-
% Make a problem with "zero literals solved" unsat. This is to trigger
89-
% looking for solutions to the ASP problem with "errors", which results
90-
% in better reporting for users. See #30669 for details.
91-
1 { literal_solved(ID) : literal(ID) }.
92-
93-
opt_criterion(300, "number of input specs not concretized").
94-
#minimize{ 0@300: #true }.
95-
#minimize { 1@300,ID : literal_not_solved(ID) }.
77+
%-----------------------------------------------------------------------------
78+
% Map literal input specs to facts that drive the solve
79+
%-----------------------------------------------------------------------------
9680

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

9983
special_case("node_flag_source").
10084
special_case("depends_on").
10185

10286
% Map constraint on the literal ID to facts on the node
103-
attr(Name, node(root_node_id, A1)) :- literal(LiteralID, Name, A1), literal_solved(LiteralID).
104-
attr(Name, node(root_node_id, A1), A2) :- literal(LiteralID, Name, A1, A2), literal_solved(LiteralID).
105-
attr(Name, node(root_node_id, A1), A2, A3) :- literal(LiteralID, Name, A1, A2, A3), literal_solved(LiteralID), not special_case(Name).
106-
attr(Name, node(root_node_id, A1), A2, A3, A4) :- literal(LiteralID, Name, A1, A2, A3, A4), literal_solved(LiteralID).
87+
attr(Name, node(root_node_id, A1)) :- literal(LiteralID, Name, A1), solve_literal(LiteralID).
88+
attr(Name, node(root_node_id, A1), A2) :- literal(LiteralID, Name, A1, A2), solve_literal(LiteralID).
89+
attr(Name, node(root_node_id, A1), A2, A3) :- literal(LiteralID, Name, A1, A2, A3), solve_literal(LiteralID), not special_case(Name).
90+
attr(Name, node(root_node_id, A1), A2, A3, A4) :- literal(LiteralID, Name, A1, A2, A3, A4), solve_literal(LiteralID).
10791

10892
% Special cases where nodes occur in arguments other than A1
109-
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).
110-
attr("depends_on", node(root_node_id, A1), node(root_node_id, A2), A3) :- literal(LiteralID, "depends_on", A1, A2, A3), literal_solved(LiteralID).
93+
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).
94+
attr("depends_on", node(root_node_id, A1), node(root_node_id, A2), A3) :- literal(LiteralID, "depends_on", A1, A2, A3), solve_literal(LiteralID).
11195

11296
#defined concretize_everything/0.
11397
#defined literal/1.

‎lib/spack/spack/solver/heuristic.lp‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,6 @@
66
%-----------------
77
% Domain heuristic
88
%-----------------
9-
#heuristic literal_solved(ID) : literal(ID). [1, sign]
10-
#heuristic literal_solved(ID) : literal(ID). [50, init]
11-
129
#heuristic attr("hash", node(0, Package), Hash) : literal(_, "root", Package). [45, init]
1310
#heuristic attr("root", node(0, Package)) : literal(_, "root", Package). [45, true]
1411
#heuristic attr("node", node(0, Package)) : literal(_, "root", Package). [45, true]

‎lib/spack/spack/solver/when_possible.lp‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
% Copyright 2013-2023 Lawrence Livermore National Security, LLC and other
2+
% Spack Project Developers. See the top-level COPYRIGHT file for details.
3+
%
4+
% SPDX-License-Identifier: (Apache-2.0 OR MIT)
5+
6+
% Give clingo the choice to solve an input spec or not
7+
{ solve_literal(ID) } :- literal(ID).
8+
literal_not_solved(ID) :- not solve_literal(ID), literal(ID).
9+
10+
% Make a problem with "zero literals solved" unsat. This is to trigger
11+
% looking for solutions to the ASP problem with "errors", which results
12+
% in better reporting for users. See #30669 for details.
13+
1 { solve_literal(ID) : literal(ID) }.
14+
15+
opt_criterion(300, "number of input specs not concretized").
16+
#minimize{ 0@300: #true }.
17+
#minimize { 1@300,ID : literal_not_solved(ID) }.
18+
19+
#heuristic literal_solved(ID) : literal(ID). [1, sign]
20+
#heuristic literal_solved(ID) : literal(ID). [50, init]

0 commit comments

Comments
 (0)