cvc5 1.1.3~unreleased · OCaml Package

type term

val delete : term -> unit

val id : term -> int

val equal : term -> term -> bool

val kind : term -> Kind.t

val sort : term -> Sort.sort

val to_string : term -> string

val mk_const : TermManager.tm -> Sort.sort -> term

val mk_const_s : TermManager.tm -> Sort.sort -> string -> term

val mk_var : TermManager.tm -> Sort.sort -> term

val mk_var_s : TermManager.tm -> Sort.sort -> string -> term

val mk_term : TermManager.tm -> Kind.t -> term array -> term

val mk_term_1 : TermManager.tm -> Kind.t -> term -> term

val mk_term_2 : TermManager.tm -> Kind.t -> term -> term -> term

val mk_term_3 : TermManager.tm -> Kind.t -> term -> term -> term -> term

val mk_term_op : TermManager.tm -> Op.op -> term array -> term

val mk_true : TermManager.tm -> term

val mk_false : TermManager.tm -> term

val mk_bool : TermManager.tm -> bool -> term

val mk_int : TermManager.tm -> int -> term

val mk_string : TermManager.tm -> ?useEscSequences:bool -> string -> term

val mk_real_s : TermManager.tm -> string -> term

val mk_real_i : TermManager.tm -> int64 -> term

val mk_real : TermManager.tm -> int64 -> int64 -> term

val mk_bv : TermManager.tm -> int -> int64 -> term

val mk_bv_s : TermManager.tm -> int -> string -> int -> term

val mk_rm : TermManager.tm -> RoundingMode.t -> term

val mk_fp : TermManager.tm -> int -> int -> term -> term

val mk_fp_from_terms : TermManager.tm -> term -> term -> term -> term

val mk_fp_pos_inf : TermManager.tm -> int -> int -> term

val mk_fp_neg_inf : TermManager.tm -> int -> int -> term

val mk_fp_nan : TermManager.tm -> int -> int -> term

val mk_fp_pos_zero : TermManager.tm -> int -> int -> term

val mk_fp_neg_zero : TermManager.tm -> int -> int -> term

val is_int : term -> bool

val is_real : term -> bool

val is_string : term -> bool

val is_bool : term -> bool

val is_int32 : term -> bool

val is_bv : term -> bool

val is_int64 : term -> bool

val is_uint32 : term -> bool

val is_uint64 : term -> bool

val is_rm : term -> bool

val get_int : term -> int

val get_real : term -> float

val get_string : term -> string

val get_bool : term -> bool

val get_int32 : term -> int32

val get_int64 : term -> int64

val get_uint32 : term -> int

val get_uint64 : term -> int

val get_bv : term -> int -> string

val get_rm : term -> RoundingMode.t

package cvc5