concretizer: use conditional literals for versions.

2 files changed, 31 insertions, 24 deletions

diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py
index 0a1bdc3057..d573d8d074 100644
--- a/lib/spack/spack/solver/asp.py
+++ b/lib/spack/spack/solver/asp.py
@@ -159,9 +159,8 @@ class AspGenerator(object):
 
     def pkg_version_rules(self, pkg):
         pkg = packagize(pkg)
-        self.rule(
-            self._or(fn.version(pkg.name, v) for v in pkg.versions),
-            fn.node(pkg.name))
+        for v in pkg.versions:
+            self.fact(fn.version_declared(pkg.name, v))
 
     def spec_versions(self, spec):
         spec = specify(spec)
@@ -170,23 +169,20 @@ class AspGenerator(object):
             self.rule(fn.version(spec.name, spec.version),
                       fn.node(spec.name))
         else:
-            version = spec.versions
-            impossible, possible = [], []
-            for v in spec.package.versions:
-                if v.satisfies(version):
-                    possible.append(v)
-                else:
-                    impossible.append(v)
-
-            if impossible:
-                self.rule(
-                    self._and(self._not(fn.version(spec.name, v))
-                              for v in impossible),
-                    fn.node(spec.name))
-            if possible:
-                self.rule(
-                    self._or(fn.version(spec.name, v) for v in possible),
-                    fn.node(spec.name))
+            versions = list(spec.package.versions)
+
+            # if the spec declares a new version, add it to the
+            # possibilities.
+            if spec.versions.concrete and spec.version not in versions:
+                self.fact(fn.version_declared(spec.name, spec.version))
+                versions.append(spec.version)
+
+            # conflict with any versions that do not satisfy the spec
+            # TODO: need to traverse allspecs beforehand and ensure all
+            # TODO: versions are known so we can disallow them.
+            for v in versions:
+                if not v.satisfies(spec.versions):
+                    self.fact(fn.version_conflict(spec.name, v))
 
     def compiler_defaults(self):
         """Facts about available compilers."""
diff --git a/lib/spack/spack/solver/concretize.lp b/lib/spack/spack/solver/concretize.lp
index 9dc2efd7bd..8eca18655e 100644
--- a/lib/spack/spack/solver/concretize.lp
+++ b/lib/spack/spack/solver/concretize.lp
@@ -1,8 +1,20 @@
 %=============================================================================
 % Generate
 %=============================================================================
+
+%-----------------------------------------------------------------------------
+% Version semantics
+%-----------------------------------------------------------------------------
+
+% If something is a package, it has only one version and that must be a
+% possible version.
+1 { version(P, V) : version_possible(P, V) } 1 :- node(P).
+
+% If a version is declared but conflicted, it's not possible.
+version_possible(P, V) :- version_declared(P, V), not version_conflict(P, V).
+#defined version_conflict/2.
+
 % One version, arch, etc. per package
-{ version(P, V) : version(P, V)} = 1              :- node(P).
 { arch_platform(P, A) : arch_platform(P, A) } = 1 :- node(P).
 { arch_os(P, A) : arch_os(P, A) } = 1             :- node(P).
 { arch_target(P, T) : arch_target(P, T) } = 1     :- node(P).
@@ -92,9 +104,8 @@ node_compiler_version(P, C, V)
      node_compiler_version_set(P, C, V).
 
 % node compiler versions can only be from the available compiler versions
-node_compiler_version(P, C, V)
-  :- node(P), compiler(C), node_compiler(P, C),
-     compiler_version(C, V).
+:- node(P), compiler(C), node_compiler(P, C), node_compiler_version(P, C, V),
+   not compiler_version(C, V).
 
 % if no compiler is set, fall back to default.
 node_compiler(P, C)