concretizer: convert virtuals to facts; move all rules to `concretize.lp`

This converts the virtual handling in the new concretizer from
already-ground rules to facts. This is the last thing that needs to be
refactored, and it converts the entire concretizer to just use facts.

The previous way of handling virtuals hinged on rules involving
`single_provider_for` facts that were tied to the virtual and a version
range. The new method uses the condition pattern we've been using for
dependencies, externals, and conflicts.

To handle virtuals as conditions, we impose constraints on "fake" virtual
specs in the logic program. i.e., `version_satisfies("mpi", "2.0:",
"2.0")` is legal whereas before we wouldn't have seen something like
this. Currently, constriants are only handled on versions -- we don't
handle variants or anything else yet, but they key change here is that we
*could*. For a long time, virtual handling in Spack has only dealt with
versions, and we'd like to be able to handle variants as well. We could
easily add an integrity constraint to handle variants like the one we use
for versions.

One issue with the implementation here is that virtual packages don't
actually declare possible versions like regular packages do. To get
around that, we implement an integrity constraint like this:

    :- virtual_node(Virtual),
       version_satisfies(Virtual, V1), version_satisfies(Virtual, V2),
       not version_constraint_satisfies(Virtual, V1, V2).

This requires us to compare every version constraint to every other, both
in program generation and within the concretizer -- so there's a
potentially quadratic evaluation time on virtual constraints because we
don't have a real version to "anchor" things to. We just say that all the
constraints need to agree for the virtual constraint to hold.

We can investigate adding synthetic versions for virtuals in the future,
to speed this up.

2 files changed, 164 insertions, 116 deletions

diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py
index 7f7ceeafc0..19b7b438be 100644
--- a/lib/spack/spack/solver/asp.py
+++ b/lib/spack/spack/solver/asp.py
@@ -456,8 +456,6 @@ class SpackSolverSetup(object):
         self.variant_values_from_specs = set()
         self.version_constraints = set()
         self.target_constraints = set()
-        self.providers_by_vspec_name = collections.defaultdict(list)
-        self.virtual_constraints = set()
         self.compiler_version_constraints = set()
         self.post_facts = []
 
@@ -686,6 +684,9 @@ class SpackSolverSetup(object):
         # default compilers for this package
         self.package_compiler_defaults(pkg)
 
+        # virtuals
+        self.package_provider_rules(pkg)
+
         # dependencies
         self.package_dependencies_rules(pkg, tests)
 
@@ -697,18 +698,74 @@ class SpackSolverSetup(object):
             )
         )
 
+    def _condition_facts(
+            self, pkg_name, cond_spec, dep_spec,
+            cond_fn, require_fn, impose_fn
+    ):
+        """Generate facts for a dependency or virtual provider condition.
+
+        Arguments:
+            pkg_name (str): name of the package that triggers the
+                condition (e.g., the dependent or the provider)
+            cond_spec (Spec): the dependency spec representing the
+                condition that needs to be True (can be anonymous)
+            dep_spec (Spec): the sepc of the dependency or provider
+                to be depended on/provided if the condition holds.
+            cond_fn (AspFunction): function to use to declare the condition;
+                will be called with the cond id, pkg_name, an dep_spec.name
+            require_fn (AspFunction): function to use to declare the conditions
+                required of the dependent/provider to trigger
+            impose_fn (AspFunction): function to use for constraints imposed
+                on the dependency/virtual
+
+        Returns:
+            (int): id of the condition created by this function
+        """
+        condition_id = next(self._condition_id_counter)
+        named_cond = cond_spec.copy()
+        named_cond.name = named_cond.name or pkg_name
+
+        self.gen.fact(cond_fn(condition_id, pkg_name, dep_spec.name))
+
+        # conditions that trigger the condition
+        conditions = self.spec_clauses(named_cond, body=True)
+        for pred in conditions:
+            self.gen.fact(require_fn(condition_id, pred.name, *pred.args))
+
+        imposed_constraints = self.spec_clauses(dep_spec)
+        for pred in imposed_constraints:
+            # imposed "node"-like conditions are no-ops
+            if pred.name in ("node", "virtual_node"):
+                continue
+            self.gen.fact(impose_fn(condition_id, pred.name, *pred.args))
+
+        return condition_id
+
+    def package_provider_rules(self, pkg):
+        for provider_name in sorted(set(s.name for s in pkg.provided.keys())):
+            self.gen.fact(fn.possible_provider(pkg.name, provider_name))
+
+        for provided, whens in pkg.provided.items():
+            for when in whens:
+                self._condition_facts(
+                    pkg.name, when, provided,
+                    fn.provider_condition,
+                    fn.required_provider_condition,
+                    fn.imposed_dependency_condition
+                )
+
+            self.gen.newline()
+
     def package_dependencies_rules(self, pkg, tests):
         """Translate 'depends_on' directives into ASP logic."""
         for _, conditions in sorted(pkg.dependencies.items()):
             for cond, dep in sorted(conditions.items()):
