From ac9405a80ebc60101ca099ffb3041f5ce9cf6720 Mon Sep 17 00:00:00 2001
From: Todd Gamblin <tgamblin@llnl.gov>
Date: Thu, 14 May 2020 17:38:21 -0700
Subject: concretizer: refactor to support multiple solver backends

There are now three parts:

- `SpackSolverSetup`
  - Spack-specific logic for generating constraints. Calls methods on
    `AspTextGenerator` to set up the solver with a Spack problem. This
    shouln't change much from solver backend to solver backend.

- ClingoDriver
  - The solver driver provides methods for SolverSetup to generates an ASP
    program, send it to `clingo` (run as an external tool), and parse the
    output into function tuples suitable for `SpecBuilder`.
  - The interface is generic and should not have to change much for a
    driver for, say, the Clingo Python interface.

- SpecBuilder
  - Builds Spack specs from function tuples parsed by the solver driver.
---
 lib/spack/spack/solver/asp.py | 561 +++++++++++++++++++++---------------------
 1 file changed, 276 insertions(+), 285 deletions(-)

diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py
index 7c1a344bf1..6952126921 100644
--- a/lib/spack/spack/solver/asp.py
+++ b/lib/spack/spack/solver/asp.py
@@ -35,6 +35,27 @@ from spack.version import ver
 _max_line = 80
 
 
+class Timer(object):
+    """Simple timer for timing phases of a solve"""
+    def __init__(self):
+        self.start = time.time()
+        self.last = self.start
+        self.phases = {}
+
+    def phase(self, name):
+        last = self.last
+        now = time.time()
+        self.phases[name] = now - last
+        self.last = now
+
+    def write(self, out=sys.stdout):
+        now = time.time()
+        out.write("Time:\n")
+        for phase, t in self.phases.items():
+            out.write("    %-15s%.4f\n" % (phase + ":", t))
+        out.write("Total: %.4f\n" % (now - self.start))
+
+
 def issequence(obj):
     if isinstance(obj, string_types):
         return False
@@ -106,15 +127,6 @@ class AspAnd(AspObject):
         return s
 
 
-class AspOr(AspObject):
-    def __init__(self, *args):
-        args = listify(args)
-        self.args = args
-
-    def __str__(self):
-        return " | ".join(str(arg) for arg in self.args)
-
-
 class AspNot(AspObject):
     def __init__(self, arg):
         self.arg = arg
@@ -181,13 +193,22 @@ def check_packages_exist(specs):
                 raise spack.repo.UnknownPackageError(s.name)
 
 
-class AspGenerator(object):
-    def __init__(self, out):
-        self.out = out
-        self.func = AspFunctionBuilder()
-        self.possible_versions = {}
-        self.possible_virtuals = None
-        self.possible_compilers = []
+class Result(object):
+    """Result of an ASP solve."""
+    def __init__(self, asp):
+        self.asp = asp
+        self.satisfiable = None
+        self.optimal = None
+        self.warnings = None
+
+        # specs ordered by optimization level
+        self.answers = []
+
+
+class ClingoDriver(object):
+    def __init__(self):
+        self.clingo = which("clingo", required=True)
+        self.out = None
 
     def title(self, name, char):
         self.out.write('\n')
@@ -203,18 +224,12 @@ class AspGenerator(object):
     def h2(self, name):
         self.title(name, "-")
 
-    def section(self, name):
-        self.out.write("\n")
-        self.out.write("%\n")
-        self.out.write("%% %s\n" % name)
-        self.out.write("%\n")
+    def newline(self):
+        self.out.write('\n')
 
     def one_of(self, *args):
         return AspOneOf(*args)
 
-    def _or(self, *args):
-        return AspOr(*args)
-
     def _and(self, *args):
         return AspAnd(*args)
 
@@ -232,9 +247,152 @@ class AspGenerator(object):
             rule_line = re.sub(r' \| ', "\n| ", rule_line)
         self.out.write(rule_line)
 
