From 14e179398fc8dcfc58ff7f9b95506ccc9aab3359 Mon Sep 17 00:00:00 2001 From: Josh Essman <68349992+joshessman-llnl@users.noreply.github.com> Date: Tue, 23 Feb 2021 17:46:37 -0600 Subject: 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) --- lib/spack/spack/solver/asp.py | 28 +++++++++++++++++++--------- 1 file changed, 19 insertions(+), 9 deletions(-) (limited to 'lib') 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) -- cgit v1.2.3-60-g2f50