diff --git a/src/ocaml-output/FStar_SMTEncoding_Z3.ml b/src/ocaml-output/FStar_SMTEncoding_Z3.ml index 8719ac2005d..0290c9a710b 100644 --- a/src/ocaml-output/FStar_SMTEncoding_Z3.ml +++ b/src/ocaml-output/FStar_SMTEncoding_Z3.ml @@ -77,23 +77,6 @@ let (check_z3version : unit -> unit) = FStar_Errors.log_issue FStar_Range.dummyRange (e, msg1))) else () -let (ini_params : unit -> Prims.string Prims.list) = - fun uu____257 -> - check_z3version (); - (let uu____259 = - let uu____263 = - let uu____267 = - let uu____271 = - let uu____273 = - let uu____275 = FStar_Options.z3_seed () in - FStar_Util.string_of_int uu____275 in - FStar_Util.format1 "smt.random_seed=%s" uu____273 in - [uu____271] in - "-in" :: uu____267 in - "-smt2" :: uu____263 in - let uu____284 = FStar_Options.z3_cliopt () in - FStar_List.append uu____259 uu____284) - type label = Prims.string type unsat_core = Prims.string Prims.list FStar_Pervasives_Native.option type z3status = @@ -107,13 +90,13 @@ type z3status = | KILLED let (uu___is_UNSAT : z3status -> Prims.bool) = fun projectee -> - match projectee with | UNSAT _0 -> true | uu____347 -> false + match projectee with | UNSAT _0 -> true | uu____307 -> false let (__proj__UNSAT__item___0 : z3status -> unsat_core) = fun projectee -> match projectee with | UNSAT _0 -> _0 let (uu___is_SAT : z3status -> Prims.bool) = fun projectee -> - match projectee with | SAT _0 -> true | uu____373 -> false + match projectee with | SAT _0 -> true | uu____333 -> false let (__proj__SAT__item___0 : z3status -> @@ -122,7 +105,7 @@ let (__proj__SAT__item___0 : = fun projectee -> match projectee with | SAT _0 -> _0 let (uu___is_UNKNOWN : z3status -> Prims.bool) = fun projectee -> - match projectee with | UNKNOWN _0 -> true | uu____420 -> false + match projectee with | UNKNOWN _0 -> true | uu____380 -> false let (__proj__UNKNOWN__item___0 : z3status -> @@ -131,7 +114,7 @@ let (__proj__UNKNOWN__item___0 : = fun projectee -> match projectee with | UNKNOWN _0 -> _0 let (uu___is_TIMEOUT : z3status -> Prims.bool) = fun projectee -> - match projectee with | TIMEOUT _0 -> true | uu____467 -> false + match projectee with | TIMEOUT _0 -> true | uu____427 -> false let (__proj__TIMEOUT__item___0 : z3status -> @@ -140,16 +123,16 @@ let (__proj__TIMEOUT__item___0 : = fun projectee -> match projectee with | TIMEOUT _0 -> _0 let (uu___is_KILLED : z3status -> Prims.bool) = fun projectee -> - match projectee with | KILLED -> true | uu____506 -> false + match projectee with | KILLED -> true | uu____466 -> false type z3statistics = Prims.string FStar_Util.smap let (status_tag : z3status -> Prims.string) = - fun uu___0_517 -> - match uu___0_517 with - | SAT uu____519 -> "sat" - | UNSAT uu____528 -> "unsat" - | UNKNOWN uu____530 -> "unknown" - | TIMEOUT uu____539 -> "timeout" + fun uu___0_477 -> + match uu___0_477 with + | SAT uu____479 -> "sat" + | UNSAT uu____488 -> "unsat" + | UNKNOWN uu____490 -> "unknown" + | TIMEOUT uu____499 -> "timeout" | KILLED -> "killed" let (status_string_and_errors : @@ -157,72 +140,34 @@ let (status_string_and_errors : fun s -> match s with | KILLED -> ((status_tag s), []) - | UNSAT uu____566 -> ((status_tag s), []) + | UNSAT uu____526 -> ((status_tag s), []) | SAT (errs,msg) -> - let uu____576 = + let uu____536 = FStar_Util.format2 "%s%s" (status_tag s) (match msg with | FStar_Pervasives_Native.None -> "" | FStar_Pervasives_Native.Some msg1 -> Prims.op_Hat " because " msg1) in - (uu____576, errs) + (uu____536, errs) | UNKNOWN (errs,msg) -> - let uu____595 = + let uu____555 = FStar_Util.format2 "%s%s" (status_tag s) (match msg with | FStar_Pervasives_Native.None -> "" | FStar_Pervasives_Native.Some msg1 -> Prims.op_Hat " because " msg1) in - (uu____595, errs) + (uu____555, errs) | TIMEOUT (errs,msg) -> - let uu____614 = + let uu____574 = FStar_Util.format2 "%s%s" (status_tag s) (match msg with | FStar_Pervasives_Native.None -> "" | FStar_Pervasives_Native.Some msg1 -> Prims.op_Hat " because " msg1) in - (uu____614, errs) - -let (tid : unit -> Prims.string) = - fun uu____631 -> - let uu____632 = FStar_Util.current_tid () in - FStar_All.pipe_right uu____632 FStar_Util.string_of_int - -let (new_z3proc : Prims.string -> FStar_Util.proc) = - fun id1 -> - let uu____644 = FStar_Options.z3_exe () in - let uu____646 = ini_params () in - FStar_Util.start_process id1 uu____644 uu____646 (fun s -> s = "Done!") - -let (new_z3proc_with_id : unit -> FStar_Util.proc) = - let ctr = FStar_Util.mk_ref (~- (Prims.parse_int "1")) in - fun uu____666 -> - let uu____667 = - let uu____669 = - FStar_Util.incr ctr; - (let uu____672 = FStar_ST.op_Bang ctr in - FStar_All.pipe_right uu____672 FStar_Util.string_of_int) - in - FStar_Util.format1 "bg-%s" uu____669 in - new_z3proc uu____667 - -type bgproc = - { - ask: Prims.string -> Prims.string ; - refresh: unit -> unit ; - restart: unit -> unit } -let (__proj__Mkbgproc__item__ask : bgproc -> Prims.string -> Prims.string) = - fun projectee -> match projectee with | { ask; refresh; restart;_} -> ask -let (__proj__Mkbgproc__item__refresh : bgproc -> unit -> unit) = - fun projectee -> - match projectee with | { ask; refresh; restart;_} -> refresh - -let (__proj__Mkbgproc__item__restart : bgproc -> unit -> unit) = - fun projectee -> - match projectee with | { ask; refresh; restart;_} -> restart + (uu____574, errs) type query_log = { @@ -268,38 +213,38 @@ let (query_logging : query_log) = FStar_ST.op_Colon_Equals current_module_name (FStar_Pervasives_Native.Some n1) in - let get_module_name uu____1144 = - let uu____1145 = FStar_ST.op_Bang current_module_name in - match uu____1145 with + let get_module_name uu____914 = + let uu____915 = FStar_ST.op_Bang current_module_name in + match uu____915 with | FStar_Pervasives_Native.None -> failwith "Module name not set" | FStar_Pervasives_Native.Some n1 -> n1 in - let next_file_name uu____1187 = + let next_file_name uu____957 = let n1 = get_module_name () in let file_name = - let uu____1192 = - let uu____1201 = FStar_ST.op_Bang used_file_names in + let uu____962 = + let uu____971 = FStar_ST.op_Bang used_file_names in FStar_List.tryFind - (fun uu____1254 -> - match uu____1254 with | (m,uu____1263) -> n1 = m) uu____1201 + (fun uu____1024 -> + match uu____1024 with | (m,uu____1033) -> n1 = m) uu____971 in - match uu____1192 with + match uu____962 with | FStar_Pervasives_Native.None -> - ((let uu____1277 = - let uu____1286 = FStar_ST.op_Bang used_file_names in - (n1, (Prims.parse_int "0")) :: uu____1286 in - FStar_ST.op_Colon_Equals used_file_names uu____1277); + ((let uu____1047 = + let uu____1056 = FStar_ST.op_Bang used_file_names in + (n1, (Prims.parse_int "0")) :: uu____1056 in + FStar_ST.op_Colon_Equals used_file_names uu____1047); n1) - | FStar_Pervasives_Native.Some (uu____1374,k) -> - ((let uu____1387 = - let uu____1396 = FStar_ST.op_Bang used_file_names in - (n1, (k + (Prims.parse_int "1"))) :: uu____1396 in - FStar_ST.op_Colon_Equals used_file_names uu____1387); - (let uu____1484 = + | FStar_Pervasives_Native.Some (uu____1144,k) -> + ((let uu____1157 = + let uu____1166 = FStar_ST.op_Bang used_file_names in + (n1, (k + (Prims.parse_int "1"))) :: uu____1166 in + FStar_ST.op_Colon_Equals used_file_names uu____1157); + (let uu____1254 = FStar_Util.string_of_int (k + (Prims.parse_int "1")) in - FStar_Util.format2 "%s-%s" n1 uu____1484)) + FStar_Util.format2 "%s-%s" n1 uu____1254)) in FStar_Util.format1 "queries-%s.smt2" file_name in - let new_log_file uu____1499 = + let new_log_file uu____1269 = let file_name = next_file_name () in FStar_ST.op_Colon_Equals current_file_name (FStar_Pervasives_Native.Some file_name); @@ -308,79 +253,171 @@ let (query_logging : query_log) = (FStar_Pervasives_Native.Some (fh, file_name)); (fh, file_name)) in - let get_log_file uu____1581 = - let uu____1582 = FStar_ST.op_Bang log_file_opt in - match uu____1582 with + let get_log_file uu____1351 = + let uu____1352 = FStar_ST.op_Bang log_file_opt in + match uu____1352 with | FStar_Pervasives_Native.None -> new_log_file () | FStar_Pervasives_Native.Some fh -> fh in let append_to_log str = - let uu____1653 = get_log_file () in - match uu____1653 with | (f,nm) -> (FStar_Util.append_to_file f str; nm) + let uu____1423 = get_log_file () in + match uu____1423 with | (f,nm) -> (FStar_Util.append_to_file f str; nm) in let write_to_new_log str = let file_name = next_file_name () in FStar_Util.write_file file_name str; file_name in let write_to_log fresh str = - let uu____1693 = + let uu____1463 = fresh || - (let uu____1696 = FStar_Options.n_cores () in - uu____1696 > (Prims.parse_int "1")) + (let uu____1466 = FStar_Options.n_cores () in + uu____1466 > (Prims.parse_int "1")) in - if uu____1693 then write_to_new_log str else append_to_log str in - let close_log uu____1708 = - let uu____1709 = FStar_ST.op_Bang log_file_opt in - match uu____1709 with + if uu____1463 then write_to_new_log str else append_to_log str in + let close_log uu____1478 = + let uu____1479 = FStar_ST.op_Bang log_file_opt in + match uu____1479 with | FStar_Pervasives_Native.None -> () - | FStar_Pervasives_Native.Some (fh,uu____1756) -> + | FStar_Pervasives_Native.Some (fh,uu____1526) -> (FStar_Util.close_file fh; FStar_ST.op_Colon_Equals log_file_opt FStar_Pervasives_Native.None) in - let log_file_name uu____1809 = - let uu____1810 = FStar_ST.op_Bang current_file_name in - match uu____1810 with + let log_file_name uu____1579 = + let uu____1580 = FStar_ST.op_Bang current_file_name in + match uu____1580 with | FStar_Pervasives_Native.None -> failwith "no log file" | FStar_Pervasives_Native.Some n1 -> n1 in { get_module_name; set_module_name; write_to_log; close_log } +let (z3_cmd_and_args : unit -> (Prims.string * Prims.string Prims.list)) = + fun uu____1629 -> + let cmd = FStar_Options.z3_exe () in + let cmd_args = + let uu____1636 = + let uu____1640 = + let uu____1644 = + let uu____1648 = + let uu____1650 = + let uu____1652 = FStar_Options.z3_seed () in + FStar_Util.string_of_int uu____1652 in + FStar_Util.format1 "smt.random_seed=%s" uu____1650 in + [uu____1648] in + "-in" :: uu____1644 in + "-smt2" :: uu____1640 in + let uu____1661 = FStar_Options.z3_cliopt () in + FStar_List.append uu____1636 uu____1661 in + (cmd, cmd_args) + +let (new_z3proc : + Prims.string -> (Prims.string * Prims.string Prims.list) -> FStar_Util.proc) + = + fun id1 -> + fun cmd_and_args -> + check_z3version (); + FStar_Util.start_process id1 (FStar_Pervasives_Native.fst cmd_and_args) + (FStar_Pervasives_Native.snd cmd_and_args) (fun s -> s = "Done!") + +let (new_z3proc_with_id : + (Prims.string * Prims.string Prims.list) -> FStar_Util.proc) = + let ctr = FStar_Util.mk_ref (~- (Prims.parse_int "1")) in + fun cmd_and_args -> + let uu____1741 = + let uu____1743 = + FStar_Util.incr ctr; + (let uu____1746 = FStar_ST.op_Bang ctr in + FStar_All.pipe_right uu____1746 FStar_Util.string_of_int) + in + FStar_Util.format1 "bg-%s" uu____1743 in + new_z3proc uu____1741 cmd_and_args + +type bgproc = + { + ask: Prims.string -> Prims.string ; + refresh: unit -> unit ; + restart: unit -> unit } +let (__proj__Mkbgproc__item__ask : bgproc -> Prims.string -> Prims.string) = + fun projectee -> match projectee with | { ask; refresh; restart;_} -> ask +let (__proj__Mkbgproc__item__refresh : bgproc -> unit -> unit) = + fun projectee -> + match projectee with | { ask; refresh; restart;_} -> refresh + +let (__proj__Mkbgproc__item__restart : bgproc -> unit -> unit) = + fun projectee -> + match projectee with | { ask; refresh; restart;_} -> restart + +let (cmd_and_args_to_string : + (Prims.string * Prims.string Prims.list) -> Prims.string) = + fun cmd_and_args -> + FStar_String.concat "" + ["cmd="; + FStar_Pervasives_Native.fst cmd_and_args; + " args=["; + FStar_String.concat ", " (FStar_Pervasives_Native.snd cmd_and_args); + "]"] + let (bg_z3_proc : bgproc FStar_ST.ref) = let the_z3proc = FStar_Util.mk_ref FStar_Pervasives_Native.None in - let z3proc uu____1861 = - (let uu____1863 = - let uu____1865 = FStar_ST.op_Bang the_z3proc in - uu____1865 = FStar_Pervasives_Native.None in - if uu____1863 - then - let uu____1894 = - let uu____1897 = new_z3proc_with_id () in - FStar_Pervasives_Native.Some uu____1897 in - FStar_ST.op_Colon_Equals the_z3proc uu____1894 + let the_z3proc_params = + FStar_Util.mk_ref (FStar_Pervasives_Native.Some ("", [""])) in + let the_z3proc_ask_count = FStar_Util.mk_ref (Prims.parse_int "0") in + let make_new_z3_proc cmd_and_args = + (let uu____2009 = + let uu____2012 = new_z3proc_with_id cmd_and_args in + FStar_Pervasives_Native.Some uu____2012 in + FStar_ST.op_Colon_Equals the_z3proc uu____2009); + FStar_ST.op_Colon_Equals the_z3proc_params + (FStar_Pervasives_Native.Some cmd_and_args); + FStar_ST.op_Colon_Equals the_z3proc_ask_count (Prims.parse_int "0") in + let z3proc uu____2111 = + (let uu____2113 = + let uu____2115 = FStar_ST.op_Bang the_z3proc in + uu____2115 = FStar_Pervasives_Native.None in + if uu____2113 + then let uu____2144 = z3_cmd_and_args () in make_new_z3_proc uu____2144 else ()); - (let uu____1923 = FStar_ST.op_Bang the_z3proc in - FStar_Util.must uu____1923) + (let uu____2155 = FStar_ST.op_Bang the_z3proc in + FStar_Util.must uu____2155) in - let x = [] in + let next_params = z3_cmd_and_args () in let ask input = - let kill_handler uu____1967 = "\nkilled\n" in - let uu____1969 = z3proc () in - FStar_Util.ask_process uu____1969 input kill_handler in - let refresh uu____1975 = - (let uu____1977 = FStar_Options.debug_any () in - if uu____1977 - then FStar_Errors.diag FStar_Range.dummyRange "Restarting SMT solver..." + FStar_Util.incr the_z3proc_ask_count; + (let kill_handler uu____2206 = "\nkilled\n" in + let uu____2208 = z3proc () in + FStar_Util.ask_process uu____2208 input kill_handler) + in + let refresh uu____2214 = + let old_params = + let uu____2224 = FStar_ST.op_Bang the_z3proc_params in + FStar_Util.must uu____2224 in + (let uu____2283 = + ((FStar_Options.log_queries ()) || + (let uu____2286 = FStar_ST.op_Bang the_z3proc_ask_count in + uu____2286 > (Prims.parse_int "0"))) + || (Prims.op_Negation (old_params = next_params)) + in + if uu____2283 + then + ((let uu____2320 = + (FStar_Options.query_stats ()) && + (let uu____2323 = + let uu____2325 = FStar_ST.op_Bang the_z3proc in + uu____2325 = FStar_Pervasives_Native.None in + Prims.op_Negation uu____2323) + in + if uu____2320 + then + let uu____2354 = + let uu____2356 = FStar_ST.op_Bang the_z3proc_ask_count in + FStar_Util.string_of_int uu____2356 in + FStar_Util.print3 + "Refreshing the z3proc (ask_count=%s old=[%s] new=[%s]) \n" + uu____2354 (cmd_and_args_to_string old_params) + (cmd_and_args_to_string next_params) + else ()); + (let uu____2383 = z3proc () in FStar_Util.kill_process uu____2383); + make_new_z3_proc next_params) else ()); - (let uu____1984 = z3proc () in FStar_Util.kill_process uu____1984); - (let uu____1986 = - let uu____1989 = new_z3proc_with_id () in - FStar_Pervasives_Native.Some uu____1989 in - FStar_ST.op_Colon_Equals the_z3proc uu____1986); query_logging.close_log () in - let restart uu____2018 = - query_logging.close_log (); - FStar_ST.op_Colon_Equals the_z3proc FStar_Pervasives_Native.None; - (let uu____2044 = - let uu____2047 = new_z3proc_with_id () in - FStar_Pervasives_Native.Some uu____2047 in - FStar_ST.op_Colon_Equals the_z3proc uu____2044) - in + let restart uu____2391 = + query_logging.close_log (); make_new_z3_proc next_params in + let x = [] in FStar_Util.mk_ref { ask = (FStar_Util.with_monitor x ask); @@ -388,8 +425,6 @@ let (bg_z3_proc : bgproc FStar_ST.ref) = restart = (FStar_Util.with_monitor x restart) } -let (set_bg_z3_proc : bgproc -> unit) = - fun bgp -> FStar_ST.op_Colon_Equals bg_z3_proc bgp type smt_output_section = Prims.string Prims.list type smt_output = { @@ -447,22 +482,22 @@ let (smt_output_sections : if tag = l then FStar_Pervasives_Native.Some ([], lines2) else - (let uu____2373 = until tag lines2 in - FStar_Util.map_opt uu____2373 - (fun uu____2409 -> - match uu____2409 with + (let uu____2673 = until tag lines2 in + FStar_Util.map_opt uu____2673 + (fun uu____2709 -> + match uu____2709 with | (until_tag,rest) -> ((l :: until_tag), rest))) in let start_tag tag = Prims.op_Hat "<" (Prims.op_Hat tag ">") in let end_tag tag = Prims.op_Hat "") in let find_section tag lines1 = - let uu____2516 = until (start_tag tag) lines1 in - match uu____2516 with + let uu____2816 = until (start_tag tag) lines1 in + match uu____2816 with | FStar_Pervasives_Native.None -> (FStar_Pervasives_Native.None, lines1) | FStar_Pervasives_Native.Some (prefix1,suffix) -> - let uu____2586 = until (end_tag tag) suffix in - (match uu____2586 with + let uu____2886 = until (end_tag tag) suffix in + (match uu____2886 with | FStar_Pervasives_Native.None -> failwith (Prims.op_Hat "Parse error: " @@ -471,25 +506,25 @@ let (smt_output_sections : ((FStar_Pervasives_Native.Some section), (FStar_List.append prefix1 suffix1))) in - let uu____2671 = find_section "result" lines in - match uu____2671 with + let uu____2971 = find_section "result" lines in + match uu____2971 with | (result_opt,lines1) -> let result = FStar_Util.must result_opt in - let uu____2710 = find_section "reason-unknown" lines1 in - (match uu____2710 with + let uu____3010 = find_section "reason-unknown" lines1 in + (match uu____3010 with | (reason_unknown,lines2) -> - let uu____2742 = find_section "unsat-core" lines2 in - (match uu____2742 with + let uu____3042 = find_section "unsat-core" lines2 in + (match uu____3042 with | (unsat_core,lines3) -> - let uu____2774 = find_section "statistics" lines3 in - (match uu____2774 with + let uu____3074 = find_section "statistics" lines3 in + (match uu____3074 with | (statistics,lines4) -> - let uu____2806 = find_section "labels" lines4 in - (match uu____2806 with + let uu____3106 = find_section "labels" lines4 in + (match uu____3106 with | (labels,lines5) -> let remaining = - let uu____2842 = until "Done!" lines5 in - match uu____2842 with + let uu____3142 = until "Done!" lines5 in + match uu____3142 with | FStar_Pervasives_Native.None -> lines5 | FStar_Pervasives_Native.Some (prefix1,suffix) -> @@ -497,7 +532,7 @@ let (smt_output_sections : in ((match remaining with | [] -> () - | uu____2896 -> + | uu____3196 -> let msg = FStar_Util.format2 "%sUnexpected output from Z3: %s\n" @@ -511,10 +546,10 @@ let (smt_output_sections : FStar_Errors.log_issue r (FStar_Errors.Warning_UnexpectedZ3Output, msg)); - (let uu____2912 = FStar_Util.must result_opt + (let uu____3212 = FStar_Util.must result_opt in { - smt_result = uu____2912; + smt_result = uu____3212; smt_reason_unknown = reason_unknown; smt_unsat_core = unsat_core; smt_statistics = statistics; @@ -553,11 +588,11 @@ let (doZ3Exe : if FStar_Util.starts_with s2 "error" then FStar_Pervasives_Native.None else - (let uu____3007 = + (let uu____3307 = FStar_All.pipe_right (FStar_Util.split s2 " ") (FStar_Util.sort_with FStar_String.compare) in - FStar_Pervasives_Native.Some uu____3007) + FStar_Pervasives_Native.Some uu____3307) in let labels = match smt_output.smt_labels with @@ -567,28 +602,28 @@ let (doZ3Exe : match lines2 with | lname::"false"::rest when FStar_Util.starts_with lname "label_" -> - let uu____3052 = lblnegs rest in lname :: - uu____3052 - | lname::uu____3058::rest when + let uu____3352 = lblnegs rest in lname :: + uu____3352 + | lname::uu____3358::rest when FStar_Util.starts_with lname "label_" -> lblnegs rest - | uu____3068 -> [] in + | uu____3368 -> [] in let lblnegs1 = lblnegs lines1 in FStar_All.pipe_right lblnegs1 (FStar_List.collect (fun l -> - let uu____3092 = + let uu____3392 = FStar_All.pipe_right label_messages (FStar_List.tryFind - (fun uu____3132 -> - match uu____3132 with - | (m,uu____3142,uu____3143) -> - let uu____3146 = + (fun uu____3432 -> + match uu____3432 with + | (m,uu____3442,uu____3443) -> + let uu____3446 = FStar_SMTEncoding_Term.fv_name m in - uu____3146 = l)) + uu____3446 = l)) in - match uu____3092 with + match uu____3392 with | FStar_Pervasives_Native.None -> [] | FStar_Pervasives_Native.Some (lbl,msg,r1) -> [(lbl, msg, r1)])) @@ -636,7 +671,7 @@ let (doZ3Exe : (Prims.parse_int "1")) else ltok in FStar_Util.smap_add statistics key value - | uu____3275 -> () in + | uu____3575 -> () in (FStar_List.iter parse_line lines1; statistics) in let reason_unknown = @@ -658,14 +693,14 @@ let (doZ3Exe : else ru) in let status = - (let uu____3308 = FStar_Options.debug_any () in - if uu____3308 + (let uu____3608 = FStar_Options.debug_any () in + if uu____3608 then - let uu____3311 = + let uu____3611 = FStar_Util.format1 "Z3 says: %s\n" (FStar_String.concat "\n" smt_output.smt_result) in - FStar_All.pipe_left FStar_Util.print_string uu____3311 + FStar_All.pipe_left FStar_Util.print_string uu____3611 else ()); (match smt_output.smt_result with | "unsat"::[] -> UNSAT unsat_core @@ -673,32 +708,34 @@ let (doZ3Exe : | "unknown"::[] -> UNKNOWN (labels, reason_unknown) | "timeout"::[] -> TIMEOUT (labels, reason_unknown) | "killed"::[] -> - ((let uu____3343 = - let uu____3348 = FStar_ST.op_Bang bg_z3_proc in - uu____3348.restart in - uu____3343 ()); + ((let uu____3643 = + let uu____3648 = FStar_ST.op_Bang bg_z3_proc in + uu____3648.restart in + uu____3643 ()); KILLED) - | uu____3368 -> - let uu____3369 = + | uu____3668 -> + let uu____3669 = FStar_Util.format1 "Unexpected output from Z3: got output result: %s\n" (FStar_String.concat "\n" smt_output.smt_result) in - failwith uu____3369) + failwith uu____3669) in (status, statistics) in let stdout1 = if fresh then - let proc = new_z3proc_with_id () in - let kill_handler uu____3384 = "\nkilled\n" in + let proc = + let uu____3678 = z3_cmd_and_args () in + new_z3proc_with_id uu____3678 in + let kill_handler uu____3693 = "\nkilled\n" in let out = FStar_Util.ask_process proc input kill_handler in (FStar_Util.kill_process proc; out) else - (let uu____3391 = - let uu____3398 = FStar_ST.op_Bang bg_z3_proc in - uu____3398.ask in - uu____3391 input) + (let uu____3700 = + let uu____3707 = FStar_ST.op_Bang bg_z3_proc in + uu____3707.ask in + uu____3700 input) in parse (FStar_Util.trim_string stdout1) @@ -761,43 +798,43 @@ let (pending_jobs : Prims.int FStar_ST.ref) = FStar_Util.mk_ref (Prims.parse_int "0") let (running : Prims.bool FStar_ST.ref) = FStar_Util.mk_ref false let rec (dequeue' : unit -> unit) = - fun uu____3701 -> + fun uu____4010 -> let j = - let uu____3703 = FStar_ST.op_Bang job_queue in - match uu____3703 with + let uu____4012 = FStar_ST.op_Bang job_queue in + match uu____4012 with | [] -> failwith "Impossible" | hd1::tl1 -> (FStar_ST.op_Colon_Equals job_queue tl1; hd1) in FStar_Util.incr pending_jobs; FStar_Util.monitor_exit job_queue; run_job j; FStar_Util.with_monitor job_queue - (fun uu____3771 -> FStar_Util.decr pending_jobs) (); + (fun uu____4080 -> FStar_Util.decr pending_jobs) (); dequeue () and (dequeue : unit -> unit) = - fun uu____3773 -> - let uu____3774 = FStar_ST.op_Bang running in - if uu____3774 + fun uu____4082 -> + let uu____4083 = FStar_ST.op_Bang running in + if uu____4083 then - let rec aux uu____3802 = + let rec aux uu____4111 = FStar_Util.monitor_enter job_queue; - (let uu____3808 = FStar_ST.op_Bang job_queue in - match uu____3808 with + (let uu____4117 = FStar_ST.op_Bang job_queue in + match uu____4117 with | [] -> (FStar_Util.monitor_exit job_queue; FStar_Util.sleep (Prims.parse_int "50"); aux ()) - | uu____3841 -> dequeue' ()) + | uu____4150 -> dequeue' ()) in aux () else () and (run_job : z3job -> unit) = fun j -> - let uu____3845 = j.job () in FStar_All.pipe_left j.callback uu____3845 + let uu____4154 = j.job () in FStar_All.pipe_left j.callback uu____4154 let (init : unit -> unit) = - fun uu____3851 -> + fun uu____4160 -> FStar_ST.op_Colon_Equals running true; (let n_cores1 = FStar_Options.n_cores () in if n_cores1 > (Prims.parse_int "1") @@ -813,26 +850,26 @@ let (init : unit -> unit) = let (enqueue : z3job -> unit) = fun j -> FStar_Util.with_monitor job_queue - (fun uu____3908 -> - (let uu____3910 = - let uu____3913 = FStar_ST.op_Bang job_queue in - FStar_List.append uu____3913 [j] in - FStar_ST.op_Colon_Equals job_queue uu____3910); + (fun uu____4217 -> + (let uu____4219 = + let uu____4222 = FStar_ST.op_Bang job_queue in + FStar_List.append uu____4222 [j] in + FStar_ST.op_Colon_Equals job_queue uu____4219); FStar_Util.monitor_pulse job_queue) () let (finish : unit -> unit) = - fun uu____3971 -> - let rec aux uu____3977 = - let uu____3978 = + fun uu____4280 -> + let rec aux uu____4286 = + let uu____4287 = FStar_Util.with_monitor job_queue - (fun uu____3996 -> - let uu____3997 = FStar_ST.op_Bang pending_jobs in - let uu____4020 = - let uu____4021 = FStar_ST.op_Bang job_queue in - FStar_List.length uu____4021 in - (uu____3997, uu____4020)) () + (fun uu____4305 -> + let uu____4306 = FStar_ST.op_Bang pending_jobs in + let uu____4329 = + let uu____4330 = FStar_ST.op_Bang job_queue in + FStar_List.length uu____4330 in + (uu____4306, uu____4329)) () in - match uu____3978 with + match uu____4287 with | (n1,m) -> if (n1 + m) = (Prims.parse_int "0") then FStar_ST.op_Colon_Equals running false @@ -843,49 +880,49 @@ let (finish : unit -> unit) = type scope_t = FStar_SMTEncoding_Term.decl Prims.list Prims.list let (fresh_scope : scope_t FStar_ST.ref) = FStar_Util.mk_ref [[]] let (mk_fresh_scope : unit -> scope_t) = - fun uu____4097 -> FStar_ST.op_Bang fresh_scope + fun uu____4406 -> FStar_ST.op_Bang fresh_scope let (flatten_fresh_scope : unit -> FStar_SMTEncoding_Term.decl Prims.list) = - fun uu____4124 -> - let uu____4125 = - let uu____4130 = FStar_ST.op_Bang fresh_scope in - FStar_List.rev uu____4130 in - FStar_List.flatten uu____4125 + fun uu____4433 -> + let uu____4434 = + let uu____4439 = FStar_ST.op_Bang fresh_scope in + FStar_List.rev uu____4439 in + FStar_List.flatten uu____4434 let (bg_scope : FStar_SMTEncoding_Term.decl Prims.list FStar_ST.ref) = FStar_Util.mk_ref [] let (push : Prims.string -> unit) = fun msg -> FStar_Util.atomically - (fun uu____4174 -> - (let uu____4176 = - let uu____4177 = FStar_ST.op_Bang fresh_scope in + (fun uu____4483 -> + (let uu____4485 = + let uu____4486 = FStar_ST.op_Bang fresh_scope in [FStar_SMTEncoding_Term.Caption msg; FStar_SMTEncoding_Term.Push] - :: uu____4177 + :: uu____4486 in - FStar_ST.op_Colon_Equals fresh_scope uu____4176); - (let uu____4222 = - let uu____4225 = FStar_ST.op_Bang bg_scope in - FStar_List.append uu____4225 + FStar_ST.op_Colon_Equals fresh_scope uu____4485); + (let uu____4531 = + let uu____4534 = FStar_ST.op_Bang bg_scope in + FStar_List.append uu____4534 [FStar_SMTEncoding_Term.Push; FStar_SMTEncoding_Term.Caption msg] in - FStar_ST.op_Colon_Equals bg_scope uu____4222)) + FStar_ST.op_Colon_Equals bg_scope uu____4531)) let (pop : Prims.string -> unit) = fun msg -> FStar_Util.atomically - (fun uu____4285 -> - (let uu____4287 = - let uu____4288 = FStar_ST.op_Bang fresh_scope in - FStar_List.tl uu____4288 in - FStar_ST.op_Colon_Equals fresh_scope uu____4287); - (let uu____4333 = - let uu____4336 = FStar_ST.op_Bang bg_scope in - FStar_List.append uu____4336 + (fun uu____4594 -> + (let uu____4596 = + let uu____4597 = FStar_ST.op_Bang fresh_scope in + FStar_List.tl uu____4597 in + FStar_ST.op_Colon_Equals fresh_scope uu____4596); + (let uu____4642 = + let uu____4645 = FStar_ST.op_Bang bg_scope in + FStar_List.append uu____4645 [FStar_SMTEncoding_Term.Caption msg; FStar_SMTEncoding_Term.Pop] in - FStar_ST.op_Colon_Equals bg_scope uu____4333)) + FStar_ST.op_Colon_Equals bg_scope uu____4642)) let (snapshot : Prims.string -> (Prims.int * unit)) = fun msg -> FStar_Common.snapshot push fresh_scope msg @@ -893,92 +930,92 @@ let (rollback : Prims.string -> Prims.int FStar_Pervasives_Native.option -> unit) = fun msg -> fun depth -> - FStar_Common.rollback (fun uu____4423 -> pop msg) fresh_scope depth + FStar_Common.rollback (fun uu____4732 -> pop msg) fresh_scope depth let (giveZ3 : FStar_SMTEncoding_Term.decl Prims.list -> unit) = fun decls -> FStar_All.pipe_right decls (FStar_List.iter - (fun uu___1_4438 -> - match uu___1_4438 with + (fun uu___1_4747 -> + match uu___1_4747 with | FStar_SMTEncoding_Term.Push -> failwith "Unexpected push/pop" | FStar_SMTEncoding_Term.Pop -> failwith "Unexpected push/pop" - | uu____4441 -> ())); - (let uu____4443 = FStar_ST.op_Bang fresh_scope in - match uu____4443 with + | uu____4750 -> ())); + (let uu____4752 = FStar_ST.op_Bang fresh_scope in + match uu____4752 with | hd1::tl1 -> FStar_ST.op_Colon_Equals fresh_scope ((FStar_List.append hd1 decls) :: tl1) - | uu____4494 -> failwith "Impossible"); - (let uu____4496 = - let uu____4499 = FStar_ST.op_Bang bg_scope in - FStar_List.append uu____4499 decls in - FStar_ST.op_Colon_Equals bg_scope uu____4496) + | uu____4803 -> failwith "Impossible"); + (let uu____4805 = + let uu____4808 = FStar_ST.op_Bang bg_scope in + FStar_List.append uu____4808 decls in + FStar_ST.op_Colon_Equals bg_scope uu____4805) let (refresh : unit -> unit) = - fun uu____4553 -> - (let uu____4555 = - let uu____4557 = FStar_Options.n_cores () in - uu____4557 < (Prims.parse_int "2") in - if uu____4555 + fun uu____4862 -> + (let uu____4864 = + let uu____4866 = FStar_Options.n_cores () in + uu____4866 < (Prims.parse_int "2") in + if uu____4864 then - let uu____4561 = - let uu____4566 = FStar_ST.op_Bang bg_z3_proc in uu____4566.refresh + let uu____4870 = + let uu____4875 = FStar_ST.op_Bang bg_z3_proc in uu____4875.refresh in - uu____4561 () + uu____4870 () else ()); - (let uu____4588 = flatten_fresh_scope () in - FStar_ST.op_Colon_Equals bg_scope uu____4588) + (let uu____4897 = flatten_fresh_scope () in + FStar_ST.op_Colon_Equals bg_scope uu____4897) let (context_profile : FStar_SMTEncoding_Term.decl Prims.list -> unit) = fun theory -> - let uu____4624 = + let uu____4933 = FStar_List.fold_left - (fun uu____4657 -> + (fun uu____4966 -> fun d -> - match uu____4657 with + match uu____4966 with | (out,_total) -> (match d with | FStar_SMTEncoding_Term.Module (name,decls) -> let decls1 = FStar_List.filter - (fun uu___2_4726 -> - match uu___2_4726 with - | FStar_SMTEncoding_Term.Assume uu____4728 -> + (fun uu___2_5035 -> + match uu___2_5035 with + | FStar_SMTEncoding_Term.Assume uu____5037 -> true - | uu____4730 -> false) decls + | uu____5039 -> false) decls in let n1 = FStar_List.length decls1 in (((name, n1) :: out), (n1 + _total)) - | uu____4747 -> (out, _total))) ([], (Prims.parse_int "0")) + | uu____5056 -> (out, _total))) ([], (Prims.parse_int "0")) theory in - match uu____4624 with + match uu____4933 with | (modules,total_decls) -> let modules1 = FStar_List.sortWith - (fun uu____4809 -> - fun uu____4810 -> - match (uu____4809, uu____4810) with - | ((uu____4836,n1),(uu____4838,m)) -> m - n1) modules + (fun uu____5118 -> + fun uu____5119 -> + match (uu____5118, uu____5119) with + | ((uu____5145,n1),(uu____5147,m)) -> m - n1) modules in (if modules1 <> [] then - (let uu____4876 = FStar_Util.string_of_int total_decls in + (let uu____5185 = FStar_Util.string_of_int total_decls in FStar_Util.print1 "Z3 Proof Stats: context_profile with %s assertions\n" - uu____4876) + uu____5185) else (); FStar_List.iter - (fun uu____4891 -> - match uu____4891 with + (fun uu____5200 -> + match uu____5200 with | (m,n1) -> if n1 <> (Prims.parse_int "0") then - let uu____4907 = FStar_Util.string_of_int n1 in + let uu____5216 = FStar_Util.string_of_int n1 in FStar_Util.print2 "Z3 Proof Stats: %s produced %s SMT decls\n" m - uu____4907 + uu____5216 else ()) modules1) let (mk_input : @@ -990,27 +1027,27 @@ let (mk_input : fun fresh -> fun theory -> let options = FStar_ST.op_Bang z3_options in - (let uu____4966 = FStar_Options.print_z3_statistics () in - if uu____4966 then context_profile theory else ()); - (let uu____4971 = - let uu____4980 = + (let uu____5275 = FStar_Options.print_z3_statistics () in + if uu____5275 then context_profile theory else ()); + (let uu____5280 = + let uu____5289 = (FStar_Options.record_hints ()) || ((FStar_Options.use_hints ()) && (FStar_Options.use_hint_hashes ())) in - if uu____4980 + if uu____5289 then - let uu____4991 = - let uu____5002 = + let uu____5300 = + let uu____5311 = FStar_All.pipe_right theory (FStar_Util.prefix_until - (fun uu___3_5030 -> - match uu___3_5030 with + (fun uu___3_5339 -> + match uu___3_5339 with | FStar_SMTEncoding_Term.CheckSat -> true - | uu____5033 -> false)) + | uu____5342 -> false)) in - FStar_All.pipe_right uu____5002 FStar_Option.get in - match uu____4991 with + FStar_All.pipe_right uu____5311 FStar_Option.get in + match uu____5300 with | (prefix1,check_sat,suffix) -> let pp = FStar_List.map (FStar_SMTEncoding_Term.declToSmt options) @@ -1021,37 +1058,37 @@ let (mk_input : let ps = FStar_String.concat "\n" ps_lines in let ss = FStar_String.concat "\n" ss_lines in let hs = - let uu____5116 = FStar_Options.keep_query_captions () in - if uu____5116 + let uu____5425 = FStar_Options.keep_query_captions () in + if uu____5425 then - let uu____5120 = + let uu____5429 = FStar_All.pipe_right prefix1 (FStar_List.map (FStar_SMTEncoding_Term.declToSmt_no_caps options)) in - FStar_All.pipe_right uu____5120 (FStar_String.concat "\n") + FStar_All.pipe_right uu____5429 (FStar_String.concat "\n") else ps in - let uu____5137 = - let uu____5141 = FStar_Util.digest_of_string hs in - FStar_Pervasives_Native.Some uu____5141 in - ((Prims.op_Hat ps (Prims.op_Hat "\n" ss)), uu____5137) + let uu____5446 = + let uu____5450 = FStar_Util.digest_of_string hs in + FStar_Pervasives_Native.Some uu____5450 in + ((Prims.op_Hat ps (Prims.op_Hat "\n" ss)), uu____5446) else - (let uu____5151 = - let uu____5153 = + (let uu____5460 = + let uu____5462 = FStar_List.map (FStar_SMTEncoding_Term.declToSmt options) theory in - FStar_All.pipe_right uu____5153 (FStar_String.concat "\n") in - (uu____5151, FStar_Pervasives_Native.None)) + FStar_All.pipe_right uu____5462 (FStar_String.concat "\n") in + (uu____5460, FStar_Pervasives_Native.None)) in - match uu____4971 with + match uu____5280 with | (r,hash) -> let log_file_name = - let uu____5195 = FStar_Options.log_queries () in - if uu____5195 + let uu____5504 = FStar_Options.log_queries () in + if uu____5504 then - let uu____5201 = query_logging.write_to_log fresh r in - FStar_Pervasives_Native.Some uu____5201 + let uu____5510 = query_logging.write_to_log fresh r in + FStar_Pervasives_Native.Some uu____5510 else FStar_Pervasives_Native.None in (r, hash, log_file_name)) @@ -1065,11 +1102,11 @@ let (cache_hit : fun cache -> fun qhash -> fun cb -> - let uu____5259 = + let uu____5568 = (FStar_Options.use_hints ()) && (FStar_Options.use_hint_hashes ()) in - if uu____5259 + if uu____5568 then match qhash with | FStar_Pervasives_Native.Some x when qhash = cache -> @@ -1084,7 +1121,7 @@ let (cache_hit : z3result_log_file = log_file } in cb result; true)) - | uu____5284 -> false + | uu____5593 -> false else false let (z3_job : @@ -1101,28 +1138,28 @@ let (z3_job : fun label_messages -> fun input -> fun qhash -> - fun uu____5335 -> + fun uu____5644 -> let start = FStar_Util.now () in - let uu____5345 = + let uu____5654 = try - (fun uu___530_5355 -> + (fun uu___541_5664 -> match () with | () -> doZ3Exe log_file r fresh input label_messages) () with - | uu___529_5361 -> + | uu___540_5670 -> if (refresh (); false) then - Obj.magic (Obj.repr (FStar_Exn.raise uu___529_5361)) + Obj.magic (Obj.repr (FStar_Exn.raise uu___540_5670)) else Obj.magic (Obj.repr (failwith "unreachable")) in - match uu____5345 with + match uu____5654 with | (status,statistics) -> - let uu____5374 = - let uu____5380 = FStar_Util.now () in - FStar_Util.time_diff start uu____5380 in - (match uu____5374 with - | (uu____5381,elapsed_time) -> + let uu____5683 = + let uu____5689 = FStar_Util.now () in + FStar_Util.time_diff start uu____5689 in + (match uu____5683 with + | (uu____5690,elapsed_time) -> { z3result_status = status; z3result_time = elapsed_time; @@ -1159,19 +1196,19 @@ let (ask_1_core : (FStar_List.append [FStar_SMTEncoding_Term.Push] (FStar_List.append qry [FStar_SMTEncoding_Term.Pop])) in - let uu____5519 = filter_theory theory1 in - match uu____5519 with + let uu____5828 = filter_theory theory1 in + match uu____5828 with | (theory2,_used_unsat_core) -> - let uu____5535 = mk_input fresh theory2 in - (match uu____5535 with + let uu____5844 = mk_input fresh theory2 in + (match uu____5844 with | (input,qhash,log_file_name) -> - let uu____5566 = - let uu____5568 = + let uu____5875 = + let uu____5877 = fresh && (cache_hit log_file_name cache qhash cb) in - Prims.op_Negation uu____5568 in - if uu____5566 + Prims.op_Negation uu____5877 in + if uu____5875 then run_job { @@ -1200,31 +1237,31 @@ let (ask_n_cores : fun scope -> fun cb -> let theory = - let uu____5651 = + let uu____5960 = match scope with | FStar_Pervasives_Native.Some s -> FStar_List.rev s | FStar_Pervasives_Native.None -> (FStar_ST.op_Colon_Equals bg_scope []; - (let uu____5687 = FStar_ST.op_Bang fresh_scope in - FStar_List.rev uu____5687)) + (let uu____5996 = FStar_ST.op_Bang fresh_scope in + FStar_List.rev uu____5996)) in - FStar_List.flatten uu____5651 in + FStar_List.flatten uu____5960 in let theory1 = FStar_List.append theory (FStar_List.append [FStar_SMTEncoding_Term.Push] (FStar_List.append qry [FStar_SMTEncoding_Term.Pop])) in - let uu____5716 = filter_theory theory1 in - match uu____5716 with + let uu____6025 = filter_theory theory1 in + match uu____6025 with | (theory2,used_unsat_core) -> - let uu____5732 = mk_input true theory2 in - (match uu____5732 with + let uu____6041 = mk_input true theory2 in + (match uu____6041 with | (input,qhash,log_file_name) -> - let uu____5764 = - let uu____5766 = + let uu____6073 = + let uu____6075 = cache_hit log_file_name cache qhash cb in - Prims.op_Negation uu____5766 in - if uu____5764 + Prims.op_Negation uu____6075 in + if uu____6073 then enqueue { @@ -1254,10 +1291,10 @@ let (ask : fun scope -> fun cb -> fun fresh -> - let uu____5854 = - let uu____5856 = FStar_Options.n_cores () in - uu____5856 = (Prims.parse_int "1") in - if uu____5854 + let uu____6163 = + let uu____6165 = FStar_Options.n_cores () in + uu____6165 = (Prims.parse_int "1") in + if uu____6163 then ask_1_core r filter1 cache label_messages qry cb fresh else ask_n_cores r filter1 cache label_messages qry scope cb