diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py index fa9ac2e0fcaf6c46c884b50995a16ce8592fe70e..83f03359983d14df74fc197f234dcf26b17d5be7 100644 --- a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py +++ b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py @@ -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.