concretizer: use clingo json output instead of text

Clingo actually has an option to output JSON -- use that instead of
parsing the raw otuput ourselves.

This also allows us to pick the best answer -- modify the parser to
*only* construct a spec for that one rather than building all of them
like we did before.
This commit is contained in:
Todd Gamblin 2019-10-13 21:05:35 -07:00
parent a332981f2f
commit 36ec66d997
2 changed files with 85 additions and 69 deletions

View File

@ -22,7 +22,7 @@
level = 'long'
#: output options
dump_options = ('asp', 'warnings', 'output', 'solutions')
dump_options = ('asp', 'output', 'solutions')
def setup_parser(subparser):
@ -87,6 +87,8 @@ def solve(parser, args):
# dump generated ASP program
result = asp.solve(specs, dump=dump, models=models)
if dump == ['asp']:
return
# die if no solution was found
# TODO: we need to be able to provide better error messages than this
@ -95,8 +97,15 @@ def solve(parser, args):
# dump the solutions as concretized specs
if 'solutions' in dump:
for i, answer in enumerate(result.answers):
tty.msg("Answer %d" % (i + 1))
best = min(result.answers)
assert best[1] == result.answers[-1][1]
opt, i, answer = best
tty.msg(
"%d Answers. Best optimization %s:" % (i + 1, opt)
)
# iterate over roots from command line
for spec in specs:
answer_spec = answer[spec.name]
if args.yaml:

View File

@ -6,6 +6,7 @@
from __future__ import print_function
import collections
import json
import pkgutil
import re
import sys
@ -503,36 +504,13 @@ def depends_on(self, pkg, dep):
self._specs[pkg]._add_dependency(
self._specs[dep], ('link', 'run'))
def parse(self, stream, result):
for line in stream:
match = re.match(r'SATISFIABLE', line)
if match:
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
continue
match = re.match(r'Answer: (\d+)', line)
if not match:
continue
answer_number = int(match.group(1))
assert answer_number == len(result.answers) + 1
answer = next(stream)
tty.debug("Answer: %d" % answer_number, answer)
def call_actions_for_functions(self, function_strings):
function_re = re.compile(r'(\w+)\(([^)]*)\)')
# parse functions out of ASP output
functions = []
for m in re.finditer(r'(\w+)\(([^)]*)\)', answer):
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)
@ -553,14 +531,33 @@ def parse(self, stream, result):
assert action and callable(action)
action(*args)
result.answers.append(self._specs)
def parse_json(self, data, result):
if data["Result"] == "UNSATISFIABLE":
result.satisfiable = False
return
result.satisfiable = True
if data["Result"] == "OPTIMUM FOUND":
result.optimal = True
nmodels = data["Models"]["Number"]
best_model_number = nmodels - 1
best_model = data["Call"][0]["Witnesses"][best_model_number]
opt = list(best_model["Costs"])
functions = best_model["Value"]
self.call_actions_for_functions(functions)
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 = []
@ -625,12 +622,18 @@ def colorize(string):
if 'asp' in dump:
if sys.stdout.isatty():
tty.msg('ASP program:')
if dump == ['asp']:
print(result.asp)
return
else:
colorize(result.asp)
with tempfile.TemporaryFile("w+") as output:
with tempfile.TemporaryFile() as warnings:
clingo(
'--models=%d' % models,
'--models=0',
'--outf=2',
input=program,
output=output,
error=warnings,
@ -640,7 +643,6 @@ def colorize(string):
result.warnings = warnings.read().decode("utf-8")
# dump any warnings generated by the solver
if 'warnings' in dump:
if result.warnings:
if sys.stdout.isatty():
tty.msg('Clingo gave the following warnings:')
@ -651,14 +653,19 @@ def colorize(string):
output.seek(0)
result.output = output.read()
data = json.loads(result.output)
# dump the raw output of the solver
if 'output' in dump:
if sys.stdout.isatty():
tty.msg('Clingo output:')
colorize(result.output)
print(result.output)
if 'solutions' not in dump:
return
output.seek(0)
parser.parse(output, result)
parser.parse_json(data, result)
return result