Module Sidekick_smt_solver.Model

SMT models.

The solver models are partially evaluated; the frontend might ask for values for terms not explicitly present in them.

type t = {
  1. eval : Sidekick_core.Term.t -> Sigs.value option;
  2. map : Sigs.value Sidekick_smt_solver__.Sigs.Term.Map.t;
}
val is_empty : t -> bool
val eval : t -> Sidekick_core.Term.t -> Sigs.value option
val pp : Sidekick_smt_solver__.Sigs.Fmt.t -> t -> unit