module T: sig .. end
Term constructors. Direct calls to the Z3 api.
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