From e6e109cbc5f1fa3b077bf9f10f65bcd18cf919e6 Mon Sep 17 00:00:00 2001 From: Massimiliano Culpo Date: Thu, 10 Feb 2022 20:37:10 +0100 Subject: 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 --- lib/spack/spack/solver/asp.py | 44 +++++++++++++------------------- lib/spack/spack/solver/concretize.lp | 49 +++++++++++++++++++++++------------- 2 files changed, 49 insertions(+), 44 deletions(-) (limited to 'lib') 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] -- cgit v1.2.3-60-g2f50