Commit 8f1041d4 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] CLUnfolder: \! Refactor and audit __shift_variant and __init_variant_constraints_0

=> These functions are problematic and NOT TESTED
parent 22ef8b2c
......@@ -728,23 +728,40 @@ class CLUnfolder(object):
)
def __shift_variant(self):
"""
shift variant property - depends on unfolding direction
"""Shift variant property - depends on unfolding direction
## TODO audit...
.. warning:: Refactor note: unclear function. No apparent reason for
only the first clause to be shifted...
Process:
- Take the clauses (constraint) of the current step
- Shift the first clause
- Append it to __variant_constraints
- Stop ????
Example:
current_step: 2 (shift for step 3)
[[], [[4], [4]], [[6], [7]], []]
=> Only [6] is shifted...
.. note:: Called by shift()
"""
if not self.__list_variant_constraints:
return
if self.__shift_direction == "FORWARD":
index = self.__current_step # constraint t0 already included
current_constraint = self.__list_variant_constraints[index]
# Constraint t0 already included from the query during initialisation
current_constraint = self.__list_variant_constraints[self.__current_step]
# shift constraint at current step and add to var_constraints
for clause in current_constraint:
s_clause = self.__m_shift_clause(clause, index)
s_clause = self.__m_shift_clause(clause, self.__current_step)
self.__variant_constraints.append(s_clause)
return
elif self.__shift_direction == 'BACKWARD':
return # ?????
elif self.__shift_direction == "BACKWARD":
raise MCLException("Not yet implemented")
else:
raise MCLException("Shift incoherent data: "+self.__shift_direction)
raise MCLException("Shift incoherent data: " + self.__shift_direction)
def shift(self):
......@@ -909,46 +926,67 @@ class CLUnfolder(object):
self.__invariant_constraints = self.__invariant_constraints + d_inv
def __init_variant_constraints_0(self):
"""
if variant_property is set, compile each property into clauses and
"""Code variant constraints in a numerical clause.
variant_property list d'étapes, chaque étape a une formule logique impliquant les évènements (et les places? pas sur.;)
=> ensemble de place/propriétés devant ^etre valides à chaque étape
If variant_property is set, compile each property into clauses and
encode these clauses. Clauses already in dimacs form are added.
The two variant constraint forms must be compatible (same length)
self.__list_variant_constraints is built here and is used later to shift
given variant properties in __shift_variant().
"""
# coding of variant properties
# Take __variant_property in priority on __dimacs_variant
if self.__variant_property:
self.__list_variant_constraints = []
self.__list_variant_constraints = list()
for prop in self.__variant_property:
# compile initial (X0) property
l_clauses = self.__compile_event(prop)
# encode the clauses
dim_cl = []
for clause in l_clauses:
dim_cl.append(self.__code_clause(clause))
self.__list_variant_constraints.append(dim_cl)
# add variant properties in dimacs form
if self.__dim_variant:
vp_length = len(self.__variant_property)
if vp_length != len(self.__dim_variant):
mess = "Incoherent variant properties"
raise MCLException(mess)
for i in range(vp_length):
c_var = self.__list_variant_constraints[i]
c_var = c_var + self.__dim_variant[i]
self.__list_variant_constraints[i] = c_var
else:
if self.__dim_variant:
self.__list_variant_constraints = self.__dim_variant
# initialisation
# compile initial (X0) property into numeric form
# For each property in step of __variant_property
self.__list_variant_constraints.append(
[self.__code_clause(clause)
for clause in self.__compile_event(prop)]
)
print(self.__list_variant_constraints)
if self.__dimacs_variant:
# Add DIMACS aux clauses initial properties
# Check if the number of steps is equal
if len(self.__variant_property) != len(self.__dimacs_variant):
raise MCLException(
"Incoherent variant properties; sizes of "
"__variant_property and __dimacs_variant differ"
)
# Merge together all steps content
# Ex:
# __list_variant_constraints due to __variant_property convertion:
# [[], [[4]], [], []]
# __dimacs_variant:
# [[], [[4]], [[6], [7]], []]
# Result:
# [[], [[4], [4]], [[6], [7]], []]
self.__list_variant_constraints = \
[list(it.chain(*cpl)) for cpl
in zip(self.__dimacs_variant, self.__list_variant_constraints)]
elif self.__dimacs_variant:
# No __variant_property, keep only __dimacs_variant
self.__list_variant_constraints = self.__dimacs_variant
# Initialisation
if self.__list_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]
elif self.__shift_direction == "BACKWARD":
raise MCLException("Not yet implemented")
else:
raise MCLException("Shift incoherent data: "
+ self.__shift_direction)
raise MCLException("Shift incoherent data: " + self.__shift_direction)
## Whole initialisations ###################################################
def init_forward_unfolding(self):
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment