z3 4.11.2 · OCaml Package

z3

To focus the search input from anywhere on the page, press the 'S' key.

in-package search v0.1.0

z3ml
- Z3
  - AST
    
    ASTMap
    
    ASTVector
  - Arithmetic
    
    Integer
    
    Real
    
    AlgebraicNumber
  - BitVector
  - Boolean
  - Datatype
    
    Constructor
  - Enumeration
  - Expr
  - FiniteDomain
  - Fixedpoint
  - FloatingPoint
    
    RoundingMode
  - FuncDecl
    
    Parameter
  - Goal
  - Log
  - Memory
  - Model
    
    FuncInterp
    
    FuncEntry
  - Optimize
  - Params
    
    ParamDescrs
  - Probe
  - Proof
  - Quantifier
    
    Pattern
  - Relation
  - SMT
  - Seq
  - Set
  - Solver
  - Sort
  - Statistics
    
    Entry
  - Symbol
  - Tactic
    
    ApplyResult
  - Tuple
  - Version
  - Z3Array
  - Z3List
- Z3enums
- Z3native

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Constructor : sig ... end

val mk_constructor : 
  context ->
  Symbol.symbol ->
  Symbol.symbol ->
  Symbol.symbol list ->
  Sort.sort option list ->
  int list ->
  Constructor.constructor

val mk_constructor_s : 
  context ->
  string ->
  Symbol.symbol ->
  Symbol.symbol list ->
  Sort.sort option list ->
  int list ->
  Constructor.constructor

val mk_sort_ref : context -> Symbol.symbol -> Sort.sort

val mk_sort_ref_s : context -> string -> Sort.sort

val mk_sort : 
  context ->
  Symbol.symbol ->
  Constructor.constructor list ->
  Sort.sort

val mk_sort_s : context -> string -> Constructor.constructor list -> Sort.sort

val mk_sorts : 
  context ->
  Symbol.symbol list ->
  Constructor.constructor list list ->
  Sort.sort list

val mk_sorts_s : 
  context ->
  string list ->
  Constructor.constructor list list ->
  Sort.sort list

val get_num_constructors : Sort.sort -> int

val get_constructors : Sort.sort -> FuncDecl.func_decl list

val get_recognizers : Sort.sort -> FuncDecl.func_decl list

val get_accessors : Sort.sort -> FuncDecl.func_decl list list