-                condition_id = next(self._condition_id_counter)
-                named_cond = cond.copy()
-                named_cond.name = named_cond.name or pkg.name
-
-                # each independent condition has an id
-                self.gen.fact(fn.dependency_condition(
-                    condition_id, dep.pkg.name, dep.spec.name
-                ))
+                condition_id = self._condition_facts(
+                    pkg.name, cond, dep.spec,
+                    fn.dependency_condition,
+                    fn.required_dependency_condition,
+                    fn.imposed_dependency_condition
+                )
 
                 for t in sorted(dep.type):
                     # Skip test dependencies if they're not requested at all
@@ -723,35 +780,6 @@ class SpackSolverSetup(object):
                     # there is a declared dependency of type t
                     self.gen.fact(fn.dependency_type(condition_id, t))
 
-                # if it has conditions, declare them.
-                conditions = self.spec_clauses(named_cond, body=True)
-                for cond in conditions:
-                    self.gen.fact(fn.required_dependency_condition(
-                        condition_id, cond.name, *cond.args
-                    ))
-
-                # add constraints on the dependency from dep spec.
-
-                # TODO: nest this in the type loop so that dependency
-                # TODO: constraints apply only for their deptypes and
-                # TODO: specific conditions.
-                if spack.repo.path.is_virtual(dep.spec.name):
-                    self.virtual_constraints.add(str(dep.spec))
-                    conditions = ([fn.real_node(pkg.name)] +
-                                  self.spec_clauses(named_cond, body=True))
-                    self.gen.rule(
-                        head=fn.single_provider_for(
-                            str(dep.spec.name), str(dep.spec.versions)
-                        ),
-                        body=self.gen._and(*conditions)
-                    )
-                else:
-                    clauses = self.spec_clauses(dep.spec)
-                    for clause in clauses:
-                        self.gen.fact(fn.imposed_dependency_condition(
-                            condition_id, clause.name, *clause.args
-                        ))
-
                 self.gen.newline()
 
     def virtual_preferences(self, pkg_name, func):
@@ -1166,24 +1194,7 @@ class SpackSolverSetup(object):
         # what provides what
         for vspec in sorted(self.possible_virtuals):
             self.gen.fact(fn.virtual(vspec))
-            all_providers = sorted(spack.repo.path.providers_for(vspec))
-            for idx, provider in enumerate(all_providers):
-                provides_atom = fn.provides_virtual(provider.name, vspec)
-                possible_provider_fn = fn.possible_provider(
-                    vspec, provider.name, idx
-                )
-                item = (idx, provider, possible_provider_fn)
-                self.providers_by_vspec_name[vspec].append(item)
-                clauses = self.spec_clauses(provider, body=True)
-                clauses_but_node = [c for c in clauses if c.name != 'node']
-                if clauses_but_node:
-                    self.gen.rule(provides_atom, AspAnd(*clauses_but_node))
-                else:
-                    self.gen.fact(provides_atom)
-                for clause in clauses:
-                    self.gen.rule(clause, possible_provider_fn)
-                self.gen.newline()
-            self.gen.newline()
+        self.gen.newline()
 
     def generate_possible_compilers(self, specs):
         compilers = all_compilers_in_config()
@@ -1232,26 +1243,20 @@ class SpackSolverSetup(object):
             self.gen.newline()
 
     def define_virtual_constraints(self):
-        for vspec_str in sorted(self.virtual_constraints):
-            vspec = spack.spec.Spec(vspec_str)
-
-            self.gen.h2("Virtual spec: {0}".format(vspec_str))
-            providers = spack.repo.path.providers_for(vspec_str)
-            candidates = self.providers_by_vspec_name[vspec.name]
-            possible_providers = [
-                func for idx, spec, func in candidates if spec in providers
-            ]
-
-            self.gen.newline()
-            single_provider_for = fn.single_provider_for(
-                vspec.name, vspec.versions
-            )
-            one_of_the_possibles = self.gen.one_of(*possible_providers)
-            single_provider_rule = "{0} :- {1}.\n{1} :- {0}.\n".format(
-                single_provider_for, str(one_of_the_possibles)
-            )
-            self.gen.out.write(single_provider_rule)
-            self.gen.control.add("base", [], single_provider_rule)
+        # aggregate constraints into per-virtual sets
+        constraint_map = collections.defaultdict(lambda: set())
+        for pkg_name, versions in self.version_constraints:
+            if not spack.repo.path.is_virtual(pkg_name):
+                continue
+            constraint_map[pkg_name].add(versions)
+
+        for pkg_name, versions in sorted(constraint_map.items()):
+            for v1 in sorted(versions):
+                for v2 in sorted(versions):
+                    if v1.satisfies(v2):
+                        self.gen.fact(
+                            fn.version_constraint_satisfies(pkg_name, v1, v2)
+                        )
 
     def define_compiler_version_constraints(self):
         compiler_list = spack.compilers.all_compiler_specs()
