zhangyiss/spack
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

ASP-based solver: reduce input facts and add heuristic (#28848)

Browse Source 
* Remove node_target_satisfies/3 in favor of target_satisfies/2

When emitting input facts we don't need to couple target with
packages, but we can emit fewer facts independently and let
the grounder combine them.

* Remove compiler_version_satisfies/4 in favor of compiler_version_satisfies/3

When emitting input facts we don't need to couple compilers with
packages, but we can emit fewer facts independently and let
the grounder combine them.

* Introduce heuristic in the ASP-program

With heuristic we can drive clingo to make better
initial guesses, which lead to fewer choices and
conflicts in the overall solve
This commit is contained in:
Massimiliano Culpo
2022-02-10 20:37:10 +01:00
committed by GitHub
parent 81a6d17f4c
commit e6e109cbc5
2 changed files with 49 additions and 44 deletions
Download Patch File Download Diff File Expand all files Collapse all files

44
lib/spack/spack/solver/asp.py
View File

@@ -535,10 +535,9 @@ def solve(
# Initialize the control object for the solver
self.control = clingo.Control()
self.control.configuration.solve.models = nmodels
self.control.configuration.asp.trans_ext = 'all'
self.control.configuration.asp.eq = '5'
self.control.configuration.configuration = 'tweety'
self.control.configuration.solve.models = nmodels
self.control.configuration.solver.heuristic = 'Domain'
self.control.configuration.solve.parallel_mode = '1'
self.control.configuration.solver.opt_strategy = "usc,one"
@@ -717,7 +716,7 @@ def target_ranges(self, spec, single_target_fn):
if str(target) in archspec.cpu.TARGETS:
return [single_target_fn(spec.name, target)]
self.target_constraints.add((spec.name, target))
self.target_constraints.add(target)
return [fn.node_target_satisfies(spec.name, target)]
def conflict_rules(self, pkg):
@@ -1218,8 +1217,7 @@ class Body(object):
clauses.append(
fn.node_compiler_version_satisfies(
spec.name, spec.compiler.name, spec.compiler.versions))
self.compiler_version_constraints.add(
(spec.name, spec.compiler))
self.compiler_version_constraints.add(spec.compiler)
# compiler flags
for flag_type, flags in spec.compiler_flags.items():
@@ -1405,9 +1403,12 @@ def target_defaults(self, specs):
for target in supported:
best_targets.add(target.name)
self.gen.fact(fn.compiler_supports_target(
compiler.name, compiler.version, target.name))
self.gen.fact(fn.compiler_supports_target(
compiler.name, compiler.version, uarch.family.name))
compiler.name, compiler.version, target.name
))
self.gen.fact(fn.compiler_supports_target(
compiler.name, compiler.version, uarch.family.name
))
# add any targets explicitly mentioned in specs
for spec in specs:
@@ -1536,18 +1537,12 @@ def versions_for(v):
def define_compiler_version_constraints(self):
compiler_list = spack.compilers.all_compiler_specs()
compiler_list = list(sorted(set(compiler_list)))
for pkg_name, cspec in self.compiler_version_constraints:
for constraint in sorted(self.compiler_version_constraints):
for compiler in compiler_list:
if compiler.satisfies(cspec):
self.gen.fact(
fn.node_compiler_version_satisfies(
pkg_name,
cspec.name,
cspec.versions,
compiler.version
)
)
if compiler.satisfies(constraint):
self.gen.fact(fn.compiler_version_satisfies(
constraint.name, constraint.versions, compiler.version
))
self.gen.newline()
def define_target_constraints(self):
@@ -1572,8 +1567,7 @@ def _all_targets_satisfiying(single_constraint):
return allowed_targets
cache = {}
for spec_name, target_constraint in sorted(self.target_constraints):
for target_constraint in sorted(self.target_constraints):
# Construct the list of allowed targets for this constraint
allowed_targets = []
for single_constraint in str(target_constraint).split(','):
@@ -1584,11 +1578,7 @@ def _all_targets_satisfiying(single_constraint):
allowed_targets.extend(cache[single_constraint])
for target in allowed_targets:
self.gen.fact(
fn.node_target_satisfies(
spec_name, target_constraint, target
)
)
self.gen.fact(fn.target_satisfies(target_constraint, target))
self.gen.newline()
def define_variant_values(self):

49
lib/spack/spack/solver/concretize.lp
View File

