package cvc5

  1. Overview
  2. Docs

Module Cvc5.OpSource

Sourcetype op
Sourceval mk_op : TermManager.tm -> Kind.t -> int array -> op

Create operator of Kind:

  • BITVECTOR_EXTRACT
  • BITVECTOR_REPEAT
  • BITVECTOR_ROTATE_LEFT
  • BITVECTOR_ROTATE_RIGHT
  • BITVECTOR_SIGN_EXTEND
  • BITVECTOR_ZERO_EXTEND
  • DIVISIBLE
  • FLOATINGPOINT_TO_FP_FROM_FP
  • FLOATINGPOINT_TO_FP_FROM_IEEE_BV
  • FLOATINGPOINT_TO_FP_FROM_REAL
  • FLOATINGPOINT_TO_FP_FROM_SBV
  • FLOATINGPOINT_TO_FP_FROM_UBV
  • FLOATINGPOINT_TO_SBV
  • FLOATINGPOINT_TO_UBV
  • INT_TO_BITVECTOR
  • TUPLE_PROJECT

Parameters: - The kind of the operator.

  • The arguments (indices) of the operator.
Sourceval equal : op -> op -> bool

Syntactic equality operator.

Sourceval to_string : op -> string

Get the string representation of the operator.

Sourceval delete : op -> unit

Op instance destructor

Sourceval is_indexed : op -> bool

Determine if the operator is indexed.

Sourceval kind : op -> Kind.t

Get the kind of the operator.

Sourceval hash : op -> int

Hash function for Ops.

Sourceval get_num_indices : op -> int

Get the number of indices of the operator.