From 4d38764b5d4e7c9185fb00b9ccb286f71ae4bc75 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 14 Oct 2024 00:05:31 -0700 Subject: [PATCH 1/3] Solver.Cache: fix missing case --- src/smtencoding/FStarC.SMTEncoding.Solver.Cache.fst | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/smtencoding/FStarC.SMTEncoding.Solver.Cache.fst b/src/smtencoding/FStarC.SMTEncoding.Solver.Cache.fst index 94f54b09444..45741c96ed7 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Solver.Cache.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Solver.Cache.fst @@ -65,12 +65,13 @@ instance hashable_letbinding : hashable letbinding = { instance hashable_pragma : hashable pragma = { hash = (function - | SetOptions s -> hash 1 `mix` hash s - | ResetOptions s -> hash 2 `mix` hash s - | PushOptions s -> hash 3 `mix` hash s - | PopOptions -> hash 4 - | RestartSolver -> hash 5 - | PrintEffectsGraph -> hash 6); + | ShowOptions -> hash 1 + | SetOptions s -> hash 2 `mix` hash s + | ResetOptions s -> hash 3 `mix` hash s + | PushOptions s -> hash 4 `mix` hash s + | PopOptions -> hash 5 + | RestartSolver -> hash 6 + | PrintEffectsGraph -> hash 7); } let rec hash_sigelt (se:sigelt) : hash_code = From 75d71f88cbedea80c7b595dceefe63688b7c43a2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 14 Oct 2024 07:36:16 -0700 Subject: [PATCH 2/3] AST.Util: missed ShowOptions case --- src/parser/FStarC.Parser.AST.Util.fst | 1 + 1 file changed, 1 insertion(+) diff --git a/src/parser/FStarC.Parser.AST.Util.fst b/src/parser/FStarC.Parser.AST.Util.fst index 87d8bc70552..7b10da1be41 100644 --- a/src/parser/FStarC.Parser.AST.Util.fst +++ b/src/parser/FStarC.Parser.AST.Util.fst @@ -462,6 +462,7 @@ let eq_lift (t1 t2: lift) = let eq_pragma (t1 t2: pragma) = match t1, t2 with + | ShowOptions, ShowOptions -> true | SetOptions s1, SetOptions s2 -> s1 = s2 | ResetOptions s1, ResetOptions s2 -> eq_option (fun s1 s2 -> s1 = s2) s1 s2 | PushOptions s1, PushOptions s2 -> eq_option (fun s1 s2 -> s1 = s2) s1 s2 From 0dcc1e133fe29293217a485d454cfdca43e61dc9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 14 Oct 2024 06:53:04 -0700 Subject: [PATCH 3/3] snap --- .../fstar-lib/generated/FStarC_Parser_AST_Util.ml | 2 ++ .../generated/FStarC_SMTEncoding_Solver_Cache.ml | 15 +++++++++------ 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStarC_Parser_AST_Util.ml b/ocaml/fstar-lib/generated/FStarC_Parser_AST_Util.ml index 4ece69e79bd..2e021cd4abc 100644 --- a/ocaml/fstar-lib/generated/FStarC_Parser_AST_Util.ml +++ b/ocaml/fstar-lib/generated/FStarC_Parser_AST_Util.ml @@ -514,6 +514,8 @@ let (eq_pragma : fun t1 -> fun t2 -> match (t1, t2) with + | (FStarC_Parser_AST.ShowOptions, FStarC_Parser_AST.ShowOptions) -> + true | (FStarC_Parser_AST.SetOptions s1, FStarC_Parser_AST.SetOptions s2) -> s1 = s2 | (FStarC_Parser_AST.ResetOptions s1, FStarC_Parser_AST.ResetOptions diff --git a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Solver_Cache.ml b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Solver_Cache.ml index 89241361214..ef134ecf9a9 100644 --- a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Solver_Cache.ml +++ b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Solver_Cache.ml @@ -84,10 +84,13 @@ let (hashable_pragma : FStarC_Class_Hashable.hash = (fun uu___ -> match uu___ with + | FStarC_Syntax_Syntax.ShowOptions -> + FStarC_Class_Hashable.hash FStarC_Class_Hashable.hashable_int + Prims.int_one | FStarC_Syntax_Syntax.SetOptions s -> let uu___1 = FStarC_Class_Hashable.hash FStarC_Class_Hashable.hashable_int - Prims.int_one in + (Prims.of_int (2)) in let uu___2 = FStarC_Class_Hashable.hash FStarC_Class_Hashable.hashable_string s in @@ -95,7 +98,7 @@ let (hashable_pragma : | FStarC_Syntax_Syntax.ResetOptions s -> let uu___1 = FStarC_Class_Hashable.hash FStarC_Class_Hashable.hashable_int - (Prims.of_int (2)) in + (Prims.of_int (3)) in let uu___2 = FStarC_Class_Hashable.hash (FStarC_Class_Hashable.hashable_option @@ -104,7 +107,7 @@ let (hashable_pragma : | FStarC_Syntax_Syntax.PushOptions s -> let uu___1 = FStarC_Class_Hashable.hash FStarC_Class_Hashable.hashable_int - (Prims.of_int (3)) in + (Prims.of_int (4)) in let uu___2 = FStarC_Class_Hashable.hash (FStarC_Class_Hashable.hashable_option @@ -112,13 +115,13 @@ let (hashable_pragma : FStarC_Hash.mix uu___1 uu___2 | FStarC_Syntax_Syntax.PopOptions -> FStarC_Class_Hashable.hash FStarC_Class_Hashable.hashable_int - (Prims.of_int (4)) + (Prims.of_int (5)) | FStarC_Syntax_Syntax.RestartSolver -> FStarC_Class_Hashable.hash FStarC_Class_Hashable.hashable_int - (Prims.of_int (5)) + (Prims.of_int (6)) | FStarC_Syntax_Syntax.PrintEffectsGraph -> FStarC_Class_Hashable.hash FStarC_Class_Hashable.hashable_int - (Prims.of_int (6))) + (Prims.of_int (7))) } let rec (hash_sigelt : FStarC_Syntax_Syntax.sigelt -> FStarC_Hash.hash_code) = fun se -> hash_sigelt' se.FStarC_Syntax_Syntax.sigel