Interface

It consists in two modules Yices and Yicesl (l for light). These modules closely follow the API of their C counterpart. Thus, most yices_* functions are accessible through Yices.*, whereas yicesl_* functions are translated into Yicesl.*. See Yices C API and C API Lite documentations.

Though, big integers and rationals are accessible through:

• val get_rational_value_as_string : model -> var_decl -> string
• val get_integer_value_as_string : model -> var_decl -> string
• val get_ratio_value : model -> var_decl -> Ratio.ratio
• val get_big_int_value : model -> var_decl -> Big_int.big_int

Also, the iterator over boolean variables is replaced by:

• val iter_bool_var_decl: (var_decl -> unit) -> context -> unit

Finally, some exception handling are added:

• Functions that may return NULL in the C API may rise a Failure exception instead (that is functions returning Yices.expr, Yices.typ, Yices.var_decl, Yices.context, Yices.model, or Yices.var_decl_iterator).
• Functions that extract value from model (Yices.get_*) return directly the value (not a parameter) instead of an error code. If there is an error, a Failure is raised.
• Yicesl.read may fail (Failure) with a meaningful message (the C function yicesl_get_last_error_message is automatically called).