package alt-ergo-lib

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val clear_cache : unit -> unit

Empties the internal cache of the module.

val dty_to_ty : ?update:bool -> ?is_var:bool -> AltErgoLib.D_loop.DStd.Expr.ty -> Ty.t

dty_to_ty update is_var subst tyv_substs dty

Converts a Dolmen type to an Alt-Ergo type.

  • If update is true then for each type variable of type DE.Ty.Var.t, if it was not encountered before, a new type variable of type Ty.t is created and added to the cache.
  • If dty is a type application, or an arrow type, only its return type is converted since those have no counterpart in AE's Ty module. The function arguments' types or the type paramters ought to be converted individually.
val make_form : string -> AltErgoLib.D_loop.DStd.Expr.term -> Loc.t -> decl_kind:Expr.decl_kind -> Expr.t

make acc stmt Makes one or more Commands.sat_tdecl from the type-checked statement stmt and appends them to acc.

OCaml

Innovation. Community. Security.