Module `clintest.solver`

The abstract class Solver and off-the-shelf solver implementations.

Classes

class Clingo (arguments: Sequence[str] | None = None, program: str | None = None, files: Sequence[str] | None = None)

Expand source code

class Clingo(Solver):
    """A solver using `clingo.control.Control`.

    Parameters
    ----------

    Arguments:
        A list of arguments.

    program
        The program as a `str`.

    files
        A list of files to read the program from.
    """

    def __init__(
        self,
        arguments: Optional[Sequence[str]] = None,
        program: Optional[str] = None,
        files: Optional[Sequence[str]] = None,
    ) -> None:
        self.__arguments = [] if arguments is None else arguments
        self.__program = "" if program is None else program
        self.__files = [] if files is None else files

    @override
    def solve(self, test: Test) -> None:  # noqa: D102
        ctl = Control(self.__arguments)

        ctl.add("base", [], self.__program)

        for file in self.__files:
            ctl.load(file)

        ctl.ground([("base", [])])

        if not test.outcome().is_certain():
            ctl.solve(
                on_model=_adapt_on_model(test.on_model),
                on_unsat=test.on_unsat,
                on_core=test.on_core,
                on_statistics=test.on_statistics,
                on_finish=_adapt_on_finish(test.on_finish),
            )

    def __repr__(self):
        name = self.__class__.__name__
        arguments = repr(self.__arguments)
        program = repr(self.__program)
        files = repr(self.__files)
        return f"{name}({arguments}, {program}, {files})"

A solver using clingo.control.Control.

Parameters

Arguments

A list of arguments.

program The program as a str.

files A list of files to read the program from.

Ancestors

Solver
abc.ABC

Inherited members

Solver:
- solve

class Iterate (models: Iterable[Model])

Expand source code

class Iterate(Solver):
    """A solver that iterates over an `typing.Iterable` of `clintest.protocol.Model`s."""

    def __init__(self, models: Iterable[Model]) -> None:
        self.__models = models

    @override
    def solve(self, test: Test) -> None:  # noqa: D102
        exhausted = True
        satisfiable = False

        for model in self.__models:
            satisfiable = True
            if not test.on_model(model):
                exhausted = False
                break

        test.on_finish(
            PersistedSolveResult(
                exhausted=exhausted, interrupted=False, satisfiable=satisfiable, unsatisfiable=not satisfiable
            )
        )

A solver that iterates over an typing.Iterable of Models.

Ancestors

Solver
abc.ABC

Inherited members

Solver:
- solve

class Solver

Expand source code

class Solver(ABC):
    """An initialized solver that may solve any test."""

    @abstractmethod
    def solve(self, test: Test) -> None:
        """Use this solver to solve a given `test`.

        Parameters
        ----------
        test
            The `clintest.test.Test` to be solved by this solver.
        """

An initialized solver that may solve any test.

Ancestors

abc.ABC

Methods

def solve(self, test: Test) ‑> None

Expand source code

@abstractmethod
def solve(self, test: Test) -> None:
    """Use this solver to solve a given `test`.

    Parameters
    ----------
    test
        The `clintest.test.Test` to be solved by this solver.
    """

Use this solver to solve a given test.

Parameters

test: The Test to be solved by this solver.