package yices2_bindings

  1. Overview
  2. Docs
type t = Yices2_low.Types.model_t Ctypes.ptr
val free : t -> unit
val collect_defined_terms : t -> Yices2_low.Types.term_t list
val get_bool_value : t -> Yices2_low.Types.term_t -> bool eh
val get_int32_value : t -> Yices2_low.Types.term_t -> Signed.sint eh
val get_int64_value : t -> Yices2_low.Types.term_t -> Signed.long eh
val get_rational32_value : t -> Yices2_low.Types.term_t -> (Signed.sint * Unsigned.uint) eh
val get_rational64_value : t -> Yices2_low.Types.term_t -> (Signed.long * Unsigned.ulong) eh
val get_double_value : t -> Yices2_low.Types.term_t -> float eh
val get_mpz_value : t -> Yices2_low.Types.term_t -> Z.t eh
val get_mpq_value : t -> Yices2_low.Types.term_t -> Q.t eh
val get_bv_value : t -> Yices2_low.Types.term_t -> Signed.sint eh
val get_scalar_value : t -> Yices2_low.Types.term_t -> Signed.sint eh
val get_value : t -> Yices2_low.Types.term_t -> Yices2_low.Types.yval_t Ctypes.ptr eh
val val_is_int32 : t -> Yices2_low.Types.yval_t Ctypes.ptr -> bool eh
val val_is_int64 : t -> Yices2_low.Types.yval_t Ctypes.ptr -> bool eh
val val_is_rational32 : t -> Yices2_low.Types.yval_t Ctypes.ptr -> bool eh
val val_is_rational64 : t -> Yices2_low.Types.yval_t Ctypes.ptr -> bool eh
val val_is_integer : t -> Yices2_low.Types.yval_t Ctypes.ptr -> bool eh
val val_bitsize : t -> Yices2_low.Types.yval_t Ctypes.ptr -> int eh
val val_tuple_arity : t -> Yices2_low.Types.yval_t Ctypes.ptr -> int eh
val val_mapping_arity : t -> Yices2_low.Types.yval_t Ctypes.ptr -> int eh
val val_function_arity : t -> Yices2_low.Types.yval_t Ctypes.ptr -> int eh
val val_function_type : t -> Yices2_low.Types.yval_t Ctypes.ptr -> Yices2_low.Types.type_t eh
val val_get_bool : t -> Yices2_low.Types.yval_t Ctypes.ptr -> bool eh
val val_get_int32 : t -> Yices2_low.Types.yval_t Ctypes.ptr -> Signed.sint eh
val val_get_int64 : t -> Yices2_low.Types.yval_t Ctypes.ptr -> Signed.long eh
val val_get_rational32 : t -> Yices2_low.Types.yval_t Ctypes.ptr -> (Signed.sint * Unsigned.uint) eh
val val_get_rational64 : t -> Yices2_low.Types.yval_t Ctypes.ptr -> (Signed.long * Unsigned.ulong) eh
val val_get_double : t -> Yices2_low.Types.yval_t Ctypes.ptr -> float eh
val val_get_mpz : Yices2_low.Types.model_t Ctypes.ptr -> Yices2_low.Types.yval_t Ctypes.ptr -> Z.t eh
val val_get_mpq : Yices2_low.Types.model_t Ctypes.ptr -> Yices2_low.Types.yval_t Ctypes.ptr -> Q.t eh
val val_get_bv : t -> Yices2_low.Types.yval_t Ctypes.ptr -> Signed.sint eh
val val_get_scalar : t -> Yices2_low.Types.yval_t Ctypes.ptr -> (Signed.sint * Yices2_low.Types.type_t) eh
val val_expand_tuple : t -> Yices2_low.Types.yval_t Ctypes.ptr -> Yices2_low.Types.yval_t Ctypes.ptr list eh
val val_expand_function : t -> Yices2_low.Types.yval_t Ctypes.ptr -> (Yices2_low.Types.yval_t Ctypes.ptr * Yices2_low.Types.yval_t Ctypes.ptr list) eh
val val_expand_mapping : t -> Yices2_low.Types.yval_t Ctypes.ptr -> (Yices2_low.Types.yval_t Ctypes.ptr list * Yices2_low.Types.yval_t Ctypes.ptr) eh
val formula_true_in_model : t -> Yices2_low.Types.term_t -> bool eh
val formulas_true_in_model : t -> Yices2_low.Types.term_t list -> bool eh
val get_value_as_term : t -> Yices2_low.Types.term_t -> Yices2_low.Types.term_t eh
val terms_value : t -> Yices2_low.Types.term_t list -> Yices2_low.Types.term_t list eh
val model_term_support : t -> Yices2_low.Types.term_t -> Yices2_low.Types.term_t list eh
val model_terms_support : t -> Yices2_low.Types.term_t list -> Yices2_low.Types.term_t list eh
val implicant_for_formula : t -> Yices2_low.Types.term_t -> Yices2_low.Types.term_t list eh
val implicant_for_formulas : t -> Yices2_low.Types.term_t list -> Yices2_low.Types.term_t list eh
OCaml

Innovation. Community. Security.