package yices2_bindings

  1. Overview
  2. Docs
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.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 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_get_bool : t -> Yices2_low.Types.yval_t Ctypes.ptr -> bool EH.t
val val_get_double : t -> Yices2_low.Types.yval_t Ctypes.ptr -> float 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 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