Module clintest.test

The abstract class Test and off-the-shelf test implementations.

Classes

class And (*args: Test,
short_circuit: bool = True,
ignore_certain: bool = True)

Expand source code

class And(Test):
    """The conjunction of a list given tests.

    This test succeeds if all `args` succeed.

    Parameters
    ----------

    Args:
        The `Test`s to be combined.

    short_circuit
        Whether this test should employ short circuit optimization, i.e., abort all remaining tests
        once the outcome of a test is certainly false.

    ignore_certain
        Whether this test should employ the ignore certain optimization, i.e., not send artifacts
        to test that are already certain.
    """

    def __init__(self, *args: Test, short_circuit: bool = True, ignore_certain: bool = True) -> None:
        self.__operands = list(args)
        self.__short_circuit = short_circuit
        self.__ignore_certain = ignore_certain

        self.__ongoing = list(args)
        self.__outcome = Outcome(True, False)

        def call_operand(_operand: Test) -> None:
            pass

        self.__on_whatever(call_operand)

    def __repr__(self):
        name = self.__class__.__name__

        operands = ", ".join(repr(operand) for operand in self.__operands)
        short_circuit = repr(self.__short_circuit)
        ignore_certain = repr(self.__ignore_certain)

        ongoing = repr(self.__ongoing)
        outcome = repr(self.__outcome)

        return (
            f"{name}("
            f"{operands}, "
            f"short_circuit={short_circuit}, "
            f"ignore_certain={ignore_certain}, "
            f"__ongoing={ongoing}, "
            f"__outcome={outcome})"
        )

    def __str__(self):
        if self.__operands:
            operands = ""
            width = len(str(len(self.__operands) - 1))
            for i, operand in enumerate(self.__operands):
                i_str = str(i)
                operands += os.linesep
                operands += (width - len(i_str)) * " "
                operands += [" ", "*"][operand in self.__ongoing]
                operands += f"{i_str}: {operand}"
            operands = indent(operands, 8 * " ")
        else:
            operands = " <none>"

        return os.linesep.join(
            [
                f"[{self.outcome()}] {self.__class__.__name__} ",
                f"    operands:{operands}",
                f"    short_circuit:  {self.__short_circuit}",
                f"    ignore_certain: {self.__ignore_certain}",
            ]
        )

    def __on_whatever(self, call_operand: Callable[[Test], None]) -> bool:
        still_ongoing = []

        for operand in self.__ongoing:
            call_operand(operand)

            if operand.outcome().is_certainly_false():
                if self.__short_circuit:
                    self.__ongoing = []
                    self.__outcome = Outcome(False, True)
                    return False
                else:
                    self.__outcome = Outcome(False, False)

            if not (self.__ignore_certain and operand.outcome().is_certain()):
                still_ongoing.append(operand)

        self.__ongoing = still_ongoing
        self.__outcome = Outcome(self.__outcome.current_value(), not bool(still_ongoing))

        return not self.__outcome.is_certain()

    @override
    def on_model(self, model: Model) -> bool:  # noqa: D102
        def call_operand(operand: Test) -> None:
            operand.on_model(model)

        return self.__on_whatever(call_operand)

    @override
    def on_unsat(self, lower_bound: Sequence[int]) -> None:  # noqa: D102
        def call_operand(operand: Test) -> None:
            operand.on_unsat(lower_bound)

        self.__on_whatever(call_operand)

    @override
    def on_core(self, core: Sequence[int]) -> None:  # noqa: D102
        def call_operand(operand: Test) -> None:
            operand.on_core(core)

        self.__on_whatever(call_operand)

    @override
    def on_statistics(self, step: StatisticsMap, accumulated: StatisticsMap) -> None:  # noqa: D102
        def call_operand(operand: Test) -> None:
            operand.on_statistics(step, accumulated)

        self.__on_whatever(call_operand)

    @override
    def on_finish(self, result: SolveResult) -> None:  # noqa: D102
        def call_operand(operand: Test) -> None:
            operand.on_finish(result)

        ignore_certain_bck = self.__ignore_certain
        self.__ignore_certain = True
        self.__on_whatever(call_operand)
        self.__ignore_certain = ignore_certain_bck

        assert not self.__ongoing  # noqa: S101
        assert self.__outcome.is_certain()  # noqa: S101

    @override
    def outcome(self) -> Outcome:  # noqa: D102
        return self.__outcome

