Module `Z3`

exception Error of string

type context

val mk_context : (string * string) list -> context

val interrupt : context -> unit

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 Simplifier : sig ... end

module Statistics : sig ... end

module Solver : sig ... end

module Fixedpoint : sig ... end

module Optimize : sig ... end

module SMT : sig ... end

module RCF : 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