Various improvements to menhir parser, and performance improvments for Z3 calls

New option -memo_z3 memoizes calls to the Z3 solver, and saves these
results between calls to sail. This greatly increases the performance
of sail when re-checking large specifications by about an order of
magnitude. For example:

time sail -no_effects prelude.sail aarch64_no_vector.sail

real	0m4.391s
user	0m0.856s
sys	0m0.464s

After running with -memo_z3 once, running again gives:

time sail -memo_z3 -no_effects prelude.sail aarch64_no_vector.sail

real	0m0.457s
user	0m0.448s
sys	0m0.008s

Both the old and the new parser should now have better error messages
where the location of the parse error is displayed visually in the
error message and highlighted.

9 files changed, 223 insertions, 77 deletions

diff --git a/src/constraint.ml b/src/constraint.ml
index e8252f2a..37d1fae9 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -212,7 +212,44 @@ let smtlib_of_constraint constr : string =
 
 type t = nexp constraint_bool
 
-type smt_result = Unknown of t list | Unsat of t
+type smt_result = Unknown | Sat | Unsat
+
+module DigestMap = Map.Make(Digest)
+
+let known_problems = ref (DigestMap.empty)
+
+let load_digests_err () =
+  let in_chan = open_in_bin "z3_problems" in
+  let rec load () =
+    let digest = Digest.input in_chan in
+    let result = input_byte in_chan in
+    begin
+      match result with
+      | 0 -> known_problems := DigestMap.add digest Unknown !known_problems
+      | 1 -> known_problems := DigestMap.add digest Sat !known_problems
+      | 2 -> known_problems := DigestMap.add digest Unsat !known_problems
+      | _ -> assert false
+    end;
+    load ()
+  in
+  try load () with
+  | End_of_file -> close_in in_chan
+
+let load_digests () =
+  try load_digests_err () with
+  | Sys_error _ -> ()
+
+let save_digests () =
+  let out_chan = open_out_bin "z3_problems" in
+  let output digest result =
+    Digest.output out_chan digest;
+    match result with
+    | Unknown -> output_byte out_chan 0
+    | Sat -> output_byte out_chan 1
+    | Unsat -> output_byte out_chan 2
+  in
+  DigestMap.iter output !known_problems;
+  close_out out_chan
 
 let rec call_z3 constraints : smt_result =
   let problems = unbranch constraints in
@@ -235,24 +272,31 @@ let rec call_z3 constraints : smt_result =
        end
   in
 
-  begin
-    let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".sat" in
-    output_string tmp_chan z3_file;
-    close_out tmp_chan;
-    let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
-    let z3_output = List.combine problems (input_lines z3_chan (List.length problems)) in
-    let _ = Unix.close_process_in z3_chan in
-    Sys.remove input_file;
-    try
-      let (problem, _) = List.find (fun (_, result) -> result = "unsat") z3_output in
-      Unsat problem
-    with
-    | Not_found ->
-       z3_output
-       |> List.filter (fun (_, result) -> result = "unknown")
-       |> List.map fst
-       |> (fun unsolved -> Unknown unsolved)
-  end
+  let digest = Digest.string z3_file in
+  try
+    let result = DigestMap.find digest !known_problems in
+    result
+  with
+  | Not_found ->
+    begin
+      let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".sat" in
+      output_string tmp_chan z3_file;
+      close_out tmp_chan;
+      let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
+      let z3_output = List.combine problems (input_lines z3_chan (List.length problems)) in
+      let _ = Unix.close_process_in z3_chan in
+      Sys.remove input_file;
+      try
+        let (problem, _) = List.find (fun (_, result) -> result = "unsat") z3_output in
+        known_problems := DigestMap.add digest Unsat !known_problems;
+        Unsat
+      with
+      | Not_found ->
+         let unsolved = List.filter (fun (_, result) -> result = "unknown") z3_output in
+         if unsolved == []
+         then (known_problems := DigestMap.add digest Sat !known_problems; Sat)
+         else (known_problems := DigestMap.add digest Unknown !known_problems; Unknown)
+    end
 
 let string_of constr =
   constr
