summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/spack/spack/solver/asp.py82
-rw-r--r--lib/spack/spack/solver/concretize.lp26
2 files changed, 50 insertions, 58 deletions
diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py
index 37246e5e8c..713f9a50ae 100644
--- a/lib/spack/spack/solver/asp.py
+++ b/lib/spack/spack/solver/asp.py
@@ -389,36 +389,6 @@ class PyclingoDriver(object):
+ rule_atoms
)
- def iff(self, expr1, expr2):
- self.rule(head=expr1, body=expr2)
- self.rule(head=expr2, body=expr1)
-
- def one_of_iff(self, head, versions):
- # if there are no versions, skip this one_of_iff
- if not versions:
- return
-
- 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, tests=False
@@ -894,6 +864,9 @@ class SpackSolverSetup(object):
self.gen.rule(clause, spec_id.symbol())
spec_id_list.append(spec_id)
+ # TODO: find another way to do everything below, without
+ # TODO: generating ground rules.
+
# If one of the external specs is selected then the package
# is external and viceversa
# TODO: make it possible to declare the rule like below
@@ -1267,14 +1240,11 @@ class SpackSolverSetup(object):
if exact_match:
allowed_versions = exact_match
- predicates = [fn.version(pkg_name, v) for v in allowed_versions]
+ # generate facts for each package constraint and the version
+ # that satisfies it
+ for v in allowed_versions:
+ self.gen.fact(fn.version_satisfies(pkg_name, versions, v))
- # 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 define_virtual_constraints(self):
@@ -1303,19 +1273,17 @@ class SpackSolverSetup(object):
compiler_list = list(sorted(set(compiler_list)))
for pkg_name, cspec in self.compiler_version_constraints:
- possible_compiler_versions = [
- fn.node_compiler_version(
- pkg_name, compiler.name, compiler.version)
- for compiler in compiler_list
- if compiler.satisfies(cspec)
- ]
-
- self.gen.one_of_iff(
- fn.node_compiler_version_satisfies(
- pkg_name, cspec.name, cspec.versions),
- possible_compiler_versions,
- )
- self.gen.newline()
+ 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
+ )
+ )
+ self.gen.newline()
def define_target_constraints(self):
@@ -1346,14 +1314,12 @@ class SpackSolverSetup(object):
)
allowed_targets.extend(cache[single_constraint])
- allowed_targets = [
- fn.node_target(spec_name, t) for t in allowed_targets
- ]
-
- self.gen.one_of_iff(
- fn.node_target_satisfies(spec_name, target_constraint),
- allowed_targets,
- )
+ for target in allowed_targets:
+ self.gen.fact(
+ fn.node_target_satisfies(
+ spec_name, 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 728331d91c..e991e66ff2 100644
--- a/lib/spack/spack/solver/concretize.lp
+++ b/lib/spack/spack/solver/concretize.lp
@@ -21,7 +21,15 @@ version_weight(Package, Weight)
version_weight(Package, Weight)
:- version(Package, Version), preferred_version_declared(Package, Version, Weight).
+% version_satisfies implies that exactly one of the satisfying versions
+% is the package's version, and vice versa.
+1 { version(Package, Version) : version_satisfies(Package, Constraint, Version) } 1
+ :- version_satisfies(Package, Constraint).
+version_satisfies(Package, Constraint)
+ :- version(Package, Version), version_satisfies(Package, Constraint, Version).
+
#defined preferred_version_declared/3.
+#defined version_satisfies/3.
%-----------------------------------------------------------------------------
% Dependency semantics
@@ -299,6 +307,13 @@ node_os(Package, OS)
% one target per node -- optimization will pick the "best" one
1 { node_target(Package, Target) : target(Target) } 1 :- node(Package).
+% node_target_satisfies semantics
+1 { node_target(Package, Target) : node_target_satisfies(Package, Constraint, Target) } 1
+ :- node_target_satisfies(Package, Constraint).
+node_target_satisfies(Package, Constraint)
+ :- node_target(Package, Target), node_target_satisfies(Package, Constraint, Target).
+#defined node_target_satisfies/3.
+
% The target weight is either the default target weight
% or a more specific per-package weight if set
target_weight(Target, Package, Weight)
@@ -366,6 +381,17 @@ derive_target_from_parent(Parent, Package)
1 { compiler_weight(Package, Weight) : compiler_weight(Package, Weight) } 1
:- node(Package).
+% 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.
+1 { node_compiler_version(Package, Compiler, Version)
+ : node_compiler_version_satisfies(Package, Compiler, Constraint, Version) } 1
+ :- node_compiler_version_satisfies(Package, Compiler, Constraint).
+node_compiler_version_satisfies(Package, Compiler, Constraint)
+ :- node_compiler_version(Package, Compiler, Version),
+ node_compiler_version_satisfies(Package, Compiler, Constraint, Version).
+#defined node_compiler_version_satisfies/4.
+
% If the compiler version was set from the command line,
% respect it verbatim
node_compiler_version(Package, Compiler, Version) :- node_compiler_version_hard(Package, Compiler, Version).