[lib] MCLA/CLU: Save some cycles when there is no more solution for a given...

[lib] MCLA/CLU: Save some cycles when there is no more solution for a given step; Auto-adjust max_step until max_user_step is reached

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

@@ -1680,9 +1680,9 @@ class CLUnfolder(object):
             # Return the satisfiability status in all cases
             return satisfiability_test
 
-    def squery_solve(self, vvars, max_step, max_sol):
-        """Search max_sol number of solutions with max_step steps, involving vvars
-        (frontiers) variables of interest.
+    def squery_solve(self, vvars, max_step, max_sol, max_user_step=None):
+        """Search max_sol number of solutions with max_step steps, involving
+        variables of interest (frontiers).
 
         Assert a query is loaded (start_condition, inv_condition, final_condition)
 
@@ -1696,13 +1696,38 @@ class CLUnfolder(object):
             __steps_before_check can't be >= max_step.
             max_step can't be >= to __precomputed_variant_constraints.
 
+        .. note:: À propos de l'auto-ajustement du nombre maximal d'étapes (max_step)
+            à l'aide de max_user_step:
+
+            Lorsqu'il n'y a plus de solutions pour 1 étape donnée, mais que ce
+            nombre d'étapes est < au nombre fixé par l'utilisateur, on peut
+            bénéficier des shifts précédents sur le modèle et on éviter de
+            reconstruire le problème pour un nouveau test de satisfiabilité à
+            l'étape suivante.
+            Le fait de rechercher 1 propriété est déjà un test de satisfiabilité.
+            Rien de plus ou de moins n'est fait par le solveur.
+            Concrètement squery_solve est capable d'incrémenter tout seul le
+            max_step jusqu'au max_user_step durant l'étape de solving.
+
+            Aucun risque d'augmenter le min_step lors de l'étape d'élagage d'une
+            solution connue car :
+            - le pb n'est pas moins contraint que lorsqu'il a trouvé la solution
+            à élaguer => 1 solution au moins est toujours retournée.
+            - max_user_step est laissé à None
+
+
         :param max_step: bounded horizon for computations
         :param max_sol: The maximum number of solutions to be returned
         :param vvars: Variables for which solutions must differ.
             In practice, it is a list with the values (Dimacs code)
             of all frontier places of the system.
+        :key max_user_step: (Optional) If max_user_step is set, we increment the
+            current max_step until it reaches max_user_step. This saves some
+            cycles by reusing the current CLUnfolder for an extra step.
+            .. seealso:: :meth:`cadbiom.models.clause_constraints.mcl.MCLAnalyser.__mac_exhaustive_search`
         :type max_step: <int>
         :type max_sol: <int>
+        :type max_user_step: <int> or None
         :type vvars: <list <int>>
         :return: RawSolution objects
             RawSolution objects contain a solution got from SAT solver with all
@@ -1763,7 +1788,18 @@ class CLUnfolder(object):
                     "max_step", max_step,
                     "current_step", self.__current_step
                 )
-                #raw_input("pause")
+                if (not temp_raw_solutions and max_user_step
+                    and max_step + 1 <= max_user_step):
+                        # No more solution for this step; if max_user_step is set
+                        # we increment the current max_step in order to reuse the
+                        # current CLUnfolder.
+                        max_step += 1
+                        LOGGER.info(
+                            "Solve:: Auto-adjust max_step from %s to %s ",
+                            max_step - 1,
+                            max_step
+                        )
+                        continue
 
                 raw_solutions += temp_raw_solutions
 

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

@@ -501,7 +501,7 @@ class MCLAnalyser(object):
         return self.unfolder.squery_is_satisfied(max_step)
 
 
-    def sq_solutions(self, query, max_step, max_sol, vvars):
+    def sq_solutions(self, query, max_step, max_sol, vvars, max_user_step=None):
         """Return a list of RawSolution objects
 
         This function is the lowest level function exploiting the solver results.
@@ -549,9 +549,11 @@ class MCLAnalyser(object):
         :param vvars: Variables for which solutions must differ.
             In practice, it is a list with the values (Dimacs code)
             of all frontier places of the system.
+        :key max_user_step: (Optional) See :meth:`__mac_exhaustive_search`.
         :type query: <MCLSimpleQuery>
         :type max_step: <int>
         :type vvars: <list <int>>
+        :type max_user_step: <int>
         :return: a list of RawSolutions from the solver
         :rtype: <list <RawSolution>>
 
@@ -568,7 +570,7 @@ class MCLAnalyser(object):
         #    variant_prop, dim_variant, steps_before_check
         self.unfolder.init_with_query(query, check_query=False)
         # go
-        return self.unfolder.squery_solve(vvars, max_step, max_sol)
+        return self.unfolder.squery_solve(vvars, max_step, max_sol, max_user_step=max_user_step)
 
 
     def sq_frontier_solutions(self, query, max_step, max_sol):
@@ -620,17 +622,22 @@ class MCLAnalyser(object):
                 in self.sq_solutions(query, max_step, max_sol, vvars)]
 
 
-    def __sq_dimacs_frontier_solutions(self, query, max_step, max_sol):
+    def __sq_dimacs_frontier_solutions(self, query, max_step, max_sol, max_user_step=None):
         """Search set of minimal solutions for the given query, with a maximum of steps
 
         DimacsFrontierSol objects provides some interesting attributes like:
         activated_frontier_values (raw values of literals).
         Note: FrontierSolution are of higher level without such attributes.
 
