concretizer: Use "competition" output format to avoid extra parsing

Competition output only prints out one model, so we do not have to
unnecessarily parse all the non-optimal models.  We'll just look at the
best model and bring that in.

In practice, this saves a lot of JSON parsing and spec construction time.
This commit is contained in:
Todd Gamblin
2019-10-13 23:34:22 -07:00
parent b4e6d9d28e
commit 18fba433f6
2 changed files with 45 additions and 18 deletions

View File

@@ -32,8 +32,8 @@ def setup_parser(subparser):
help="outputs: a list with any of: " help="outputs: a list with any of: "
"%s (default), all" % ', '.join(dump_options)) "%s (default), all" % ', '.join(dump_options))
subparser.add_argument( subparser.add_argument(
'--models', action='store', type=int, default=1, '--models', action='store', type=int, default=0,
help="number of solutions to display (0 for all)") help="number of solutions to search (default 0 for all)")
# Below are arguments w.r.t. spec display (like spack spec) # Below are arguments w.r.t. spec display (like spack spec)
arguments.add_common_arguments( arguments.add_common_arguments(
@@ -87,7 +87,7 @@ def solve(parser, args):
# dump generated ASP program # dump generated ASP program
result = asp.solve(specs, dump=dump, models=models) result = asp.solve(specs, dump=dump, models=models)
if dump == ['asp']: if 'solutions' not in dump:
return return
# die if no solution was found # die if no solution was found
@@ -101,9 +101,8 @@ def solve(parser, args):
assert best[1] == result.answers[-1][1] assert best[1] == result.answers[-1][1]
opt, i, answer = best opt, i, answer = best
tty.msg( tty.msg("Best of %d answers." % (i + 1))
"%d Answers. Best optimization %s:" % (i + 1, opt) tty.msg("Optimization %s" % opt)
)
# iterate over roots from command line # iterate over roots from command line
for spec in specs: for spec in specs:

View File

@@ -6,7 +6,6 @@
from __future__ import print_function from __future__ import print_function
import collections import collections
import json
import pkgutil import pkgutil
import re import re
import sys import sys
@@ -299,7 +298,7 @@ def pkg_rules(self, pkg):
union.update(s) union.update(s)
values = union values = union
for value in values: for value in values:
self.fact(fn.variant_possible_value(pkg.name, name, value)) self.fact(fn.variant_possible_value(pkg.name, name, value))
self.out.write('\n') self.out.write('\n')
@@ -583,6 +582,11 @@ def call_actions_for_functions(self, function_strings):
action(*args) action(*args)
def parse_json(self, data, result): 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": if data["Result"] == "UNSATISFIABLE":
result.satisfiable = False result.satisfiable = False
return return
@@ -601,6 +605,33 @@ def parse_json(self, data, result):
self.call_actions_for_functions(functions) self.call_actions_for_functions(functions)
result.answers.append((opt, best_model_number, self._specs)) 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:]]
result.answers.append((opt, best_model_number, self._specs))
class Result(object): class Result(object):
def __init__(self, asp): def __init__(self, asp):
self.asp = asp self.asp = asp
@@ -648,13 +679,13 @@ def highlight(string):
# #
# These are handwritten parts for the Spack ASP model. # These are handwritten parts for the Spack ASP model.
# #
def solve(specs, dump=None, models=1): def solve(specs, dump=None, models=0):
"""Solve for a stable model of specs. """Solve for a stable model of specs.
Arguments: Arguments:
specs (list): list of Specs to solve. specs (list): list of Specs to solve.
dump (tuple): what to dump dump (tuple): what to dump
models (int): number of satisfying specs to find (default: 1) models (int): number of models to search (default: 0)
""" """
clingo = which('clingo', required=True) clingo = which('clingo', required=True)
parser = ResultParser() parser = ResultParser()
@@ -683,8 +714,10 @@ def colorize(string):
with tempfile.TemporaryFile("w+") as output: with tempfile.TemporaryFile("w+") as output:
with tempfile.TemporaryFile() as warnings: with tempfile.TemporaryFile() as warnings:
clingo( clingo(
'--models=0', '--models=%d' % models,
'--outf=2', # 1 is "competition" format with just optimal answer
# 2 is JSON format with all explored answers
'--outf=1',
input=program, input=program,
output=output, output=output,
error=warnings, error=warnings,
@@ -698,25 +731,20 @@ def colorize(string):
if sys.stdout.isatty(): if sys.stdout.isatty():
tty.msg('Clingo gave the following warnings:') tty.msg('Clingo gave the following warnings:')
colorize(result.warnings) colorize(result.warnings)
else:
if sys.stdout.isatty():
tty.msg('No warnings.')
output.seek(0) output.seek(0)
result.output = output.read() result.output = output.read()
data = json.loads(result.output)
# dump the raw output of the solver # dump the raw output of the solver
if 'output' in dump: if 'output' in dump:
if sys.stdout.isatty(): if sys.stdout.isatty():
tty.msg('Clingo output:') tty.msg('Clingo output:')
print(result.output) print(result.output)
if 'solutions' not in dump: if 'solutions' not in dump:
return return
output.seek(0) output.seek(0)
parser.parse_json(data, result) parser.parse_best(output, result)
return result return result