package cvc5

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

Sort instance destructor.

val equal : sort -> sort -> bool

Comparison for structural equality.

val to_string : sort -> string

Get a string representation of the sort.

val mk_bool_sort : TermManager.tm -> sort

Get the Boolean sort.

val mk_int_sort : TermManager.tm -> sort

Get the Integer sort.

val mk_real_sort : TermManager.tm -> sort

Get the Real sort.

val mk_string_sort : TermManager.tm -> sort

Get the String sort.

val mk_bv_sort : TermManager.tm -> int -> sort

Create a bit-vector sort.

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

val bv_size : sort -> int32

Get the bit-width of the bit-vector sort.

val mk_rm_sort : TermManager.tm -> sort

Get the rounding mode sort.

val mk_fp_sort : TermManager.tm -> int -> int -> sort

Create a floating-point sort.

Parameters: – The bit-width of the exponent of the floating-point sort.

  • The bit-width of the significand of the floating-point sort.
val mk_seq_sort : TermManager.tm -> sort -> sort

Create a sequence sort.

Parameters: - The sort of the sequence elements.

val mk_uninterpreted_sort : TermManager.tm -> string -> sort

Create an uninterpreted sort.

Parameters: - The name of the sort.

OCaml

Innovation. Community. Security.