Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 4d2ee9b0 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] CLUnfolder: Refactor and audit __init_initial_constraint_0...

[lib] CLUnfolder: Refactor and audit __init_initial_constraint_0 __init_final_constraint_0 __init_invariant_constraint_0
parent 8f1041d4
......@@ -849,81 +849,99 @@ class CLUnfolder(object):
return prop_visitor.clauses
def __init_initial_constraint_0(self, no_frontier_init=True):
"""
if initial property is set, generate constraints clauses in numeric form
base variable form - we have to wait until all variables are num coded
before shifting anything!!
"""
# OLD
# self.__initial_constraints = []
# if no_frontier_init:
# # initialize no frontier places to False
# for nfp in self.__no_frontier_init:
# self.__initial_constraints.append(nfp)
# if self.__initial_property:
# # compile initial property
# l_clauses = self.__compile_property(self.__initial_property)
# # compile numeric form
# for clause in l_clauses:
# self.__initial_constraints.append(self.__code_clause(clause))
# # dimacs aux initial properties
# dim_init = self.__dim_initial
# if dim_init:
# self.__initial_constraints = self.__initial_constraints + dim_init
"""Code initial constraints in a numerical clause.
If initial property is set (in text format of logical formulas, or
in dimacs format of numerical values), this function generates
constraints clauses in numerical form.
Initialisation of self.__initial_constraints:
List of DIMACS clauses (lists of values).
We have to wait until all variables are num coded before shifting anything!
.. note:: Compilation of properties in text format (logical formulas)
to numeric format is expensive when they must be parsed at each query.
:key no_frontier_init: (optional) boolean to force all variables of
places/entities to be disabled before each search.
default: True
:type no_frontier_init: <boolean>
"""
self.__initial_constraints = list()
# initialize no frontier places to False
if no_frontier_init:
self.__initial_constraints += [elem for elem in self.__no_frontier_init]
# Disable all variables of places (entities) in the model (except frontiers)
self.__initial_constraints += self.__no_frontier_init
if self.__initial_property:
# compile initial property
# compile numeric form
self.__initial_constraints += [self.__code_clause(clause) for clause in self.__compile_property(self.__initial_property)]
# Compile initial property from text logical formulas to numeric form
# __initial_property: is taken from the current query
# Costly...
self.__initial_constraints += \
[self.__code_clause(clause) for clause
in self.__compile_property(self.__initial_property)]
# dimacs aux initial properties
if self.__dim_initial:
self.__initial_constraints += self.__dim_initial
if self.__dimacs_initial:
# Add DIMACS aux clauses initial properties
self.__initial_constraints += self.__dimacs_initial
def __init_final_constraint_0(self):
"""Code final constraints in a numerical clause.
If final property is set (in text format of logical formulas, or
in dimacs format of numerical values), this function generates
constraints clauses in numerical form.
Initialisation of self.__final_constraints:
List of DIMACS clauses (lists of values).
We have to wait until all variables are num coded before shifting anything!
.. note:: Compilation of properties in text format (logical formulas)
to numeric format is expensive when they must be parsed at each query.
"""
if final property is set, generate constraints clauses in numeric form
base variable used - we have to wait until all variables are num coded
before shifting anything!!
"""
self.__final_constraints = list()
self.__final_constraints = []
if self.__final_property:
# compile initial (X0) property
# ex: Px => [$Px$]
l_clauses = self.__compile_property(self.__final_property)
# compile numeric form
# ex: [$Px$] => self.__final_constraints = [[7]]
for clause in l_clauses:
self.__final_constraints.append(self.__code_clause(clause))
dim_fin = self.__dim_final
if dim_fin:
self.__final_constraints = self.__final_constraints + dim_fin
# compile initial (X0) property into numeric form
# Ex: [$Px$] => self.__final_constraints = [[7]]
self.__final_constraints += \
[self.__code_clause(clause) for clause
in self.__compile_property(self.__final_property)]
if self.__dimacs_final:
# Add DIMACS aux clauses initial properties
self.__final_constraints += self.__dimacs_final
def __init_invariant_constraint_0(self):
"""Code final constraints in a numerical clause.
If trajectory property is set (in text format of logical formulas, or
in dimacs format of numerical values), this function generates
constraints clauses in numerical form.
Initialisation of self.__invariant_constraints:
List of lists of DIMACS clauses (lists of values).
We have to wait until all variables are num coded before shifting anything!
.. note:: Compilation of properties in text format (logical formulas)
to numeric format is expensive when they must be parsed at each query.
"""
if trajectory property is set, generate constraints clauses in numeric form
base variable used - we have to wait until all variables are num coded
before shifting anything!!
"""
self.__invariant_constraints = []
self.__invariant_constraints = list()
if self.__invariant_property:
# compile initial (X0) property
l_clauses = self.__compile_property(self.__invariant_property)
# compile numeric form
init_const = []
for clause in l_clauses:
init_const.append(self.__code_clause(clause))
self.__invariant_constraints.append(init_const)
d_inv = self.__dim_invariant
if d_inv:
self.__invariant_constraints = self.__invariant_constraints + d_inv
# compile initial (X0) property into numeric form
self.__invariant_constraints.append(
[self.__code_clause(clause) for clause
in self.__compile_property(self.__invariant_property)]
)
if self.__dimacs_invariant:
# Add DIMACS aux clauses initial properties
## TODO: pas de append ? tester avec... => aucun changement, pas de test unitaire ici...
self.__invariant_constraints += self.__dimacs_invariant
def __init_variant_constraints_0(self):
"""Code variant constraints in a numerical clause.
......
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