From 635daa3f6514efc8397adc2006a0e985e5eda1f7 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Tue, 3 Sep 2024 12:47:53 -0700 Subject: [PATCH] fix a comment and bug in SolverState---given_decls at a level does not include decls at prior levels:an exception is the top-most level for pruned query --- .../FStar_SMTEncoding_SolverState.ml | 23 +++++++++++-------- .../FStar.SMTEncoding.SolverState.fst | 18 +++++++++------ .../FStar.SMTEncoding.SolverState.fsti | 2 +- 3 files changed, 26 insertions(+), 17 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_SolverState.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_SolverState.ml index 24868c6e027..181e83857dd 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_SolverState.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_SolverState.ml @@ -255,14 +255,14 @@ let (filter_using_facts_from : using_facts_from_setting FStar_Pervasives_Native.option -> FStar_SMTEncoding_Term.assumption FStar_Compiler_Util.psmap -> decl_name_set -> - decl_name_set -> + (Prims.string -> Prims.bool) -> FStar_SMTEncoding_Term.decl Prims.list -> FStar_SMTEncoding_Term.decl Prims.list) = fun using_facts_from -> fun named_assumptions -> fun retain_assumptions -> - fun given_decl_names -> + fun already_given_decl -> fun ds -> match using_facts_from with | FStar_Pervasives_Native.None -> ds @@ -294,9 +294,8 @@ let (filter_using_facts_from : FStar_Compiler_Util.smap_try_find already_given_map a.FStar_SMTEncoding_Term.assumption_name in FStar_Pervasives_Native.uu___is_Some uu___) || - (decl_names_contains - a.FStar_SMTEncoding_Term.assumption_name - given_decl_names) in + (already_given_decl + a.FStar_SMTEncoding_Term.assumption_name) in let map_decl d = match d with | FStar_SMTEncoding_Term.Assume a -> @@ -324,6 +323,12 @@ let (filter_using_facts_from : assumptions | uu___ -> [d] in let ds1 = FStar_Compiler_List.collect map_decl ds in ds1 +let (already_given_decl : solver_state -> Prims.string -> Prims.bool) = + fun s -> + fun aname -> + FStar_Compiler_Util.for_some + (fun level -> decl_names_contains aname level.given_decl_names) + s.levels let rec (flatten : FStar_SMTEncoding_Term.decl -> FStar_SMTEncoding_Term.decl Prims.list) = fun d -> @@ -448,7 +453,7 @@ let (give_now : let ds_to_flush = filter_using_facts_from s.using_facts_from named_assumptions s.retain_assumptions - hd.given_decl_names decls in + (already_given_decl s) decls in let given = FStar_Compiler_List.fold_left (fun given1 -> @@ -527,7 +532,7 @@ let (reset : levels = (s_new.levels); pending_flushes_rev = (s_new.pending_flushes_rev); using_facts_from; - retain_assumptions = (s_new.retain_assumptions) + retain_assumptions = (s.retain_assumptions) } in let set_pruning_roots level s1 = let uu___ = peek s1 in @@ -621,7 +626,7 @@ let (prune_level : | (given_decl_names, can_give) -> let can_give1 = filter_using_facts_from s.using_facts_from hd.named_assumptions - s.retain_assumptions hd.given_decl_names can_give in + s.retain_assumptions (already_given_decl s) can_give in let hd1 = { pruning_state = (hd.pruning_state); @@ -646,7 +651,7 @@ let (prune_sim : FStar_SMTEncoding_Pruning.prune hd.pruning_state roots in let can_give = filter_using_facts_from s.using_facts_from hd.named_assumptions - s.retain_assumptions hd.given_decl_names to_give in + s.retain_assumptions (already_given_decl s) to_give in let uu___1 = let uu___2 = FStar_Compiler_List.filter diff --git a/src/smtencoding/FStar.SMTEncoding.SolverState.fst b/src/smtencoding/FStar.SMTEncoding.SolverState.fst index cd3677af7d9..cfa2f1d0ddb 100644 --- a/src/smtencoding/FStar.SMTEncoding.SolverState.fst +++ b/src/smtencoding/FStar.SMTEncoding.SolverState.fst @@ -35,7 +35,7 @@ let add_name (x:string) (s:decl_name_set) = BU.psmap_add s x true type decls_at_level = { pruning_state: Pruning.pruning_state; (* the context pruning state representing all declarations visible at this level and prior levels *) - given_decl_names: decl_name_set; (* all declarations that have been given to the solver at this level, and prior levels *) + given_decl_names: decl_name_set; (* all declarations that have been given to the solver at this level *) all_decls_at_level_rev: list (list decl); (* all decls at this level; in reverse order of pushes *) given_some_decls: bool; (* Have some declarations been flushed at this level? If not, we can pop this level without needing to flush pop to the solver *) to_flush_rev: list (list decl); (* declarations to be given to the solver at the next flush, in reverse order, though each nested list is in order *) @@ -137,7 +137,7 @@ let filter_using_facts_from (using_facts_from:option using_facts_from_setting) (named_assumptions:BU.psmap assumption) (retain_assumptions:decl_name_set) - (given_decl_names:decl_name_set) + (already_given_decl: string -> bool) (ds:list decl) //flattened decls : list decl = match using_facts_from with @@ -160,7 +160,7 @@ let filter_using_facts_from let already_given (a:assumption) : bool = Some? (BU.smap_try_find already_given_map a.assumption_name) || - decl_names_contains a.assumption_name given_decl_names + already_given_decl a.assumption_name in let map_decl (d:decl) : list decl @@ -187,6 +187,10 @@ let filter_using_facts_from let ds = List.collect map_decl ds in ds +let already_given_decl (s:solver_state) (aname:string) +: bool += s.levels |> BU.for_some (fun level -> decl_names_contains aname level.given_decl_names) + let rec flatten (d:decl) : list decl = match d with | Module (_, ds) -> List.collect flatten ds @@ -282,7 +286,7 @@ let give_now (resetting:bool) (ds:list decl) (s:solver_state) s.using_facts_from named_assumptions s.retain_assumptions - hd.given_decl_names + (already_given_decl s) decls in let given = @@ -334,7 +338,7 @@ let give = give_aux false let reset (using_facts_from:option using_facts_from_setting) (s:solver_state) : solver_state = let s_new = init () in - let s_new = { s_new with using_facts_from } in + let s_new = { s_new with using_facts_from; retain_assumptions = s.retain_assumptions } in let set_pruning_roots level s = let hd,tl = peek s in let hd = { hd with pruning_roots = level.pruning_roots } in @@ -402,7 +406,7 @@ let prune_level (roots:list decl) (hd:decls_at_level) (s:solver_state) s.using_facts_from hd.named_assumptions s.retain_assumptions - hd.given_decl_names + (already_given_decl s) can_give in let hd = { hd with given_decl_names; @@ -420,7 +424,7 @@ let prune_sim (roots:list decl) (s:solver_state) s.using_facts_from hd.named_assumptions s.retain_assumptions - hd.given_decl_names + (already_given_decl s) to_give in List.map name_of_assumption (List.filter Assume? roots@can_give) diff --git a/src/smtencoding/FStar.SMTEncoding.SolverState.fsti b/src/smtencoding/FStar.SMTEncoding.SolverState.fsti index dcfe50e5559..d9373e84cc1 100644 --- a/src/smtencoding/FStar.SMTEncoding.SolverState.fsti +++ b/src/smtencoding/FStar.SMTEncoding.SolverState.fsti @@ -15,7 +15,7 @@ *) module FStar.SMTEncoding.SolverState (** - This modules is an abstraction of state of the SMT solver, expressed in terms of the facts + This module is an abstraction of state of the SMT solver, expressed in terms of the facts that are visible to it currently. As such, it also encapsulates the various notions of filtering the facts that