Export (dolmen_loop.Dolmen

type language = Logic.language

type file = language State.output_file

val enum : (string * Logic.language) list

val rename_num_postfix : int -> Dolmen_std.Name.t -> int * Dolmen_std.Name.t

module type NS = sig ... end

module Env (E : Expr_intf.Export) (N : NS) : sig ... end

val code : Code.t

val internal_error : string Report.Error.t

val missing_language : unit Report.Error.t

val extension_not_found : string Report.Error.t

val unsupported_language : Logic.language Report.Error.t

val polymorphic_function_in_smt2 : unit Report.Error.t

module type S = sig ... end

module type Make_smt2_printer =
  functor (Env : Dolmen_intf.Env.Print with type name := Dolmen_std.Name.t) ->
  functor (S : Dolmen_intf.View.Sexpr.S with type id := Dolmen_std.Id.t) ->
  functor (V : Dolmen_intf.View.TFF.S
                 with type ty = Env.ty
                  and type ty_var = Env.ty_var
                  and type ty_cst = Env.ty_cst
                  and type term = Env.term
                  and type term_var = Env.term_var
                  and type term_cst = Env.term_cst) ->
  Dolmen_intf.Print.Smtlib2
    with type env := Env.t
     and type sexpr := S.t
     and type ty := Env.ty
     and type ty_var := Env.ty_var
     and type ty_cst := Env.ty_cst
     and type term := Env.term
     and type term_var := Env.term_var
     and type term_cst := Env.term_cst

module Smtlib2
  (State : State.S)
  (Printer : Make_smt2_printer)
  (Expr : Expr_intf.Export)
  (Sexpr : 
    Dolmen_intf.View.Sexpr.S
      with type t = Dolmen_std.Term.t
       and type id := Dolmen_std.Id.t)
  (View : 
    Dolmen_intf.View.TFF.S
      with type ty = Expr.Ty.t
       and type ty_var = Expr.Ty.Var.t
       and type ty_cst = Expr.Ty.Const.t
       and type ty_def = Expr.ty_def
       and type term = Expr.Term.t
       and type term_var = Expr.Term.Var.t
       and type term_cst = Expr.Term.Const.t)
  (Typer_Types : 
    Typer.Types
      with type ty = Expr.ty
       and type ty_var = Expr.ty_var
       and type ty_cst = Expr.ty_cst
       and type ty_def = Expr.ty_def
       and type term = Expr.term
       and type term_var = Expr.term_var
       and type term_cst = Expr.term_cst
       and type formula = Expr.term) : 
  sig ... end

module Dummy
  (Expr : Expr_intf.S)
  (Typer_Types : 
    Typer.Types
      with type ty = Expr.ty
       and type ty_var = Expr.ty_var
       and type ty_cst = Expr.ty_cst
       and type ty_def = Expr.ty_def
       and type term = Expr.term
       and type term_var = Expr.term_var
       and type term_cst = Expr.term_cst
       and type formula = Expr.term) : 
  sig ... end

module Make
  (Expr : Expr_intf.Export)
  (Sexpr : 
    Dolmen_intf.View.Sexpr.S
      with type t = Dolmen_std.Term.t
       and type id := Dolmen_std.Id.t)
  (View : 
    Dolmen_intf.View.TFF.S
      with type ty = Expr.Ty.t
       and type ty_var = Expr.Ty.Var.t
       and type ty_cst = Expr.Ty.Const.t
       and type ty_def = Expr.ty_def
       and type term = Expr.Term.t
       and type term_var = Expr.Term.Var.t
       and type term_cst = Expr.Term.Const.t)
  (State : State.S)
  (Typer_Types : 
    Typer.Types
      with type ty = Expr.ty
       and type ty_var = Expr.ty_var
       and type ty_cst = Expr.ty_cst
       and type ty_def = Expr.ty_def
       and type term = Expr.term
       and type term_var = Expr.term_var
       and type term_cst = Expr.term_cst
       and type formula = Expr.term) : 
  sig ... end