The conjunction of a list given tests.

This test succeeds if all args succeed.

Parameters

Args

The Tests to be combined. short_circuit Whether this test should employ short circuit optimization, i.e., abort all remaining tests once the outcome of a test is certainly false.

ignore_certain Whether this test should employ the ignore certain optimization, i.e., not send artifacts to test that are already certain.

Ancestors

• Test
• abc.ABC

Inherited members

• Test:
  • assert_
  • on_core
  • on_finish
  • on_model
  • on_statistics
  • on_unsat
  • outcome

class Assert (quantifier: Quantifier,
assertion: Assertion)

Expand source code

class Assert(Test):
    """A test that asserts certain properties about the `clingo.model.Model`s of a program.

    This test can be highly customized using a `clintest.quantifier.Quantifier` and a
    `clintest.assertion.Assertion`.

    Parameters
    ----------
    quantifier
        The `clintest.quantifier.Quantifier` used with this test.

    assertion
        The `clintest.assertion.Assertion` used with this test.
    """

    def __init__(self, quantifier: Quantifier, assertion: Assertion) -> None:
        self.__quantifier = quantifier
        self.__assertion = assertion

    def __repr__(self):
        name = self.__class__.__name__
        quantifier = repr(self.__quantifier)
        assertion = repr(self.__assertion)
        return f"{name}({quantifier}, {assertion})"

    def __str__(self):
        return os.linesep.join(
            [
                f"[{self.outcome()}] {self.__class__.__name__}",
                f"    quantifier: {self.__quantifier}",
                f"    assertion:  {self.__assertion}",
            ]
        )

    @override
    def on_model(self, model: Model) -> bool:  # noqa: D102
        if not self.__quantifier.outcome().is_certain():
            self.__quantifier.consume(self.__assertion.holds_for(model))

        return not self.__quantifier.outcome().is_certain()

    @override
    def on_finish(self, result: SolveResult) -> None:  # noqa: D102
        self.__quantifier = Finished(self.__quantifier)

    @override
    def outcome(self) -> Outcome:  # noqa: D102
        return self.__quantifier.outcome()

A test that asserts certain properties about the clingo.model.Models of a program.

This test can be highly customized using a Quantifier and a Assertion.

Parameters

quantifier

The Quantifier used with this test.

assertion

The Assertion used with this test.

Ancestors

• Test
• abc.ABC

Inherited members

• Test:
  • assert_
  • on_core
  • on_finish
  • on_model
  • on_statistics
  • on_unsat
  • outcome

class Context (test: Test,
str_: Callable[[Test], str] = builtins.str,
repr_: Callable[[Test], str] = <built-in function repr>)

Expand source code

class Context(Test):
    """A test that behaves identical to a given other `test` but permits changes to its string representation.

    This can be helpful to create human-readable error messages.

    Parameters
    ----------
    test
        A `Test` that determines how this test should behave.
    """

    def __init__(
        self,
        test: Test,
        str_: Callable[[Test], str] = str,
        repr_: Callable[[Test], str] = repr,
    ):
        self.test: Test = test
        self.__str = str_
        self.__repr = repr_

    def __repr__(self):
        return self.__repr(self.test)

    def __str__(self):
        return self.__str(self.test)

    @override
    def on_model(self, model: Model) -> bool:  # noqa: D102
        return self.test.on_model(model)

    @override
    def on_unsat(self, lower_bound: Sequence[int]) -> None:  # noqa: D102
        self.test.on_unsat(lower_bound)

    @override
    def on_core(self, core: Sequence[int]) -> None:  # noqa: D102
        self.test.on_core(core)

    @override
    def on_statistics(self, step: StatisticsMap, accumulated: StatisticsMap) -> None:  # noqa: D102
        self.test.on_statistics(step, accumulated)

    @override
    def on_finish(self, result: SolveResult) -> None:  # noqa: D102
        self.test.on_finish(result)

    @override
    def outcome(self) -> Outcome:  # noqa: D102
        return self.test.outcome()

A test that behaves identical to a given other test but permits changes to its string representation.

