Add option to linearize constraints containing exponentials

When adding a constraint such as `x <= 2^n-1` to an environment
containing e.g. `n in {32, 64}` or similar, we can enumerate all
values of n and add `n == 32 & x <= 2^32-1 | n == 64 & x <= 2^64-1`
instead. The exponentials then get simplified away, which means that
we stay on the SMT solver's happy path.

This is enabled by the (experimental, name subject to change) flag
-smt_linearize, as this both allows some things to typecheck that
didn't before (see pow_32_64.sail in test/typecheck/pass), but also
may potentially cause some things that typecheck to no longer
typecheck for SMT solvers like z3 that have some support for reasoning
with power functions, or where we could simply treat the exponential
as a uninterpreted function.

Also make the -dsmt_verbose option print the smtlib2 files for the
solve functions in constraint.ml. We currently ignore the -smt_solver
option for these, because smtlib does not guarantee a standard format
for the output of get-model, so we always use z3 in this case.

Following the last commit where solve got renamed solve_unique, there
are now 3 functions for solving constraints:

* Constraint.solve_smt, which finds a solution if one exists

* Constraint.solve_all_smt, which returns all possible
  solutions. Currently there's no bound, so this could loop forever if
  there are infinite solutions.

* Constraint.solve_unique, which returns a unique solution if one exists

Fix a bug where $option pragmas were dropped unnecessarily.

0 files changed, 0 insertions, 0 deletions