package z3

  1. Overview
  2. Docs
exception Error of string
type context
val mk_context : (string * string) list -> context
module Log : sig ... end
module Version : sig ... end
module Symbol : sig ... end
module AST : sig ... end
module Sort : sig ... end
module FuncDecl : sig ... end
module Params : sig ... end
module Expr : sig ... end
module Boolean : sig ... end
module Quantifier : sig ... end
module Z3Array : sig ... end
module Set : sig ... end
module FiniteDomain : sig ... end
module Relation : sig ... end
module Datatype : sig ... end
module Enumeration : sig ... end
module Z3List : sig ... end
module Tuple : sig ... end
module Arithmetic : sig ... end
module BitVector : sig ... end
module Seq : sig ... end
module FloatingPoint : sig ... end
module Proof : sig ... end
module Goal : sig ... end
module Model : sig ... end
module Probe : sig ... end
module Tactic : sig ... end
module Statistics : sig ... end
module Solver : sig ... end
module Fixedpoint : sig ... end
module Optimize : sig ... end
module SMT : sig ... end
val set_global_param : string -> string -> unit
val get_global_param : string -> string option
val global_param_reset_all : unit -> unit
val toggle_warning_messages : bool -> unit
val enable_trace : string -> unit
val disable_trace : string -> unit
module Memory : sig ... end