This can be helpful to create human-readable error messages.

Parameters

test

A Test that determines how this test should behave.

Ancestors

• Test
• abc.ABC

Inherited members

• Test:
  • assert_
  • on_core
  • on_finish
  • on_model
  • on_statistics
  • on_unsat
  • outcome

class False_ (lazy: bool = True)

Expand source code

class False_(Test):
    """The test which always failes.

    Parameters
    ----------
    lazy
        Whether this test should be lazy, i.e., not consume any models.
    """

    def __init__(self, lazy: bool = True) -> None:
        self.__outcome = Outcome(False, lazy)

    def __repr__(self):
        name = self.__class__.__name__
        outcome = repr(self.__outcome)
        return f"{name}(__outcome={outcome})"

    def __str__(self):
        return f"[{self.__outcome}] {self.__class__.__name__}"

    @override
    def on_model(self, _model: Model) -> bool:  # noqa: D102
        return not self.__outcome.is_certain()

    @override
    def on_finish(self, result: SolveResult) -> None:  # noqa: D102
        self.__outcome = Outcome(False, True)

    @override
    def outcome(self) -> Outcome:  # noqa: D102
        return self.__outcome

The test which always failes.

Parameters

lazy

Whether this test should be lazy, i.e., not consume any models.

Ancestors

• Test
• abc.ABC

Inherited members

• Test:
  • assert_
  • on_core
  • on_finish
  • on_model
  • on_statistics
  • on_unsat
  • outcome

class Not (operand: Test)

Expand source code

class Not(Test):
    """The negation of a given test.

    This test failes if `operand` succeeds and vice versa.

    Parameters
    ----------
    operand
        The `Test` to be negated.
    """

    def __init__(self, operand: Test) -> None:
        self.__operand = operand

    def __repr__(self):
        name = self.__class__.__name__
        operand = repr(self.__operand)
        return f"{name}({operand})"

    def __str__(self):
        return os.linesep.join(
            [
                f"[{self.outcome()}] {self.__class__.__name__}",
                f"    operand: {indent(str(self.__operand), 4 * ' ')[4:]}",
            ]
        )

    @override
    def on_model(self, model: Model) -> bool:  # noqa: D102
        return self.__operand.on_model(model)

    @override
    def on_unsat(self, lower_bound: Sequence[int]) -> None:  # noqa: D102
        self.__operand.on_unsat(lower_bound)

    @override
    def on_core(self, core: Sequence[int]) -> None:  # noqa: D102
        self.__operand.on_core(core)

    @override
    def on_statistics(self, step: StatisticsMap, accumulated: StatisticsMap) -> None:  # noqa: D102
        self.__operand.on_statistics(step, accumulated)

    @override
    def on_finish(self, result: SolveResult) -> None:  # noqa: D102
        self.__operand.on_finish(result)

    @override
    def outcome(self) -> Outcome:  # noqa: D102
        outcome = self.__operand.outcome()
        return Outcome(not outcome.current_value(), outcome.is_certain())

The negation of a given test.

This test failes if operand succeeds and vice versa.

Parameters

operand

The Test to be negated.

Ancestors

• Test
• abc.ABC

Inherited members

• Test:
  • assert_
  • on_core
  • on_finish
  • on_model
  • on_statistics
  • on_unsat
  • outcome

class Or (*args: Test,
short_circuit: bool = True,
ignore_certain: bool = True)

Expand source code

