package yices2

  1. Overview
  2. Docs

Module Yices2

val version : string
val build_arch : string
val build_mode : string
val build_date : string
type typ
type term
type config
type context
type params
type model
type status =
  1. | IDLE
  2. | SEARCHING
  3. | UNKNOWN
  4. | SAT
  5. | UNSAT
  6. | INTERRUPTED
  7. | ERROR
val string_of_status : status -> string
module Error : sig ... end
exception YicesError of Error.code * Error.report
val register_exn : unit -> unit

register_exn must be called before any use of Yices2 functions. In most cases, the main function of the Yices2 package will call register_exn) by itself, so you won't have to do anything. But in some cases, the main wont be executed and will need to run register_exn yourself.

val print_supported : unit -> bool

On some systems, like mingw or alpine, fopen or fcookieopen are not available and thus the functions Type.print, Term.print and Model.print are not available. This function tells you if it is available.

module Experimental : sig ... end
module Type : sig ... end

Types

module Term : sig ... end
module Context : sig ... end

Context

module Model : sig ... end

Model