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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

val pph : int -> t Containers.Format.printer

val pp : t Containers.Format.printer

package yices2_bindings