class Or(Test):
    """The disjunction of a list given tests.

    This test succeeds if any `args` succeed.

    Parameters
    ----------

    Args:
        The `Test`s to be combined.

    short_circuit
        Whether this test should employ short circuit optimization, i.e., abort all remaining tests
        once the outcome of a test is certainly true.

    ignore_certain
        Whether this test should employ the ignore certain optimization, i.e., not send artifacts
        to test that are already certain.
    """

    def __init__(self, *args: Test, short_circuit: bool = True, ignore_certain: bool = True) -> None:
        self.__operands = list(args)
        self.__short_circuit = short_circuit
        self.__ignore_certain = ignore_certain

        self.__ongoing = list(args)
        self.__outcome = Outcome(False, False)

        def call_operand(_operand: Test) -> None:
            pass

        self.__on_whatever(call_operand)

    def __repr__(self):
        name = self.__class__.__name__

        operands = ", ".join(repr(operand) for operand in self.__operands)
        short_circuit = repr(self.__short_circuit)
        ignore_certain = repr(self.__ignore_certain)

        ongoing = repr(self.__ongoing)
        outcome = repr(self.__outcome)

        return (
            f"{name}("
            f"{operands}, "
            f"short_circuit={short_circuit}, "
            f"ignore_certain={ignore_certain}, "
            f"__ongoing={ongoing}, "
            f"__outcome={outcome})"
        )

    def __str__(self):
        if self.__operands:
            operands = ""
            width = len(str(len(self.__operands) - 1))
            for i, operand in enumerate(self.__operands):
                i_str = str(i)
                operands += os.linesep
                operands += (width - len(i_str)) * " "
                operands += [" ", "*"][operand in self.__ongoing]
                operands += f"{i_str}: {operand}"
            operands = indent(operands, 8 * " ")
        else:
            operands = " <none>"

        return os.linesep.join(
            [
                f"[{self.outcome()}] {self.__class__.__name__} ",
                f"    operands:{operands}",
                f"    short_circuit:  {self.__short_circuit}",
                f"    ignore_certain: {self.__ignore_certain}",
            ]
        )

    def __on_whatever(self, call_operand: Callable[[Test], None]) -> bool:
        still_ongoing = []

        for operand in self.__ongoing:
            call_operand(operand)

            if operand.outcome().is_certainly_true():
                if self.__short_circuit:
                    self.__ongoing = []
                    self.__outcome = Outcome(True, True)
                    return False
                else:
                    self.__outcome = Outcome(True, False)

            if not (self.__ignore_certain and operand.outcome().is_certain()):
                still_ongoing.append(operand)

        self.__ongoing = still_ongoing
        self.__outcome = Outcome(self.__outcome.current_value(), not bool(still_ongoing))

        return not self.__outcome.is_certain()

    @override
    def on_model(self, model: Model) -> bool:  # noqa: D102
        def call_operand(operand: Test) -> None:
            operand.on_model(model)

        return self.__on_whatever(call_operand)

    @override
    def on_unsat(self, lower_bound: Sequence[int]) -> None:  # noqa: D102
        def call_operand(operand: Test) -> None:
            operand.on_unsat(lower_bound)

        self.__on_whatever(call_operand)

    @override
    def on_core(self, core: Sequence[int]) -> None:  # noqa: D102
        def call_operand(operand: Test) -> None:
            operand.on_core(core)

        self.__on_whatever(call_operand)

    @override
    def on_statistics(self, step: StatisticsMap, accumulated: StatisticsMap) -> None:  # noqa: D102
        def call_operand(operand: Test) -> None:
            operand.on_statistics(step, accumulated)

        self.__on_whatever(call_operand)

    @override
    def on_finish(self, result: SolveResult) -> None:  # noqa: D102
        def call_operand(operand: Test) -> None:
            operand.on_finish(result)

        ignore_certain_bck = self.__ignore_certain
        self.__ignore_certain = True
        self.__on_whatever(call_operand)
        self.__ignore_certain = ignore_certain_bck

        assert not self.__ongoing  # noqa: S101
        assert self.__outcome.is_certain()  # noqa: S101

    @override
    def outcome(self) -> Outcome:  # noqa: D102
        return self.__outcome

The disjunction of a list given tests.

This test succeeds if any args succeed.

Parameters

Args

The Tests to be combined. short_circuit Whether this test should employ short circuit optimization, i.e., abort all remaining tests once the outcome of a test is certainly true.

ignore_certain Whether this test should employ the ignore certain optimization, i.e., not send artifacts to test that are already certain.

Ancestors

• Test
• abc.ABC

Inherited members

• Test:
  • assert_
  • on_core
  • on_finish
  • on_model
  • on_statistics
  • on_unsat
  • outcome

class Record (test: Test | None = None)

Expand source code

