From e6a72df6a92401cad666fbc618c8165923db6d33 Mon Sep 17 00:00:00 2001
From: VIGNET Pierre <pierre.vignet@irisa.fr>
Date: Thu, 19 Dec 2019 22:57:38 +0100
Subject: [PATCH] [lib] CLUnfolder Fix: ability to check the validity of the
given query
---
.../clause_constraints/mcl/CLUnfolder.py | 68 ++++++++++++++++++-
1 file changed, 66 insertions(+), 2 deletions(-)
diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
index 72938cb..e97a122 100644
--- a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
+++ b/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
--
GitLab