Smt2 (dolmen_loop.Dolmen_loop.Transform.Make.Smt2)

val pipe : string

module View = Dolmen_std.Expr.View.TFF

module S : sig ... end

type old_logic = Smtlib2(State)(Typer_Types).old_logic =

| Not_seen_yet
| Logic of (string * Typer_Types.typechecked Typer_Types.stmt) option

type acc = Smtlib2(State)(Typer_Types).acc = {

seen_exit : bool;
scan_acc : S.acc option;
old_logic : old_logic;
pre_logic_stmts : Typer_Types.typechecked Typer_Types.stmt list;
post_logic_stmts : Typer_Types.typechecked Typer_Types.stmt list;

}

val init : compute_logic:bool -> acc

val need_logic : old_logic -> old_logic

val compute_logic : 
  State.t ->
  acc ->
  State.t * Typer_Types.typechecked Typer_Types.stmt list

val flush : 
  State.t ->
  acc ->
  Typer_Types.typechecked Typer_Types.stmt list ->
  State.t * acc * Typer_Types.typechecked Typer_Types.stmt list

val reduce_post_logic_stmts : 'a -> 'a

val add_post_logic_stmt : 
  acc ->
  Typer_Types.typechecked Typer_Types.stmt ->
  acc

val add_pre_logic_stmt : acc -> Typer_Types.typechecked Typer_Types.stmt -> acc

val add_stmt : acc -> Typer_Types.typechecked Typer_Types.stmt -> acc

val accumulate_logic_aux : 
  (State.t * acc * Typer_Types.typechecked Typer_Types.stmt list) ->
  Typer_Types.typechecked Typer_Types.stmt ->
  State.t * acc * Typer_Types.typechecked Typer_Types.stmt list

val accumulate_logic : 
  (State.t * acc * Typer_Types.typechecked Typer_Types.stmt list) ->
  Typer_Types.typechecked Typer_Types.stmt ->
  State.t * acc * Typer_Types.typechecked Typer_Types.stmt list

val transform : 
  State.t ->
  acc ->
  Typer_Types.typechecked Typer_Types.stmt list ->
  State.t * acc * Typer_Types.typechecked Typer_Types.stmt list