diff --git a/lib/spack/spack/solver/concretize.lp b/lib/spack/spack/solver/concretize.lp
index 77f225742b..c1e94509d2 100644
--- a/lib/spack/spack/solver/concretize.lp
+++ b/lib/spack/spack/solver/concretize.lp
@@ -4,7 +4,7 @@
 % SPDX-License-Identifier: (Apache-2.0 OR MIT)
 
 %=============================================================================
-% Generate
+% This logic program implements Spack's concretizer
 %=============================================================================
 
 %-----------------------------------------------------------------------------
@@ -29,7 +29,8 @@ version_weight(Package, 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),
+  not virtual(Package).   % TODO: fix this and handle versionless virtuals separately
 version_satisfies(Package, Constraint)
   :- version(Package, Version), version_satisfies(Package, Constraint, Version).
 
@@ -49,15 +50,25 @@ depends_on(Package, Dependency, Type)
     not virtual(Dependency),
     not external(Package).
 
-% if you declare a dependency on a virtual AND the package is not an external,
-% you depend on one of its providers
-1 {
-  depends_on(Package, Provider, Type)
-  : provides_virtual(Provider, Virtual)
-} 1
- :- dependency_conditions(Package, Virtual, Type),
-    virtual(Virtual),
-    not external(Package).
+% every root must be a node
+node(Package) :- root(Package).
+
+% dependencies imply new nodes
+node(Dependency) :- node(Package), depends_on(Package, Dependency).
+
+% all nodes in the graph must be reachable from some root
+% this ensures a user can't say `zlib ^libiconv` (neither of which have any
+% dependencies) and get a two-node unconnected graph
+needed(Package) :- root(Package).
+needed(Dependency) :- needed(Package), depends_on(Package, Dependency).
+:- node(Package), not needed(Package).
+
+% Avoid cycles in the DAG
+% some combinations of conditional dependencies can result in cycles;
+% this ensures that we solve around them
+path(Parent, Child) :- depends_on(Parent, Child).
+path(Parent, Descendant) :- path(Parent, A), depends_on(A, Descendant).
+:- path(A, B), path(B, A).
 
 %-----------------------------------------------------------------------------
 % Conditional dependencies
@@ -72,8 +83,8 @@ dependency_conditions(Package, Dependency, Type) :-
 #defined dependency_type/2.
 
 % collect all the dependency conditions into a single conditional rule
-% distinguishing between Parent and Package is needed to account for
-% conditions like:
+% distinguishing between Parent and Package (Arg1) is needed to account
+% for conditions like:
 %
 % depends_on('patchelf@0.9', when='@1.0:1.1 ^python@:2')
 %
@@ -91,23 +102,20 @@ dependency_conditions_hold(ID, Parent, Dependency) :-
 #defined required_dependency_condition/5.
 
 %-----------------------------------------------------------------------------
-% Imposed dependencies
+% Imposed constraints on dependencies
 %
-% This handles the `@1.0+bar` in `depends_on("foo@1.0+bar", when="SPEC")`.
+% This handles the `@1.0+bar` in `depends_on("foo@1.0+bar", when="SPEC")`, or
+% the `mpi@2:` in `provides("mpi@2:", when="@1.9:")`.
 %-----------------------------------------------------------------------------
-% this rule instantiates every non-root node in the DAG
-node(Dependency) :-
-  dependency_conditions_hold(ID, Package, Dependency),
-  depends_on(Package, Dependency).
+% NOTE: `attr(Name, Arg1)` is omitted here b/c the only single-arg attribute is
+% NOTE: `node()`, which is handled above under "Dependency Semantics"
 
 attr(Name, Arg1, Arg2) :-
   dependency_conditions_hold(ID, Package, Dependency),
-  depends_on(Package, Dependency),
   imposed_dependency_condition(ID, Name, Arg1, Arg2).
 
 attr(Name, Arg1, Arg2, Arg3) :-
   dependency_conditions_hold(ID, Package, Dependency),
