From ab3f53d78197da12402e5e742fc6f12911bbb17b Mon Sep 17 00:00:00 2001 From: Massimiliano Culpo Date: Thu, 17 Dec 2020 20:57:21 +0100 Subject: concretizer: emit facts for integrity constraints --- lib/spack/spack/solver/asp.py | 46 +++++++----------------------------- lib/spack/spack/solver/concretize.lp | 31 ++++++++++++++++++++++++ 2 files changed, 40 insertions(+), 37 deletions(-) diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py index c57cf68aa6..3c7a1bfd17 100644 --- a/lib/spack/spack/solver/asp.py +++ b/lib/spack/spack/solver/asp.py @@ -356,39 +356,6 @@ class PyclingoDriver(object): [atoms[s] for s in body_symbols] + rule_atoms ) - def integrity_constraint(self, clauses, default_negated=None): - """Add an integrity constraint to the solver. - - Args: - clauses: clauses to be added to the integrity constraint - default_negated: clauses to be added to the integrity - constraint after with a default negation - """ - symbols, negated_symbols, atoms = _normalize(clauses), [], {} - if default_negated: - negated_symbols = _normalize(default_negated) - - for s in symbols + negated_symbols: - atoms[s] = self.backend.add_atom(s) - - symbols_str = ",".join(str(a) for a in symbols) - if negated_symbols: - negated_symbols_str = ",".join( - "not " + str(a) for a in negated_symbols - ) - symbols_str += ",{0}".format(negated_symbols_str) - rule_str = ":- {0}.".format(symbols_str) - rule_atoms = self._register_rule_for_cores(rule_str) - - # print rule before adding - self.out.write("{0}\n".format(rule_str)) - self.backend.add_rule( - [], - [atoms[s] for s in symbols] + - [-atoms[s] for s in negated_symbols] - + rule_atoms - ) - def solve( self, solver_setup, specs, dump=None, nmodels=0, timers=False, stats=False, tests=False @@ -588,11 +555,16 @@ class SpackSolverSetup(object): # TODO: of a rule and filter unwanted functions. to_be_filtered = ['node_compiler_hard'] clauses = [x for x in clauses if x.name not in to_be_filtered] - external = fn.external(pkg.name) - self.gen.integrity_constraint( - AspAnd(*clauses), AspAnd(external) - ) + # Emit facts based on clauses + cond_id = self._condition_id_counter + self._condition_id_counter += 1 + self.gen.fact(fn.conflict(cond_id, pkg.name)) + for clause in clauses: + self.gen.fact(fn.conflict_condition( + cond_id, clause.name, *clause.args + )) + self.gen.newline() def available_compilers(self): """Facts about available compilers.""" diff --git a/lib/spack/spack/solver/concretize.lp b/lib/spack/spack/solver/concretize.lp index 233de6f58e..75f2af1e59 100644 --- a/lib/spack/spack/solver/concretize.lp +++ b/lib/spack/spack/solver/concretize.lp @@ -59,6 +59,8 @@ dependency_conditions(P, D, T) :- dependency_conditions_hold(P, D, I), dependency_type(I, T). +#defined dependency_type/2. + % collect all the dependency conditions into a single conditional rule dependency_conditions_hold(Package, Dependency, ID) :- version(Package, Version) @@ -82,6 +84,32 @@ dependency_conditions_hold(Package, Dependency, ID) :- dependency_condition(Package, Dependency, ID); node(Package). +#defined dependency_condition/3. +#defined required_dependency_condition/3. +#defined required_dependency_condition/4. +#defined required_dependency_condition/5. +#defined required_dependency_condition/5. + +% general rules for conflicts +:- node(Package) : conflict_condition(ID, "node", Package); + not external(Package) : conflict_condition(ID, "node", Package); + version(Package, Version) : conflict_condition(ID, "version", Package, Version); + version_satisfies(Package, Constraint) : conflict_condition(ID, "version_satisfies", Package, Constraint); + node_platform(Package, Platform) : conflict_condition(ID, "node_platform", Package, Platform); + node_os(Package, OS) : conflict_condition(ID, "node_os", Package, OS); + node_target(Package, Target) : conflict_condition(ID, "node_target", Package, Target); + variant_value(Package, Variant, Value) : conflict_condition(ID, "variant_value", Package, Variant, Value); + node_compiler(Package, Compiler) : conflict_condition(ID, "node_compiler", Package, Compiler); + node_compiler_version(Package, Compiler, Version) : conflict_condition(ID, "node_compiler_version", Package, Compiler, Version); + node_compiler_version_satisfies(Package, Compiler, Version) : conflict_condition(ID, "node_compiler_version_satisfies", Package, Compiler, Version); + node_flag(Package, FlagType, Flag) : conflict_condition(ID, "node_flag", Package, FlagType, Flag); + conflict(ID, Package). + +#defined conflict/2. +#defined conflict_condition/3. +#defined conflict_condition/4. +#defined conflict_condition/5. + % Implications from matching a dependency condition node(Dependency) :- dependency_conditions_hold(Package, Dependency, ID), @@ -137,6 +165,9 @@ node_flag(Dependency, FlagType, Flag) :- depends_on(Package, Dependency), imposed_dependency_condition(ID, "node_flag", Dependency, FlagType, Flag). +#defined imposed_dependency_condition/4. +#defined imposed_dependency_condition/5. + % if a virtual was required by some root spec, one provider is in the DAG 1 { node(Package) : provides_virtual(Package, Virtual) } 1 :- virtual_node(Virtual). -- cgit v1.2.3-70-g09d2