Model (docs.other.smtml.Smtml.Z3

val get_symbols : model -> Symbol.t list

get_symbols model retrieves the list of symbols in the model.

val eval : 
  ?ctx:term Symbol.Map.t ->
  ?completion:bool ->
  model ->
  term ->
  interp option

eval ?completion model t evaluates the term t in the given model. If completion is true, missing values are completed.