Abstractor (imandra-base.Imandra_interactive.Abstractor)

module P = Imandra_protocol

include module type of struct include Imandra_surface.Abstractor end

module Predicate = Imandra_surface__Abstractor.Predicate

module Node_data = Imandra_surface__Abstractor.Node_data

module Edge_data = Imandra_surface__Abstractor.Edge_data

module Lit = Imandra_surface__Abstractor.Lit

val is_predicate : f:Lit.t option -> Lit.t list -> bool

module Node = Imandra_surface__Abstractor.Node

module Edge = Imandra_surface__Abstractor.Edge

module G = Imandra_surface__Abstractor.G

module type Dot_Attributes = sig ... end

val merge : G.t -> G.t -> G.t

module Make_Dot = Imandra_surface__Abstractor.Make_Dot

module Json = Imandra_surface__Abstractor.Json

module Dot = Imandra_surface__Abstractor.Dot

module Stage = Imandra_surface__Abstractor.Stage

module Unsat_core = Imandra_surface__Abstractor.Unsat_core

module FSM = Imandra_surface__Abstractor.FSM

val top : 
  ?scope:Opentelemetry.Trace.scope ->
  state_ty:string ->
  valid_state:string ->
  transitions:string list ->
  predicates:string list ->
  ?hints:Imandra_surface.Uid.t Imandra_surface.Hints.t ->
  ?fsm:Imandra_protocol.Abstractor.fsm ->
  ?stages:Imandra_surface.Abstractor.Stage.t list ->
  unit ->
  Imandra_surface.Abstractor.FSM.t