package yices2

You can search for identifiers within the package.

in-package search v0.2.0

package yices2

yices2
- Yices2
  - Context
    
    Config
    
    Params
  - Error
  - Experimental
  - Model
  - Term
    
    Arith
    
    Bitvector
    
    Bool
    
    Fun
    
    Int
    
    Poly
    
    Ratio
    
    RatioPoly
    
    Tuple
  - Type

Legend:
Library
Module
Module type
Parameter
Class
Class type

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