alt-ergo-lib 2.5.3 (latest)

type state = State.t

type ty_state

type env

type !'a fragment

type error

type warning

type builtin_symbols =
  Dolmen_loop__Typer.T.env ->
  Dolmen_type.Intf.symbol ->
  [ Dolmen_loop__Typer.T.builtin_res | Dolmen_loop__Typer.T.not_found ]

val ty_state : ty_state State.key

val check_model : bool State.key

val smtlib2_forced_logic : string option State.key

type input = [

| `Logic of Dolmen_loop.Logic.language Dolmen_loop.State.file
| `Response of Dolmen_loop.Response.language Dolmen_loop.State.file

]

type lang = [

| `Logic of Dolmen_loop.Logic.language
| `Response of Dolmen_loop.Response.language

]

val reset : state -> ?loc:Dolmen.Std.Loc.t -> unit -> state

val reset_assertions : state -> ?loc:Dolmen.Std.Loc.t -> unit -> state

val push : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> int -> state

val pop : state -> input:input -> ?loc:Dolmen.Std.Loc.t -> int -> state

val set_logic : 
  state ->
  input:input ->
  ?loc:Dolmen.Std.Loc.t ->
  string ->
  state * Dolmen_type.Logic.t

val defs : 
  mode:[ `Create_id | `Use_declared_id ] ->
  state ->
  input:input ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Statement.defs ->
  state
  * [ `Instanceof of
        Dolmen.Std.Id.t
        * Dolmen.Std.Expr.term_cst
        * Dolmen.Std.Expr.ty list
        * Dolmen.Std.Expr.ty_var list
        * Dolmen.Std.Expr.term_var list
        * Dolmen.Std.Expr.term
    | `Term_def of
      Dolmen.Std.Id.t
      * Dolmen.Std.Expr.term_cst
      * Dolmen.Std.Expr.ty_var list
      * Dolmen.Std.Expr.term_var list
      * Dolmen.Std.Expr.term
    | `Type_alias of
      Dolmen.Std.Id.t
      * Dolmen.Std.Expr.ty_cst
      * Dolmen.Std.Expr.ty_var list
      * Dolmen.Std.Expr.ty ]
      list

val decls : 
  state ->
  input:input ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Statement.decls ->
  state
  * [ `Term_decl of Dolmen.Std.Expr.term_cst
    | `Type_decl of Dolmen.Std.Expr.ty_cst * Dolmen.Std.Expr.ty_def option ]
      list

val terms : 
  state ->
  input:input ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Term.t list ->
  state * Dolmen.Std.Expr.term list

val formula : 
  state ->
  input:input ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  goal:bool ->
  Dolmen.Std.Term.t ->
  state * Dolmen.Std.Expr.formula

val formulas : 
  state ->
  input:input ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Term.t list ->
  state * Dolmen.Std.Expr.formula list

val typing_wrap : 
  ?attrs:Dolmen.Std.Term.t list ->
  ?loc:Dolmen.Std.Loc.t ->
  input:input ->
  state ->
  f:(env -> 'a) ->
  state * 'a

val init : 
  ?ty_state:ty_state ->
  ?smtlib2_forced_logic:string option ->
  ?additional_builtins:(state -> lang -> builtin_symbols) ->
  state ->
  state

val additional_builtins : (state -> lang -> builtin_symbols) State.key

val report_error : input:input -> state -> error -> state

val report_warning : input:input -> state -> warning -> state

val pop_inferred_model_constants : state -> Dolmen.Std.Expr.term_cst list

package alt-ergo-lib