class Record(Test):
    """A test that behaves identical to a given other `test` but records any call to one of its `on_*`-methods.

    This can be very helpful for debugging.

    Parameters
    ----------
    test
        A `Test` that determines how this test should behave.
    """

    def __init__(self, test: Test | None = None):
        self.test: Test = test if test is not None else True_(lazy=False)
        self.recording: Recording = Recording(
            [
                {
                    "__f": "__init__",
                    "__outcome": self.outcome(),
                }
            ]
        )

    def __repr__(self):
        name = self.__class__.__name__
        test = repr(self.test)
        recording = repr(self.recording)
        return f"{name}(test={test}, recording={recording})"

    def __str__(self):
        return os.linesep.join(
            [
                f"[{self.outcome()}] {self.__class__.__name__}",
                f"    test: {indent(str(self.test), 4 * ' ')[4:]}",
                "    recording:",
                indent(str(self.recording), 8 * " "),
            ]
        )

    @override
    def on_model(self, model: Model) -> bool:  # noqa: D102
        self.recording.append(
            {
                "__f": "on_model",
                "str(model)": str(model),
            }
        )
        result = self.test.on_model(model)
        self.recording.amend(
            {
                "__result": result,
                "__outcome": self.outcome(),
            }
        )
        return result

    @override
    def on_unsat(self, lower_bound: Sequence[int]) -> None:  # noqa: D102
        self.recording.append(
            {
                "__f": "on_unsat",
                "lower_bound": lower_bound,
            }
        )
        self.test.on_unsat(lower_bound)
        self.recording.amend({"__outcome": self.outcome()})

    @override
    def on_core(self, core: Sequence[int]) -> None:  # noqa: D102
        self.recording.append(
            {
                "__f": "on_core",
                "core": core,
            }
        )
        self.test.on_core(core)
        self.recording.amend({"__outcome": self.outcome()})

    @override
    def on_statistics(self, step: StatisticsMap, accumulated: StatisticsMap) -> None:  # noqa: D102
        self.recording.append(
            {
                "__f": "on_statistics",
                "step": step,
                "accumulated": accumulated,
            }
        )
        self.test.on_statistics(step, accumulated)
        self.recording.amend({"__outcome": self.outcome()})

    @override
    def on_finish(self, result: SolveResult) -> None:  # noqa: D102
        self.recording.append(
            {
                "__f": "on_finish",
                "result": result,
            }
        )
        self.test.on_finish(result)
        self.recording.amend({"__outcome": self.outcome()})

    @override
    def outcome(self) -> Outcome:  # noqa: D102
        return self.test.outcome()

A test that behaves identical to a given other test but records any call to one of its on_*-methods.

This can be very helpful for debugging.

Parameters

test

A Test that determines how this test should behave.

Ancestors

• Test
• abc.ABC

Inherited members

• Test:
  • assert_
  • on_core
  • on_finish
  • on_model
  • on_statistics
  • on_unsat
  • outcome

class Recording (entries: Sequence[Dict[str, Any]] | None = None)

Expand source code

class Recording:
    """A recording of the calls to the `on_*`-methods of a `Test`.

    This class is mainly used inside of `Record`.
    """

    def __init__(self, entries: Optional[Sequence[Dict[str, Any]]] = None):
        if entries is None:
            entries = []
        self.__entries = list(entries)

    def __repr__(self):
        name = self.__class__.__name__
        return f"{name}({self.__entries})"

    def __str__(self):
        def fmt(entry):
            result = f"[{entry['__outcome']}] {entry['__f']}"
            if entry["__f"] == "on_model":
                result += os.linesep + 4 * " " + entry["str(model)"]
            return result

        width = len(str(len(self.__entries) - 1))
        return os.linesep.join(
            (f"{(width - len(str(i))) * ' '}{i}: {fmt(entry)}" for i, entry in enumerate(self.__entries))
        )

    def __eq__(self, other):
        return self.__entries == other.__entries

    def __hash__(self):
        return hash(self.__entries)

    def amend(self, changes: Dict[str, Any]):
        """Update the last entry of this encoding.

        Parameters
        ----------
        changes
            The changes.
        """
        self.__entries[-1].update(changes)

    def append(self, entry: Dict[str, Any]):
        """Append a new entry at the end of this recording.

        Parameters
        ----------
        entry
            The entry.
        """
        self.__entries.append(entry)

    def subsumes(self, other) -> bool:
        """Determine whether this recording subsumes another recording.

        Parameters
        ----------
        other
            The other recording.
        """
        return len(self.__entries) == len(other.__entries) and all(
            all(item in other_entry.items() for item in self_entry.items())
            for self_entry, other_entry in zip(self.__entries, other.__entries, strict=True)
        )

