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.
This commit is contained in:
Massimiliano Culpo
Todd Gamblin
parent
e25dcf73cd
commit
b94e22b284
4 changed files with 33 additions and 30 deletions
|
|
@ -779,6 +779,8 @@ def visit(node):
|
|||
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 @@ def literal_specs(self, specs):
|
|||
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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
20
lib/spack/spack/solver/when_possible.lp
Normal file
20
lib/spack/spack/solver/when_possible.lp
Normal file
|
|
@ -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]
|
||||
Loading…
Reference in a new issue