summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorMassimiliano Culpo <massimiliano.culpo@gmail.com>2020-12-17 20:57:21 +0100
committerTamara Dahlgren <dahlgren1@llnl.gov>2021-02-17 17:07:30 -0800
commitab3f53d78197da12402e5e742fc6f12911bbb17b (patch)
treeb69199daba2bb727150d846cd2dfab9c1950c32b /lib
parent364c5b636cf4f5dda858c85be3fa9cfb6e6a1e08 (diff)
downloadspack-ab3f53d78197da12402e5e742fc6f12911bbb17b.tar.gz
spack-ab3f53d78197da12402e5e742fc6f12911bbb17b.tar.bz2
spack-ab3f53d78197da12402e5e742fc6f12911bbb17b.tar.xz
spack-ab3f53d78197da12402e5e742fc6f12911bbb17b.zip
concretizer: emit facts for integrity constraints
Diffstat (limited to 'lib')
-rw-r--r--lib/spack/spack/solver/asp.py46
-rw-r--r--lib/spack/spack/solver/concretize.lp31
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).