sig
  val ctx : Z3.context
  type zint = [ `Int ]
  type zbool = [ `Bool ]
  type zreal = [ `Real ]
  type znum = [ `Int | `Real ]
  type zany = [ `Bool | `Int | `Real ]
  type ('domain, 'range) zarray = [ `Zarray of 'domain * 'range ]
  type (_, _) typ =
      Int : (Z.t, [> ZZ3_sigs.S.zint ]) ZZ3_sigs.S.typ
    | Bool : (bool, [> ZZ3_sigs.S.zbool ]) ZZ3_sigs.S.typ
    | Real : (Q.t, [> ZZ3_sigs.S.zreal ]) ZZ3_sigs.S.typ
    | Num : (Q.t, [> ZZ3_sigs.S.znum ]) ZZ3_sigs.S.typ
    | Array : ('a, 'x) ZZ3_sigs.S.typ *
        ('b, 'y) ZZ3_sigs.S.typ -> ('a -> 'b, ('x, 'y) ZZ3_sigs.S.zarray)
                                   ZZ3_sigs.S.typ
  type +'a term = private Z3.Expr.expr
  type ('a, 'b) symbol
  module Symbol :
    sig
      val get_typ : ('a, 'b) ZZ3_sigs.S.symbol -> ('a, 'b) ZZ3_sigs.S.typ
      val declare :
        ('a, 'b) ZZ3_sigs.S.typ -> string -> ('a, 'b) ZZ3_sigs.S.symbol
      val term :
        ('a, 'b) ZZ3_sigs.S.typ ->
        'b ZZ3_sigs.S.term -> ('a, 'b) ZZ3_sigs.S.symbol
      val trustme :
        ('a, 'b) ZZ3_sigs.S.typ -> Z3.Expr.expr -> ('a, 'b) ZZ3_sigs.S.symbol
    end
  module T :
    sig
      val symbol : ('b, 'a) ZZ3_sigs.S.symbol -> 'a ZZ3_sigs.S.term
      val simplify :
        ?params:Z3.Params.params -> 'a ZZ3_sigs.S.term -> 'a ZZ3_sigs.S.term
      val eq :
        'a ZZ3_sigs.S.term ->
        'a ZZ3_sigs.S.term -> [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val distinct :
        'a ZZ3_sigs.S.term list -> [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val ite :
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        ([< ZZ3_sigs.S.zany ] as 'a) ZZ3_sigs.S.term ->
        'a ZZ3_sigs.S.term -> 'a ZZ3_sigs.S.term
      val int : int -> [> ZZ3_sigs.S.zint ] ZZ3_sigs.S.term
      val bigint : Z.t -> [> ZZ3_sigs.S.zint ] ZZ3_sigs.S.term
      val rat : Q.t -> [> ZZ3_sigs.S.zreal ] ZZ3_sigs.S.term
      val i2q :
        [< ZZ3_sigs.S.zint ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zreal ] ZZ3_sigs.S.term
      val q2i :
        [< ZZ3_sigs.S.zreal ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zint ] ZZ3_sigs.S.term
      val true_ : [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val false_ : [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val bool : bool -> [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val and_ :
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term list ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val or_ :
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term list ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val not :
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val imply :
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val iff :
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val xor :
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val ge :
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val le :
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val gt :
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val lt :
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val neg :
        ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term -> 'a ZZ3_sigs.S.term
      val add :
        ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term list ->
        'a ZZ3_sigs.S.term
      val sub :
        ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term list ->
        'a ZZ3_sigs.S.term
      val mul :
        ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term list ->
        'a ZZ3_sigs.S.term
      val ixor :
        [< ZZ3_sigs.S.zint ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.zint ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zint ] ZZ3_sigs.S.term
      val div :
        ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term ->
        'a ZZ3_sigs.S.term -> 'a ZZ3_sigs.S.term
      val mod_ :
        [< ZZ3_sigs.S.zint ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.zint ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zint ] ZZ3_sigs.S.term
      val rem :
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.znum ] ZZ3_sigs.S.term
      val ( ! ) : ('b, 'a) ZZ3_sigs.S.symbol -> 'a ZZ3_sigs.S.term
      val ( = ) :
        'a ZZ3_sigs.S.term ->
        'a ZZ3_sigs.S.term -> [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val ( <> ) :
        'a ZZ3_sigs.S.term ->
        'a ZZ3_sigs.S.term -> [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val ( && ) :
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val ( || ) :
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val ( <=> ) :
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val ( ==> ) :
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val ( lxor ) :
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val ( < ) :
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val ( <= ) :
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val ( > ) :
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val ( >= ) :
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.znum ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zbool ] ZZ3_sigs.S.term
      val ( + ) :
        ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term ->
        'a ZZ3_sigs.S.term -> 'a ZZ3_sigs.S.term
      val ( - ) :
        ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term ->
        'a ZZ3_sigs.S.term -> 'a ZZ3_sigs.S.term
      val ( * ) :
        ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term ->
        'a ZZ3_sigs.S.term -> 'a ZZ3_sigs.S.term
      val ( / ) :
        ([< ZZ3_sigs.S.znum ] as 'a) ZZ3_sigs.S.term ->
        'a ZZ3_sigs.S.term -> 'a ZZ3_sigs.S.term
      val ( mod ) :
        [< ZZ3_sigs.S.zint ] ZZ3_sigs.S.term ->
        [< ZZ3_sigs.S.zint ] ZZ3_sigs.S.term ->
        [> ZZ3_sigs.S.zint ] ZZ3_sigs.S.term
      val with_typ : ('a, 'b) ZZ3_sigs.S.typ -> 'a -> 'b ZZ3_sigs.S.term
      val to_string : 'a ZZ3_sigs.S.term -> string
      val raw : 'a ZZ3_sigs.S.term -> Z3.Expr.expr
    end
  module Z3Array :
    sig
      val get :
        [< ('d, 'r) ZZ3_sigs.S.zarray ] ZZ3_sigs.S.term ->
        'd ZZ3_sigs.S.term -> 'r ZZ3_sigs.S.term
      val set :
        [< ('d, 'r) ZZ3_sigs.S.zarray ] ZZ3_sigs.S.term ->
        'd ZZ3_sigs.S.term ->
        'r ZZ3_sigs.S.term -> [> ('d, 'r) ZZ3_sigs.S.zarray ] ZZ3_sigs.S.term
      val make :
        ('a -> 'b, ('d, 'r) ZZ3_sigs.S.zarray) ZZ3_sigs.S.typ ->
        'r ZZ3_sigs.S.term -> [> ('d, 'r) ZZ3_sigs.S.zarray ] ZZ3_sigs.S.term
      val default :
        [< ('d, 'r) ZZ3_sigs.S.zarray ] ZZ3_sigs.S.term -> 'r ZZ3_sigs.S.term
      val of_indexed :
        typ:('a, 'r) ZZ3_sigs.S.typ ->
        default:'r ZZ3_sigs.S.term ->
        'r ZZ3_sigs.S.term array ->
        ([> ZZ3_sigs.S.zint ], 'r) ZZ3_sigs.S.zarray ZZ3_sigs.S.term
      val of_array :
        typ:('a -> 'b, ('d, 'r) ZZ3_sigs.S.zarray) ZZ3_sigs.S.typ ->
        default:'r ZZ3_sigs.S.term ->
        ('d ZZ3_sigs.S.term * 'r ZZ3_sigs.S.term) array ->
        ('d, 'r) ZZ3_sigs.S.zarray ZZ3_sigs.S.term
      val of_list :
        typ:('a -> 'b, ('d, 'r) ZZ3_sigs.S.zarray) ZZ3_sigs.S.typ ->
        default:'r ZZ3_sigs.S.term ->
        ('d ZZ3_sigs.S.term * 'r ZZ3_sigs.S.term) list ->
        ('d, 'r) ZZ3_sigs.S.zarray ZZ3_sigs.S.term
    end
  type sat =
      Unsat of Z3.Expr.expr Lazy.t
    | Sat of Z3.Model.model Lazy.t
    | Unkown of string
  module Solver :
    sig
      val make : unit -> Z3.Solver.solver
      val add :
        solver:Z3.Solver.solver -> ZZ3_sigs.S.zbool ZZ3_sigs.S.term -> unit
      val check :
        solver:Z3.Solver.solver ->
        ZZ3_sigs.S.zbool ZZ3_sigs.S.term list -> ZZ3_sigs.S.sat
    end
  module Model :
    sig
      val get_value :
        model:Z3.Model.model -> ('a, 'b) ZZ3_sigs.S.symbol -> 'a
    end
end