diff --git a/src/constraint.mli b/src/constraint.mli
index 3fb3d2f6..ad75f453 100644
--- a/src/constraint.mli
+++ b/src/constraint.mli
@@ -1,12 +1,15 @@
 type nexp
 type t
 
-type smt_result = Unknown of t list | Unsat of t
-       
+type smt_result = Unknown | Sat | Unsat
+
+val load_digests : unit -> unit
+val save_digests : unit -> unit
+
 val call_z3 : t -> smt_result
 
 val string_of : t -> string
-                                           
+
 val implies : t -> t -> t
 val conj : t -> t -> t
 val disj : t -> t -> t
diff --git a/src/initial_check.ml b/src/initial_check.ml
index b7505391..efda0da1 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -958,6 +958,8 @@ let generate_undefineds vs_ids (Defs defs) =
      gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}";
      gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}";
      gen_vs (mk_id "undefined_int") "unit -> int effect {undef}";
+     gen_vs (mk_id "undefined_nat") "unit -> nat effect {undef}";
+     gen_vs (mk_id "undefined_real") "unit -> real effect {undef}";
      gen_vs (mk_id "undefined_string") "unit -> string effect {undef}";
      gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
      (* FIXME: How to handle inc/dec order correctly? *)
diff --git a/src/parser2.mly b/src/parser2.mly
index 16e93a59..59db84a1 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -46,9 +46,9 @@ let r = fun x -> x (* Ulib.Text.of_latin1 *)
 
 open Parse_ast
 
-let loc n m = Range (m, n)
+let loc n m = Range (n, m)
 
-let mk_id i n m = Id_aux (i, loc m n)
+let mk_id i n m = Id_aux (i, loc n m)
 let mk_kid str n m = Kid_aux (Var str, loc n m)
 
 let id_of_kid = function
@@ -434,16 +434,19 @@ typ8:
   | typ8l op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | typ9 op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos }
+  | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos}
   | typ9 { $1 }
 typ8l:
   | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | typ8l op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos }
+  | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos}
   | typ9 { $1 }
 typ8r:
   | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | typ9 op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
   | TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos }
+  | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos}
   | typ9 { $1 }
 
 typ9:
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
index d9bc0c7c..bb7aa3b4 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -19,24 +19,56 @@ let doc_ord (Ord_aux(o,_)) = match o with
   | Ord_inc -> string "inc"
   | Ord_dec -> string "dec"
 
-let rec doc_nexp (Nexp_aux (n_aux, _)) =
-  match n_aux with
-  | Nexp_constant c -> string (string_of_int c)
-  | Nexp_id id -> doc_id id
-  | Nexp_var kid -> doc_kid kid
-  | _ -> string "NEXP"
+let rec doc_nexp =
+  let rec atomic_nexp (Nexp_aux (n_aux, _) as nexp) =
+    match n_aux with
+    | Nexp_constant c -> string (string_of_int c)
+    | Nexp_id id -> doc_id id
+    | Nexp_var kid -> doc_kid kid
+    | _ -> parens (nexp0 nexp)
+  and nexp0 (Nexp_aux (n_aux, _) as nexp) =
+    match n_aux with
+    | Nexp_sum (n1, Nexp_aux (Nexp_neg n2, _)) | Nexp_minus (n1, n2) ->
+       separate space [nexp0 n1; string "-"; nexp1 n2]
+    | Nexp_sum (n1, Nexp_aux (Nexp_constant c, _)) when c < 0 ->
+       separate space [nexp0 n1; string "-"; doc_int (abs c)]
+    | Nexp_sum (n1, n2) -> separate space [nexp0 n1; string "+"; nexp1 n2]
+    | _ -> nexp1 nexp
+  and nexp1 (Nexp_aux (n_aux, _) as nexp) =
+    match n_aux with
+    | Nexp_times (n1, n2) -> separate space [nexp1 n1; string "*"; nexp2 n2]
+    | _ -> nexp2 nexp
+  and nexp2 (Nexp_aux (n_aux, _) as nexp) =
+    match n_aux with
+    | Nexp_neg n -> separate space [string "-"; atomic_nexp n]
+    | Nexp_exp n -> separate space [string "2"; string "^"; atomic_nexp n]
+    | _ -> atomic_nexp nexp
+  in
+  nexp0
 
 let doc_nc =
