Skip to content

API

The API reference is organized to mirror the package structure of anthem-cx. This page documents the top-level anthem_cx package and its high-level public API; the pages below cover the individual modules and subpackages.

  • cx_program — core algorithm: normalization, public reduct, and CX program assembly.
  • Analysis — conflict, dependency, and input analysis.
  • Transformation — the AST transformer pipeline.
  • Utils — shared data types, solving, parsing, output, logging, and errors.

The anthem_cx project.

assemble_and_execute(programs: Programs, options: Options, verdict: UniquenessVerdict) -> Counterexample | None

Assemble the counterexample program from its components and execute/output it.

Returns the counterexample if solving is enabled and one is found, otherwise None.

determine_uniqueness(left: list[AST], right: list[AST], public_predicates: set[Predicate], check: UniquenessCheck) -> UniquenessVerdict

Decide how to solve the counterexample program based on the selected uniqueness check.

Returns:

Name Type Description
UniquenessVerdict UniquenessVerdict

solve directly, use guess-and-check, or defer to local check

reject_recursive_aggregates(left: list[AST], right: list[AST]) -> None

Reject programs containing recursive aggregates, which are not supported.