Evaluating typed symbols in models

[sim642]

Typed.symbol returns a typed expression

smtml/src/smtml/typed.mli

Lines 41 to 43 in f50d5bf

	(** [symbol ty name] creates a symbolic constant of type [ty] with the given
	[name]. *)
	val symbol : 'a ty -> string -> 'a expr

I guess because there aren't typed symbols.
This is convenient for constructing typed expressions because it can directly then be used.

But it makes it kind of impossible to look up that symbol in a model using

smtml/src/smtml/model.mli

Lines 26 to 28 in f50d5bf

	(** [evaluate tbl sym] returns the value associated with symbol [sym] in [tbl],
	if any. *)
	val evaluate : t -> Symbol.t -> Value.t option

because the underlying Symbol.t isn't available.

I can see two ways to solve this:

1. Add typed symbols (and their unwrap). This changes the API to be more complex though.
2. Allow Expr.t evaluation in models. It's kind of what I expected from the name Model.evaluate and it's how e.g. Z3 model API works. Currently Model.evaluate is just a hashtable lookup without any actual evaluation, which is strange. But changing it also affects the API.

---

Actually, in an ideal world, I'd even hope to have something like

Model.evaluate: Model.t -> 'a Typed.expr -> 'a option

or

Model.evaluate: Model.t -> 'a Typed.symbol -> 'a option

That way I wouldn't have to match on Value.t to get the results in the expected type. Not sure how achievable such API would be though.

[redianthus]

I guess using the name to find the symbol's value in the model is not an option for you?