package yices2

You can search for identifiers within the package.

in-package search v0.2.0

Yices2 SMT solver binding

Install

Dune Dependency

micdel.fr Edit opam file Versions (2)

Authors

M

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

Maintainers

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 =

| IDLE
| SEARCHING
| UNKNOWN
| SAT
| UNSAT
| INTERRUPTED
| 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