summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--lib/spack/spack/solver/asp.py561
1 files 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)