remove StageRank and instead introduce int ConfigVar ranks

ProConPy/config_var.py

@@ -7,7 +7,6 @@
 from ProConPy.dummy_widget import DummyWidget
 from ProConPy.dev_utils import ProConPyError, DEBUG
 from ProConPy.stage import Stage
-from ProConPy.stage_rank import StageRank
 
 
 logger = logging.getLogger(f"  {__name__.split('.')[-1]}")
@@ -96,10 +95,9 @@ def __init__(self, name, default_value=None, widget_none_val=None, hide_invalid=
 
         # The rank of a ConfigVar indicates the order of the Stage it belongs to. The lower 
         # the rank, the earlier the Stage is in the sequence of Stages and thus the higher 
-        # the precedence of the ConfigVar in CSP solver. The rank is set when the stage the
-        # ConfigVar belongs to is enabled. If a ConfigVar belongs to multiple stages, its rank
-        # depends on which execution trace is being followed.
-        self._rank = StageRank(None)
+        # the precedence of the ConfigVar in CSP solver. The ranks are determined by the
+        # CSP solver during initialization and via full traversal of the stage tree.
+        self._rank = None
 
         # properties for instances that have finite options
         self._options = []
@@ -204,9 +202,8 @@ def rank(self):
     @rank.setter
     def rank(self, new_rank):
         """Set the rank of the variable. This method is called by the Stage class when the stage is enabled."""
-        assert isinstance(new_rank, StageRank), "new_rank must be a StageRank"
-        assert new_rank.is_none() or self._rank.is_none() or new_rank == self._rank, \
-            "Cannot change the rank of a ConfigVar before resetting it."
+        assert self._rank is None, "Cannot reassign the rank of a variable"
+        assert isinstance(new_rank, int), "new_rank must be an integer"
         self._rank = new_rank
 
     @property
@@ -223,7 +220,7 @@ def is_guard_var(self, value):
     @property
     def is_aux_var(self):
         """Returns True if this variable is an auxiliary variable of the current stage."""
-        return Stage.active() is not None and Stage.active().rank == self._rank and self._widget.disabled is True
+        return Stage.active() is not None and self in Stage.active()._aux_varlist
 
     @property
     def options(self):

ProConPy/csp_solver.py

@@ -1,10 +1,9 @@
 import logging
-from z3 import Solver, sat, unsat, BoolRef, Or
-from z3 import BoolRef
+from z3 import Solver, Optimize, sat, unsat, Or
+from z3 import BoolRef, Int
 from z3 import z3util
 
 from ProConPy.dev_utils import ConstraintViolation
-from ProConPy.stage_rank import StageRank
 from ProConPy.csp_utils import TraversalLock
 from ProConPy.out_handler import handler as owh
 
@@ -103,22 +102,102 @@ def initialize(self, cvars, relational_constraints, first_stage):
         # Store the relational constraints
         self._relational_constraints = relational_constraints
 
+        # Determine variable ranks and ensure variable precedence is consistent
+        self._determine_variable_ranks(first_stage, cvars)
+
         # Construct constraint hypergraph and add constraints to solver
         self._process_relational_constraints(cvars)
 
-        # Determine the ranks of the stages
-        self._determine_stage_ranks(first_stage, 0, cvars)
-
-        # Look for conflicts in precedence of variables
-        #todo self._check_variable_precedence(cvars, first_stage)
-
         # Having read in the constraints, update validities of variables that have options:
         for var in cvars.values():
             if var.has_options():
                 var.update_options_validities()
 
         self._initialized = True
         logger.info("CspSolver initialized.")
+
+    def _determine_variable_ranks(self, stage, cvars):
+
+        # Solver to check if a consistent ranking of variables is possible
+        s = Solver()
+
+        # Instantiate temporary rank variables for each config variable to determine their ranks
+        [Int(f'{var}_rank') for var in cvars]
+
+        # The maximum rank
+        max_rank = Int('max_rank')
+
+        while stage is not None:
+
+            varlist = stage._varlist
+            assert len(varlist) > 0, "Stage has no variables."
+
+            curr_rank = Int(f'{varlist[0]}_rank')
+
+            # All ranks must be nonnegative and less than or equal to the maximum rank
+            s.add([0 <= curr_rank, curr_rank <= max_rank])
+
+            # All stage vars must have the same rank
+            for var in varlist[1:]:
+                s.add(curr_rank == Int(f'{var}_rank'))
+
+            # The next stage in stage tree (via full DFS traversal)
+            dfs_next_stage = stage.get_next(full_dfs=True)
+            if dfs_next_stage is None:
+                break
+            elif dfs_next_stage.has_condition():
+                condition = dfs_next_stage._condition
+                # Skip the guard and move on to its first child as the next stage
+                dfs_next_stage = dfs_next_stage.get_next(full_dfs=True)
+                # Now, process the guard variables.
+                if isinstance(condition, BoolRef):
+                    guard_vars = [cvars[var.sexpr()] for var in z3util.get_vars(condition)]
+                    for guard_var in guard_vars:
+                        # Mark guard variables
+                        guard_var.is_guard_var = True
+                        # All guard variables must have a lower rank than the variables in the next stage:
+                        s.add(Int(f'{guard_var}_rank') < Int(f'{dfs_next_stage._varlist[0]}_rank'))
+
+            # Find out the stage that would follow the current stage in an actual run.
+            true_next_stage = dfs_next_stage
+            if not(stage.is_sibling_of(dfs_next_stage) or stage.is_ancestor_of(dfs_next_stage)):
+                ancestor = stage._parent
+                while ancestor is not None:
+                    if (not ancestor.has_condition()) and ancestor._right is not None:
+                        true_next_stage = ancestor._right
+                        break
+                    ancestor = ancestor._parent
+
+            # All variables in the current stage must have a lower rank than the variables in the (true) next stage:
+            s.add(curr_rank < Int(f'{true_next_stage._varlist[0]}_rank'))
+
+            for aux_var in stage._aux_varlist:
+                # All auxiliary variables must have a higher rank than the variables in the current stage:
+                s.add(curr_rank < Int(f'{aux_var}_rank'))
+                # All auxiliary variables must have a lower rank than the variables in the (true) next stage:
+                s.add(Int(f'{aux_var}_rank') < Int(f'{true_next_stage._varlist[0]}_rank'))
+
+
+            # Check if the current stage is consistent
+            if s.check() == unsat:
+                raise RuntimeError("Inconsistent variable ranks encountered.")
+
+            # continue dfs traversal:
+            stage = dfs_next_stage
+
+        # Now minimize the maximum rank (This is optional and can be removed if performance becomes an issue)
+        opt = Optimize()
+        opt.add(s.assertions())
+        opt.minimize(max_rank)
+        opt.check()
+        model = opt.model()
+
+        for var in cvars:
+            try:
+                cvars[var].rank = model.eval(Int(f'{var}_rank')).as_long()
+            except AttributeError:
+                # This variable is not contained by any stage. Set its rank to max_rank + 1
+                cvars[var].rank = model.eval(Int('max_rank')).as_long() + 1
 
     def _process_relational_constraints(self, cvars):
         """Process the relational constraints to construct a constraint graph and add constraints
@@ -152,86 +231,6 @@ def _process_relational_constraints(self, cvars):
             for var in constr_vars:
                 self._cgraph[var].update(constr_vars - {var})
 
-    def _determine_stage_ranks(self, stage, rank, cvars):
-        """Recursive depth-first traversal of the stage tree to determine the rank of the stages
-        and to determine which of the variables appear in guards of the stages."""
-
-        # set rank
-        stage.rank = StageRank(rank)
-
-        logger.debug("Traversing stage: %s, rank: %s", stage, rank)
-
-        # flag variables that appear in guards
-        if stage.has_condition():
-            assert stage.has_children(), (
-                f"The stage {stage} is guarded but has no children."
-            )
-
-            guard = stage._condition
-            if isinstance(guard, BoolRef):
-                guard_vars = [cvars[var.sexpr()] for var in z3util.get_vars(guard)]
-                for var in guard_vars:
-                    var.is_guard_var = True
-
-        # move on to the following stage
-        stage = stage.get_next(full_dfs=True)
-        if stage is not None:
-            self._determine_stage_ranks(stage, rank+1, cvars)
-
-
-    #tododef _check_variable_precedence(self, cvars, first_stage):
-    #todo    """Check the precedence of the variables. The precedence of the variables is determined by the
-    #todo    rank of the stages in which the variables appear. The relational constraints and options specs
-    #todo    must adhere to the precedence of the variables."""
-
-    #todo    # Now that all stages are traversed and ranks are determined, traverse them again to make sure
-    #todo    # that guard variables have higher precedence than the variables in the stages they guard.
-    #todo    stage = first_stage
-    #todo    while stage is not None:
-    #todo        if stage.is_guarded():
-    #todo            guard = stage._activation_guard
-    #todo            if isinstance(guard, BoolRef):
-    #todo                guard_vars = [cvars[var.sexpr()] for var in z3util.get_vars(guard)]
-    #todo                for var in guard_vars:
-    #todo                    assert var.is_guard_var, (
-    #todo                        f"The variable {var} appears in the guard of stage {stage} but is not a guard variable."
-    #todo                    )
-    #todo                    assert all(var.max_rank < stage_var.min_rank for stage_var in stage._varlist), (
-    #todo                        f"The guard variable {var} has lower precedence than the stage it guards."
-    #todo                    )
-    #todo        # move on to the following stage
-    #todo        stage = stage.get_following_stage(visit_all=True)
-
-    #todo    for var in cvars.values():
-
-    #todo        # Confirm that each variable has either higher or lower precedence than its related variables
-    #todo        # (i.e., no variable has both higher and lower precedence than another variable)
-    #todo        if var.has_related_vars():
-    #todo            if var.max_rank is None:
-    #todo                assert var.min_rank is None, (
-    #todo                    f"Variable has a min_rank but no max_rank: {var}."
-    #todo                )
-    #todo                continue
-    #todo            for related_var in var._related_vars:
-    #todo                if related_var.max_rank is None:
-    #todo                    assert related_var.min_rank is None, (
-    #todo                        f"\tVariable has a min_rank but no max_rank: {var}."
-    #todo                    )
-    #todo                    continue
-    #todo                assert var.max_rank <= related_var.min_rank or related_var.max_rank <= var.min_rank, (
-    #todo                    f"Variable precedence conflict: {var} and {related_var}."
-    #todo                )
-    #todo        
-    #todo        # Confirm that each variable has higher precedence (lower rank) than its dependent variables
-    #todo        for dependent_var in var._dependent_vars:
-    #todo            assert var.max_rank is not None, (
-    #todo                f"Variable has a dependent variable but doesn't belong to any stage: {var}."
-    #todo            )
-    #todo            if dependent_var.min_rank is not None:
-    #todo                assert var.max_rank < dependent_var.min_rank, (
-    #todo                    f"Variable precedence conflict: {var} and {dependent_var}."
-    #todo                )
-
     @property
     def initialized(self):
         """Return True if the CSP solver is initialized."""

ProConPy/stage.py

@@ -10,7 +10,6 @@
 from ProConPy.out_handler import handler as owh
 from ProConPy.dev_utils import DEBUG
 from ProConPy.stage_stat import StageStat
-from ProConPy.stage_rank import StageRank
 
 logger = logging.getLogger("\t" + __name__.split(".")[-1])
 
@@ -101,6 +100,22 @@ def has_condition(self):
     def children_have_conditions(self):
         """Return True if any of the children of the node have conditions."""
         return any([child.has_condition() for child in self._children])
+
+    def is_sibling_of(self, node):
+        """Return True if the node is a sibling of the given node."""
+        return self._parent is node._parent
+
+    def is_descendant_of(self, other):
+        """Return True if the node is a descendant of the given other node."""
+        node = self
+        while (node := node._parent) is not None:
+            if node is other:
+                return True
+        return False
+
+    def is_ancestor_of(self, other):
+        """Return True if the node is an ancestor of the given other node."""
+        return other.is_descendant_of(self)
 
     @property
     def title(self):
@@ -167,7 +182,7 @@ def __init__(self, title, parent, condition):
         super().__init__(title, parent)
         self._condition = condition
 
-    def get_next(self, full_dfs):
+    def get_next(self, full_dfs=None):
         """Return the next node in the stage tree, which is always the first child for a guard node."""
         return self._children[0]
 
@@ -244,10 +259,13 @@ def __init__(
 
         assert (
             widget is not None
-        ), f'The unguarded "{self._title}" stage must have a widget.'
+        ), f'The "{title}" stage must have a widget.'
+        assert isinstance(
+            varlist, list
+        ), f'The "{title}" stage must have a variable list.'
         assert (
             len(varlist) > 0
-        ), f'The unguarded "{self._title}" stage must have a non-empty variable list.'
+        ), f'The "{title}" stage must have a non-empty variable list.'
 
         super().__init__(title, parent)
 