-    def constraint(self, body):
-        """ASP integrity constraint (rule with no head; can't be true)."""
-        self.out.write(":- %s.\n" % body)
+    def before_setup(self):
+        """Must be called before program is generated."""
+        # read the main ASP program from concrtize.lp
+        concretize_lp = pkgutil.get_data('spack.solver', 'concretize.lp')
+        self.out.write(concretize_lp.decode("utf-8"))
+        return self
+
+    def after_setup(self):
+        """Must be called after program is generated."""
+        self.out.write('\n')
+        display_lp = pkgutil.get_data('spack.solver', 'display.lp')
+        self.out.write(display_lp.decode("utf-8"))
+
+    def parse_model_functions(self, function_strings):
+        function_re = re.compile(r'(\w+)\(([^)]*)\)')
+
+        # parse functions out of ASP output
+        functions = []
+        for string in function_strings:
+            m = function_re.match(string)
+            name, arg_string = m.groups()
+            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))
+        return functions
+
+    def parse_competition_format(self, output, builder, result):
+        """Parse Clingo's competition output format, which gives one answer."""
+        best_model_number = 0
+        for line in output:
+            match = re.match(r"% Answer: (\d+)", line)
+            if match:
+                best_model_number = int(match.group(1))
+
+            if re.match("INCONSISTENT", line):
+                result.satisfiable = False
+                return
+
+            if re.match("ANSWER", line):
+                result.satisfiable = True
+
+                answer = next(output)
+                functions = [
+                    f.rstrip(".") for f in re.split(r"\s+", answer.strip())
+                ]
+                function_tuples = self.parse_model_functions(functions)
+                specs = builder.build_specs(function_tuples)
+
+                costs = re.split(r"\s+", next(output).strip())
+                opt = [int(x) for x in costs[1:]]
+
+                result.answers.append((opt, best_model_number, specs))
+
+    def solve(self, solver_setup, specs, dump=None, models=0, timers=False):
+        def colorize(string):
+            color.cprint(highlight(color.cescape(string)))
+
+        timer = Timer()
+        with tempfile.TemporaryFile("w+") as program:
+            self.out = program
+
+            self.before_setup()
+            solver_setup.setup(self, specs)
+            self.after_setup()
+            timer.phase("generate")
+
+            program.seek(0)
+
+            result = Result(program.read())
+            program.seek(0)
+
+            if dump and 'asp' in dump:
+                if sys.stdout.isatty():
+                    tty.msg('ASP program:')
+
+                if dump == ['asp']:
+                    print(result.asp)
+                    return
+                else:
+                    colorize(result.asp)
+                timer.phase("dump")
+
+            with tempfile.TemporaryFile("w+") as output:
+                with tempfile.TemporaryFile() as warnings:
+                    self.clingo(
+                        '--models=%d' % models,
+                        # 1 is "competition" format with just optimal answer
+                        # 2 is JSON format with all explored answers
+                        '--outf=1',
+                        # Use a highest priority criteria-first optimization
+                        # strategy, which means we'll explore recent
+                        # versions, preferred packages first.  This works
+                        # well because Spack solutions are pretty easy to
+                        # find -- there are just a lot of them.  Without
+                        # this, it can take a VERY long time to find good
+                        # solutions, and a lot of models are explored.
+                        '--opt-strategy=bb,hier',
+                        input=program,
+                        output=output,
+                        error=warnings,
+                        fail_on_error=False)
+                    timer.phase("solve")
+
+                    warnings.seek(0)
+                    result.warnings = warnings.read().decode("utf-8")
+
+                    # dump any warnings generated by the solver
+                    if result.warnings:
+                        if sys.stdout.isatty():
+                            tty.msg('Clingo gave the following warnings:')
+                        colorize(result.warnings)
+
+                    output.seek(0)
+                    result.output = output.read()
+                    timer.phase("read")
+
+                    # dump the raw output of the solver
+                    if dump and 'output' in dump:
+                        if sys.stdout.isatty():
+                            tty.msg('Clingo output:')
+                        print(result.output)
+
+                        if 'solutions' not in dump:
+                            return
+
+                    output.seek(0)
+                    builder = SpecBuilder(specs)
+                    self.parse_competition_format(output, builder, result)
+                    timer.phase("parse")
+
+            if timers:
+                timer.write()
+                print()
+
+        return result
+
+
+class SpackSolverSetup(object):
+    """Class to set up and run a Spack concretization solve."""
+
+    def __init__(self):
+        self.gen = None  # set by setup()
+        self.possible_versions = {}
+        self.possible_virtuals = None
+        self.possible_compilers = []
 
     def pkg_version_rules(self, pkg):
         """Output declared versions of a package.
@@ -280,7 +438,7 @@ class AspGenerator(object):
         )
 
         for i, v in enumerate(most_to_least_preferred):
-            self.fact(fn.version_declared(pkg.name, v, i))
+            self.gen.fact(fn.version_declared(pkg.name, v, i))
 
     def spec_versions(self, spec):
         """Return list of clauses expressing spec's version constraints."""
