yices2_bindings 0.2 · OCaml Package

type t = Yices2_low.Types.model_t Ctypes.ptr

val free : t -> unit

val from_map : (Yices2_low.Types.term_t * Yices2_low.Types.term_t) list -> t eh

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

val generalize_model : 
  t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t list ->
  Yices2_low.Types.yices_gen_mode ->
  Yices2_low.Types.term_t list eh

val generalize_model_list : 
  t ->
  Yices2_low.Types.term_t list ->
  Yices2_low.Types.term_t list ->
  Yices2_low.Types.yices_gen_mode ->
  Yices2_low.Types.term_t list eh

package yices2_bindings