From ade6379345d0bdfb912e2db067d2af9197205bf5 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Sat, 29 Nov 2025 15:24:56 -0800 Subject: [PATCH] Explicitly store whether to use association lists Instead of checking for the presence of helper names each time we need to determine whether to use association lists, explicitly store a boolean flag indicating whether association list helpers are being used. --- backends/functional/smtlib_rosette.cc | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/backends/functional/smtlib_rosette.cc b/backends/functional/smtlib_rosette.cc index 9a64c203a..4396e6714 100644 --- a/backends/functional/smtlib_rosette.cc +++ b/backends/functional/smtlib_rosette.cc @@ -188,6 +188,7 @@ struct SmtrModule { Functional::IR ir; SmtrScope scope; std::string name; + bool use_assoc_list_helpers; std::optional input_helper_name; std::optional output_helper_name; @@ -196,7 +197,7 @@ struct SmtrModule { SmtrStruct state_struct; SmtrModule(Module *module, bool assoc_list_helpers) - : ir(Functional::IR::from_module(module)), scope(), name(scope.unique_name(module->name)), + : ir(Functional::IR::from_module(module)), scope(), name(scope.unique_name(module->name)), use_assoc_list_helpers(assoc_list_helpers), input_struct(scope.unique_name(module->name.str() + "_Inputs"), scope), output_struct(scope.unique_name(module->name.str() + "_Outputs"), scope), state_struct(scope.unique_name(module->name.str() + "_State"), scope) @@ -265,6 +266,9 @@ struct SmtrModule { void write_assoc_list_helpers(SExprWriter &w) { + if (!output_helper_name || !input_helper_name) + log_error("if using keyword helpers, both input and output helper names are expected"); + // Input struct keyword-based constructor. w.push(); w.open(list("define")); @@ -308,9 +312,7 @@ struct SmtrModule { output_struct.write_definition(w); state_struct.write_definition(w); - if (input_helper_name || output_helper_name) { - if (!output_helper_name || !input_helper_name) - log_error("if keyword helpers are enabled, both input and output helper names are expected"); + if (use_assoc_list_helpers) { write_assoc_list_helpers(w); }