Module Const_eval.Make

Parameters

module Terms : Sig.TERMS

Signature

exception Empty

exception Not_a_constant

Returns the value if the term is indeed a singleton value;

• raises Empty

  if it is the empty value;

• raises Not_a_constant

  if it is not constant.

val integer : Operator.Function_symbol.integer Terms.t -> Z.t

val boolean : Operator.Function_symbol.boolean Terms.t -> bool

val binary : Operator.Function_symbol.binary Terms.t -> Z.t

val bitvector : Operator.Function_symbol.bitvector Terms.t -> Z.t

val enum : Operator.Function_symbol.enum Terms.t -> Z.t