concretizer: add compiler version constraints

Add rules to account for compiler version
constraints in concretize.lp.

6 files changed, 59 insertions, 61 deletions

diff --git a/lib/spack/spack/architecture.py b/lib/spack/spack/architecture.py
index ceb188064f..c0930fe2d0 100644
--- a/lib/spack/spack/architecture.py
+++ b/lib/spack/spack/architecture.py
@@ -242,7 +242,7 @@ class Platform(object):
 
     front_end       = None
     back_end        = None
-    default         = None   # The default back end target. On cray ivybridge
+    default         = None   # The default back end target.
 
     front_os        = None
     back_os         = None
diff --git a/lib/spack/spack/platforms/test.py b/lib/spack/spack/platforms/test.py
index 32007394b1..9c6143946e 100644
--- a/lib/spack/spack/platforms/test.py
+++ b/lib/spack/spack/platforms/test.py
@@ -15,8 +15,8 @@ class Test(Platform):
         binary_formats = ['macho']
 
     front_end   = 'x86_64'
-    back_end    = 'core2'
-    default     = 'core2'
+    back_end    = 'broadwell'
+    default     = 'broadwell'
 
     front_os = 'redhat6'
     back_os = 'debian6'
diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py
index 6fb838109e..07b8eb18b3 100644
--- a/lib/spack/spack/solver/asp.py
+++ b/lib/spack/spack/solver/asp.py
@@ -540,7 +540,7 @@ class PyclingoDriver(object):
         cores = []   # unsatisfiable cores if they do not
 
         def on_model(model):
-            models.append((model.cost, model.symbols(shown=True)))
+            models.append((model.cost, model.symbols(shown=True, terms=True)))
 
         solve_result = self.control.solve(
             assumptions=self.assumptions,
@@ -594,6 +594,7 @@ class SpackSolverSetup(object):
         self.possible_virtuals = None
         self.possible_compilers = []
         self.version_constraints = set()
+        self.compiler_version_constraints = set()
         self.post_facts = []
 
         # id for dummy variables
@@ -904,23 +905,11 @@ class SpackSolverSetup(object):
                     spec.name, spec.compiler.name, spec.compiler.version))
 
             elif spec.compiler.versions:
-                f.node_compiler_version_satisfies(
-                    spec.name, spec.compiler.namd, spec.compiler.version)
-
-                compiler_list = spack.compilers.all_compiler_specs()
-                possible_compiler_versions = [
-                    f.node_compiler_version(
-                        spec.name, spec.compiler.name, compiler.version
-                    )
-                    for compiler in compiler_list
-                    if compiler.satisfies(spec.compiler)
-                ]
-
-                clauses.append(self.gen.one_of(*possible_compiler_versions))
-                for version in possible_compiler_versions:
-                    clauses.append(
-                        fn.node_compiler_version_hard(
-                            spec.name, spec.compiler.name, version))
+                clauses.append(
+                    fn.node_compiler_version_satisfies(
+                        spec.name, spec.compiler.name, spec.compiler.versions))
+                self.compiler_version_constraints.add(
+                    (spec.name, spec.compiler))
 
         # compiler flags
         for flag_type, flags in spec.compiler_flags.items():
@@ -956,27 +945,18 @@ class SpackSolverSetup(object):
         supported = []
 
         for target in targets:
-            compiler_info = target.compilers.get(compiler.name)
-            if not compiler_info:
-                # if we don't know, we assume it's supported and leave it
-                # to the user to debug
+            try:
+                target.optimization_flags(compiler.name, compiler.version)
                 supported.append(target)
+            except llnl.util.cpu.UnsupportedMicroarchitecture as e:
                 continue
 
-            if not isinstance(compiler_info, list):
-                compiler_info = [compiler_info]
-
-            for info in compiler_info:
-                version = ver(info['versions'])
-                if compiler.version.satisfies(version):
-                    supported.append(target)
-
         return sorted(supported, reverse=True)
 
     def platform_defaults(self):
         self.gen.h2('Default platform')
-        default = default_arch()
-        self.gen.fact(fn.node_platform_default(default.platform))
+        platform = spack.architecture.platform()
+        self.gen.fact(fn.node_platform_default(platform))
 
     def os_defaults(self, specs):
         self.gen.h2('Possible operating systems')
@@ -999,17 +979,12 @@ class SpackSolverSetup(object):
     def target_defaults(self, specs):
         """Add facts about targets and target compatibility."""
         self.gen.h2('Default target')
-        default = default_arch()
-        self.gen.fact(fn.node_target_default(default_arch().target))
 
-        uarch = default.target.microarchitecture
+        platform = spack.architecture.platform()
+        uarch = llnl.util.cpu.targets.get(platform.default)
 
         self.gen.h2('Target compatibility')
 
-        # listing too many targets can be slow, at least with our current
-        # encoding. To reduce the number of options to consider, only
-        # consider the *best* target that each compiler supports, along
-        # with the family.
         compatible_targets = [uarch] + uarch.ancestors
         compilers = self.possible_compilers
 
@@ -1020,6 +995,9 @@ class SpackSolverSetup(object):
         best_targets = set([uarch.family.name])
         for compiler in sorted(compilers):
             supported = self._supported_targets(compiler, compatible_targets)
+
+#            print("   ", compiler, "supports", [t.name for t in supported])
+
             if not supported:
                 continue
 
@@ -1035,6 +1013,7 @@ class SpackSolverSetup(object):
             if not spec.architecture or not spec.architecture.target:
                 continue
 
