Module `Eval`

Term evaluator

author: Christoph Sticksel

type value = | ValBool of bool | ValNum of Numeral.t | ValDec of Decimal.t | 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 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