[lib] Rename __list_variant_constraints to __precomputed_variant_constraints; Update doc

max_step can't be >= to __precomputed_variant_constraints

library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py

@@ -99,10 +99,14 @@ init_forward_unfolding():
             Query data
         - __invariant_constraints:
             List of Query data
-        - __list_variant_constraints:
+        - __precomputed_variant_constraints:
             Query data (automatic merge of textual and DIMACS forms)
         - __variant_constraints:
-            Initilized with the first item of __list_variant_constraints
+            Initialized with the first item of __precomputed_variant_constraints
+        - __precomputed_dynamic_constraints:
+            Initialized with the whole previously shifted system
+            if the size of the system hasn't changed, and if no auxiliary
+            clauses has been added meanwhile.
 
     Shifted attributes with __shift_step (nb of variables in the system):
         - __forward_init_dynamic(): __dynamic_constraints:
@@ -138,8 +142,8 @@ shift():
         - __shift_dynamic(): __dynamic_constraints:
             Shift + append of the last element of __dynamic_constraints
         - __shift_variant(): __variant_constraints:
-            Shift clauses of the current step in __list_variant_constraints, and
-            append them to __variant_constraints.
+            Shift clauses of the current step in __precomputed_variant_constraints,
+            and append them to __variant_constraints.
         - __shift_invariant()
             ...
         - __shift_final()
@@ -359,7 +363,7 @@ class CLUnfolder(object):
         """Reset the unfolder before a new query
 
         Reset only properties and dimacs clauses from the current query;
-        AND __list_variant_constraints.
+        AND __precomputed_variant_constraints.
 
         => __initial_constraints, __final_constraints, __invariant_constraints,
         __variant_constraints and __dynamic_constraints ARE NOT reset here
@@ -379,7 +383,7 @@ class CLUnfolder(object):
         self.__variant_property = None            # list<logic formulas>
         self.__dimacs_variant = None              # list<list<DIMACS clauses>>
         # list of variant temporal constraints in Dimacs ground code
-        self.__list_variant_constraints = None    # list<list<DIMACS clauses>>
+        self.__precomputed_variant_constraints = None  # list<list<DIMACS clauses>>
 
         # If this function is called from the constructor,
         # the following variables are just redefined here.
@@ -918,8 +922,8 @@ class CLUnfolder(object):
     def __shift_variant(self):
         """Shift variant property - depends on unfolding direction
 
-        Shift clauses of the current step in __list_variant_constraints, and
-        append them to __variant_constraints.
+        Shift clauses of the current step in __precomputed_variant_constraints,
+        and append them to __variant_constraints.
 
         .. warning:: Refactor note: unclear function. No apparent reason for
             only the first clause to be shifted...
@@ -937,11 +941,11 @@ class CLUnfolder(object):
 
         .. note:: Called by shift()
         """
-        if not self.__list_variant_constraints:
+        if not self.__precomputed_variant_constraints:
             return
         if self.__shift_direction == "FORWARD":
             # Constraint t0 already included from the query during initialisation
-            current_constraint = self.__list_variant_constraints[self.__current_step]
+            current_constraint = self.__precomputed_variant_constraints[self.__current_step]
             # Shift constraints at current step and append them to __variant_constraints
             for clause in current_constraint:
                 s_clause = self.__m_shift_clause(clause, self.__current_step)
@@ -963,8 +967,8 @@ class CLUnfolder(object):
                 Shift + append of the last element of __dynamic_constraints
             - __invariant_constraints[-1] (last element)
                 Shift + append of the last element of __invariant_constraints
-            - __list_variant_constraints[current_step]
-                Shift clauses of the current step in __list_variant_constraints,
+            - __precomputed_variant_constraints[current_step]
+                Shift clauses of the current step in __precomputed_variant_constraints,
                 and append them to __variant_constraints.
             - __final_constraints if __shift_direction is "FORWARD"
             - __initial_constraints if __shift_direction is "BACKWARD"
@@ -1166,27 +1170,27 @@ class CLUnfolder(object):
             The two variant constraint forms must be compatible (same length) in
             order to allow a merge.
 
-        self.__list_variant_constraints:
+        self.__precomputed_variant_constraints:
             Built here and is used later to shift current variant properties
             and update self.__variant_constraints in __shift_variant().
 
         self.__variant_constraints:
             - the only element passed to the solver.
-            - initilised with the first item of self.__list_variant_constraints
+            - initilised with the first item of self.__precomputed_variant_constraints
         """
         # coding of variant properties
         # Take __variant_property in priority on __dimacs_variant
         if self.__variant_property:
-            self.__list_variant_constraints = list()
+            self.__precomputed_variant_constraints = list()
 
             for prop in self.__variant_property:
                 # compile initial (X0) property into numeric form
                 # For each property in step of __variant_property
