Skip to content

Clingo

ClingoSolver

Bases: Solver

clingo solver.

get_name() -> str classmethod

Get the name under which the solver will be listed in options.

Returns:

Type Description
str

Name of the solver.

interrupt_handler(sig: int, frame: Union[None, FrameType], lns_object: LNS) -> None

Signal handler for interrupts (SIGINT, SIGTERM).

Parameters:

Name Type Description Default
sig int

Signal number.

 required
frame Union[None, FrameType]

Current stack frame.

 required
lns_object LNS

LNS object.

 required

setup(lns_object: LNS, args: list[str] = [], files: Optional[list[str]] = None) -> None

Initialize clingo.Control object using clingo.

Parameters:

Name Type Description Default
lns_object LNS

LNS object.

 required
args list[str]

clingo arguments, default: lns_object.clingo_options.

 []
files Optional[list[str]]

ASP files to be loaded, default: lns_object.files.

 None

setup_interrupt_handling(lns_object: LNS) -> None

Setup signal handling for interrupts (SIGINT, SIGTERM).

Parameters:

Name Type Description Default
lns_object LNS

LNS object.

 required

solve(config: Optional[SolverConfig] = None, assumptions: list[tuple[clingo.symbol.Symbol, bool]] = [], require_model: bool = False) -> Optional[Model]

Solve under assumptions using clingo.

:config: Solver configuration.

Parameters:

Name Type Description Default
assumptions list[tuple[Symbol, bool]]

Assumptions for solving (fixed atoms).

 []
require_model bool

If True, ignore cutoff time until a model is found.

 False

Returns:

Type Description
Optional[Model]

Last obtained model.