Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package cvc5
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
val mk_op : TermManager.tm -> Kind.t -> int array -> opCreate operator of Kind:
BITVECTOR_EXTRACTBITVECTOR_REPEATBITVECTOR_ROTATE_LEFTBITVECTOR_ROTATE_RIGHTBITVECTOR_SIGN_EXTENDBITVECTOR_ZERO_EXTENDDIVISIBLEFLOATINGPOINT_TO_FP_FROM_FPFLOATINGPOINT_TO_FP_FROM_IEEE_BVFLOATINGPOINT_TO_FP_FROM_REALFLOATINGPOINT_TO_FP_FROM_SBVFLOATINGPOINT_TO_FP_FROM_UBVFLOATINGPOINT_TO_SBVFLOATINGPOINT_TO_UBVINT_TO_BITVECTORTUPLE_PROJECT
Parameters: - The kind of the operator.
- The arguments (indices) of the operator.
val to_string : op -> stringGet the string representation of the operator.
val delete : op -> unitOp instance destructor
val is_indexed : op -> boolDetermine if the operator is indexed.
val hash : op -> intHash function for Ops.
val get_num_indices : op -> intGet the number of indices of the operator.