sig
type t
type id
type location
val const :
?loc:Ast_smtlib.Term.location -> Ast_smtlib.Term.id -> Ast_smtlib.Term.t
val int : ?loc:Ast_smtlib.Term.location -> string -> Ast_smtlib.Term.t
val real : ?loc:Ast_smtlib.Term.location -> string -> Ast_smtlib.Term.t
val hexa : ?loc:Ast_smtlib.Term.location -> string -> Ast_smtlib.Term.t
val binary : ?loc:Ast_smtlib.Term.location -> string -> Ast_smtlib.Term.t
val colon :
?loc:Ast_smtlib.Term.location ->
Ast_smtlib.Term.t -> Ast_smtlib.Term.t -> Ast_smtlib.Term.t
val apply :
?loc:Ast_smtlib.Term.location ->
Ast_smtlib.Term.t -> Ast_smtlib.Term.t list -> Ast_smtlib.Term.t
val letin :
?loc:Ast_smtlib.Term.location ->
Ast_smtlib.Term.t list -> Ast_smtlib.Term.t -> Ast_smtlib.Term.t
val forall :
?loc:Ast_smtlib.Term.location ->
Ast_smtlib.Term.t list -> Ast_smtlib.Term.t -> Ast_smtlib.Term.t
val exists :
?loc:Ast_smtlib.Term.location ->
Ast_smtlib.Term.t list -> Ast_smtlib.Term.t -> Ast_smtlib.Term.t
val sexpr :
?loc:Ast_smtlib.Term.location ->
Ast_smtlib.Term.t list -> Ast_smtlib.Term.t
val annot :
?loc:Ast_smtlib.Term.location ->
Ast_smtlib.Term.t -> Ast_smtlib.Term.t list -> Ast_smtlib.Term.t
end