Updates to support clingo-cffi (#20657)

* Support clingo when used with cffi

Clingo recently merged in a new Python module option based on cffi.

Compatibility with this module requires a few changes to spack - it does not automatically convert strings/ints/etc to Symbol and clingo.Symbol.string throws on failure.

manually convert str/int to clingo.Symbol types
catch stringify exceptions
add job for clingo-cffi to Spack CI
switch to potassco-vendored wheel for clingo-cffi CI
on_unsat argument when cffi
This commit is contained in:
Josh Essman
2021-02-23 17:46:37 -06:00
committed by GitHub
parent 6622856076
commit 93ed1a410c
2 changed files with 70 additions and 9 deletions

View File

@@ -18,6 +18,8 @@
try:
import clingo
# There may be a better way to detect this
clingo_cffi = hasattr(clingo.Symbol, '_rep')
except ImportError:
clingo = None # type: ignore
@@ -119,11 +121,11 @@ def __call__(self, *args):
def symbol(self, positive=True):
def argify(arg):
if isinstance(arg, bool):
return str(arg)
return clingo.String(str(arg))
elif isinstance(arg, int):
return arg
return clingo.Number(arg)
else:
return str(arg)
return clingo.String(str(arg))
return clingo.Function(
self.name, [argify(arg) for arg in self.args], positive=positive)
@@ -318,18 +320,26 @@ def solve(
def on_model(model):
models.append((model.cost, model.symbols(shown=True, terms=True)))
solve_result = self.control.solve(
assumptions=self.assumptions,
on_model=on_model,
on_core=cores.append
)
solve_kwargs = {"assumptions": self.assumptions,
"on_model": on_model,
"on_core": cores.append}
if clingo_cffi:
solve_kwargs["on_unsat"] = cores.append
solve_result = self.control.solve(**solve_kwargs)
timer.phase("solve")
# once done, construct the solve result
result.satisfiable = solve_result.satisfiable
def stringify(x):
return x.string or str(x)
if clingo_cffi:
# Clingo w/ CFFI will throw an exception on failure
try:
return x.string
except RuntimeError:
return str(x)
else:
return x.string or str(x)
if result.satisfiable:
builder = SpecBuilder(specs)