-                self.__list_variant_constraints.append(
+                self.__precomputed_variant_constraints.append(
                     [self.__code_clause(clause)
                      for clause in self.__compile_event(prop)]
                 )
-                print(self.__list_variant_constraints)
+                print(self.__precomputed_variant_constraints)
 
             if self.__dimacs_variant:
                 # Add DIMACS aux clauses initial properties
@@ -1199,26 +1203,26 @@ class CLUnfolder(object):
 
                 # Merge together all steps content
                 # Ex:
-                # __list_variant_constraints due to __variant_property convertion:
+                # __precomputed_variant_constraints due to __variant_property convertion:
                 # [[], [[4]], [], []]
                 # __dimacs_variant:
                 # [[], [[4]], [[6], [7]], []]
                 # Result:
                 # [[], [[4], [4]], [[6], [7]], []]
-                self.__list_variant_constraints = \
+                self.__precomputed_variant_constraints = \
                     [list(it.chain(*cpl)) for cpl
-                     in zip(self.__dimacs_variant, self.__list_variant_constraints)]
+                     in zip(self.__dimacs_variant, self.__precomputed_variant_constraints)]
 
         elif self.__dimacs_variant:
             # No __variant_property, keep only __dimacs_variant
-            self.__list_variant_constraints = self.__dimacs_variant
+            self.__precomputed_variant_constraints = self.__dimacs_variant
 
         # Initialisation
-        if self.__list_variant_constraints:
+        if self.__precomputed_variant_constraints:
             if self.__shift_direction == "FORWARD":
                 # For now, keep only the events of the first step (t0)
                 # Other steps are taken during shift() calls
-                self.__variant_constraints = self.__list_variant_constraints[0]
+                self.__variant_constraints = self.__precomputed_variant_constraints[0]
             elif  self.__shift_direction == "BACKWARD":
                 raise MCLException("Not yet implemented")
             else:
@@ -1242,10 +1246,14 @@ class CLUnfolder(object):
                 Query data
             - __invariant_constraints:
                 List of Query data
-            - __list_variant_constraints:
+            - __precomputed_variant_constraints:
                 Query data (automatic merge of textual and DIMACS forms)
             - __variant_constraints:
-                Initilized with the first item of __list_variant_constraints
+                Initialized with the first item of __precomputed_variant_constraints
+            - __precomputed_dynamic_constraints:
+                Initialized with the whole previously shifted system
+                if the size of the system hasn't changed, and if no auxiliary
+                clauses has been added meanwhile.
 
         Shifted attributes with __shift_step (nb of variables in the system):
             - __dynamic_constraints:
@@ -1447,7 +1455,8 @@ class CLUnfolder(object):
             is not tested for interesting variables like in squery_solve().
 
         .. note:: This function checks and corrects incoherent data on step number.
-            __steps_before_check can't be >= max_step
+            __steps_before_check can't be >= max_step.
+            max_step can't be >= to __precomputed_variant_constraints.
 
         :param max_step: The horizon on which the properties must be satisfied.
         :type max_step: <int>
@@ -1455,8 +1464,8 @@ class CLUnfolder(object):
         # Initialization
         self.init_forward_unfolding()
         # Horizon adjustment
-        if self.__list_variant_constraints:
-            max_step = min(max_step, len(self.__list_variant_constraints)-1) ## TODO:  -1 ?
+        if self.__precomputed_variant_constraints:
+            max_step = min(max_step, len(self.__precomputed_variant_constraints)-1)
 
         if self.__invariant_property and not self.__final_property:
             # 1 satisfiability test is made only after all shift() calls for each step
@@ -1511,7 +1520,8 @@ class CLUnfolder(object):
         Otherwise, 1 test is made for each remaining step after each shift() call.
 
         .. note:: This function checks and corrects incoherent data on step number.
-            __steps_before_check can't be >= max_step
+            __steps_before_check can't be >= max_step.
+            max_step can't be >= to __precomputed_variant_constraints.
 
         :param max_step: bounded horizon for computations
         :param max_sol: The maximum number of solutions to be returned
@@ -1529,8 +1539,8 @@ class CLUnfolder(object):
         # Initialization
         self.init_forward_unfolding()
         # Horizon adjustment
-        if self.__list_variant_constraints:
-            max_step = min(max_step, len(self.__list_variant_constraints)-1) ## TODO:  -1 ?
+        if self.__precomputed_variant_constraints:
+            max_step = min(max_step, len(self.__precomputed_variant_constraints)-1)
 
         if self.__invariant_property and not self.__final_property:
             # Shift all remaining steps

library/cadbiom/models/clause_constraints/mcl/TestCLUnfolder.py

@@ -462,7 +462,7 @@ def test_init_forward(feed_mclanalyser, textual_properties, numerical_properties
     self.__dimacs_variant = None              # list<list<DIMACS clauses>>
 
     CLUnfolder attributes that contain clauses:
-    self.__list_variant_constraints = None    # list<list<DIMACS clauses>>
+    self.__precomputed_variant_constraints = None  # list<list<DIMACS clauses>>
 
     dynamic_constraints => __dynamic_constraints
     initial_constraints => __initial_constraints