SmallModels (astral.Astral_internal.SmallModels)

module Logger : sig ... end

module Abstraction = PredicateAbstraction

module SL_graph : sig ... end

module Hyperedge : sig ... end

Hyperedge represents an unprocessed predicate occurrence.

module Hypergraph : sig ... end

module Derivation : sig ... end

val compute_fixpoint : 
  ?n:int ->
  SL.t ->
  SID_checks.distinguisher SID_checks.M.t ->
  InductiveDefinition.t ->
  Derivation.t ->
  Derivation.t * Abstraction.t

val debug_results : PredicateAbstraction.M.t -> unit

val compute : 
  SL.t ->
  SID_checks.distinguisher SID_checks.M.t ->
  Abstraction.M.t