+  let nc_op op n1 n2 = separate space [doc_nexp n1; string op; doc_nexp n2] in
   let rec atomic_nc (NC_aux (nc_aux, _) as nc) =
     match nc_aux with
     | NC_true -> string "true"
     | NC_false -> string "false"
+    | NC_equal (n1, n2) -> nc_op "=" n1 n2
+    | NC_not_equal (n1, n2) -> nc_op "!=" n1 n2
+    | NC_bounded_ge (n1, n2) -> nc_op ">=" n1 n2
+    | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2
     | NC_set (kid, ints) ->
        separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)]
     | _ -> parens (nc0 nc)
-  and nc0 (NC_aux (nc_aux, _)) = string "NC0"
+  and nc0 (NC_aux (nc_aux, _) as nc) =
+    match nc_aux with
+    | NC_or (c1, c2) -> separate space [nc0 c1; string "|"; nc1 c2]
+    | _ -> nc1 nc
+  and nc1 (NC_aux (nc_aux, _) as nc) =
+    match nc_aux with
+    | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2]
+    | _ -> atomic_nc nc
   in
-  atomic_nc
+  nc0
 
 let rec doc_typ (Typ_aux (typ_aux, _)) =
   match typ_aux with
@@ -49,8 +81,8 @@ let rec doc_typ (Typ_aux (typ_aux, _)) =
   | Typ_var kid -> doc_kid kid
   | Typ_wild -> assert false
   (* Resugar set types like {|1, 2, 3|} *)
-  | Typ_exist ([kid1], NC_aux (NC_set (kid2, ints), _), Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_var kid3, _)), _)]), _))
-         when Kid.compare kid1 kid2 == 0 && Kid.compare kid2 kid3 == 0 ->
+  | Typ_exist ([kid1], NC_aux (NC_set (kid2, ints), _), Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid3, _)), _)]), _))
+         when Kid.compare kid1 kid2 == 0 && Kid.compare kid2 kid3 == 0 && Id.compare (mk_id "atom") id == 0 ->
      enclose (string "{|") (string "|}") (separate_map (string ", ") doc_int ints)
   | Typ_exist (kids, nc, typ) ->
      braces (separate_map space doc_kid kids ^^ comma ^^ space ^^ doc_nc nc ^^ dot ^^ space ^^ doc_typ typ)
@@ -62,14 +94,42 @@ and doc_typ_arg (Typ_arg_aux (ta_aux, _)) =
   | Typ_arg_nexp nexp -> doc_nexp nexp
   | Typ_arg_order o -> doc_ord o
 
+let doc_quants quants =
+  let doc_qi_kopt (QI_aux (qi_aux, _)) =
+    match qi_aux with
+    | QI_id (KOpt_aux (KOpt_none kid, _)) -> [doc_kid kid]
+    | QI_id kopt when is_nat_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])]
+    | QI_id kopt when is_typ_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])]
+    | QI_id kopt when is_order_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])]
+    | QI_const nc -> []
+  in
+  let qi_nc (QI_aux (qi_aux, _)) =
+    match qi_aux with
+    | QI_const nc -> [nc]
+    | _ -> []
+  in
+  let kdoc = separate space (List.concat (List.map doc_qi_kopt quants)) in
+  let ncs = List.concat (List.map qi_nc quants) in
+  match ncs with
+  | [] -> kdoc
+  | [nc] -> kdoc ^^ comma ^^ space ^^ doc_nc nc
+  | nc :: ncs -> kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs)
+
 let doc_typschm (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) =
   match tq_aux with
   | TypQ_no_forall -> doc_typ typ
   | TypQ_tq [] -> doc_typ typ
