Module Eval

Term evaluator

type value =
  1. | ValBool of bool
  2. | ValNum of Numeral.t
  3. | ValDec of Decimal.t
  4. | ValUBV of Bitvector.t
  5. | ValTerm of Term.t

Type of value of a term

val pp_print_value : Stdlib.Format.formatter -> value -> unit
val bool_of_value : value -> bool

Cast a value to a Boolean, raise Invalid_argument if value is not a Boolean

val num_of_value : value -> Numeral.t

Cast a value to an integer, raise Invalid_argument if value is not an integer

val dec_of_value : value -> Decimal.t

Cast a value to a float, raise Invalid_argument if value is not a float

val ubv_of_value : value -> Bitvector.t

Cast a value to an unsigned bit-vector, raise Invalid_argument if value is not an unsigned bit-vector

val term_of_value : value -> Term.t

Cast a value to a term, raise Invalid_argument if value is unknown

val value_is_unknown : value -> bool

Check if the value is unknown

val eval_term : (UfSymbol.t * (Var.t list * Term.t)) list -> Model.t -> Term.t -> value

Evaluate a term to a value, given an assignment to all free variables