@@ -15,7 +15,7 @@
:- not 1 { version(Package, _) } 1, node(Package).
% each node must have a single platform, os and target
:- not 1 { node_platform(Package, _) } 1, node(Package).
:- not 1 { node_platform(Package, _) } 1, node(Package), error("A node must have exactly one platform").
:- not 1 { node_os(Package, _) } 1, node(Package).
:- not 1 { node_target(Package, _) } 1, node(Package).
@@ -34,7 +34,7 @@ version_declared(Package, Version, Weight) :- version_declared(Package, Version,
% We can't emit the same version **with the same weight** from two different sources
:- version_declared(Package, Version, Weight, Origin1),
version_declared(Package, Version, Weight, Origin2),
Origin1 != Origin2,
Origin1 < Origin2,
error("Internal error: two versions with identical weights").
% versions are declared w/priority -- declared with priority implies declared
@@ -450,7 +450,7 @@ variant_set(Package, Variant) :- variant_set(Package, Variant, _).
variant_value(Package, Variant, Value2),
variant_value_from_disjoint_sets(Package, Variant, Value1, Set1),
variant_value_from_disjoint_sets(Package, Variant, Value2, Set2),
Set1 != Set2,
Set1 < Set2,
build(Package),
error("Variant values selected from multiple disjoint sets").
@@ -546,9 +546,6 @@ variant_single_value(Package, "dev_path")
% Platform semantics
%-----------------------------------------------------------------------------
% one platform per node
:- M = #count { Platform : node_platform(Package, Platform) }, M !=1, node(Package), error("A node must have exactly one platform").
% if no platform is set, fall back to the default
node_platform(Package, Platform)
:- node(Package),
@@ -614,15 +611,21 @@ node_os(Package, OS) :- node_os_set(Package, OS), node(Package).
%-----------------------------------------------------------------------------
% Target semantics
%-----------------------------------------------------------------------------
% one target per node -- optimization will pick the "best" one
% Each node has only one target chosen among the known targets
1 { node_target(Package, Target) : target(Target) } 1 :- node(Package), error("Each node must have exactly one target").
% node_target_satisfies semantics
1 { node_target(Package, Target) : node_target_satisfies(Package, Constraint, Target) } 1
% If a node must satisfy a target constraint the choice is reduced among the targets
% that satisfy that constraint
1 { node_target(Package, Target) : target_satisfies(Constraint, Target) } 1
:- node_target_satisfies(Package, Constraint), error("Each node must have exactly one target").
% If a node has a target and the target satisfies a constraint, then the target
% associated with the node satisfies the same constraint
node_target_satisfies(Package, Constraint)
:- node_target(Package, Target), node_target_satisfies(Package, Constraint, Target).
#defined node_target_satisfies/3.
:- node_target(Package, Target), target_satisfies(Constraint, Target).
#defined target_satisfies/2.
% The target weight is either the default target weight
% or a more specific per-package weight if set
@@ -702,20 +705,21 @@ node_compiler(Package, Compiler) :- node_compiler_version(Package, Compiler, _).
Compiler1 != Compiler2,
error("Internal error: mismatch between selected compiler and compiler version").
% define node_compiler_version_satisfies/3 from node_compiler_version_satisfies/4
% version_satisfies implies that exactly one of the satisfying versions
% is the package's version, and vice versa.
% If the compiler of a node must satisfy a constraint, then its version
% must be chosen among the ones that satisfy said constraint
1 { node_compiler_version(Package, Compiler, Version)
: node_compiler_version_satisfies(Package, Compiler, Constraint, Version) } 1 :-
: compiler_version_satisfies(Compiler, Constraint, Version) } 1 :-
node_compiler_version_satisfies(Package, Compiler, Constraint),
error("Internal error: node compiler version mismatch").
% 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
node_compiler_version_satisfies(Package, Compiler, Constraint)
:- node_compiler_version(Package, Compiler, Version),
node_compiler_version_satisfies(Package, Compiler, Constraint, Version),
compiler_version_satisfies(Compiler, Constraint, Version),
build(Package).
#defined node_compiler_version_satisfies/4.
#defined compiler_version_satisfies/3.
% If the compiler version was set from the command line,
% respect it verbatim
@@ -1017,3 +1021,14 @@ opt_criterion(1, "non-preferred targets").
: node_target_weight(Package, Weight),
build_priority(Package, Priority)
}.
%-----------------
% Domain heuristic
%-----------------
#heuristic version(Package, Version) : version_declared(Package, Version, 0), node(Package). [10, true]
#heuristic version_weight(Package, 0) : version_declared(Package, Version, 0), node(Package). [10, true]
#heuristic node_target(Package, Target) : default_target_weight(Target, 0), node(Package). [10, true]
#heuristic node_target_weight(Package, 0) : node(Package). [10, true]
#heuristic variant_value(Package, Variant, Value) : variant_default_value(Package, Variant, Value), node(Package). [10, true]
#heuristic provider(Package, Virtual) : possible_provider_weight(Package, Virtual, 0, _), virtual_node(Virtual). [10, true]
#heuristic node(Package) : possible_provider_weight(Package, Virtual, 0, _), virtual_node(Virtual). [10, true]