summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMassimiliano Culpo <massimiliano.culpo@gmail.com>2022-02-10 20:37:10 +0100
committerGitHub <noreply@github.com>2022-02-10 11:37:10 -0800
commite6e109cbc5f1fa3b077bf9f10f65bcd18cf919e6 (patch)
treeaecb8bd54e9f20957ada69095470479a340bdb2c
parent81a6d17f4cfac04107c8560e7b3364cb57d2df97 (diff)
downloadspack-e6e109cbc5f1fa3b077bf9f10f65bcd18cf919e6.tar.gz
spack-e6e109cbc5f1fa3b077bf9f10f65bcd18cf919e6.tar.bz2
spack-e6e109cbc5f1fa3b077bf9f10f65bcd18cf919e6.tar.xz
spack-e6e109cbc5f1fa3b077bf9f10f65bcd18cf919e6.zip
ASP-based solver: reduce input facts and add heuristic (#28848)
* 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
-rw-r--r--lib/spack/spack/solver/asp.py44
-rw-r--r--lib/spack/spack/solver/concretize.lp49
2 files changed, 49 insertions, 44 deletions
diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py
index ea603fd92f..6b656efba0 100644
--- a/lib/spack/spack/solver/asp.py
+++ b/lib/spack/spack/solver/asp.py
@@ -535,10 +535,9 @@ class PyclingoDriver(object):
# 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 @@ class SpackSolverSetup(object):
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 SpackSolverSetup(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 @@ class SpackSolverSetup(object):
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 @@ class SpackSolverSetup(object):
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 @@ class SpackSolverSetup(object):
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 @@ class SpackSolverSetup(object):
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):
diff --git a/lib/spack/spack/solver/concretize.lp b/lib/spack/spack/solver/concretize.lp
index f4c15397e2..13902d0892 100644
--- a/lib/spack/spack/solver/concretize.lp
+++ b/lib/spack/spack/solver/concretize.lp
@@ -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]