@@ -259,7 +277,6 @@ def __init__(
         self._auto_proceed = auto_proceed
         self._auto_set_default_value = auto_set_default_value
         self._auto_set_valid_option = auto_set_valid_option
-        self._rank = StageRank(None)  # to be set by the csp solver
 
         self._construct_observances()
 
@@ -302,21 +319,6 @@ def description(self):
     def enabled(self):
         return not self._disabled
 
-    @property
-    def rank(self):
-        if self.is_first():
-            return StageRank(0)
-        return self._rank
-
-    @rank.setter
-    def rank(self, new_rank):
-        assert self._rank.is_none(), "The rank of the stage is already set."
-        assert isinstance(new_rank, StageRank), "The rank must be an integer."
-        assert not self.is_first() or new_rank == StageRank(
-            0
-        ), "The rank of the first stage must be 0."
-        self._rank = new_rank
-
     def _construct_observances(self):
         for var in self._varlist:
             var.observe(
@@ -462,13 +464,6 @@ def _disable(self):
         self._disabled = True
         self.refresh_status()
 
-        # Reset the rank of the variables in the stage
-        if self.status != StageStat.COMPLETE and self.status != StageStat.SEALED:
-            for var in self._varlist:
-                var.rank = StageRank(None)
-            for var in self._aux_varlist:
-                var.rank = StageRank(None)
-
     @owh.out.capture()
     def _enable(self):
         """Activate the stage, allowing the user to set the parameters in the varlist."""
@@ -487,12 +482,6 @@ def _enable(self):
         if len(self._varlist) == 0:
             self._proceed()
 
-        # Set the rank of the variables in the stage
-        for var in self._varlist:
-            var.rank = self.rank
-        for var in self._aux_varlist:
-            var.rank = self.rank
-
         # If a default vaulue is assigned, set the value of the ConfigVar to the default value
         # Otherwise, set the value of the ConfigVar to the valid option if there is only one.
         if self._auto_set_default_value is True: