From 3265ba578b31d9096cb9edc378d89798eafd9f7a Mon Sep 17 00:00:00 2001 From: Alper Altuntas Date: Wed, 25 Mar 2026 15:41:07 -0600 Subject: [PATCH 1/2] minor optimizations in csp_solver (deque for BFS, id-based set lookups, fast path in apply_options_assertions) --- .gitignore | 3 +++ ProConPy/csp_solver.py | 57 +++++++++++++++++++++--------------------- 2 files changed, 32 insertions(+), 28 deletions(-) diff --git a/.gitignore b/.gitignore index e99221a..f9ac9a0 100644 --- a/.gitignore +++ b/.gitignore @@ -159,3 +159,6 @@ internal/sdb_*.json # netcdf files *.nc + +# TopoLibrary files +mom6_bathy_notebooks/TopoLibrary/ \ No newline at end of file diff --git a/ProConPy/csp_solver.py b/ProConPy/csp_solver.py index 465855a..c367468 100644 --- a/ProConPy/csp_solver.py +++ b/ProConPy/csp_solver.py @@ -1,4 +1,5 @@ import logging +from collections import deque from z3 import Solver, Optimize, sat, unsat, Or from z3 import BoolRef, Int from z3 import z3util @@ -69,11 +70,11 @@ def _refresh_solver(self): be more efficient than the initial approach of using push/pop to manage the solver. """ self._solver.reset() - self._solver.add([asrt for asrt, _ in self._relational_constraints.items()]) + self._solver.add(list(self._relational_constraints)) for scope in self._past_assignment_assertions: - self._solver.add([asrt for _, asrt in scope.items()]) + self._solver.add(list(scope.values())) for scope in self._past_options_assertions: - self._solver.add([asrt for _, asrt in scope.items()]) + self._solver.add(list(scope.values())) def initialize(self, cvars, relational_constraints, first_stage): """Initialize the CSP solver with relational constraints. The relational constraints are @@ -432,9 +433,9 @@ def retrieve_error_msg(self, var, new_value): s.set(":core.minimize", True) # apply past assertions for stage in self._past_assignment_assertions: - s.add([asrt for _, asrt in stage.items()]) + s.add(list(stage.values())) for stage in self._past_options_assertions: - s.add([asrt for _, asrt in stage.items()]) + s.add(list(stage.values())) # apply current assertions self.apply_assignment_assertions(s, exclude_var=var) self.apply_options_assertions(s) @@ -567,28 +568,23 @@ def _refresh_options_validities(self, var): """ # Queue of variables to be visited - queue = [neig for neig in self._cgraph[var] if neig.has_options()] + queue = deque([neig for neig in self._cgraph[var] if neig.has_options()]) # Set of all variables that have been queued queued = {var} | set(queue) # Traverse the constraint graph to refresh the options validities of all possibly affected variables while queue: - - # Pop the first variable from the queue - var = queue.pop(0) + var = queue.popleft() logger.debug("Refreshing options validities of %s.", var) - # Update the validities of the variable and extend the queue if necessary - validities_changed = var.update_options_validities() - if validities_changed: - extension = [ - neig - for neig in self._cgraph[var] - if neig.has_options() and neig not in queued - ] - queue.extend(extension) - queued.update(extension) + if not var.update_options_validities(): + continue + + for neig in self._cgraph[var]: + if neig.has_options() and neig not in queued: + queue.append(neig) + queued.add(neig) def apply_assignment_assertions(self, solver, exclude_var=None, exclude_vars=None): """Apply the assignment assertions to the given solver. The assignment assertions are @@ -611,11 +607,12 @@ def apply_assignment_assertions(self, solver, exclude_var=None, exclude_vars=Non ), "Cannot provide both exclude_var and exclude_vars." if exclude_vars: + exclude_ids = {id(v) for v in exclude_vars} solver.add( [ asrt for var, asrt in self._assignment_assertions.items() - if not any(exclude_var is var for exclude_var in exclude_vars) + if id(var) not in exclude_ids ] ) else: @@ -627,7 +624,7 @@ def apply_assignment_assertions(self, solver, exclude_var=None, exclude_vars=Non ] ) - def apply_options_assertions(self, solver, exclude_vars=[]): + def apply_options_assertions(self, solver, exclude_vars=()): """Apply the options assertions to the given solver. The options assertions are the assertions that are determined at the current stage but are the options for the variables of the future stages. The options assertions are added to the temporary assertions container @@ -641,13 +638,17 @@ def apply_options_assertions(self, solver, exclude_vars=[]): exclude_vars : list or set A list or set of variables for which the options assertions are not to be applied. """ - solver.add( - [ - asrt - for var, asrt in self._options_assertions.items() - if not any(exclude_var is var for exclude_var in exclude_vars) - ] - ) + if not exclude_vars: + solver.add(list(self._options_assertions.values())) + else: + exclude_ids = {id(v) for v in exclude_vars} + solver.add( + [ + asrt + for var, asrt in self._options_assertions.items() + if id(var) not in exclude_ids + ] + ) def register_options(self, var, new_options): """Register the new options for the given variable. The registry is made to the temporary From 6e3dbb7aeb8e5071e9211aec073ef4d7a5d39723 Mon Sep 17 00:00:00 2001 From: Alper Altuntas Date: Wed, 25 Mar 2026 15:47:35 -0600 Subject: [PATCH 2/2] add citation info --- README.md | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/README.md b/README.md index b710795..dd0536e 100644 --- a/README.md +++ b/README.md @@ -20,3 +20,25 @@ Welcome to **visualCaseGen**, an intuitive graphical user interface (GUI) design ## User Manual For detailed instructions on how to use visualCaseGen, including setup and configuration guidance, please refer to the [User Manual](https://esmci.github.io/visualCaseGen/). + +## Citing + +If you use visualCaseGen in your research, please cite it as follows: + +Altuntas, A., Simpson, I.R., Bachman, S.D., Venumuddula, M., Levis, S., Dobbins, B., Sacks, W.J. and +Danabasoglu, G., 2026. "visualCaseGen: An SMT-based Experiment Configurator for Community Earth System +Model." Journal of Open Source Software, 11(119), p.9130. doi: [10.21105/joss.09130](https://doi.org/10.21105/joss.09130). + +BibTeX entry: + +```bibtex +@article{altuntas2026visualcasegen, + title={visualCaseGen: An SMT-based Experiment Configurator for Community Earth System Model}, + author={Altuntas, Alper and Simpson, Isla R and Bachman, Scott D and Venumuddula, Manish and Levis, Samuel and Dobbins, Brian and Sacks, William J and Danabasoglu, Gokhan}, + journal={Journal of Open Source Software}, + volume={11}, + number={119}, + pages={9130}, + year={2026} +} +``` \ No newline at end of file