+            print("TTYPE:", type(platform.target(spec.target.name)))
             target = llnl.util.cpu.targets.get(spec.target.name)
             if not target:
                 raise ValueError("Invalid target: ", spec.target.name)
@@ -1070,8 +1049,7 @@ class SpackSolverSetup(object):
                 self.gen.fact(fn.provides_virtual(provider.name, vspec))
 
     def generate_possible_compilers(self, specs):
-        default_arch = spack.spec.ArchSpec(spack.architecture.sys_type())
-        compilers = spack.compilers.compilers_for_arch(default_arch)
+        compilers = compilers_for_default_arch()
         cspecs = set([c.spec for c in compilers])
 
         # add compiler specs from the input line to possibilities if we
@@ -1115,6 +1093,24 @@ class SpackSolverSetup(object):
             )
             self.gen.newline()
 
+    def define_compiler_version_constraints(self):
+        compiler_list = spack.compilers.all_compiler_specs()
+
+        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()
+
     def setup(self, driver, specs):
         """Generate an ASP program with relevant constraints for specs.
 
@@ -1181,6 +1177,9 @@ class SpackSolverSetup(object):
         self.gen.h1("Version Constraints")
         self.define_version_constraints()
 
+        self.gen.h1("Compiler Version Constraints")
+        self.define_compiler_version_constraints()
+
 
 class SpecBuilder(object):
     """Class with actions to rebuild a spec from ASP results."""
@@ -1316,6 +1315,7 @@ class SpecBuilder(object):
             # print out unknown actions so we can display them for debugging
             if not action:
                 print("%s(%s)" % (name, ", ".join(str(a) for a in args)))
+                print("    ", args)
                 continue
 
             assert action and callable(action)
@@ -1372,7 +1372,7 @@ def highlight(string):
 #
 # These are handwritten parts for the Spack ASP model.
 #
-def solve(specs, dump=None, models=0, timers=False, stats=False):
+def solve(specs, dump=(), models=0, timers=False, stats=False):
     """Solve for a stable model of specs.
 
     Arguments:
diff --git a/lib/spack/spack/solver/concretize.lp b/lib/spack/spack/solver/concretize.lp
index 513f9e3e4a..0fb9353819 100644
--- a/lib/spack/spack/solver/concretize.lp
+++ b/lib/spack/spack/solver/concretize.lp
@@ -228,16 +228,6 @@ node_target_match(Package, 1)
 1 { compiler_weight(Package, Weight) : compiler_weight(Package, Weight) } 1
  :- node(Package).
 
-% no conflicting compiler versions
-:- node_compiler_version(Package, Compiler, Version),
-   node_compiler_version_satisfies(Package, Compiler, Constraint),
-   0 = @version_satisfies(Version, Constraint).
-
-node_compiler_version_satisfies(Package, Constraint)
-  :- node_compiler_version(Package, Compiler, Version),
-     node_compiler_version_constraint(Package, Compiler, Constraint),
-     1 = @version_satisfies(Version, Constraint).
-
 % dependencies imply we should try to match hard compiler constraints
 % todo: look at what to do about intersecting constraints here. we'd
 % ideally go with the "lowest" pref in the DAG
@@ -252,19 +242,17 @@ compiler_match(Package, 1)
     node_compiler_match_pref(Package, Compiler).
 
 node_compiler_version_match_pref(Package, Compiler, V)
- :- node_compiler_version_hard(Package, Compiler, V).
+ :- node_compiler_hard(Package, Compiler),
+    node_compiler_version(Package, Compiler, V).
 node_compiler_version_match_pref(Dependency, Compiler, V)
  :- depends_on(Package, Dependency),
     node_compiler_version_match_pref(Package, Compiler, V),
-    not node_compiler_version_hard(Dependency, Compiler, _).
+    not node_compiler_hard(Dependency, Compiler).
 compiler_version_match(Package, 1)
  :- node_compiler_version(Package, Compiler, V),
     node_compiler_version_match_pref(Package, Compiler, V).
 
 #defined node_compiler_hard/2.
-#defined node_compiler_version_hard/3.
-#defined node_compiler_version_constraint/3.
-#defined node_compiler_version_satisfies/3.
 
 % compilers weighted by preference acccording to packages.yaml
 compiler_weight(Package, Weight)
diff --git a/lib/spack/spack/solver/display.lp b/lib/spack/spack/solver/display.lp
index 74f4a7189f..6778c2fbe0 100644
--- a/lib/spack/spack/solver/display.lp
+++ b/lib/spack/spack/solver/display.lp
@@ -16,3 +16,13 @@
 #show node_flag_compiler_default/1.
 #show node_flag_source/2.
 #show no_flags/2.
+
+
+
+#show variant_not_default/4.
+#show provider_weight/2.
+#show version_weight/2.
+#show compiler_match/2.
+#show compiler_weight/2.
+#show node_target_match/2.
+#show node_target_weight/2.
diff --git a/lib/spack/spack/test/concretize.py b/lib/spack/spack/test/concretize.py
index b90a948204..dcfaf31bdd 100644
--- a/lib/spack/spack/test/concretize.py
+++ b/lib/spack/spack/test/concretize.py
@@ -619,7 +619,7 @@ class TestConcretize(object):
     ])
     @pytest.mark.regression('13361')
     def test_adjusting_default_target_based_on_compiler(
-            self, spec, best_achievable, current_host
+            self, spec, best_achievable, current_host, mock_targets
     ):
         best_achievable = archspec.cpu.TARGETS[best_achievable]
         expected = best_achievable if best_achievable < current_host \