concretizer: handle variant defaults with optimization

- Instead of using default logic, handle variant defaults by minimizing
  the number of non-default variants in the solution.

- This actually seems to be pretty fast, and it fixes the long-standing
  issue that writing this:

      spack install hdf5 ^mpich

  will fail if you don't specify hdf5+mpi.  With optimization and
  allowing enums to be enumerated, the solver seems to be able to quickly
  discover that +mpi is the only way hdf5 can depend on mpich, and it
  forces the switch to be thrown.

2 files changed, 49 insertions, 9 deletions

diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py
index f8417434e6..4975bcd452 100644
--- a/lib/spack/spack/solver/asp.py
+++ b/lib/spack/spack/solver/asp.py
@@ -275,6 +275,19 @@ class AspGenerator(object):
                     self.rule(
                         fn.variant_default_value(pkg.name, name, val),
                         fn.node(pkg.name))
+
+            values = variant.values
+            if values is None:
+                values = []
+            elif isinstance(values, spack.variant.DisjointSetsOfValues):
+                union = set()
+                for s in values.sets:
+                    union.update(s)
+                values = union
+
+            for  value in values:
+                self.fact(fn.variant_possible_value(pkg.name, name, value))
+
             self.out.write('\n')
 
         # default compilers for this package
@@ -430,6 +443,7 @@ class AspGenerator(object):
 
         self.h1('Spec Constraints')
         for spec in specs:
+            self.fact(fn.root(spec.name))
             for dep in spec.traverse():
                 self.h2('Spec: %s' % str(dep))
                 self.fact(fn.node(dep.name))
@@ -498,6 +512,11 @@ class ResultParser(object):
                 result.satisfiable = True
                 continue
 
+            match = re.match(r'OPTIMUM FOUND', line)
+            if match:
+                result.satisfiable = True
+                continue
+
             match = re.match(r'UNSATISFIABLE', line)
             if match:
                 result.satisfiable = False
@@ -517,17 +536,22 @@ class ResultParser(object):
             functions = []
             for m in re.finditer(r'(\w+)\(([^)]*)\)', answer):
                 name, arg_string = m.groups()
-                args = re.findall(r'"([^"]*)"', arg_string)
+                args = re.split(r'\s*,\s*', arg_string)
+                args = [s.strip('"') if s.startswith('"') else int(s)
+                        for s in args]
                 functions.append((name, args))
 
             # Functions don't seem to be in particular order in output.
-            # Sort them here so that nodes are created before directives
-            # that need them, (depends_on(), etc.)
+            # Sort them here so that nodes are first, and so created
+            # before directives that need them (depends_on(), etc.)
             functions.sort(key=lambda f: f[0] != "node")
 
             self._specs = {}
             for name, args in functions:
-                action = getattr(self, name)
+                action = getattr(self, name, None)
+                if not action:
+                    print("%s(%s)" % (name, ", ".join(str(a) for a in args)))
+                    continue
                 assert action and callable(action)
                 action(*args)
 
@@ -570,6 +594,7 @@ def highlight(string):
     string = re.sub(r'\bUNSATISFIABLE', "@R{UNSATISFIABLE}", string)
     string = re.sub(r'\bINCONSISTENT', "@R{INCONSISTENT}", string)
     string = re.sub(r'\bSATISFIABLE', "@G{SATISFIABLE}", string)
+    string = re.sub(r'\bOPTIMUM FOUND', "@G{OPTIMUM FOUND}", string)
 
     return string
 
@@ -614,7 +639,7 @@ def solve(specs, dump=None, models=1):
                     fail_on_error=False)
 
                 warnings.seek(0)
-                result.warnings = warnings.read()
+                result.warnings = warnings.read().decode("utf-8")
 
                 # dump any warnings generated by the solver
                 if 'warnings' in dump:
diff --git a/lib/spack/spack/solver/concretize.lp b/lib/spack/spack/solver/concretize.lp
index 2a8be91382..006a5e39ed 100644
--- a/lib/spack/spack/solver/concretize.lp
+++ b/lib/spack/spack/solver/concretize.lp
@@ -24,6 +24,11 @@ depends_on(P, D) :- declared_dependency(P, D), not virtual(D), node(P).
 1 { depends_on(P, Q) : provides_virtual(Q, V) } 1
     :- declared_dependency(P, V), virtual(V), node(P).
 
+needed(D) :- depends_on(_, D), node(D).
+needed(P) :- root(P).
+:- node(P), not needed(P).
+#defined root/1.
+
 % real dependencies imply new nodes.
 node(D) :- node(P), depends_on(P, D).
 
@@ -36,9 +41,8 @@ node(D) :- node(P), depends_on(P, D).
 %-----------------------------------------------------------------------------
 % Variant semantics
 %-----------------------------------------------------------------------------
-
 % one variant value for single-valued variants.
-1 { variant_value(P, V, X) : variant_value(P, V, X) } 1
+1 { variant_value(P, V, X) : variant_possible_value(P, V, X) } 1
     :- node(P), variant(P, V), variant_single_value(P, V).
 
 % if a variant is set to anything, it is considered 'set'.
@@ -47,8 +51,19 @@ variant_set(P, V) :- variant_set(P, V, _).
 % variant_set is an explicitly set variant value. If it's not 'set',
 % we revert to the default value. If it is set, we force the set value
 variant_value(P, V, X) :- node(P), variant(P, V), variant_set(P, V, X).
-variant_value(P, V, X) :- node(P), variant(P, V), not variant_set(P, V),
-                 variant_default_value(P, V, X).
+
+% prefer default values.
+variant_not_default(P, V, X, 1)
+    :- variant_value(P, V, X),
+       not variant_default_value(P, V, X),
+       node(P).
+
+variant_not_default(P, V, X, 0)
+    :- variant_value(P, V, X),
+       variant_default_value(P, V, X),
+       node(P).
+
+#minimize { N@1,P,V,X : variant_not_default(P, V, X, N) }.
 
 % suppress wranings about this atom being unset.  It's only set if some
 % spec or some package sets it, and without this, clingo will give