A recording of the calls to the on_*-methods of a Test.

This class is mainly used inside of Record.

Methods

def amend(self, changes: Dict[str, Any])

Expand source code

def amend(self, changes: Dict[str, Any]):
    """Update the last entry of this encoding.

    Parameters
    ----------
    changes
        The changes.
    """
    self.__entries[-1].update(changes)

Update the last entry of this encoding.

Parameters

changes

The changes.

def append(self, entry: Dict[str, Any])

Expand source code

def append(self, entry: Dict[str, Any]):
    """Append a new entry at the end of this recording.

    Parameters
    ----------
    entry
        The entry.
    """
    self.__entries.append(entry)

Append a new entry at the end of this recording.

Parameters

entry

The entry.

def subsumes(self, other) ‑> bool

Expand source code

def subsumes(self, other) -> bool:
    """Determine whether this recording subsumes another recording.

    Parameters
    ----------
    other
        The other recording.
    """
    return len(self.__entries) == len(other.__entries) and all(
        all(item in other_entry.items() for item in self_entry.items())
        for self_entry, other_entry in zip(self.__entries, other.__entries, strict=True)
    )

Determine whether this recording subsumes another recording.

Parameters

other

The other recording.

class Test

Expand source code

class Test(ABC):
    """An abstract test consuming the `clintest.solver.Solver` artifacts to compute an `clintest.outcome.Outcome`."""

    def on_model(self, _model: Model) -> bool:
        """Consume a `clingo.model.Model` and possibly alter the current outcome of this test.

        Parameters
        ----------
        model
            The `clingo.model.Model` to consume.

        Returns:
        -------
        Whether further models a needed to decide this test.
        """
        return True

    def on_unsat(self, lower_bound: Sequence[int]) -> None:  # noqa: B027
        """Consume a `lower_bound` during optimization and possibly alter the current outcome of this test.

        Parameters
        ----------
        lower_bound
            The lower bound.
        """

    def on_core(self, core: Sequence[int]) -> None:  # noqa: B027
        """Consume an unsat `core` and possibly alter the current outcome of this test.

        Parameters
        ----------
        core
            The unsat core.
        """

    def on_statistics(self, step: StatisticsMap, accumulated: StatisticsMap) -> None:  # noqa: B027
        """Consume the solving statistics and possibly alter the current outcome of this test.

        Parameters
        ----------
        step
            The step statistics.

        accumulated
            The accumulated statistics.
        """

    @abstractmethod
    def on_finish(self, result: SolveResult) -> None:
        """Consume the final solve result and possibly alter the current outcome of this test.

        This should be the last `on_*`-method ever called on a test.
        Afterwards the outcome must be certain.

        Parameters
        ----------
        result
            The `clingo.solving.SolveResult`.
        """

    @abstractmethod
    def outcome(self) -> Outcome:
        """Returns the current `Outcome` of this test.

        Returns:
        -------
        The current outcome of this test.
        """

    def assert_(self) -> None:
        """Assert the outcome of this test to be certainly true.

        Raise an `AssertionError` if the test is either incomplete or has failed.
        """
        if not self.outcome().is_certainly_true():
            msg = "The following test "
            msg += ["is incomplete.", "has failed."][self.outcome().is_certain()]
            msg += os.linesep
            msg += indent(str(self), 4 * " ")

            raise AssertionError(msg)

An abstract test consuming the Solver artifacts to compute an Outcome.

Ancestors

• abc.ABC

Subclasses

• And
• Assert
• Context
• False_
• Not
• Or
• Record
• True_

Methods

def assert_(self) ‑> None

Expand source code

def assert_(self) -> None:
    """Assert the outcome of this test to be certainly true.

    Raise an `AssertionError` if the test is either incomplete or has failed.
    """
    if not self.outcome().is_certainly_true():
        msg = "The following test "
        msg += ["is incomplete.", "has failed."][self.outcome().is_certain()]
        msg += os.linesep
        msg += indent(str(self), 4 * " ")

        raise AssertionError(msg)

