yices2_bindings 0.1 · 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.t

val collect_defined_terms : t -> Yices2_low.Types.term_t list

val get_bool_value : t -> Yices2_low.Types.term_t -> bool EH.t

val get_int32_value : t -> Yices2_low.Types.term_t -> Signed.sint EH.t

val get_int64_value : t -> Yices2_low.Types.term_t -> Signed.long EH.t

val get_rational32_value : 
  t ->
  Yices2_low.Types.term_t ->
  (Signed.sint * Unsigned.uint) EH.t

val get_rational64_value : 
  t ->
  Yices2_low.Types.term_t ->
  (Signed.long * Unsigned.ulong) EH.t

val get_double_value : t -> Yices2_low.Types.term_t -> float EH.t

val get_mpz_value : t -> Yices2_low.Types.term_t -> Z.t EH.t

val get_mpq_value : t -> Yices2_low.Types.term_t -> Q.t EH.t

val get_bv_value : t -> Yices2_low.Types.term_t -> Signed.sint EH.t

val get_scalar_value : t -> Yices2_low.Types.term_t -> Signed.sint EH.t

val get_value : 
  t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.yval_t Ctypes.ptr EH.t

val val_is_int32 : t -> Yices2_low.Types.yval_t Ctypes.ptr -> bool EH.t

val val_is_int64 : t -> Yices2_low.Types.yval_t Ctypes.ptr -> bool EH.t

val val_is_rational32 : t -> Yices2_low.Types.yval_t Ctypes.ptr -> bool EH.t

val val_is_rational64 : t -> Yices2_low.Types.yval_t Ctypes.ptr -> bool EH.t

val val_is_integer : t -> Yices2_low.Types.yval_t Ctypes.ptr -> bool EH.t

val val_bitsize : t -> Yices2_low.Types.yval_t Ctypes.ptr -> int EH.t

val val_tuple_arity : t -> Yices2_low.Types.yval_t Ctypes.ptr -> int EH.t

val val_mapping_arity : t -> Yices2_low.Types.yval_t Ctypes.ptr -> int EH.t

val val_function_arity : t -> Yices2_low.Types.yval_t Ctypes.ptr -> int EH.t

val val_function_type : 
  t ->
  Yices2_low.Types.yval_t Ctypes.ptr ->
  Yices2_low.Types.type_t EH.t

val val_get_bool : t -> Yices2_low.Types.yval_t Ctypes.ptr -> bool EH.t

val val_get_int32 : t -> Yices2_low.Types.yval_t Ctypes.ptr -> Signed.sint EH.t

val val_get_int64 : t -> Yices2_low.Types.yval_t Ctypes.ptr -> Signed.long EH.t

val val_get_rational32 : 
  t ->
  Yices2_low.Types.yval_t Ctypes.ptr ->
  (Signed.sint * Unsigned.uint) EH.t

val val_get_rational64 : 
  t ->
  Yices2_low.Types.yval_t Ctypes.ptr ->
  (Signed.long * Unsigned.ulong) EH.t

val val_get_double : t -> Yices2_low.Types.yval_t Ctypes.ptr -> float EH.t

val val_get_mpz : 
  Yices2_low.Types.model_t Ctypes.ptr ->
  Yices2_low.Types.yval_t Ctypes.ptr ->
  Z.t EH.t

val val_get_mpq : 
  Yices2_low.Types.model_t Ctypes.ptr ->
  Yices2_low.Types.yval_t Ctypes.ptr ->
  Q.t EH.t

val val_get_bv : t -> Yices2_low.Types.yval_t Ctypes.ptr -> Signed.sint EH.t

val val_get_scalar : 
  t ->
  Yices2_low.Types.yval_t Ctypes.ptr ->
  (Signed.sint * Yices2_low.Types.type_t) EH.t

val val_expand_tuple : 
  t ->
  Yices2_low.Types.yval_t Ctypes.ptr ->
  Yices2_low.Types.yval_t Ctypes.ptr list EH.t

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.t

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.t

val formula_true_in_model : t -> Yices2_low.Types.term_t -> bool EH.t

val formulas_true_in_model : t -> Yices2_low.Types.term_t list -> bool EH.t

val get_value_as_term : 
  t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t EH.t

val terms_value : 
  t ->
  Yices2_low.Types.term_t list ->
  Yices2_low.Types.term_t list EH.t

val model_term_support : 
  t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t list EH.t

val model_terms_support : 
  t ->
  Yices2_low.Types.term_t list ->
  Yices2_low.Types.term_t list EH.t

val implicant_for_formula : 
  t ->
  Yices2_low.Types.term_t ->
  Yices2_low.Types.term_t list EH.t

val implicant_for_formulas : 
  t ->
  Yices2_low.Types.term_t list ->
  Yices2_low.Types.term_t list EH.t

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.t

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.t

package yices2_bindings