[lib] CLUnfolder Fix: ability to check the validity of the given query

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

@@ -398,7 +398,57 @@ class CLUnfolder(object):
         self.__shift_direction = None     # FORWARD or BACKWARD
         self.__locked = False
 
-    def init_with_query(self, query):
+    def check_query(self, query):
+        """Check textual and DIMACS properties of the given query
+
+        If textual properties have changed since the last initialization of the
+        CLUnfolder, new auxiliary variables will be added to the dynamic system.
+
+        Also check if values of literals are in the limits of the dynamical
+        system (shift_step_init). If it's not the case, a ValueError exception
+        will be raised.
+
+        Called by:
+            :meth:`init_with_query`
+
+        :param query: Query built with start, invariant, final, variant properties
+            in textual and/or DIMACS forms.
+        :type query: <MCLSimpleQuery>
+        """
+        # Check textual properties
+        if (self.__initial_property != query.start_prop
+            or self.__final_property != query.final_prop
+            or self.__invariant_property != query.inv_prop
+            or self.__variant_property != query.variant_prop):
+            # System will be modified; Auxiliary clauses will be added
+            # Do not reload cached constraints
+            self.__include_aux_clauses_changed = True
+
+        # Check values of literals
+        values = set(it.chain(*query.dim_start))
+        values.update(it.chain(*query.dim_final))
+        values.update(it.chain(*query.dim_inv))
+        if query.dim_variant_prop:
+            # Handle empty steps:
+            # Ex: [[], [[4]], [[6], [7]], []]
+            g = (step for step in query.dim_variant_prop if step)
+            [values.update(it.chain(*step)) for step in g]
+
+        # Get all values that are not in the initial dynamic system
+        out_of_range_values = {val for val in values if abs(val) > self.shift_step_init}
+        if not out_of_range_values:
+            return
+
+        # The literal comes from an auxilary clause; not from the dynamic model.
+        # Since the auxiliary clauses are reset here, this literal is suspect
+        # and its use dangerous because its value is not reproductible.
+        raise ValueError(
+            "%s variable is not in the initial system.\n"
+            "Insertion of auxiliary variables is not allowed here."
+            % out_of_range_values
+        )
+
+    def init_with_query(self, query, check_query=True):
         """Initialise the unfolder with the given query
 
         Following attributes are used from the query:
@@ -411,8 +461,22 @@ class CLUnfolder(object):
         This compilation step is costly due to ANTLR performances...
 
         .. warning:: ALL textual properties are susceptible to add new auxiliary
-            variables in the system (increase shift_step).
+            variables in the system (increase shift_step). Thus, the system
+            will be rebuilt.
+
+        :param query: Query built with start, invariant, final, variant properties
+            in textual and/or DIMACS forms.
+        :key check_query: Check textual and DIMACS properties of the given query.
+
+            .. warning:: This option should be disable for performance reasons;
+                or if you know what you are doing.
+
+        :type query: <MCLSimpleQuery>
+        :type check_query: <boolean>
         """
+        if check_query:
+            self.check_query(query)
+
         # Reset the unfolder before a new query
         self.reset()
         # Init with query properties and clauses