package smtml

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = Ast.t
val reset : ?loc:'a -> unit -> Ast.t
val exit : ?loc:'a -> unit -> Ast.t
val push : ?loc:'a -> int -> Ast.t
val pop : ?loc:'a -> int -> Ast.t
val reset_assertions : ?loc:'a -> unit -> Ast.t
val type_decl : ?loc:'a -> 'b
val type_def : ?loc:'a -> Symbol.t -> 'b -> Expr.t -> Ast.t
val datatypes : ?loc:'a -> 'b
val fun_decl : ?loc:Loc.t -> Symbol.t -> Expr.t list -> Expr.t list -> Expr.t -> Ast.t
val fun_def : ?loc:'a -> 'b
val funs_def_rec : ?loc:'a -> 'b -> 'c
val assert_ : ?loc:'a -> Expr.t -> Ast.t
val get_assertions : ?loc:'a -> unit -> Ast.t
val check_sat : ?loc:'a -> Expr.t list -> Ast.t
val get_model : ?loc:'a -> unit -> Ast.t
val get_value : ?loc:'a -> Expr.t list -> Ast.t
val get_assignment : ?loc:'a -> unit -> Ast.t
val get_proof : ?loc:'a -> unit -> 'b
val get_unsat_core : ?loc:'a -> unit -> 'b
val get_unsat_assumptions : ?loc:'a -> unit -> 'b
val get_info : ?loc:'a -> string -> Ast.t
val get_option : ?loc:'a -> string -> Ast.t
val echo : ?loc:'a -> string -> Ast.t
val set_info : ?loc:'a -> Expr.t -> Ast.t
val set_option : ?loc:'a -> Expr.t -> Ast.t
val set_logic : ?loc:Loc.t -> string -> Ast.t
OCaml

Innovation. Community. Security.