Add a function to find unique solution for constraints

New function Type_check.solve : Env.t -> nexp -> Big_int.num option.
Takes an environment and an n-expression (nexp), and returns either
Some u, where u is a unique solution such that nexp = u, or None which
indicates that either no unique solution could be found. It is
technically possible that a unique solution could exist, but Z3 may
not find it.

Involves two calls to Z3, one of which cannot be memoised, so should
be used carefully, as over-reliance could lead to performance issues.

0 files changed, 0 insertions, 0 deletions