package smtml

  1. Overview
  2. Docs

Parameters

Signature

type 'a with_cont = {
  1. node : 'a;
  2. cont : M.cont;
}
type model = M.model with_cont
type solver = M.solver with_cont
type handle = M.handle
type optimize = M.optimizer with_cont
val err : ('a, Format.formatter, unit, 'b) format4 -> 'a
val get_type : Ty.t -> M.ty M.t
module Bool_impl : sig ... end
module Int_impl : sig ... end
module Real_impl : sig ... end
module String_impl : sig ... end
module type Bitv_sig = sig ... end
module Bitv_impl (B : Bitv_sig) : sig ... end
module I8 : sig ... end
module I32 : sig ... end
module I64 : sig ... end
module type Float_sig = sig ... end
module Float_impl (F : Float_sig) : sig ... end
module Float32_impl : sig ... end
module Float64_impl : sig ... end
val v : Value.t -> M.term M.t
val unop : Ty.t -> Ty.unop -> M.term -> M.term M.t
val binop : Ty.t -> Ty.binop -> M.term -> M.term -> M.term M.t
val triop : Ty.t -> Ty.triop -> M.term -> M.term -> M.term -> M.term M.t
val relop : Ty.t -> Ty.relop -> M.term -> M.term -> M.term M.t
val cvtop : Ty.t -> Ty.cvtop -> M.term -> M.term M.t
val encode_expr : Expr.t -> M.term M.t
val pp_smt : ?status:'a -> 'b -> 'c -> 'd
val value : model -> Expr.t -> Value.t
val values_of_model : ?symbols:Symbol.t list -> M.model with_cont -> (Symbol.t, Value.t) Hashtbl.t
val set_debug : 'a -> unit
module Solver : sig ... end
module Optimizer : sig ... end
OCaml

Innovation. Community. Security.