Skip to content

solving

Module to solve counterexample programs.

solve_for_counterexample(cx_program_forward: str | None, cx_program_backward: str | None, inputs: set[Predicate], outputs: set[Predicate], domain_start: int, domain_max: int | None, clingo_args: list[str], size_placeholder: str) -> Counterexample | None

Solve the given CX programs for counterexamples by increasing the domain size from start to max.

Returns the counterexample if one is found, otherwise None.

solve_gc_for_counterexample(forward_guess: str | None, forward_check: str | None, backward_guess: str | None, backward_check: str | None, inputs: set[Predicate], outputs: set[Predicate], domain_start: int, domain_max: int | None, clingo_args: list[str], size_placeholder: str) -> Counterexample | None

Solve the given guess and check CX programs for counterexamples by increasing the domain size from start to max.

Returns the counterexample if one is found, otherwise None.