-  | TypQ_tq qs -> string "QI" ^^ dot ^^ space ^^ doc_typ typ
+  | TypQ_tq qs ->
+     string "forall" ^^ space ^^ doc_quants qs ^^ dot ^//^ doc_typ typ
 
 let doc_typschm_typ (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = doc_typ typ
 
+let doc_typschm_quants (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) =
+  match tq_aux with
+  | TypQ_no_forall -> None
+  | TypQ_tq [] -> None
+  | TypQ_tq qs -> Some (doc_quants qs)
+
 let doc_lit (L_aux(l,_)) =
   utf8string (match l with
   | L_unit  -> "()"
@@ -111,26 +171,27 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
   | E_app (id, [E_aux (E_lit (L_aux (L_unit, _)), _)]) -> doc_id id ^^ string "()"
   | E_app (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps)
   | E_app_infix (x, id, y) -> doc_op (doc_id id) (doc_exp x) (doc_exp y)
-  | E_tuple exps -> assert false
-  | E_if (if_exp, then_exp, else_exp) -> assert false
-  | E_for (id, exp1, exp2, exp3, order, exp4) -> assert false
-  | E_vector exps -> assert false
-  | E_vector_access (exp1, exp2) -> assert false
+  | E_tuple exps -> parens (separate_map (comma ^^ space) doc_exp exps)
+  | E_if (if_exp, then_exp, else_exp) -> string "E_if"
+  | E_for (id, exp1, exp2, exp3, order, exp4) -> string "E_for"
+  | E_vector exps -> string "E_vector"
+  | E_vector_access (exp1, exp2) -> string "E_vector_access"
   | E_vector_subrange (exp1, exp2, exp3) -> doc_exp exp1 ^^ brackets (separate space [doc_exp exp2; string ".."; doc_exp exp3])
-  | E_vector_update (exp1, exp2, exp3) -> assert false
-  | E_vector_update_subrange (exp1, exp2, exp3, exp4) -> assert false
-  | E_list exps -> assert false
-  | E_cons (exp1, exp2) -> assert false
-  | E_record fexps -> assert false
-  | E_record_update (exp, fexps) -> assert false
-  | E_field (exp, id) -> assert false
+  | E_vector_update (exp1, exp2, exp3) -> string "E_vector_update"
+  | E_vector_update_subrange (exp1, exp2, exp3, exp4) -> string "E_vector_update_subrange"
+  | E_list exps -> string "E_list"
+  | E_cons (exp1, exp2) -> string "E_cons"
+  | E_record fexps -> string "E_record"
+  | E_record_update (exp, fexps) -> string "E_record_update"
+  | E_field (exp, id) -> string "E_field"
   | E_case (exp, pexps) ->
      separate space [string "match"; doc_exp exp; doc_pexps pexps]
   | E_let (LB_aux (LB_val (pat, binding), _), exp) ->
      separate space [string "let"; doc_pat pat; equals; doc_exp binding; string "in"; doc_exp exp]
   | E_assign (lexp, exp) ->
      separate space [doc_lexp lexp; equals; doc_exp exp]
-  | E_sizeof nexp -> assert false
+  | E_sizeof (Nexp_aux (Nexp_var kid, _)) -> doc_kid kid
+  | E_sizeof nexp -> string "sizeof" ^^ parens (doc_nexp nexp)
   | E_constraint nc -> string "constraint" ^^ parens (doc_nc nc)
   | E_exit exp -> assert false
   (* Resugar an assert with an empty message *)
@@ -138,7 +199,7 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
   | E_assert (exp1, exp2) -> string "assert" ^^ parens (doc_exp exp1 ^^ comma ^^ space ^^ doc_exp exp2)
   | E_throw exp -> assert false
   | E_try (exp, pexps) -> assert false
-  | E_return exp -> assert false
+  | E_return exp -> string "return" ^^ parens (doc_exp exp)
 and doc_block = function
   | [] -> assert false
   | [E_aux (E_let (LB_aux (LB_val (pat, binding), _), E_aux (E_block exps, _)), _)] ->
@@ -187,13 +248,29 @@ let doc_dec (DEC_aux (reg,_)) =
 
 let doc_typdef (TD_aux(td,_)) = match td with
   | TD_abbrev(id, _, typschm) ->
-      doc_op equals (concat [string "type"; space; doc_id id]) (doc_typschm_typ typschm)
+     begin
+       match doc_typschm_quants typschm with
+       | Some qdoc ->
+          doc_op equals (concat [string "type"; space; doc_id id; space; qdoc]) (doc_typschm_typ typschm)
+       | None ->
+          doc_op equals (concat [string "type"; space; doc_id id]) (doc_typschm_typ typschm)
+     end
   | _ -> string "TYPEDEF"
 
-let doc_spec (VS_aux(v,_)) = match v with
-  | VS_val_spec(ts,id,_,_) ->
-     separate space [string "val"; doc_id id; colon; doc_typschm ts]
-  | _ -> string "VS?"
+let doc_spec (VS_aux(v,_)) =
+  let doc_extern = function
+    | Some s -> equals ^^ space ^^ utf8string ("\"" ^ String.escaped s ^ "\"") ^^ space
+    | None -> empty
+  in
+  match v with
+  | VS_val_spec(ts,id,ext,is_cast) ->
+     string "val" ^^ space
+     ^^ (if is_cast then (string "cast" ^^ space) else empty)
+     ^^ doc_id id ^^ space
+     ^^ doc_extern ext
+     ^^ colon ^^ space
+     ^^ doc_typschm ts
+
 (*
   | VS_cast_spec (ts, id) ->
      separate space [string "val"; string "cast"; doc_typscm ts; doc_id id]
@@ -212,7 +289,7 @@ let rec doc_def def = group (match def with
   | DEF_reg_dec dec -> doc_dec dec
   | DEF_scattered sdef -> string "TOPLEVEL"
   | DEF_overload (id, ids) ->
-      string "TOPLEVEL"
+      separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (semi ^^ break 1) doc_id ids) rbrace]
   | DEF_comm (DC_comm s) -> string "TOPLEVEL"
   | DEF_comm (DC_comm_struct d) -> string "TOPLEVEL"
   ) ^^ hardline
diff --git a/src/process_file.ml b/src/process_file.ml
index 0f789c9d..1749bc03 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -82,13 +82,16 @@ let parse_file (f : string) : Parse_ast.defs =
       in
       close_in in_chan; ast
     with
-      | Parsing.Parse_error ->
-          let pos = Lexing.lexeme_start_p lexbuf in
-          raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "main")))
-      | Parse_ast.Parse_error_locn(l,m) ->
-          raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
-      | Lexer.LexError(s,p) ->
-          raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s)))
+    | Parser2.Error ->
+       let pos = Lexing.lexeme_start_p lexbuf in
+       raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "no information")))
+    | Parsing.Parse_error ->
+       let pos = Lexing.lexeme_start_p lexbuf in
+       raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "main")))
+    | Parse_ast.Parse_error_locn(l,m) ->
+       raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
+    | Lexer.LexError(s,p) ->
+       raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s)))
 
 let convert_ast (order : Ast.order) (defs : Parse_ast.defs) : unit Ast.defs = Initial_check.process_ast order defs
 
