data

Utility data structures.

Auxiliaries dataclass

Dataclass storing the names of auxiliary predicates, the size placeholder, and the predicate suffix.

default() -> Auxiliaries classmethod

Get a default Auxiliaries object.

predicates() -> set[Predicate]

Get all auxiliary predicates.

replace(**kwargs: str) -> Auxiliaries

Get an Auxiliaries object with certain values replaced.

The arguments specify which key to replace by what value.

replace_values(replacements: dict[Predicate, Predicate]) -> Auxiliaries

Get an Auxiliaries object with certain values replaced.

Argument is a dictionary mapping values to new values.

Counterexample dataclass

Dataclass representing counterexamples.

direction: str property

The direction label of the counterexample ('forward' or 'backward').

__str__() -> str

Obtain a string representation of the counterexample.

from_model(is_forward: bool, inputs: set[Predicate], outputs: set[Predicate], model: Model) -> Counterexample classmethod

Create a Counterexample object from a model.

The size is the number of distinct constants actually used in the input atoms, which may differ from the domain size parameter used while solving (e.g. when constants occurring in the programs are added to the domain or when not all domain elements are used).

Direction

Bases: Enum

Enum representing directions of an equivalence problem.

from_string(value: str) -> Direction classmethod

Create a Direction object from a string.

includes_backward() -> bool

Check if the direction includes backward.

includes_forward() -> bool

Check if the direction includes forward.

Options dataclass

Dataclass storing the options of the counterexample problem.

Predicate dataclass

Dataclass representing a predicate by its name and arity.

__str__() -> str

Return the name/arity notation as a string.

Programs dataclass

Dataclass storing the program parts of the counterexample program.

UniquenessCheck

Bases: Enum

The uniqueness check selected on the command line.

The decision on whether to use guess-and-check is stored separately in UniquenessVerdict.

from_string(value: str) -> UniquenessCheck classmethod

Create a UniquenessCheck object from a string.

UniquenessVerdict

Bases: Enum

The outcome of the uniqueness analysis.

uses_gc() -> bool

Check whether the verdict requires the guess and check approach.