Assert the outcome of this test to be certainly true.

Raise an AssertionError if the test is either incomplete or has failed.

def on_core(self, core: Sequence[int]) ‑> None

Expand source code

def on_core(self, core: Sequence[int]) -> None:  # noqa: B027
    """Consume an unsat `core` and possibly alter the current outcome of this test.

    Parameters
    ----------
    core
        The unsat core.
    """

Consume an unsat core and possibly alter the current outcome of this test.

Parameters

core

The unsat core.

def on_finish(self, result: clingo.solving.SolveResult) ‑> None

Expand source code

@abstractmethod
def on_finish(self, result: SolveResult) -> None:
    """Consume the final solve result and possibly alter the current outcome of this test.

    This should be the last `on_*`-method ever called on a test.
    Afterwards the outcome must be certain.

    Parameters
    ----------
    result
        The `clingo.solving.SolveResult`.
    """

Consume the final solve result and possibly alter the current outcome of this test.

This should be the last on_*-method ever called on a test. Afterwards the outcome must be certain.

Parameters

result

The clingo.solving.SolveResult.

def on_model(self,
_model: Model) ‑> bool

Expand source code

def on_model(self, _model: Model) -> bool:
    """Consume a `clingo.model.Model` and possibly alter the current outcome of this test.

    Parameters
    ----------
    model
        The `clingo.model.Model` to consume.

    Returns:
    -------
    Whether further models a needed to decide this test.
    """
    return True

Consume a clingo.model.Model and possibly alter the current outcome of this test.

Parameters

model

The clingo.model.Model to consume.

Returns:

Whether further models a needed to decide this test.

def on_statistics(self,
step: clingo.statistics.StatisticsMap,
accumulated: clingo.statistics.StatisticsMap) ‑> None

Expand source code

def on_statistics(self, step: StatisticsMap, accumulated: StatisticsMap) -> None:  # noqa: B027
    """Consume the solving statistics and possibly alter the current outcome of this test.

    Parameters
    ----------
    step
        The step statistics.

    accumulated
        The accumulated statistics.
    """

Consume the solving statistics and possibly alter the current outcome of this test.

Parameters

step

The step statistics.

accumulated

The accumulated statistics.

def on_unsat(self, lower_bound: Sequence[int]) ‑> None

Expand source code

def on_unsat(self, lower_bound: Sequence[int]) -> None:  # noqa: B027
    """Consume a `lower_bound` during optimization and possibly alter the current outcome of this test.

    Parameters
    ----------
    lower_bound
        The lower bound.
    """

Consume a lower_bound during optimization and possibly alter the current outcome of this test.

Parameters

lower_bound

The lower bound.

def outcome(self) ‑> Outcome

Expand source code

@abstractmethod
def outcome(self) -> Outcome:
    """Returns the current `Outcome` of this test.

    Returns:
    -------
    The current outcome of this test.
    """

Returns the current Outcome of this test.

Returns:

The current outcome of this test.

class True_ (lazy: bool = True)

Expand source code

class True_(Test):
    """The test which always succeeds.

    Parameters
    ----------
    lazy
        Whether this test should be lazy, i.e., not consume any models.
    """

    def __init__(self, lazy: bool = True) -> None:
        self.__outcome = Outcome(True, lazy)

    def __repr__(self):
        name = self.__class__.__name__
        outcome = repr(self.__outcome)
        return f"{name}(__outcome={outcome})"

    def __str__(self):
        return f"[{self.__outcome}] {self.__class__.__name__}"

    @override
    def on_model(self, _model: Model) -> bool:  # noqa: D102
        return not self.__outcome.is_certain()

    @override
    def on_finish(self, result: SolveResult) -> None:  # noqa: D102
        self.__outcome = Outcome(True, True)

    @override
    def outcome(self) -> Outcome:  # noqa: D102
        return self.__outcome

The test which always succeeds.

Parameters

lazy

Whether this test should be lazy, i.e., not consume any models.

Ancestors

• Test
• abc.ABC

Inherited members

• Test:
  • assert_
  • on_core
  • on_finish
  • on_model
  • on_statistics
  • on_unsat
  • outcome