From 115384afbd61f3fb82ba102431c3910ed2773f51 Mon Sep 17 00:00:00 2001 From: Todd Gamblin Date: Wed, 10 Jun 2020 20:45:16 -0700 Subject: concretizer: use cardinality constraints for versions Instead of python callbacks, use cardinality constraints for package versions. This is slightly faster and has the advantage that it can be written to an ASP program to be executed *outside* of Spack. We can use this in the future to unify the pyclingo driver and the clingo text driver. This makes use of add_weight_rule() to implement cardinality constraints. add_weight_rule() only has a lower bound parameter, but you can implement a strict "exactly one of" constraint using it. In particular, wee want to define: 1 {v1; v2; v3; ...} 1 :- version_satisfies(pkg, constraint). version_satisfies(pkg, constraint) :- 1 {v1; v2; v3; ...} 1. And we do that like this, for every version constraint: atleast1(pkg, constr) :- 1 {version(pkg, v1); version(pkg, v2); ...}. morethan1(pkg, constr) :- 2 {version(pkg, v1); version(pkg, v2); ...}. version_satisfies(pkg, constr) :- atleast1, not morethan1(pkg, constr). :- version_satisfies(pkg, constr), morethan1. :- version_satisfies(pkg, constr), not atleast1. v1, v2, v3, etc. are computed on the Python side by comparing every possible package version with the constraint. Computing things like this has the added advantage that if v1, v2, v3, etc. comprise *all* possible versions of a package, we can just omit the rules for the constraint under consideration. This happens pretty frequently in the Spack mainline. --- lib/spack/spack/cmd/solve.py | 1 + lib/spack/spack/solver/asp.py | 88 ++++++++++++++++++++++++------------ lib/spack/spack/solver/concretize.lp | 12 ----- lib/spack/spack/spec.py | 1 + 4 files changed, 60 insertions(+), 42 deletions(-) diff --git a/lib/spack/spack/cmd/solve.py b/lib/spack/spack/cmd/solve.py index 480ced6a29..b343861b55 100644 --- a/lib/spack/spack/cmd/solve.py +++ b/lib/spack/spack/cmd/solve.py @@ -105,6 +105,7 @@ def solve(parser, args): # die if no solution was found # TODO: we need to be able to provide better error messages than this if not result.satisfiable: + result.print_cores() tty.die("Unsatisfiable spec.") # dump the solutions as concretized specs diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py index eb01a4b77a..6fb838109e 100644 --- a/lib/spack/spack/solver/asp.py +++ b/lib/spack/spack/solver/asp.py @@ -218,6 +218,12 @@ class Result(object): self.answers = [] self.cores = [] + def print_cores(self): + for core in self.cores: + tty.msg( + "The following constraints are unsatisfiable:", + *sorted(str(symbol) for symbol in core)) + class ClingoDriver(object): def __init__(self): @@ -477,14 +483,30 @@ class PyclingoDriver(object): [atoms[s] for s in args] + rule_atoms ) + def one_of_iff(self, head, versions): + self.out.write("%s :- %s.\n" % (head, AspOneOf(*versions))) + self.out.write("%s :- %s.\n" % (AspOneOf(*versions), head)) + + at_least_1_sym = fn.at_least_1(*head.args).symbol() + at_least_1 = self.backend.add_atom(at_least_1_sym) + + more_than_1_sym = fn.more_than_1(*head.args).symbol() + more_than_1 = self.backend.add_atom(more_than_1_sym) + + version_atoms = [self.backend.add_atom(f.symbol()) for f in versions] + self.backend.add_weight_rule( + [at_least_1], 1, [(v, 1) for v in version_atoms]) + self.backend.add_weight_rule( + [more_than_1], 2, [(v, 1) for v in version_atoms]) + + head_atom = self.backend.add_atom(head.symbol()) + self.backend.add_rule([head_atom], [at_least_1, -more_than_1]) + + self.backend.add_rule([], [head_atom, more_than_1]) + self.backend.add_rule([], [head_atom, -at_least_1]) + def solve(self, solver_setup, specs, dump=None, nmodels=0, timers=False, stats=False): - calls = [0] - class Context(object): - def version_satisfies(self, a, b): - calls[0] += 1 - return bool(ver(a.string).satisfies(ver(b.string))) - timer = Timer() # Initialize the control object for the solver @@ -509,13 +531,14 @@ class PyclingoDriver(object): # Grounding is the first step in the solve -- it turns our facts # and first-order logic rules into propositional logic. - self.control.ground([("base", [])], context=Context()) + self.control.ground([("base", [])]) timer.phase("ground") # With a grounded program, we can run the solve. result = Result() models = [] # stable moodels if things go well cores = [] # unsatisfiable cores if they do not + def on_model(model): models.append((model.cost, model.symbols(shown=True))) @@ -549,6 +572,7 @@ class PyclingoDriver(object): sym = symbols[atom] if sym.name == "rule": sym = sym.arguments[0].string + core_symbols.append(sym) result.cores.append(core_symbols) if timers: @@ -636,23 +660,6 @@ class SpackSolverSetup(object): self.version_constraints.add((spec.name, spec.versions)) return [fn.version_satisfies(spec.name, spec.versions)] - # # version must be *one* of the ones the spec allows. - # allowed_versions = [ - # v for v in sorted(self.possible_versions[spec.name]) - # if v.satisfies(spec.versions) - # ] - - # # don't bother restricting anything if all versions are allowed - # if len(allowed_versions) == len(self.possible_versions[spec.name]): - # return [] - - # predicates = [fn.version(spec.name, v) for v in allowed_versions] - - # # conflict with any versions that do not satisfy the spec - # if predicates: - # return [self.gen.one_of(*predicates)] - # return [] - def available_compilers(self): """Facts about available compilers.""" @@ -909,7 +916,6 @@ class SpackSolverSetup(object): if compiler.satisfies(spec.compiler) ] - clauses.append(self.gen.one_of(*possible_compiler_versions)) for version in possible_compiler_versions: clauses.append( @@ -984,8 +990,8 @@ class SpackSolverSetup(object): possible.add(spec.architecture.os) # make directives for possible OS's - for os in sorted(possible): - self.gen.fact(fn.os(os)) + for possible_os in sorted(possible): + self.gen.fact(fn.os(possible_os)) # mark this one as default self.gen.fact(fn.node_os_default(platform.default_os)) @@ -1086,6 +1092,29 @@ class SpackSolverSetup(object): return cspecs + def define_version_constraints(self): + """Define what version_satisfies(...) means in ASP logic.""" + for pkg_name, versions in sorted(self.version_constraints): + # version must be *one* of the ones the spec allows. + allowed_versions = [ + v for v in sorted(self.possible_versions[pkg_name]) + if v.satisfies(versions) + ] + + # don't bother restricting anything if all versions are allowed + if len(allowed_versions) == len(self.possible_versions[pkg_name]): + continue + + predicates = [fn.version(pkg_name, v) for v in allowed_versions] + + # version_satisfies(pkg, constraint) is true if and only if a + # satisfying version is set for the package + self.gen.one_of_iff( + fn.version_satisfies(pkg_name, versions), + predicates, + ) + self.gen.newline() + def setup(self, driver, specs): """Generate an ASP program with relevant constraints for specs. @@ -1150,9 +1179,8 @@ class SpackSolverSetup(object): self.gen.fact(clause) self.gen.h1("Version Constraints") - for name, versions in sorted(self.version_constraints): - self.gen.fact(fn.version_constraint(name, versions)) - self.gen.newline() + self.define_version_constraints() + class SpecBuilder(object): """Class with actions to rebuild a spec from ASP results.""" diff --git a/lib/spack/spack/solver/concretize.lp b/lib/spack/spack/solver/concretize.lp index 604720c6a4..513f9e3e4a 100644 --- a/lib/spack/spack/solver/concretize.lp +++ b/lib/spack/spack/solver/concretize.lp @@ -14,22 +14,10 @@ version_declared(Package, Version) :- version_declared(Package, Version, _). 1 { version(Package, Version) : version_declared(Package, Version) } 1 :- node(Package). -% no conflicting versions can be assigned -:- version(Package, Version), - version_satisfies(Package, Constraint), - 0 = @version_satisfies(Version, Constraint). - -version_satisfies(Package, Constraint) - :- node(Package), - version(Package, Version), - version_constraint(Package, Constraint), - 1 = @version_satisfies(Version, Constraint). - version_weight(Package, Weight) :- version(Package, Version), version_declared(Package, Version, Weight). #defined version_conflict/2. -#defined version_constraint/2. %----------------------------------------------------------------------------- % Dependency semantics diff --git a/lib/spack/spack/spec.py b/lib/spack/spack/spec.py index ab429b5e49..bddba98d71 100644 --- a/lib/spack/spack/spec.py +++ b/lib/spack/spack/spec.py @@ -2428,6 +2428,7 @@ class Spec(object): result = spack.solver.asp.solve([self]) if not result.satisfiable: + result.print_cores() raise spack.error.UnsatisfiableSpecError( self, "unknown", "Unsatisfiable!") -- cgit v1.2.3-70-g09d2