@@ -304,13 +462,13 @@ class AspGenerator(object):
 
         # conflict with any versions that do not satisfy the spec
         if predicates:
-            return [self.one_of(*predicates)]
+            return [self.gen.one_of(*predicates)]
         return []
 
     def available_compilers(self):
         """Facts about available compilers."""
 
-        self.h2("Available compilers")
+        self.gen.h2("Available compilers")
         compilers = self.possible_compilers
 
         compiler_versions = collections.defaultdict(lambda: set())
@@ -318,16 +476,15 @@ class AspGenerator(object):
             compiler_versions[compiler.name].add(compiler.version)
 
         for compiler in sorted(compiler_versions):
-            self.fact(fn.compiler(compiler))
-            self.rule(
-                self._or(
-                    fn.compiler_version(compiler, v)
-                    for v in sorted(compiler_versions[compiler])),
-                fn.compiler(compiler))
+            self.gen.fact(fn.compiler(compiler))
+            for v in sorted(compiler_versions[compiler]):
+                self.gen.fact(fn.compiler_version(compiler, v))
+
+            self.gen.newline()
 
     def compiler_defaults(self):
         """Set compiler defaults, given a list of possible compilers."""
-        self.h2("Default compiler preferences")
+        self.gen.h2("Default compiler preferences")
 
         compiler_list = self.possible_compilers.copy()
         compiler_list = sorted(
@@ -337,7 +494,7 @@ class AspGenerator(object):
 
         for i, cspec in enumerate(matches):
             f = fn.default_compiler_preference(cspec.name, cspec.version, i)
-            self.fact(f)
+            self.gen.fact(f)
 
     def package_compiler_defaults(self, pkg):
         """Facts about packages' compiler prefs."""
@@ -354,7 +511,7 @@ class AspGenerator(object):
         matches = sorted(compiler_list, key=ppk)
 
         for i, cspec in enumerate(matches):
-            self.fact(fn.node_compiler_preference(
+            self.gen.fact(fn.node_compiler_preference(
                 pkg.name, cspec.name, cspec.version, i))
 
     def pkg_rules(self, pkg):
@@ -362,23 +519,24 @@ class AspGenerator(object):
 
         # versions
         self.pkg_version_rules(pkg)
-        self.out.write('\n')
+        self.gen.newline()
 
         # variants
         for name, variant in sorted(pkg.variants.items()):
-            self.fact(fn.variant(pkg.name, name))
+            self.gen.fact(fn.variant(pkg.name, name))
 
             single_value = not variant.multi
             single = fn.variant_single_value(pkg.name, name)
             if single_value:
-                self.fact(single)
-                self.fact(
+                self.gen.fact(single)
+                self.gen.fact(
                     fn.variant_default_value(pkg.name, name, variant.default))
             else:
-                self.fact(self._not(single))
+                self.gen.fact(self.gen._not(single))
                 defaults = variant.default.split(',')
                 for val in sorted(defaults):
-                    self.fact(fn.variant_default_value(pkg.name, name, val))
+                    self.gen.fact(
+                        fn.variant_default_value(pkg.name, name, val))
 
             values = variant.values
             if values is None:
@@ -394,9 +552,9 @@ class AspGenerator(object):
                 values = [variant.default]
 
             for value in sorted(values):
-                self.fact(fn.variant_possible_value(pkg.name, name, value))
+                self.gen.fact(fn.variant_possible_value(pkg.name, name, value))
 
-            self.out.write('\n')
+            self.gen.newline()
 
         # default compilers for this package
         self.package_compiler_defaults(pkg)
@@ -410,37 +568,37 @@ class AspGenerator(object):
 
                 if cond == spack.spec.Spec():
                     for t in sorted(dep.type):
-                        self.fact(
+                        self.gen.fact(
                             fn.declared_dependency(
                                 dep.pkg.name, dep.spec.name, t
                             )
                         )
                 else:
                     for t in sorted(dep.type):
-                        self.rule(
+                        self.gen.rule(
                             fn.declared_dependency(
                                 dep.pkg.name, dep.spec.name, t
                             ),
-                            self._and(
+                            self.gen._and(
                                 *self.spec_clauses(named_cond, body=True)
                             )
                         )
 
                 # add constraints on the dependency from dep spec.
                 for clause in self.spec_clauses(dep.spec):
-                    self.rule(
+                    self.gen.rule(
                         clause,
-                        self._and(
+                        self.gen._and(
                             fn.depends_on(dep.pkg.name, dep.spec.name),
                             *self.spec_clauses(named_cond, body=True)
                         )
                     )
-            self.out.write('\n')
+            self.gen.newline()
 
         # virtual preferences
         self.virtual_preferences(
             pkg.name,
-            lambda v, p, i: self.fact(
+            lambda v, p, i: self.gen.fact(
                 fn.pkg_provider_preference(pkg.name, v, p, i)
             )
         )
@@ -457,27 +615,28 @@ class AspGenerator(object):
                 func(vspec, provider, i)
 
     def provider_defaults(self):
-        self.h2("Default virtual providers")
+        self.gen.h2("Default virtual providers")
         assert self.possible_virtuals is not None
         self.virtual_preferences(
             "all",
-            lambda v, p, i: self.fact(fn.default_provider_preference(v, p, i))
+            lambda v, p, i: self.gen.fact(
+                fn.default_provider_preference(v, p, i))
         )
 
     def flag_defaults(self):
-        self.h2("Compiler flag defaults")
+        self.gen.h2("Compiler flag defaults")
 
         # types of flags that can be on specs
         for flag in spack.spec.FlagMap.valid_compiler_flags():
-            self.fact(fn.flag_type(flag))
-        self.out.write("\n")
+            self.gen.fact(fn.flag_type(flag))
+        self.gen.newline()
 
         # flags from compilers.yaml
         compilers = compilers_for_default_arch()
         for compiler in compilers:
             for name, flags in compiler.flags.items():
                 for flag in flags:
-                    self.fact(fn.compiler_version_flag(
+                    self.gen.fact(fn.compiler_version_flag(
                         compiler.name, compiler.version, name, flag))
 
     def spec_clauses(self, spec, body=False):
@@ -557,7 +716,7 @@ class AspGenerator(object):
                     for compiler in compiler_list
                     if compiler.satisfies(spec.compiler)
                 ]
-                clauses.append(self.one_of(*possible_compiler_versions))
+                clauses.append(self.gen.one_of(*possible_compiler_versions))
                 for version in possible_compiler_versions:
                     clauses.append(
                         fn.node_compiler_version_hard(
@@ -566,7 +725,7 @@ class AspGenerator(object):
         # compiler flags
         for flag_type, flags in spec.compiler_flags.items():
             for flag in flags:
-                self.fact(f.node_flag(spec.name, flag_type, flag))
+                self.gen.fact(f.node_flag(spec.name, flag_type, flag))
 
         # TODO
         # external_path
@@ -615,12 +774,12 @@ class AspGenerator(object):
         return sorted(supported, reverse=True)
 
     def platform_defaults(self):
-        self.h2('Default platform')
+        self.gen.h2('Default platform')
         default = default_arch()
-        self.fact(fn.node_platform_default(default.platform))
+        self.gen.fact(fn.node_platform_default(default.platform))
 
     def os_defaults(self, specs):
-        self.h2('Possible operating systems')
+        self.gen.h2('Possible operating systems')
         platform = spack.architecture.platform()
 
         # create set of OS's to consider
@@ -632,20 +791,20 @@ class AspGenerator(object):
 
         # make directives for possible OS's
         for os in sorted(possible):
-            self.fact(fn.os(os))
+            self.gen.fact(fn.os(os))
 
         # mark this one as default
-        self.fact(fn.node_os_default(platform.default_os))
+        self.gen.fact(fn.node_os_default(platform.default_os))
 
     def target_defaults(self, specs):
         """Add facts about targets and target compatibility."""
-        self.h2('Default target')
+        self.gen.h2('Default target')
         default = default_arch()
-        self.fact(fn.node_target_default(default_arch().target))
+        self.gen.fact(fn.node_target_default(default_arch().target))
 
         uarch = default.target.microarchitecture
 
-        self.h2('Target compatibility')
+        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
@@ -666,9 +825,9 @@ class AspGenerator(object):
 
             for target in supported:
                 best_targets.add(target.name)
-                self.fact(fn.compiler_supports_target(
+                self.gen.fact(fn.compiler_supports_target(
                     compiler.name, compiler.version, target.name))
-                self.fact(fn.compiler_supports_target(
+                self.gen.fact(fn.compiler_supports_target(
                     compiler.name, compiler.version, uarch.family.name))
 
         # add any targets explicitly mentioned in specs
@@ -684,31 +843,31 @@ class AspGenerator(object):
 
         i = 0
         for target in compatible_targets:
-            self.fact(fn.target(target.name))
-            self.fact(fn.target_family(target.name, target.family.name))
+            self.gen.fact(fn.target(target.name))
+            self.gen.fact(fn.target_family(target.name, target.family.name))
             for parent in sorted(target.parents):
-                self.fact(fn.target_parent(target.name, parent.name))
+                self.gen.fact(fn.target_parent(target.name, parent.name))
 
             # prefer best possible targets; weight others poorly so
             # they're not used unless set explicitly
             if target.name in best_targets:
-                self.fact(fn.target_weight(target.name, i))
+                self.gen.fact(fn.target_weight(target.name, i))
                 i += 1
             else:
-                self.fact(fn.target_weight(target.name, 100))
+                self.gen.fact(fn.target_weight(target.name, 100))
 
-            self.out.write("\n")
+            self.gen.newline()
 
     def virtual_providers(self):
-        self.h2("Virtual providers")
+        self.gen.h2("Virtual providers")
         assert self.possible_virtuals is not None
 
         # what provides what
         for vspec in sorted(self.possible_virtuals):
-            self.fact(fn.virtual(vspec))
+            self.gen.fact(fn.virtual(vspec))
             for provider in sorted(spack.repo.path.providers_for(vspec)):
                 # TODO: handle versioned and conditional virtuals
-                self.fact(fn.provides_virtual(provider.name, vspec))
+                self.gen.fact(fn.provides_virtual(provider.name, vspec))
 
     def generate_possible_compilers(self, specs):
         default_arch = spack.spec.ArchSpec(spack.architecture.sys_type())
@@ -733,13 +892,16 @@ class AspGenerator(object):
 
         return cspecs
 
-    def generate_asp_program(self, specs):
-        """Write an ASP program for specs.
+    def setup(self, driver, specs):
+        """Generate an ASP program with relevant constarints for specs.
 
-        Writes to this AspGenerator's output stream.
+        This calls methods on the solve driver to set up the problem with
+        facts and rules from all possible dependencies of the input
+        specs, as well as constraints from the specs themselves.
 
         Arguments:
             specs (list): list of Specs to solve
+
         """
         # preliminary checks
         check_packages_exist(specs)
@@ -753,17 +915,17 @@ class AspGenerator(object):
         )
         pkgs = set(possible)
 
+        # driver is used by all the functions below to add facts and
+        # rules to generate an ASP program.
+        self.gen = driver
+
         # get possible compilers
         self.possible_compilers = self.generate_possible_compilers(specs)
 
-        # read the main ASP program from concrtize.lp
-        concretize_lp = pkgutil.get_data('spack.solver', 'concretize.lp')
-        self.out.write(concretize_lp.decode("utf-8"))
-
         # traverse all specs and packages to build dict of possible versions
         self.build_version_dict(possible, specs)
 
-        self.h1('General Constraints')
+        self.gen.h1('General Constraints')
         self.available_compilers()
         self.compiler_defaults()
 
@@ -776,33 +938,28 @@ class AspGenerator(object):
         self.provider_defaults()
         self.flag_defaults()
 
-        self.h1('Package Constraints')
+        self.gen.h1('Package Constraints')
         for pkg in sorted(pkgs):
-            self.h2('Package: %s' % pkg)
+            self.gen.h2('Package: %s' % pkg)
             self.pkg_rules(pkg)
 
-        self.h1('Spec Constraints')
+        self.gen.h1('Spec Constraints')
         for spec in sorted(specs):
-            self.fact(fn.root(spec.name))
+            self.gen.fact(fn.root(spec.name))
             for dep in spec.traverse():
-                self.h2('Spec: %s' % str(dep))
+                self.gen.h2('Spec: %s' % str(dep))
 
                 if dep.virtual:
-                    self.fact(fn.virtual_node(dep.name))
+                    self.gen.fact(fn.virtual_node(dep.name))
                 else:
                     for clause in self.spec_clauses(dep):
-                        self.fact(clause)
+                        self.gen.fact(clause)
 
-        self.out.write('\n')
-        display_lp = pkgutil.get_data('spack.solver', 'display.lp')
-        self.out.write(display_lp.decode("utf-8"))
 
-
-class ResultParser(object):
-    """Class with actions that can re-parse a spec from ASP."""
+class SpecBuilder(object):
+    """Class with actions to rebuild a spec from ASP results."""
     def __init__(self, specs):
         self._result = None
-
         self._command_line_specs = specs
         self._flag_sources = collections.defaultdict(lambda: set())
         self._flag_compiler_defaults = set()
@@ -893,7 +1050,7 @@ class ResultParser(object):
             for spec in self._command_line_specs
             for s in spec.traverse())
 
-        # iterate through specs with specified flaggs
+        # iterate through specs with specified flags
         for pkg, sources in self._flag_sources.items():
             spec = self._specs[pkg]
 
@@ -917,29 +1074,17 @@ class ResultParser(object):
             check_same_flags(spec.compiler_flags, flags)
             spec.compiler_flags.update(flags)
 
-    def call_actions_for_functions(self, function_strings):
-        function_re = re.compile(r'(\w+)\(([^)]*)\)')
-
-        # parse functions out of ASP output
-        functions = []
-        for string in function_strings:
-            m = function_re.match(string)
-            name, arg_string = m.groups()
-            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))
-
+    def build_specs(self, function_tuples):
         # Functions don't seem to be in particular order in output.  Sort
         # them here so that directives that build objects (like node and
         # node_compiler) are called in the right order.
-        functions.sort(key=lambda f: {
+        function_tuples.sort(key=lambda f: {
             "node": -2,
             "node_compiler": -1,
         }.get(f[0], 0))
 
         self._specs = {}
-        for name, args in functions:
+        for name, args in function_tuples:
             action = getattr(self, name, None)
             if not action:
                 print("%s(%s)" % (name, ", ".join(str(a) for a in args)))
@@ -948,77 +1093,19 @@ class ResultParser(object):
             assert action and callable(action)
             action(*args)
 
-    def parse_json(self, data, result):
-        """Parse Clingo's JSON output format, which can give a lot of answers.
-
-        This can be slow, espeically if Clingo comes back having explored
-        a lot of models.
-        """
-        if data["Result"] == "UNSATISFIABLE":
-            result.satisfiable = False
-            return
-
-        result.satisfiable = True
-        if data["Result"] == "OPTIMUM FOUND":
-            result.optimal = True
+        # namespace assignment is done after the fact, as it is not
+        # currently part of the solve
+        for spec in self._specs.values():
+            repo = spack.repo.path.repo_for_pkg(spec)
+            spec.namespace = repo.namespace
 
-        nmodels = data["Models"]["Number"]
-        best_model_number = nmodels - 1
-        best_model = data["Call"][0]["Witnesses"][best_model_number]
-        opt = list(best_model["Costs"])
+            # once this is done, everything is concrete
+            spec._mark_concrete()
 
-        functions = best_model["Value"]
-
-        self.call_actions_for_functions(functions)
+        # fix flags after all specs are constructed
         self.reorder_flags()
-        result.answers.append((opt, best_model_number, self._specs))
-
-    def parse_best(self, output, result):
-        """Parse Clingo's competition output format, which gives one answer."""
-        best_model_number = 0
-        for line in output:
-            match = re.match(r"% Answer: (\d+)", line)
-            if match:
-                best_model_number = int(match.group(1))
-
-            if re.match("INCONSISTENT", line):
-                result.satisfiable = False
-                return
-
-            if re.match("ANSWER", line):
-                result.satisfiable = True
 
-                answer = next(output)
-                functions = [
-                    f.rstrip(".") for f in re.split(r"\s+", answer.strip())
-                ]
-                self.call_actions_for_functions(functions)
-
-                costs = re.split(r"\s+", next(output).strip())
-                opt = [int(x) for x in costs[1:]]
-
-                for spec in self._specs.values():
-                    # namespace assignment can be done after the fact, as
-                    # it is not part of the solve
-                    repo = spack.repo.path.repo_for_pkg(spec)
-                    spec.namespace = repo.namespace
-
-                    # once this is done, everything is concrete
-                    spec._mark_concrete()
-
-                self.reorder_flags()
-                result.answers.append((opt, best_model_number, self._specs))
-
-
-class Result(object):
-    def __init__(self, asp):
-        self.asp = asp
-        self.satisfiable = None
-        self.optimal = None
-        self.warnings = None
-
-        # specs ordered by optimization level
-        self.answers = []
+        return self._specs
 
 
 def highlight(string):
@@ -1054,26 +1141,6 @@ def highlight(string):
     return string
 
 
-class Timer(object):
-    def __init__(self):
-        self.start = time.time()
-        self.last = self.start
-        self.phases = {}
-
-    def phase(self, name):
-        last = self.last
-        now = time.time()
-        self.phases[name] = now - last
-        self.last = now
-
-    def write(self, out=sys.stdout):
-        now = time.time()
-        out.write("Time:\n")
-        for phase, t in self.phases.items():
-            out.write("    %-15s%.4f\n" % (phase + ":", t))
-        out.write("Total: %.4f\n" % (now - self.start))
-
-
 #
 # These are handwritten parts for the Spack ASP model.
 #
@@ -1085,82 +1152,6 @@ def solve(specs, dump=None, models=0, timers=False):
         dump (tuple): what to dump
         models (int): number of models to search (default: 0)
     """
-    clingo = which('clingo', required=True)
-    parser = ResultParser(specs)
-
-    def colorize(string):
-        color.cprint(highlight(color.cescape(string)))
-
-    timer = Timer()
-    with tempfile.TemporaryFile("w+") as program:
-        generator = AspGenerator(program)
-        generator.generate_asp_program(specs)
-        timer.phase("generate")
-        program.seek(0)
-
-        result = Result(program.read())
-        program.seek(0)
-
-        if dump and 'asp' in dump:
-            if sys.stdout.isatty():
-                tty.msg('ASP program:')
-
-            if dump == ['asp']:
-                print(result.asp)
-                return
-            else:
-                colorize(result.asp)
-            timer.phase("dump")
-
-        with tempfile.TemporaryFile("w+") as output:
-            with tempfile.TemporaryFile() as warnings:
-                clingo(
-                    '--models=%d' % models,
-                    # 1 is "competition" format with just optimal answer
-                    # 2 is JSON format with all explored answers
-                    '--outf=1',
-                    # Use a highest priority criteria-first optimization
-                    # strategy, which means we'll explore recent
-                    # versions, preferred packages first.  This works
-                    # well because Spack solutions are pretty easy to
-                    # find -- there are just a lot of them.  Without
-                    # this, it can take a VERY long time to find good
-                    # solutions, and a lot of models are explored.
-                    '--opt-strategy=bb,hier',
-                    input=program,
-                    output=output,
-                    error=warnings,
-                    fail_on_error=False)
-                timer.phase("solve")
-
-                warnings.seek(0)
-                result.warnings = warnings.read().decode("utf-8")
-
-                # dump any warnings generated by the solver
-                if result.warnings:
-                    if sys.stdout.isatty():
-                        tty.msg('Clingo gave the following warnings:')
-                    colorize(result.warnings)
-
-                output.seek(0)
-                result.output = output.read()
-                timer.phase("read")
-
-                # dump the raw output of the solver
-                if dump and 'output' in dump:
-                    if sys.stdout.isatty():
-                        tty.msg('Clingo output:')
-                    print(result.output)
-
-                    if 'solutions' not in dump:
-                        return
-
-                output.seek(0)
-                parser.parse_best(output, result)
-                timer.phase("parse")
-
-        if timers:
-            timer.write()
-            print()
-
-    return result
+    driver = ClingoDriver()
+    setup = SpackSolverSetup()
+    return driver.solve(setup, specs, dump, models, timers)
-- 
cgit v1.2.3-60-g2f50