From 6983db1392dad206d117d1ea1b3e630779a22ddd Mon Sep 17 00:00:00 2001 From: Massimiliano Culpo Date: Mon, 30 Oct 2023 07:38:53 +0100 Subject: [PATCH] ASP-based solver: avoid cycles in clingo using hidden directive (#40720) The code should be functonally equivalent to what it was before, but now to avoid cycles by design we are using a "hidden" feature of clingo --- lib/spack/spack/solver/asp.py | 29 ----------------------- lib/spack/spack/solver/concretize.lp | 4 ++++ lib/spack/spack/solver/cycle_detection.lp | 21 ---------------- 3 files changed, 4 insertions(+), 50 deletions(-) delete mode 100644 lib/spack/spack/solver/cycle_detection.lp diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py index eba1d8a3eb..729a1febc4 100644 --- a/lib/spack/spack/solver/asp.py +++ b/lib/spack/spack/solver/asp.py @@ -8,7 +8,6 @@ import enum import itertools import os -import pathlib import pprint import re import types @@ -889,14 +888,6 @@ def on_model(model): timer.start("solve") solve_result = self.control.solve(**solve_kwargs) - - if solve_result.satisfiable and self._model_has_cycles(models): - tty.debug(f"cycles detected, falling back to slower algorithm [specs={specs}]") - self.control.load(os.path.join(parent_dir, "cycle_detection.lp")) - self.control.ground([("no_cycle", [])]) - models.clear() - solve_result = self.control.solve(**solve_kwargs) - timer.stop("solve") # once done, construct the solve result @@ -950,26 +941,6 @@ def on_model(model): return result, timer, self.control.statistics - def _model_has_cycles(self, models): - """Returns true if the best model has cycles in it""" - cycle_detection = clingo.Control() - parent_dir = pathlib.Path(__file__).parent - lp_file = parent_dir / "cycle_detection.lp" - - min_cost, best_model = min(models) - with cycle_detection.backend() as backend: - for atom in best_model: - if atom.name == "attr" and str(atom.arguments[0]) == '"depends_on"': - symbol = fn.depends_on(atom.arguments[1], atom.arguments[2]) - atom_id = backend.add_atom(symbol.symbol()) - backend.add_rule([atom_id], [], choice=False) - - cycle_detection.load(str(lp_file)) - cycle_detection.ground([("base", []), ("no_cycle", [])]) - cycle_result = cycle_detection.solve() - - return cycle_result.unsatisfiable - class ConcreteSpecsByHash(collections.abc.Mapping): """Mapping containing concrete specs keyed by DAG hash. diff --git a/lib/spack/spack/solver/concretize.lp b/lib/spack/spack/solver/concretize.lp index efca3bfed2..92ba77ad82 100644 --- a/lib/spack/spack/solver/concretize.lp +++ b/lib/spack/spack/solver/concretize.lp @@ -1325,6 +1325,10 @@ build_priority(PackageNode, 0) :- not build(PackageNode), attr("node", Package #defined installed_hash/2. +% This statement, which is a hidden feature of clingo, let us avoid cycles in the DAG +#edge (A, B) : depends_on(A, B). + + %----------------------------------------------------------------- % Optimization to avoid errors %----------------------------------------------------------------- diff --git a/lib/spack/spack/solver/cycle_detection.lp b/lib/spack/spack/solver/cycle_detection.lp deleted file mode 100644 index 310c543623..0000000000 --- a/lib/spack/spack/solver/cycle_detection.lp +++ /dev/null @@ -1,21 +0,0 @@ -% Copyright 2013-2023 Lawrence Livermore National Security, LLC and other -% Spack Project Developers. See the top-level COPYRIGHT file for details. -% -% SPDX-License-Identifier: (Apache-2.0 OR MIT) - -%============================================================================= -% Avoid cycles in the DAG -% -% Some combinations of conditional dependencies can result in cycles; -% this ensures that we solve around them. Note that these rules are quite -% demanding on both grounding and solving, since they need to compute and -% consider all possible paths between pair of nodes. -%============================================================================= - - -#program no_cycle. -path(Parent, Child) :- depends_on(Parent, Child). -path(Parent, Descendant) :- path(Parent, A), depends_on(A, Descendant). -:- path(A, A). - -#defined depends_on/2.