Module Yicesl

module Yicesl: sig .. end
Light Yices binding for Ocaml

See the official C API Lite documentation and the input language specification.

type context 

Type represeting a context
val set_verbosity : int -> unit
Set the verbosity level
val version : unit -> string
Return the yices version number
val enable_type_checker : bool -> unit
Force Yices to type check expressions when they are asserted (default = false)
val enable_log_file : string -> unit
Enable a log file that will store the assertions, checks, decls, etc. If the log file is already open, then nothing happens.
val mk_context : unit -> context
Create a logical context.
val del_context : context -> unit
Delete the given logical context.
val read : context -> string -> unit
Process the given command in the given logical context. The command must use Yices input language.
Raises Failure if the command failed. The message is provided by Yices (C API Lite yicesl_get_last_error_message).
val inconsistent : context -> bool
Return true if the given logical context is inconsistent.
val set_output_file : string -> unit
Set the file that will store the output produced by yices (e.g., models). The default behavior is to send the output to standard output.