package yices2

  1. Overview
  2. Docs
Yices2 SMT solver binding

Install 

dune-project
 Dependency

micdel.fr Edit opam file Versions (2)

Authors

  1. M
    Mickaël Delahaye <mickael.delahaye@gmail.com>

Maintainers

  1. M
    Mickaël Delahaye <mickael.delahaye@gmail.com>

Sources

v0.0.3.tar.gz
sha256=2f9dfc5da61e56f49d450132325da21e1081dbde4a95a62735694e2ccd9c2b3a
md5=520065f7d81db571aacbc0e8ea3a63c7

doc/yices2/Yices2/index.html

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