Module type ZZ3_sigs.S

module type S = sig .. end

Output signature of the functor.

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, [> zint ]) typ`
`\|`	`Bool : (bool, [> zbool ]) typ`
`\|`	`Real : (Q.t, [> zreal ]) typ`
`\|`	`Num : (Q.t, [> znum ]) typ`
`\|`	`Array : ('a, 'x) typ * ('b, 'y) typ -> ('a -> 'b, ('x, 'y) zarray) typ`

type 'a term = private Z3.Expr.expr

type ('a, 'b) symbol

module Symbol: sig .. end

module T: sig .. end

Term constructors.

module Z3Array: sig .. end

type sat =

module Solver: sig .. end

module Model: sig .. end