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.