-        @param query: MCLSimpleQuery
-        @param max_step: int - Number of steps allowed in the unfolding;
+        :param query: Query
+        :param max_step: Number of steps allowed in the unfolding;
             the horizon on which the properties must be satisfied
-        @param max_sol: int - max number of solutions for each solve
+        :param max_sol: Max number of solutions for each solve
+        :key max_user_step: (Optional) See :meth:`__mac_exhaustive_search`
+        :type query: <MCLSimpleQuery>
+        :type max_step: <int>
+        :type max_sol: <int>
+        :type max_user_step: <int>
         :return: Tuple of unique DimacsFrontierSol objects built from RawSolutions
             from the solver.
             .. note:: Unicity is based on the set of activated frontier values.
@@ -638,7 +645,7 @@ class MCLAnalyser(object):
         """
         vvars = self.unfolder.frontier_values
         # sq_solutions() returns <list <RawSolution>>
-        raw_sols = self.sq_solutions(query, max_step, max_sol, vvars)
+        raw_sols = self.sq_solutions(query, max_step, max_sol, vvars, max_user_step=max_user_step)
         # Get unique DimacsFrontierSol objects from RawSolution objects
         dimacfrontsol = DimacsFrontierSol.get_unique_dimacs_front_sols_from_raw_sols(raw_sols)
 
@@ -647,7 +654,7 @@ class MCLAnalyser(object):
                 "MCLA: Nb queried: %s, steps: %s\n"
                 "\tget: %s, unique: %s\n"
                 "\tactivated fronts per dimacfrontsol: %s",
-                max_sol, max_step,
+                max_sol, self.unfolder.current_step,
                 len(raw_sols), len(dimacfrontsol),
                 [len(sol) for sol in dimacfrontsol]
             )
@@ -680,8 +687,11 @@ class MCLAnalyser(object):
         beaucoup plus de places (ces places excédentaires sont dispensables).
 
         :param query: Current query.
-        :param max_user_step: Number of steps allowed in the unfolding;
-            the horizon on which the properties must be satisfied
+        :param max_user_step: Number of steps allowed by the user in the unfolding;
+            the horizon on which the properties must be satisfied.
+            This argument is also used to auto-adjust max_step for an extra step
+            in CLUnfolder.
+            .. seealso:: :meth:`cadbiom.models.clause_constraints.mcl.CLUnfolder.squery_solve`
         :type query: <MCLSimpleQuery>
         :type max_user_step: <int>
         :return: A generator of FrontierSolution objects which are a wrapper of
@@ -722,43 +732,35 @@ class MCLAnalyser(object):
             # Solutions differ on frontiers: Search only 2 different solutions
             # to avoid all activated solutions
             # Get <tuple <DimacsFrontierSol>>
-            dimacs_front_sol = self.__sq_dimacs_frontier_solutions(query, min_step, 2)
+            dimacs_front_sol = self.__sq_dimacs_frontier_solutions(
+                query,
+                min_step,
+                2,
+                max_user_step=max_user_step
+            )
+
+            # Self-adjustment of min_step/max_step may have taken place;
+            # resynchronization of values:
+            # __steps_before_check can't be >= min_step
+            # (see squery_is_satisfied() and squery_solve())
+            # __steps_before_check should be min_step - 1 to avoid a maximum of
+            # useless checks from (min_step to current_step).
+            min_step = self.unfolder.current_step
+            query.steps_before_check = min_step - 1
+
             if not dimacs_front_sol:
-                # If we do not want to self-adjust steps, just break the loop
-                # break
-
-                LOGGER.info("MCLA: NOT FOUND -> satis test; current step %s",
-                            self.unfolder.current_step)
-                if self.unfolder.current_step == max_user_step:
-                    # Cosmetic break, avoid to do useless test
-                    break
-
-                ## TEST
-                ## Make autoadjustment... of max_steps during the solving!
-                ## Juste appeler squery_solve avec les memes parametres mais
-                ## min_step augmenté de 1
-                ## en restant inférieur au nb d'étapes demandées à l'origine
-                ## => on bénéficie des shifts précédents et on évite de reconstruire le problème...
-
-                # Hack: reuse the current Unfolder (without init with query)
-                # => do not do this at home!
-                self.unfolder._CLUnfolder__locked = False
-                # Avoid a new test of satisfiability on the same current_step
-                # (we already know that there is no more solution for it)
-                # => increment __steps_before_check
-                self.unfolder._CLUnfolder__steps_before_check += 1
-                ret = self.unfolder.squery_is_satisfied(max_user_step)
-                if not ret:
-                    # The problem is definitively not satisfiable in the given
-                    # number of steps
-                    break
-                # __steps_before_check can't be >= min_step
-                # (see squery_is_satisfied() and squery_solve())
-                min_step = self.unfolder.current_step
-                query.steps_before_check = min_step - 1
-
-                print("testing AUTO CORRECT max step:", min_step)
-                continue
+                # No more solution
+                # Note that self-adjust steps is made via max_user_step
+                # argument of CLUnfolder.squery_solve
+
+                LOGGER.info(
+                    "MCLA:__mac_exhaustive_search: No more solution; current step %s",
+                    self.unfolder.current_step
+                )
+
+                assert (self.unfolder.current_step == max_user_step)
+                # just break the loop
+                break
 
 
             # Get the solution with the less number of activated states