Smtlib2 (dolmen_loop.Dolmen_loop.Transform.Smtlib2)

Parameters

module State : State.S

module Typer_Types : 
  Typer.Types
    with type ty = Dolmen_std.Expr.ty
     and type ty_var = Dolmen_std.Expr.ty_var
     and type ty_cst = Dolmen_std.Expr.ty_cst
     and type ty_def = Dolmen_std.Expr.ty_def
     and type term = Dolmen_std.Expr.term
     and type term_var = Dolmen_std.Expr.term_var
     and type term_cst = Dolmen_std.Expr.term_cst
     and type formula = Dolmen_std.Expr.term

Signature

val pipe : string

module View = Dolmen_std.Expr.View.TFF

module S : sig ... end

type old_logic =

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

type 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

Try and simplify some series of statements. Note that the list here is in reverse order (so the first element is the last statement seen).

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