From 738fbc0a179ef20b1fd497970f8c32a62cbb1238 Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 16 Oct 2024 14:29:43 -0700 Subject: [PATCH] remove some obviously quadratic list concatenations in SMTEncoding.Encode --- .../generated/FStarC_SMTEncoding_Encode.ml | 82 ++++++++++--------- src/smtencoding/FStarC.SMTEncoding.Encode.fst | 14 +++- 2 files changed, 53 insertions(+), 43 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Encode.ml b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Encode.ml index 92a739589bc..03b60e497b9 100644 --- a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Encode.ml +++ b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Encode.ml @@ -201,22 +201,20 @@ let (prims : prims_t) = let uu___8 = let uu___9 = let uu___10 = - let uu___11 = - FStarC_SMTEncoding_Term.mk_IsTotFun - app1 in - ([[app1]], vars2, uu___11) in - FStarC_SMTEncoding_Term.mkForall - rng uu___10 in - (uu___9, - FStar_Pervasives_Native.None, - axiom_name1) in - FStarC_SMTEncoding_Util.mkAssume - uu___8 in - [uu___7] in - FStarC_Compiler_List.op_At axioms uu___6 in + FStarC_SMTEncoding_Term.mk_IsTotFun + app1 in + ([[app1]], vars2, uu___10) in + FStarC_SMTEncoding_Term.mkForall rng + uu___9 in + (uu___8, FStar_Pervasives_Native.None, + axiom_name1) in + FStarC_SMTEncoding_Util.mkAssume uu___7 in + uu___6 :: axioms in (uu___5, app1, vars2)) ([tot_fun_axiom_for_x], xtok1, []) all_vars_but_one in - match uu___3 with | (axioms, uu___4, uu___5) -> axioms in + match uu___3 with + | (axioms, uu___4, uu___5) -> + FStarC_Compiler_List.rev axioms in let rel_body = let rel_body1 = rel_type_f rel (xapp, body) in match precondition with @@ -2363,22 +2361,25 @@ let (encode_top_level_vals : fun env -> fun bindings -> fun quals -> - FStarC_Compiler_List.fold_left - (fun uu___ -> - fun lb -> - match uu___ with - | (decls, env1) -> - let uu___1 = + let uu___ = + FStarC_Compiler_List.fold_left + (fun uu___1 -> + fun lb -> + match uu___1 with + | (decls, env1) -> let uu___2 = - FStarC_Compiler_Util.right - lb.FStarC_Syntax_Syntax.lbname in - encode_top_level_val false env1 - lb.FStarC_Syntax_Syntax.lbunivs uu___2 - lb.FStarC_Syntax_Syntax.lbtyp quals in - (match uu___1 with - | (decls', env2) -> - ((FStarC_Compiler_List.op_At decls decls'), env2))) - ([], env) bindings + let uu___3 = + FStarC_Compiler_Util.right + lb.FStarC_Syntax_Syntax.lbname in + encode_top_level_val false env1 + lb.FStarC_Syntax_Syntax.lbunivs uu___3 + lb.FStarC_Syntax_Syntax.lbtyp quals in + (match uu___2 with + | (decls', env2) -> + ((FStarC_Compiler_List.rev_append decls' decls), + env2))) ([], env) bindings in + match uu___ with + | (decls, env1) -> ((FStarC_Compiler_List.rev decls), env1) exception Let_rec_unencodeable let (uu___is_Let_rec_unencodeable : Prims.exn -> Prims.bool) = fun projectee -> @@ -7675,16 +7676,19 @@ let (encode_modul : let uu___5 = get_env modul.FStarC_Syntax_Syntax.name tcenv1 in FStarC_SMTEncoding_Env.reset_current_module_fvbs uu___5 in let encode_signature env1 ses = - FStarC_Compiler_List.fold_left - (fun uu___5 -> - fun se -> - match uu___5 with - | (g, env2) -> - let uu___6 = encode_top_level_facts env2 se in - (match uu___6 with - | (g', env3) -> - ((FStarC_Compiler_List.op_At g g'), env3))) - ([], env1) ses in + let uu___5 = + FStarC_Compiler_List.fold_left + (fun uu___6 -> + fun se -> + match uu___6 with + | (g, env2) -> + let uu___7 = encode_top_level_facts env2 se in + (match uu___7 with + | (g', env3) -> + ((FStarC_Compiler_List.rev_append g' g), + env3))) ([], env1) ses in + match uu___5 with + | (g', env2) -> ((FStarC_Compiler_List.rev g'), env2) in let uu___5 = encode_signature { diff --git a/src/smtencoding/FStarC.SMTEncoding.Encode.fst b/src/smtencoding/FStarC.SMTEncoding.Encode.fst index 7d813f53411..a3ebb108bcc 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Encode.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Encode.fst @@ -112,12 +112,12 @@ let prims = let app = mk_Apply app [var] in let vars = vars @ [var] in let axiom_name = axiom_name ^ "." ^ (string_of_int (vars |> List.length)) in - axioms @ [Util.mkAssume (mkForall rng ([[app]], vars, mk_IsTotFun app), None, axiom_name)], + Util.mkAssume (mkForall rng ([[app]], vars, mk_IsTotFun app), None, axiom_name) :: axioms, app, vars ) ([tot_fun_axiom_for_x], xtok, []) all_vars_but_one in - axioms + List.rev axioms in let rel_body = @@ -598,9 +598,12 @@ let encode_top_level_val uninterpreted env us fv t quals = else decls, env let encode_top_level_vals env bindings quals = + let decls, env = bindings |> List.fold_left (fun (decls, env) lb -> let decls', env = encode_top_level_val false env lb.lbunivs (BU.right lb.lbname) lb.lbtyp quals in - decls@decls', env) ([], env) + List.rev_append decls' decls, env) ([], env) + in + List.rev decls, env exception Let_rec_unencodeable @@ -1954,9 +1957,12 @@ let encode_modul tcenv modul = then BU.print2 "+++++++++++Encoding externals for %s ... %s declarations\n" name (List.length modul.declarations |> string_of_int); let env = get_env modul.name tcenv |> reset_current_module_fvbs in let encode_signature (env:env_t) (ses:sigelts) = + let g', env = ses |> List.fold_left (fun (g, env) se -> let g', env = encode_top_level_facts env se in - g@g', env) ([], env) + List.rev_append g' g, env) ([], env) + in + List.rev g', env in let decls, env = encode_signature ({env with warn=false}) modul.declarations in give_decls_to_z3_and_set_env env name decls;