sig
type t
val context : Syntax.Context.t Syntax.context
type term = (Syntax.Context.t, Syntax.typ_arith) Syntax.expr
type formula = (Syntax.Context.t, Syntax.typ_bool) Syntax.expr
val mk_symbol : ?name:string -> Syntax.typ -> Syntax.symbol
val mk_const : Syntax.symbol -> (Syntax.Context.t, 'typ) Syntax.expr
val mk_app :
Syntax.symbol ->
(Syntax.Context.t, 'b) Syntax.expr list ->
(Syntax.Context.t, 'typ) Syntax.expr
val mk_var : int -> Syntax.typ_fo -> (Syntax.Context.t, 'typ) Syntax.expr
val mk_add : Syntax.Context.term list -> Syntax.Context.term
val mk_mul : Syntax.Context.term list -> Syntax.Context.term
val mk_div :
Syntax.Context.term -> Syntax.Context.term -> Syntax.Context.term
val mk_idiv :
Syntax.Context.term -> Syntax.Context.term -> Syntax.Context.term
val mk_mod :
Syntax.Context.term -> Syntax.Context.term -> Syntax.Context.term
val mk_real : QQ.t -> Syntax.Context.term
val mk_floor : Syntax.Context.term -> Syntax.Context.term
val mk_neg : Syntax.Context.term -> Syntax.Context.term
val mk_sub :
Syntax.Context.term -> Syntax.Context.term -> Syntax.Context.term
val mk_forall :
?name:string ->
Syntax.typ_fo -> Syntax.Context.formula -> Syntax.Context.formula
val mk_exists :
?name:string ->
Syntax.typ_fo -> Syntax.Context.formula -> Syntax.Context.formula
val mk_forall_const :
Syntax.symbol -> Syntax.Context.formula -> Syntax.Context.formula
val mk_exists_const :
Syntax.symbol -> Syntax.Context.formula -> Syntax.Context.formula
val mk_and : Syntax.Context.formula list -> Syntax.Context.formula
val mk_or : Syntax.Context.formula list -> Syntax.Context.formula
val mk_not : Syntax.Context.formula -> Syntax.Context.formula
val mk_eq :
Syntax.Context.term -> Syntax.Context.term -> Syntax.Context.formula
val mk_lt :
Syntax.Context.term -> Syntax.Context.term -> Syntax.Context.formula
val mk_leq :
Syntax.Context.term -> Syntax.Context.term -> Syntax.Context.formula
val mk_true : Syntax.Context.formula
val mk_false : Syntax.Context.formula
val mk_ite :
Syntax.Context.formula ->
(Syntax.Context.t, 'a) Syntax.expr ->
(Syntax.Context.t, 'a) Syntax.expr -> (Syntax.Context.t, 'a) Syntax.expr
end