diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml index dd2b9e7bc39..6ce5f9109aa 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml @@ -62,9 +62,7 @@ let (norm_before_encoding_us : FStar_SMTEncoding_Env.encoding_quantifier = (env.FStar_SMTEncoding_Env.encoding_quantifier); FStar_SMTEncoding_Env.global_cache = - (env.FStar_SMTEncoding_Env.global_cache); - FStar_SMTEncoding_Env.tsym_global_cache = - (env.FStar_SMTEncoding_Env.tsym_global_cache) + (env.FStar_SMTEncoding_Env.global_cache) } in let uu___ = FStar_Syntax_Subst.open_univ_vars us t in match uu___ with @@ -2011,10 +2009,7 @@ let (encode_free_var : (env1.FStar_SMTEncoding_Env.encoding_quantifier); FStar_SMTEncoding_Env.global_cache = - (env1.FStar_SMTEncoding_Env.global_cache); - FStar_SMTEncoding_Env.tsym_global_cache - = - (env1.FStar_SMTEncoding_Env.tsym_global_cache) + (env1.FStar_SMTEncoding_Env.global_cache) } in let uu___12 = let uu___13 = @@ -2391,9 +2386,7 @@ let (copy_env : FStar_SMTEncoding_Env.env_t -> FStar_SMTEncoding_Env.env_t) = (en.FStar_SMTEncoding_Env.current_module_name); FStar_SMTEncoding_Env.encoding_quantifier = (en.FStar_SMTEncoding_Env.encoding_quantifier); - FStar_SMTEncoding_Env.global_cache = uu___; - FStar_SMTEncoding_Env.tsym_global_cache = - (en.FStar_SMTEncoding_Env.tsym_global_cache) + FStar_SMTEncoding_Env.global_cache = uu___ } let (encode_top_level_let : FStar_SMTEncoding_Env.env_t -> @@ -2813,10 +2806,7 @@ let (encode_top_level_let : (env2.FStar_SMTEncoding_Env.encoding_quantifier); FStar_SMTEncoding_Env.global_cache = - (env2.FStar_SMTEncoding_Env.global_cache); - FStar_SMTEncoding_Env.tsym_global_cache - = - (env2.FStar_SMTEncoding_Env.tsym_global_cache) + (env2.FStar_SMTEncoding_Env.global_cache) }, e1, t_norm1)) in (match uu___9 with | (env', e1, t_norm1) -> @@ -3174,10 +3164,7 @@ let (encode_top_level_let : (env3.FStar_SMTEncoding_Env.encoding_quantifier); FStar_SMTEncoding_Env.global_cache = - (env3.FStar_SMTEncoding_Env.global_cache); - FStar_SMTEncoding_Env.tsym_global_cache - = - (env3.FStar_SMTEncoding_Env.tsym_global_cache) + (env3.FStar_SMTEncoding_Env.global_cache) }, e1, t_norm1)) in (match uu___12 with | (env', e1, t_norm1) -> @@ -6619,9 +6606,7 @@ and (encode_sigelt' : FStar_SMTEncoding_Env.encoding_quantifier = (env.FStar_SMTEncoding_Env.encoding_quantifier); FStar_SMTEncoding_Env.global_cache = - (env.FStar_SMTEncoding_Env.global_cache); - FStar_SMTEncoding_Env.tsym_global_cache = - (env.FStar_SMTEncoding_Env.tsym_global_cache) + (env.FStar_SMTEncoding_Env.global_cache) } in let f2 = norm_before_encoding env1 f1 in let uu___2 = @@ -7184,7 +7169,6 @@ let (init_env : FStar_TypeChecker_Env.env -> unit) = let uu___5 = FStar_TypeChecker_Env.current_module tcenv in FStar_Ident.string_of_lid uu___5 in let uu___5 = FStar_Compiler_Util.smap_create (Prims.of_int (100)) in - let uu___6 = FStar_Compiler_Util.smap_create (Prims.of_int (100)) in { FStar_SMTEncoding_Env.bvar_bindings = uu___2; FStar_SMTEncoding_Env.fvar_bindings = uu___3; @@ -7196,8 +7180,7 @@ let (init_env : FStar_TypeChecker_Env.env -> unit) = FStar_SMTEncoding_Env.encode_non_total_function_typ = true; FStar_SMTEncoding_Env.current_module_name = uu___4; FStar_SMTEncoding_Env.encoding_quantifier = false; - FStar_SMTEncoding_Env.global_cache = uu___5; - FStar_SMTEncoding_Env.tsym_global_cache = uu___6 + FStar_SMTEncoding_Env.global_cache = uu___5 } in [uu___1] in FStar_Compiler_Effect.op_Colon_Equals last_env uu___ @@ -7230,9 +7213,7 @@ let (get_env : FStar_SMTEncoding_Env.encoding_quantifier = (e.FStar_SMTEncoding_Env.encoding_quantifier); FStar_SMTEncoding_Env.global_cache = - (e.FStar_SMTEncoding_Env.global_cache); - FStar_SMTEncoding_Env.tsym_global_cache = - (e.FStar_SMTEncoding_Env.tsym_global_cache) + (e.FStar_SMTEncoding_Env.global_cache) } let (set_env : FStar_SMTEncoding_Env.env_t -> unit) = fun env -> @@ -7404,13 +7385,6 @@ let (recover_caching_and_update_env : FStar_Compiler_Util.must elt.FStar_SMTEncoding_Term.key in FStar_Compiler_Util.smap_add env.FStar_SMTEncoding_Env.global_cache uu___3 elt); - (match elt.FStar_SMTEncoding_Term.sym_name with - | FStar_Pervasives_Native.None -> () - | FStar_Pervasives_Native.Some "" -> () - | FStar_Pervasives_Native.Some name -> - FStar_Compiler_Util.smap_add - env.FStar_SMTEncoding_Env.tsym_global_cache name - elt); [elt]))) decls let (encode_sig : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.sigelt -> unit) = @@ -7485,9 +7459,7 @@ let (give_decls_to_z3_and_set_env : FStar_SMTEncoding_Env.encoding_quantifier = (env.FStar_SMTEncoding_Env.encoding_quantifier); FStar_SMTEncoding_Env.global_cache = - (env.FStar_SMTEncoding_Env.global_cache); - FStar_SMTEncoding_Env.tsym_global_cache = - (env.FStar_SMTEncoding_Env.tsym_global_cache) + (env.FStar_SMTEncoding_Env.global_cache) }; (let z3_decls = let uu___1 = @@ -7568,9 +7540,7 @@ let (encode_modul : FStar_SMTEncoding_Env.encoding_quantifier = (env.FStar_SMTEncoding_Env.encoding_quantifier); FStar_SMTEncoding_Env.global_cache = - (env.FStar_SMTEncoding_Env.global_cache); - FStar_SMTEncoding_Env.tsym_global_cache = - (env.FStar_SMTEncoding_Env.tsym_global_cache) + (env.FStar_SMTEncoding_Env.global_cache) } modul.FStar_Syntax_Syntax.declarations in match uu___5 with | (decls, env1) -> diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml index 0c9ad4b93f2..012da24df74 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml @@ -1201,9 +1201,7 @@ and (encode_deeply_embedded_quantifier : (env.FStar_SMTEncoding_Env.current_module_name); FStar_SMTEncoding_Env.encoding_quantifier = true; FStar_SMTEncoding_Env.global_cache = - (env.FStar_SMTEncoding_Env.global_cache); - FStar_SMTEncoding_Env.tsym_global_cache = - (env.FStar_SMTEncoding_Env.tsym_global_cache) + (env.FStar_SMTEncoding_Env.global_cache) } in let uu___ = encode_term t env1 in match uu___ with @@ -1406,9 +1404,7 @@ and (encode_term : (env.FStar_SMTEncoding_Env.current_module_name); FStar_SMTEncoding_Env.encoding_quantifier = false; FStar_SMTEncoding_Env.global_cache = - (env.FStar_SMTEncoding_Env.global_cache); - FStar_SMTEncoding_Env.tsym_global_cache = - (env.FStar_SMTEncoding_Env.tsym_global_cache) + (env.FStar_SMTEncoding_Env.global_cache) } | FStar_Syntax_Syntax.Tm_meta { FStar_Syntax_Syntax.tm2 = t2; @@ -3392,9 +3388,7 @@ and (encode_smt_patterns : FStar_SMTEncoding_Env.encoding_quantifier = (env.FStar_SMTEncoding_Env.encoding_quantifier); FStar_SMTEncoding_Env.global_cache = - (env.FStar_SMTEncoding_Env.global_cache); - FStar_SMTEncoding_Env.tsym_global_cache = - (env.FStar_SMTEncoding_Env.tsym_global_cache) + (env.FStar_SMTEncoding_Env.global_cache) } in let encode_smt_pattern t = let uu___ = FStar_Syntax_Util.head_and_args t in @@ -3936,8 +3930,6 @@ let (encode_function_type_as_formula : FStar_SMTEncoding_Env.encoding_quantifier = (env.FStar_SMTEncoding_Env.encoding_quantifier); FStar_SMTEncoding_Env.global_cache = - (env.FStar_SMTEncoding_Env.global_cache); - FStar_SMTEncoding_Env.tsym_global_cache = - (env.FStar_SMTEncoding_Env.tsym_global_cache) + (env.FStar_SMTEncoding_Env.global_cache) } in encode_formula quant env1 \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Env.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Env.ml index 65f43808b52..f08b2671eba 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Env.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Env.ml @@ -380,9 +380,7 @@ type env_t = encode_non_total_function_typ: Prims.bool ; current_module_name: Prims.string ; encoding_quantifier: Prims.bool ; - global_cache: FStar_SMTEncoding_Term.decls_elt FStar_Compiler_Util.smap ; - tsym_global_cache: - FStar_SMTEncoding_Term.decls_elt FStar_Compiler_Util.smap } + global_cache: FStar_SMTEncoding_Term.decls_elt FStar_Compiler_Util.smap } let (__proj__Mkenv_t__item__bvar_bindings : env_t -> (FStar_Syntax_Syntax.bv * FStar_SMTEncoding_Term.term) @@ -392,8 +390,7 @@ let (__proj__Mkenv_t__item__bvar_bindings : match projectee with | { bvar_bindings; fvar_bindings; depth; tcenv; warn; nolabels; use_zfuel_name; encode_non_total_function_typ; current_module_name; - encoding_quantifier; global_cache; tsym_global_cache;_} -> - bvar_bindings + encoding_quantifier; global_cache;_} -> bvar_bindings let (__proj__Mkenv_t__item__fvar_bindings : env_t -> (fvar_binding FStar_Compiler_Util.psmap * fvar_binding Prims.list)) = @@ -401,77 +398,63 @@ let (__proj__Mkenv_t__item__fvar_bindings : match projectee with | { bvar_bindings; fvar_bindings; depth; tcenv; warn; nolabels; use_zfuel_name; encode_non_total_function_typ; current_module_name; - encoding_quantifier; global_cache; tsym_global_cache;_} -> - fvar_bindings + encoding_quantifier; global_cache;_} -> fvar_bindings let (__proj__Mkenv_t__item__depth : env_t -> Prims.int) = fun projectee -> match projectee with | { bvar_bindings; fvar_bindings; depth; tcenv; warn; nolabels; use_zfuel_name; encode_non_total_function_typ; current_module_name; - encoding_quantifier; global_cache; tsym_global_cache;_} -> depth + encoding_quantifier; global_cache;_} -> depth let (__proj__Mkenv_t__item__tcenv : env_t -> FStar_TypeChecker_Env.env) = fun projectee -> match projectee with | { bvar_bindings; fvar_bindings; depth; tcenv; warn; nolabels; use_zfuel_name; encode_non_total_function_typ; current_module_name; - encoding_quantifier; global_cache; tsym_global_cache;_} -> tcenv + encoding_quantifier; global_cache;_} -> tcenv let (__proj__Mkenv_t__item__warn : env_t -> Prims.bool) = fun projectee -> match projectee with | { bvar_bindings; fvar_bindings; depth; tcenv; warn; nolabels; use_zfuel_name; encode_non_total_function_typ; current_module_name; - encoding_quantifier; global_cache; tsym_global_cache;_} -> warn + encoding_quantifier; global_cache;_} -> warn let (__proj__Mkenv_t__item__nolabels : env_t -> Prims.bool) = fun projectee -> match projectee with | { bvar_bindings; fvar_bindings; depth; tcenv; warn; nolabels; use_zfuel_name; encode_non_total_function_typ; current_module_name; - encoding_quantifier; global_cache; tsym_global_cache;_} -> nolabels + encoding_quantifier; global_cache;_} -> nolabels let (__proj__Mkenv_t__item__use_zfuel_name : env_t -> Prims.bool) = fun projectee -> match projectee with | { bvar_bindings; fvar_bindings; depth; tcenv; warn; nolabels; use_zfuel_name; encode_non_total_function_typ; current_module_name; - encoding_quantifier; global_cache; tsym_global_cache;_} -> - use_zfuel_name + encoding_quantifier; global_cache;_} -> use_zfuel_name let (__proj__Mkenv_t__item__encode_non_total_function_typ : env_t -> Prims.bool) = fun projectee -> match projectee with | { bvar_bindings; fvar_bindings; depth; tcenv; warn; nolabels; use_zfuel_name; encode_non_total_function_typ; current_module_name; - encoding_quantifier; global_cache; tsym_global_cache;_} -> - encode_non_total_function_typ + encoding_quantifier; global_cache;_} -> encode_non_total_function_typ let (__proj__Mkenv_t__item__current_module_name : env_t -> Prims.string) = fun projectee -> match projectee with | { bvar_bindings; fvar_bindings; depth; tcenv; warn; nolabels; use_zfuel_name; encode_non_total_function_typ; current_module_name; - encoding_quantifier; global_cache; tsym_global_cache;_} -> - current_module_name + encoding_quantifier; global_cache;_} -> current_module_name let (__proj__Mkenv_t__item__encoding_quantifier : env_t -> Prims.bool) = fun projectee -> match projectee with | { bvar_bindings; fvar_bindings; depth; tcenv; warn; nolabels; use_zfuel_name; encode_non_total_function_typ; current_module_name; - encoding_quantifier; global_cache; tsym_global_cache;_} -> - encoding_quantifier + encoding_quantifier; global_cache;_} -> encoding_quantifier let (__proj__Mkenv_t__item__global_cache : env_t -> FStar_SMTEncoding_Term.decls_elt FStar_Compiler_Util.smap) = fun projectee -> match projectee with | { bvar_bindings; fvar_bindings; depth; tcenv; warn; nolabels; use_zfuel_name; encode_non_total_function_typ; current_module_name; - encoding_quantifier; global_cache; tsym_global_cache;_} -> - global_cache -let (__proj__Mkenv_t__item__tsym_global_cache : - env_t -> FStar_SMTEncoding_Term.decls_elt FStar_Compiler_Util.smap) = - fun projectee -> - match projectee with - | { bvar_bindings; fvar_bindings; depth; tcenv; warn; nolabels; - use_zfuel_name; encode_non_total_function_typ; current_module_name; - encoding_quantifier; global_cache; tsym_global_cache;_} -> - tsym_global_cache + encoding_quantifier; global_cache;_} -> global_cache let (print_env : env_t -> Prims.string) = fun e -> let bvars = @@ -597,8 +580,7 @@ let (gen_term_var : encode_non_total_function_typ = (env.encode_non_total_function_typ); current_module_name = (env.current_module_name); encoding_quantifier = (env.encoding_quantifier); - global_cache = (env.global_cache); - tsym_global_cache = (env.tsym_global_cache) + global_cache = (env.global_cache) } in (ysym, y, uu___) let (new_term_constant : @@ -626,8 +608,7 @@ let (new_term_constant : encode_non_total_function_typ = (env.encode_non_total_function_typ); current_module_name = (env.current_module_name); encoding_quantifier = (env.encoding_quantifier); - global_cache = (env.global_cache); - tsym_global_cache = (env.tsym_global_cache) + global_cache = (env.global_cache) } in (ysym, y, uu___) let (new_term_constant_from_string : @@ -655,8 +636,7 @@ let (new_term_constant_from_string : (env.encode_non_total_function_typ); current_module_name = (env.current_module_name); encoding_quantifier = (env.encoding_quantifier); - global_cache = (env.global_cache); - tsym_global_cache = (env.tsym_global_cache) + global_cache = (env.global_cache) } in (ysym, y, uu___) let (push_term_var : @@ -677,8 +657,7 @@ let (push_term_var : encode_non_total_function_typ = (env.encode_non_total_function_typ); current_module_name = (env.current_module_name); encoding_quantifier = (env.encoding_quantifier); - global_cache = (env.global_cache); - tsym_global_cache = (env.tsym_global_cache) + global_cache = (env.global_cache) } let (lookup_term_var : env_t -> FStar_Syntax_Syntax.bv -> FStar_SMTEncoding_Term.term) = @@ -760,8 +739,7 @@ let (new_term_constant_and_tok_from_lid_aux : (env.encode_non_total_function_typ); current_module_name = (env.current_module_name); encoding_quantifier = (env.encoding_quantifier); - global_cache = (env.global_cache); - tsym_global_cache = (env.tsym_global_cache) + global_cache = (env.global_cache) } in (fname, ftok_name, uu___1) let (new_term_constant_and_tok_from_lid : @@ -863,8 +841,7 @@ let (push_free_var_maybe_thunked : (env.encode_non_total_function_typ); current_module_name = (env.current_module_name); encoding_quantifier = (env.encoding_quantifier); - global_cache = (env.global_cache); - tsym_global_cache = (env.tsym_global_cache) + global_cache = (env.global_cache) } let (push_free_var : env_t -> @@ -927,8 +904,7 @@ let (push_zfuel_name : (env.encode_non_total_function_typ); current_module_name = (env.current_module_name); encoding_quantifier = (env.encoding_quantifier); - global_cache = (env.global_cache); - tsym_global_cache = (env.tsym_global_cache) + global_cache = (env.global_cache) } let (force_thunk : fvar_binding -> FStar_SMTEncoding_Term.term) = fun fvb -> @@ -1101,8 +1077,7 @@ let (reset_current_module_fvbs : env_t -> env_t) = encode_non_total_function_typ = (env.encode_non_total_function_typ); current_module_name = (env.current_module_name); encoding_quantifier = (env.encoding_quantifier); - global_cache = (env.global_cache); - tsym_global_cache = (env.tsym_global_cache) + global_cache = (env.global_cache) } let (get_current_module_fvbs : env_t -> fvar_binding Prims.list) = fun env -> FStar_Pervasives_Native.snd env.fvar_bindings @@ -1121,6 +1096,5 @@ let (add_fvar_binding_to_env : fvar_binding -> env_t -> env_t) = encode_non_total_function_typ = (env.encode_non_total_function_typ); current_module_name = (env.current_module_name); encoding_quantifier = (env.encoding_quantifier); - global_cache = (env.global_cache); - tsym_global_cache = (env.tsym_global_cache) + global_cache = (env.global_cache) } \ No newline at end of file diff --git a/src/smtencoding/FStar.SMTEncoding.Encode.fst b/src/smtencoding/FStar.SMTEncoding.Encode.fst index f1adc8b9938..3b1f04557e1 100644 --- a/src/smtencoding/FStar.SMTEncoding.Encode.fst +++ b/src/smtencoding/FStar.SMTEncoding.Encode.fst @@ -1824,8 +1824,7 @@ let init_env tcenv = last_env := [{bvar_bindings=BU.psmap_empty (); nolabels=false; use_zfuel_name=false; encode_non_total_function_typ=true; encoding_quantifier=false; current_module_name=Env.current_module tcenv |> Ident.string_of_lid; - global_cache = BU.smap_create 100; - tsym_global_cache = BU.smap_create 100}] + global_cache = BU.smap_create 100}] let get_env cmn tcenv = match !last_env with | [] -> failwith "No env; call init first!" | e::_ -> {e with tcenv=tcenv; current_module_name=Ident.string_of_lid cmn} @@ -1905,9 +1904,6 @@ let recover_caching_and_update_env (env:env_t) (decls:decls_t) :decls_t = //AND drop elt | None -> //no hit, update cache and retain elt BU.smap_add env.global_cache (elt.key |> BU.must) elt; - (match elt.sym_name with - | None | Some "" -> () - | Some name -> BU.smap_add env.tsym_global_cache name elt); [elt] ) ) diff --git a/src/smtencoding/FStar.SMTEncoding.Env.fst b/src/smtencoding/FStar.SMTEncoding.Env.fst index d893e3a15b5..8c6c5f43f90 100644 --- a/src/smtencoding/FStar.SMTEncoding.Env.fst +++ b/src/smtencoding/FStar.SMTEncoding.Env.fst @@ -172,7 +172,6 @@ type env_t = { current_module_name:string; encoding_quantifier:bool; global_cache:BU.smap decls_elt; //cache for hashconsing -- see Encode.fs where it is used and updated - tsym_global_cache: BU.smap decls_elt; } let print_env (e:env_t) : string = diff --git a/src/smtencoding/FStar.SMTEncoding.UnsatCore.fst b/src/smtencoding/FStar.SMTEncoding.UnsatCore.fst index 4690eb940d8..e612692b5c8 100644 --- a/src/smtencoding/FStar.SMTEncoding.UnsatCore.fst +++ b/src/smtencoding/FStar.SMTEncoding.UnsatCore.fst @@ -1,3 +1,18 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) module FStar.SMTEncoding.UnsatCore open FStar.Compiler.Effect open FStar diff --git a/src/smtencoding/FStar.SMTEncoding.UnsatCore.fsti b/src/smtencoding/FStar.SMTEncoding.UnsatCore.fsti index f1f0feb42c3..82ef8da97f8 100644 --- a/src/smtencoding/FStar.SMTEncoding.UnsatCore.fsti +++ b/src/smtencoding/FStar.SMTEncoding.UnsatCore.fsti @@ -1,3 +1,18 @@ +(* + Copyright 2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) module FStar.SMTEncoding.UnsatCore open FStar.Compiler.Effect open FStar