cvc5 1.2.0 (latest) · OCaml Package

type t =

| Null_term
| Uninterpreted_sort_value
| Equal
| Distinct
| Constant
| Variable
| Skolem
| Sexpr
| Lambda
| Witness
| Const_boolean
| Not
| And
| Implies
| Or
| Xor
| Ite
| Apply_uf
| Cardinality_constraint
| Ho_apply
| Add
| Mult
| Iand
| Pow2
| Sub
| Neg
| Division
| Division_total
| Ints_division
| Ints_division_total
| Ints_modulus
| Ints_modulus_total
| Abs
| Pow
| Exponential
| Sine
| Cosine
| Tangent
| Cosecant
| Secant
| Cotangent
| Arcsine
| Arccosine
| Arctangent
| Arccosecant
| Arcsecant
| Arccotangent
| Sqrt
| Divisible
| Const_rational
| Const_integer
| Lt
| Leq
| Gt
| Geq
| Is_integer
| To_integer
| To_real
| Pi
| Const_bitvector
| Bitvector_concat
| Bitvector_and
| Bitvector_or
| Bitvector_xor
| Bitvector_not
| Bitvector_nand
| Bitvector_nor
| Bitvector_xnor
| Bitvector_comp
| Bitvector_mult
| Bitvector_add
| Bitvector_sub
| Bitvector_neg
| Bitvector_udiv
| Bitvector_urem
| Bitvector_sdiv
| Bitvector_srem
| Bitvector_smod
| Bitvector_shl
| Bitvector_lshr
| Bitvector_ashr
| Bitvector_ult
| Bitvector_ule
| Bitvector_ugt
| Bitvector_uge
| Bitvector_slt
| Bitvector_sle
| Bitvector_sgt
| Bitvector_sge
| Bitvector_ultbv
| Bitvector_sltbv
| Bitvector_ite
| Bitvector_redor
| Bitvector_redand
| Bitvector_nego
| Bitvector_uaddo
| Bitvector_saddo
| Bitvector_umulo
| Bitvector_smulo
| Bitvector_usubo
| Bitvector_ssubo
| Bitvector_sdivo
| Bitvector_extract
| Bitvector_repeat
| Bitvector_zero_extend
| Bitvector_sign_extend
| Bitvector_rotate_left
| Bitvector_rotate_right
| Int_to_bitvector
| Bitvector_to_nat
| Bitvector_from_bools
| Bitvector_bit
| Const_finite_field
| Finite_field_neg
| Finite_field_add
| Finite_field_bitsum
| Finite_field_mult
| Const_floatingpoint
| Const_roundingmode
| Floatingpoint_fp
| Floatingpoint_eq
| Floatingpoint_abs
| Floatingpoint_neg
| Floatingpoint_add
| Floatingpoint_sub
| Floatingpoint_mult
| Floatingpoint_div
| Floatingpoint_fma
| Floatingpoint_sqrt
| Floatingpoint_rem
| Floatingpoint_rti
| Floatingpoint_min
| Floatingpoint_max
| Floatingpoint_leq
| Floatingpoint_lt
| Floatingpoint_geq
| Floatingpoint_gt
| Floatingpoint_is_normal
| Floatingpoint_is_subnormal
| Floatingpoint_is_zero
| Floatingpoint_is_inf
| Floatingpoint_is_nan
| Floatingpoint_is_neg
| Floatingpoint_is_pos
| Floatingpoint_to_fp_from_ieee_bv
| Floatingpoint_to_fp_from_fp
| Floatingpoint_to_fp_from_real
| Floatingpoint_to_fp_from_sbv
| Floatingpoint_to_fp_from_ubv
| Floatingpoint_to_ubv
| Floatingpoint_to_sbv
| Floatingpoint_to_real
| Select
| Store
| Const_array
| Eq_range
| Apply_constructor
| Apply_selector
| Apply_tester
| Apply_updater
| Match
| Match_case
| Match_bind_case
| Tuple_project
| Nullable_lift
| Sep_nil
| Sep_emp
| Sep_pto
| Sep_star
| Sep_wand
| Set_empty
| Set_union
| Set_inter
| Set_minus
| Set_subset
| Set_member
| Set_singleton
| Set_insert
| Set_card
| Set_complement
| Set_universe
| Set_comprehension
| Set_choose
| Set_is_empty
| Set_is_singleton
| Set_map
| Set_filter
| Set_fold
| Relation_join
| Relation_table_join
| Relation_product
| Relation_transpose
| Relation_tclosure
| Relation_join_image
| Relation_iden
| Relation_group
| Relation_aggregate
| Relation_project
| Bag_empty
| Bag_union_max
| Bag_union_disjoint
| Bag_inter_min
| Bag_difference_subtract
| Bag_difference_remove
| Bag_subbag
| Bag_count
| Bag_member
| Bag_setof
| Bag_make
| Bag_card
| Bag_choose
| Bag_map
| Bag_filter
| Bag_fold
| Bag_partition
| Table_product
| Table_project
| Table_aggregate
| Table_join
| Table_group
| String_concat
| String_in_regexp
| String_length
| String_substr
| String_update
| String_charat
| String_contains
| String_indexof
| String_indexof_re
| String_replace
| String_replace_all
| String_replace_re
| String_replace_re_all
| String_to_lower
| String_to_upper
| String_rev
| String_to_code
| String_from_code
| String_lt
| String_leq
| String_prefix
| String_suffix
| String_is_digit
| String_from_int
| String_to_int
| Const_string
| String_to_regexp
| Regexp_concat
| Regexp_union
| Regexp_inter
| Regexp_diff
| Regexp_star
| Regexp_plus
| Regexp_opt
| Regexp_range
| Regexp_repeat
| Regexp_loop
| Regexp_none
| Regexp_all
| Regexp_allchar
| Regexp_complement
| Seq_concat
| Seq_length
| Seq_extract
| Seq_update
| Seq_at
| Seq_contains
| Seq_indexof
| Seq_replace
| Seq_replace_all
| Seq_rev
| Seq_prefix
| Seq_suffix
| Const_sequence
| Seq_unit
| Seq_nth
| Forall
| Exists
| Variable_list
| Inst_pattern
| Inst_no_pattern
| Inst_pool
| Inst_add_to_pool
| Skolem_add_to_pool
| Inst_attribute
| Inst_pattern_list

val to_string : t -> string

val to_cpp : t -> int

val of_cpp : int -> t

package cvc5