package yices2

  1. Overview
  2. Docs

Model

val get_bool : model -> term -> bool
val get_int : model -> term -> int
val get_nativeint : model -> term -> nativeint
val get_int32 : model -> term -> int32
val get_int64 : model -> term -> int64
val get_rational : model -> term -> int * int
val get_rational_int32 : model -> term -> int32 * int32
val get_rational_int64 : model -> term -> int64 * int64
val get_rational_nativeint : model -> term -> nativeint * nativeint
val get_float : model -> term -> float
val get_bitvector : model -> term -> bool array
val get_z : model -> term -> Z.t
val get_q : model -> term -> Q.t
val get_scalar : model -> term -> int
val get_as_term : model -> term -> term
val get_as_terms : model -> term array -> term array

Pretty printing

val print : ?width:int -> ?height:int -> ?offset:int -> (string -> unit) -> model -> unit