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.

1 files changed, 27 insertions, 8 deletions

diff --git a/src/constraint.ml b/src/constraint.ml
index 2c5150a5..5402f6f7 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -321,12 +321,13 @@ let call_smt l vars constraints =
   Profile.finish_smt t;
   result
 
-let rec solve_unique_smt l vars constraints var =
+let solve_smt l vars constraints var =
   let smt_file, smt_var = smtlib_of_constraints ~get_model:true l vars constraints in
   let smt_var = pp_sexpr (smt_var var) in
 
-  (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" smt_file);
-     prerr_endline ("Solving for " ^ smt_var); *)
+  if !opt_smt_verbose then
+    prerr_endline (Printf.sprintf "SMTLIB2 constraints are (solve for %s): \n%s%!" smt_var smt_file)
+  else ();
 
   let rec input_all chan =
     try
@@ -355,9 +356,27 @@ let rec solve_unique_smt l vars constraints var =
   try
     let _ = Str.search_forward (Str.regexp regexp) smt_output 0 in
     let result = Big_int.of_string (Str.matched_group 1 smt_output) in
-    begin match call_smt l vars (nc_and constraints (nc_neq (nconstant result) (nvar var))) with
-    | Unsat -> Some result
-    | _ -> None
-    end
+    Some result
   with
-    Not_found -> None
+  | Not_found -> None
+
+let solve_all_smt l vars constraints var =
+  let rec aux results =
+    let constraints = List.fold_left (fun ncs r -> (nc_and ncs (nc_neq (nconstant r) (nvar var)))) constraints results in
+    match solve_smt l vars constraints var with
+    | Some result -> aux (result :: results)
+    | None ->
+       match call_smt l vars constraints with
+       | Unsat -> Some results
+       | _ -> None
+  in
+  aux []
+
+let solve_unique_smt l vars constraints var =
+  match solve_smt l vars constraints var with
+  | Some result ->
+     begin match call_smt l vars (nc_and constraints (nc_neq (nconstant result) (nvar var))) with
+     | Unsat -> Some result
+     | _ -> None
+     end
+  | None -> None