concretizer: remove clingo command-line driver (#20362)

I was keeping the old `clingo` driver code around in case we had to run
using the command line tool instad of through the Python interface.

So far, the command line is faster than running through Python, but I'm
working on fixing that.  I found that if I do this:

```python
control = clingo.Control()
control.load("concretize.lp")
control.load("hdf5.lp")       # code from spack solve --show asp hdf5
control.load("display.lp")

control.ground([("base", [])])
control.solve(...)
```

It's just as fast as the command line tool. So we can always generate the
code and load it manually if we need to -- we don't need two drivers for
clingo. Given that the python interface is also the only way to get unsat
cores, I think we pretty much have to use it.

So, I'm removing the old command line driver and other unused code. We
can dig it up again from the history if it is needed.
This commit is contained in:
Todd Gamblin 2020-12-14 00:35:53 -08:00 committed by GitHub
parent 5c43be7694
commit 495e8cfb8e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -8,11 +8,8 @@
import copy
import itertools
import os
import pkgutil
import pprint
import re
import sys
import tempfile
import time
import types
from six import string_types
@ -26,7 +23,6 @@
import llnl.util.lang
import llnl.util.tty as tty
import llnl.util.tty.color as color
import spack
import spack.architecture
@ -41,7 +37,6 @@
import spack.package_prefs
import spack.repo
import spack.variant
from spack.util.executable import which
from spack.version import ver
@ -233,182 +228,6 @@ def print_cores(self):
*sorted(str(symbol) for symbol in core))
class ClingoDriver(object):
def __init__(self):
self.clingo = which("clingo", required=True)
self.out = None
def title(self, name, char):
self.out.write('\n')
self.out.write("%" + (char * 76))
self.out.write('\n')
self.out.write("%% %s\n" % name)
self.out.write("%" + (char * 76))
self.out.write('\n')
def h1(self, name):
self.title(name, "=")
def h2(self, name):
self.title(name, "-")
def newline(self):
self.out.write('\n')
def one_of(self, *args):
return AspOneOf(*args)
def _and(self, *args):
return AspAnd(*args)
def fact(self, head):
"""ASP fact (a rule without a body)."""
self.out.write("%s.\n" % head)
def rule(self, head, body):
"""ASP rule (an implication)."""
rule_line = "%s :- %s.\n" % (head, body)
if len(rule_line) > _max_line:
rule_line = re.sub(r' \| ', "\n| ", rule_line)
self.out.write(rule_line)
def before_setup(self):
"""Must be called before program is generated."""
# read the main ASP program from concrtize.lp
def after_setup(self):
"""Must be called after program is generated."""
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, stats=False):
def colorize(string):
color.cprint(highlight(color.cescape(string)))
timer = Timer()
with tempfile.TemporaryFile("w+") as program:
self.out = program
concretize_lp = pkgutil.get_data('spack.solver', 'concretize.lp')
program.write(concretize_lp.decode("utf-8"))
solver_setup.setup(self, specs)
program.write('\n')
display_lp = pkgutil.get_data('spack.solver', 'display.lp')
program.write(display_lp.decode("utf-8"))
timer.phase("generate")
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
def _normalize(body):
"""Accept an AspAnd object or a single Symbol and return a list of
symbols.
@ -1844,41 +1663,6 @@ def build_specs(self, function_tuples):
return self._specs
def highlight(string):
"""Syntax highlighting for ASP programs"""
# variables
string = re.sub(r'\b([A-Z])\b', r'@y{\1}', string)
# implications
string = re.sub(r':-', r'@*G{:-}', string)
# final periods
pattern = re.compile(r'^([^%].*)\.$', flags=re.MULTILINE)
string = re.sub(pattern, r'\1@*G{.}', string)
# directives
string = re.sub(
r'(#\w*)( (?:\w*)?)((?:/\d+)?)', r'@*B{\1}@c{\2}\3', string)
# functions
string = re.sub(r'(\w[\w-]+)\(([^)]*)\)', r'@C{\1}@w{(}\2@w{)}', string)
# comments
pattern = re.compile(r'(%.*)$', flags=re.MULTILINE)
string = re.sub(pattern, r'@w\1@.', string)
# strings
string = re.sub(r'("[^"]*")', r'@m{\1}', string)
# result
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
def _develop_specs_from_env(spec):
env = spack.environment.get_env(None, None)
dev_info = env.dev_specs.get(spec.name, {}) if env else {}