@@ -237,7 +240,11 @@ let rewrite_step defs rewriter =
     | _ -> () in
   defs
 
-let rewrite rewriters defs = List.fold_left rewrite_step defs rewriters
+let rewrite rewriters defs =
+  try List.fold_left rewrite_step defs rewriters with
+  | Type_check.Type_error (_, err) ->
+     prerr_endline (Type_check.string_of_type_error err);
+     exit 1
 
 let rewrite_ast = rewrite [Rewriter.rewrite_defs]
 let rewrite_ast_lem = rewrite Rewriter.rewrite_defs_lem
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
index e552dca4..a47ee8ae 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting_basic.ml
@@ -87,14 +87,6 @@
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
-let format_pos ff p =
-  let open Lexing in
-  begin
-    Format.fprintf ff "file \"%s\", line %d, character %d:\n"
-                   p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol);
-    Format.pp_print_flush ff ()
-  end
-
 let rec skip_lines in_chan = function
   | n when n <= 0 -> ()
   | n -> input_line in_chan; skip_lines in_chan (n - 1)
@@ -126,6 +118,16 @@ let print_code1 ff fname lnum1 cnum1 cnum2 =
     end
   with _ -> ()
 
+let format_pos ff p =
+  let open Lexing in
+  begin
+    Format.fprintf ff "file \"%s\", line %d, character %d:\n\n"
+                   p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol);
+    print_code1 ff p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) (p.pos_cnum - p.pos_bol + 1);
+    Format.fprintf ff "\n\n";
+    Format.pp_print_flush ff ()
+  end
+
 let print_code2 ff fname lnum1 cnum1 lnum2 cnum2 =
   try
     let in_chan = open_in fname in
