Engine (astral.Astral_internal.Engine)

module Logger : Logger_sig.LOGGER

val debug_info : Context.t -> unit

val normalise : Context.t -> Context.t

Apply necessary transformations to input formula and SID.

Note: It is necessary to first initialize SID and predicate dependency graph to perform inlining correctly. Inlined predicates are removed by re-initializing SID.

val run_solver : Context.t -> Context.t

val solve : ParserContext.t -> Context.t