hlrs-software-stack/spack
7
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

concretizer: emit facts for integrity constraints

Browse source
This commit is contained in:
Massimiliano Culpo 2020-12-17 20:57:21 +01:00 committed by Todd Gamblin
parent e644255770
commit 72569a0198
2 changed files with 40 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
lib/spack/spack/solver/asp.py
View file

@ -356,39 +356,6 @@ def rule(self, head, body):
[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 @@ def conflict_rules(self, pkg):
# 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."""

31
lib/spack/spack/solver/concretize.lp
View file

@ -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).