diff --git a/src/sail.ml b/src/sail.ml
index 8083b26c..e5a5071f 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -51,6 +51,7 @@ let opt_print_lem_ast = ref false
 let opt_print_lem = ref false
 let opt_print_ocaml = ref false
 let opt_convert = ref false
+let opt_memo_z3 = ref false
 let opt_libs_lem = ref ([]:string list)
 let opt_libs_ocaml = ref ([]:string list)
 let opt_file_arguments = ref ([]:string list)
@@ -104,6 +105,9 @@ let options = Arg.align ([
   ( "-convert",
     Arg.Set opt_convert,
     " Convert sail to new syntax");
+  ( "-memo_z3",
+    Arg.Set opt_memo_z3,
+    " Memoize calls to z3");
   ( "-ddump_tc_ast",
     Arg.Set opt_ddump_tc_ast,
     " (debug) dump the typechecked ast to stdout");
@@ -143,6 +147,7 @@ let main() =
   if !(opt_print_version)
   then Printf.printf "Sail private release \n"
   else
+    if !opt_memo_z3 then Constraint.load_digests () else ();
 
     let parsed = (List.map (fun f -> (f,(parse_file f)))  !opt_file_arguments) in
     let ast =
@@ -166,6 +171,9 @@ let main() =
     let out_name = match !opt_file_out with
       | None -> fst (List.hd parsed)
       | Some f -> f ^ ".sail" in
+
+    if !opt_memo_z3 then Constraint.save_digests () else ();
+
     (*let _ = Printf.eprintf "Type checked, next to pretty print" in*)
     begin
       (if !(opt_print_verbose)
diff --git a/src/type_check.ml b/src/type_check.ml
index 76bc0d2a..06083211 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1105,9 +1105,9 @@ let prove_z3 env nc =
   in
   let constr = Constraint.conj (nc_constraints env var_of (Env.get_constraints env)) (Constraint.negate (nc_constraint env var_of nc)) in
   match Constraint.call_z3 constr with
-  | Constraint.Unsat _ -> typ_debug "unsat"; true
-  | Constraint.Unknown [] -> typ_debug "sat"; false
-  | Constraint.Unknown _ -> typ_debug "unknown"; false
+  | Constraint.Unsat -> typ_debug "unsat"; true
+  | Constraint.Sat -> typ_debug "sat"; false
+  | Constraint.Unknown -> typ_debug "unknown"; false
 
 let prove env (NC_aux (nc_aux, _) as nc) =
   let compare_const f (Nexp_aux (n1, _)) (Nexp_aux (n2, _)) =
@@ -1171,9 +1171,9 @@ let rec subtyp_tnf env tnf1 tnf2 =
        let (prop1, prop2) = props_subst kid1 (Nexp_var kid3) prop1, props_subst kid2 (Nexp_var kid3) prop2 in
        let constr = Constraint.conj (nc_constraints env var_of (Env.get_constraints env)) (Constraint.conj (pos_props prop1) (neg_props prop2)) in
        match Constraint.call_z3 constr with
-       | Constraint.Unsat _ -> typ_debug "unsat"; true
-       | Constraint.Unknown [] -> typ_debug "sat"; false
-       | Constraint.Unknown _ -> typ_debug "unknown"; false
+       | Constraint.Unsat -> typ_debug "unsat"; true
+       | Constraint.Sat -> typ_debug "sat"; false
+       | Constraint.Unknown -> typ_debug "unknown"; false
      end
   | _, _ -> false