concretizer: don't use one_of_iff for range constraints (#20383)

Currently, version range constraints, compiler version range constraints,
and target range constraints are implemented by generating ground rules
from `asp.py`, via `one_of_iff()`.  The rules look like this:

```
version_satisfies("python", "2.6:") :- 1 { version("python", "2.4"); ... } 1.
1 { version("python", "2.4"); ... } 1. :- version_satisfies("python", "2.6:").
```

So, `version_satisfies(Package, Constraint)` is true if and only if the
package is assigned a version that satisfies the constraint. We
precompute the set of known versions that satisfy the constraint, and
generate the rule in `SpackSolverSetup`.

We shouldn't need to generate already-ground rules for this. Rather, we
should leave it to the grounder to do the grounding, and generate facts
so that the constraint semantics can be defined in `concretize.lp`.

We can replace rules like the ones above with facts like this:

```
version_satisfies("python", "2.6:", "2.4")
```

And ground them in `concretize.lp` with rules like this:

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

The top rule is the same as before. It makes conditional dependencies and
other places where version constraints are used work properly. Note that
we do not need the cardinality constraint for the second rule -- we
already have rules saying there can be only one version assigned to a
package, so we can just infer from `version/2` `version_satisfies/3`.
This form is also safe for grounding -- If we used the original form we'd
have unsafe variables like `Constraint` and `Package` -- the original
form only really worked when specified as ground to begin with.

- [x] use facts instead of generating rules for package version constraints
- [x] use facts instead of generating rules for compiler version constraints
- [x] use facts instead of generating rules for target range constraints
- [x] remove `one_of_iff()` and `iff()` as they're no longer needed

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