package cvc5

  1. Overview
  2. Docs
type term
val delete : term -> unit

Term instance destructor

val id : term -> int

Get the id of the term.

val equal : term -> term -> bool

Syntactic equality operator.

val kind : term -> Kind.t

Get the kind of the term.

val sort : term -> Sort.sort

Get the sort of the term.

val to_string : term -> string

Get the string representation of the term.

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

Create a free constant.

Parameters: - The sort of the constant

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

Create a named free constant.

Parameters: - The sort of the constant

  • The name of the constant
val mk_var : TermManager.tm -> Sort.sort -> term

Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).

Parameters: - The sort of the variable

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

Create a named bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).

Parameters: - The sort of the variable

  • The name of the variable
val mk_term : TermManager.tm -> Kind.t -> term array -> term

Create n-ary term of given kind.

Parameters: - The kind of the term

  • The children of the term
val mk_term_1 : TermManager.tm -> Kind.t -> term -> term

Create a unary term of a given kind.

Parameters: - The kind of the term

  • The child of the term
val mk_term_2 : TermManager.tm -> Kind.t -> term -> term -> term

Create a binary term of a given kind.

Parameters: - The kind of the term

  • The children of the term
val mk_term_3 : TermManager.tm -> Kind.t -> term -> term -> term -> term

Create a ternary term of a given kind.

Parameters: - The kind of the term

  • The children of the term
val mk_term_op : TermManager.tm -> Op.op -> term array -> term

Create n-ary term of a given kind from a given operator.

Parameters: - The operator

  • The children of the term
val mk_true : TermManager.tm -> term

Create a Boolean true constant.

val mk_false : TermManager.tm -> term

Create a Boolean false constant.

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

Create a Boolean constant.

Parameters: - The value of the constant

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

Create an integer constant.

Parameters: - The value of the constant

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

Create a String constant from a string which may contain SMT-LIB compatible escape sequences like \u1234 to encode unicode characters.

Parameters: - The string this constant represents

  • (optional) A boolean that determines whether the escape sequences in the string should be converted to the corresponding unicode character
val mk_real_s : TermManager.tm -> string -> term

Create a real constant from a string.

Parameters: - The string representation of the constant, may represent an integer (e.g., "123") or a real constant (e.g., "12.34" or "12/34")

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

Create a real constant from an integer.

Parameters: - The value of the constant

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

Create a real constant from a rational.

Parameters: - The value of the numerator

  • The value of the denominator
val mk_bv : TermManager.tm -> int -> int64 -> term

Create a bit-vector constant of a given size and value.

Parameters: - The bit-width of the bit-vector sort

  • The value of the constant
val mk_bv_s : TermManager.tm -> int -> string -> int -> term

Create a bit-vector constant of a given bit-width from a given string of base 2, 10, or 16.

Parameters: - The bit-width of the constant

  • The string representation of the constant
  • The base of the string representation (2 for binary, 10 for decimal, and 16 for hexadecimal)

Create a rounding mode value.

Parameters: - The floating-point rounding mode this constant represents

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

Create a floating-point value from a bit-vector given in IEEE-754 format.

Parameters: - Size of the exponent

  • Size of the significand
  • Value of the floating-point constant as a bit-vector term
val mk_fp_from_terms : TermManager.tm -> term -> term -> term -> term

Create a floating-point value from its three IEEE-754 bit-vector value components (sign bit, exponent, significand)

Parameters: - The bit-vector representing the sign bit

  • The bit-vector representing the exponent
  • The bit-vector representing the significand
val mk_fp_pos_inf : TermManager.tm -> int -> int -> term

Create a positive infinity floating-point constant (SMT-LIB: +oo).

Parameters: - Number of bits in the exponent

  • Number of bits in the significand
val mk_fp_neg_inf : TermManager.tm -> int -> int -> term

Create a negative infinity floating-point constant (SMT-LIB: -oo).

Parameters: - Number of bits in the exponent

  • Number of bits in the significand
val mk_fp_nan : TermManager.tm -> int -> int -> term

Create a not-a-number floating-point constant (SMT-LIB: NaN).

Parameters: - Number of bits in the exponent

  • Number of bits in the significand
val mk_fp_pos_zero : TermManager.tm -> int -> int -> term

Create a positive zero floating-point constant (SMT-LIB: +zero).

Parameters: - Number of bits in the exponent

  • Number of bits in the significand
val mk_fp_neg_zero : TermManager.tm -> int -> int -> term

Create a negative zero floating-point constant (SMT-LIB: -zero).

Parameters: - Number of bits in the exponent

  • Number of bits in the significand
val is_int : term -> bool

Determine if the term is an int value.

val is_real : term -> bool

Determine if the term is a real value.

val is_string : term -> bool

Determine if the term is a string value.

val is_bool : term -> bool

Determine if the term is a bool value.

val is_int32 : term -> bool

Determine if the term is a int32 value.

val is_bv : term -> bool

Determine if the term is a bit-vector value.

val is_int64 : term -> bool

Determine if the term is a int64 value.

val is_uint32 : term -> bool

Determine if the term is a uint32 value.

val is_uint64 : term -> bool

Determine if the term is a uint64 value.

val is_rm : term -> bool

Determine if the term is a floating-point rounding mode value.

val is_fp : term -> bool

Determine if a given term is a floating-point value.

val get_int : term -> int

Get the integer value.

val get_real : term -> float

Get the real value.

val get_string : term -> string

Get the string value.

val get_bool : term -> bool

Get the Boolean value.

val get_int32 : term -> int32

Get the int32 value.

val get_int64 : term -> int64

Get the int64 value.

val get_uint32 : term -> int

Get the uint32 value.

val get_uint64 : term -> int

Get the uint64 value.

val get_bv : term -> int -> string

Get the string representation of the bit-vector value.

Parameters: - Base. 2 for binary, 10 for decimal, and 16 for hexadecimal

val get_rm : term -> RoundingMode.t

Get the rounding mode value.

val get_fp : term -> int * int * term

Get the representation of a floating-point value as a tuple of its exponent width, significand width and a bit-vector value term.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct