diff options
author | Josh Essman <68349992+joshessman-llnl@users.noreply.github.com> | 2021-02-23 17:46:37 -0600 |
---|---|---|
committer | Massimiliano Culpo <massimiliano.culpo@gmail.com> | 2021-05-21 15:09:08 +0200 |
commit | 14e179398fc8dcfc58ff7f9b95506ccc9aab3359 (patch) | |
tree | 68a6d1fc55212936b8d1928873e56bed0532b1cc /lib | |
parent | 8d131934345abc5f0ee61da45a74fa09c07195bb (diff) | |
download | spack-14e179398fc8dcfc58ff7f9b95506ccc9aab3359.tar.gz spack-14e179398fc8dcfc58ff7f9b95506ccc9aab3359.tar.bz2 spack-14e179398fc8dcfc58ff7f9b95506ccc9aab3359.tar.xz spack-14e179398fc8dcfc58ff7f9b95506ccc9aab3359.zip |
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
(cherry picked from commit 93ed1a410c4a202eab3a68769fd8c0d4ff8b1c8e)
Diffstat (limited to 'lib')
-rw-r--r-- | lib/spack/spack/solver/asp.py | 28 |
1 files changed, 19 insertions, 9 deletions
diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py index 789a207d1e..ac2983cecc 100644 --- a/lib/spack/spack/solver/asp.py +++ b/lib/spack/spack/solver/asp.py @@ -18,6 +18,8 @@ import archspec.cpu try: import clingo + # There may be a better way to detect this + clingo_cffi = hasattr(clingo.Symbol, '_rep') except ImportError: clingo = None @@ -119,11 +121,11 @@ class AspFunction(AspObject): 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 @@ class PyclingoDriver(object): 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) |