-  depends_on(Package, Dependency),
   imposed_dependency_condition(ID, Name, Arg1, Arg2, Arg3).
 
 #defined imposed_dependency_condition/4.
@@ -130,18 +138,60 @@ attr(Name, Arg1, Arg2, Arg3) :-
 %-----------------------------------------------------------------------------
 % Virtual dependencies
 %-----------------------------------------------------------------------------
+% if you declare a dependency on a virtual AND the package is not an external,
+% you depend on one of its providers
+1 {
+  depends_on(Package, Provider, Type) : possible_provider(Provider, Virtual)
+} 1
+  :- dependency_conditions(Package, Virtual, Type),
+     virtual(Virtual),
+     not external(Package).
+
 % if a virtual was required by some package, one provider is in the DAG
-1 { node(Package) : provides_virtual(Package, Virtual) } 1
+1 { node(Package) : provider(Package, Virtual) } 1
  :- virtual_node(Virtual).
 
+% virtual roots imply virtual nodes, and that one provider is a root
+virtual_node(Virtual) :- virtual_root(Virtual).
+1 { root(Package) : possible_provider(Package, Virtual) } 1
+  :- virtual_root(Virtual).
+
+% all virtual providers come from provider conditions like this
+dependency_conditions_hold(ID, Provider, Virtual) :-
+  attr(Name, Arg1)             : required_provider_condition(ID, Name, Arg1);
+  attr(Name, Arg1, Arg2)       : required_provider_condition(ID, Name, Arg1, Arg2);
+  attr(Name, Arg1, Arg2, Arg3) : required_provider_condition(ID, Name, Arg1, Arg2, Arg3);
+  virtual(Virtual);
+  provider_condition(ID, Provider, Virtual).
+
+% virtuals do not have well defined possible versions, so just ensure
+% that all constraints on versions are consistent
+:- virtual_node(Virtual),
+   version_satisfies(Virtual, V1), version_satisfies(Virtual, V2),
+   not version_constraint_satisfies(Virtual, V1, V2).
+
+% The provider provides the virtual if some provider condition holds.
+provides_virtual(Provider, Virtual) :-
+   provider_condition(ID, Provider, Virtual),
+   dependency_conditions_hold(ID, Provider, Virtual),
+   virtual(Virtual).
+
 % a node that provides a virtual is a provider
 provider(Package, Virtual)
   :- node(Package), provides_virtual(Package, Virtual).
 
+% dependencies on virtuals also imply that the virtual is a virtual node
+virtual_node(Virtual)
+  :- dependency_conditions(Package, Virtual, Type),
+     virtual(Virtual), not external(Package).
+
 % for any virtual, there can be at most one provider in the DAG
 0 { provider(Package, Virtual) :
     node(Package), provides_virtual(Package, Virtual) } 1 :- virtual(Virtual).
 
+%-----------------------------------------------------------------------------
+% Virtual dependency weights
+%-----------------------------------------------------------------------------
 % give dependents the virtuals they want
 provider_weight(Dependency, 0)
  :- virtual(Virtual), depends_on(Package, Dependency),
@@ -182,23 +232,11 @@ provider_weight(Package, 100)
     provider(Package, Virtual),
     not default_provider_preference(Virtual, Package, _).
 
-% all nodes must be reachable from some root
-node(Package) :- root(Package).
-
-1 { root(Package) : provides_virtual(Package, Virtual) } 1
-  :- virtual_root(Virtual).
-
-needed(Package) :- root(Package).
-needed(Dependency) :- needed(Package), depends_on(Package, Dependency).
-:- node(Package), not needed(Package).
-
-% real dependencies imply new nodes.
-node(Dependency) :- node(Package), depends_on(Package, Dependency).
-
-% Avoid cycles in the DAG
-path(Parent, Child) :- depends_on(Parent, Child).
-path(Parent, Descendant) :- path(Parent, A), depends_on(A, Descendant).
-:- path(A, B), path(B, A).
+#defined provider_condition/3.
+#defined required_provider_condition/3.
+#defined required_provider_condition/4.
+#defined required_provider_condition/5.
+#defined version_constraint_satisfies/3.
 
 %-----------------------------------------------------------------------------
 % Spec Attributes
@@ -301,6 +339,11 @@ external_spec_conditions_hold(ID, Package) :-
 % conditions hold.
 :- external(Package), not external_spec_conditions_hold(_, Package).
 
+#defined external_spec_index/3.
+#defined external_spec_condition/3.
+#defined external_spec_condition/4.
+#defined external_spec_condition/5.
+
 %-----------------------------------------------------------------------------
 % Variant semantics
 %-----------------------------------------------------------------------------