Commit 70c909d5 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] CLUnfolder: fix typos

parent 57d24c58
...@@ -311,8 +311,8 @@ class CLUnfolder(object): ...@@ -311,8 +311,8 @@ class CLUnfolder(object):
self.__final_constraints self.__final_constraints
## Variables management #################################################### ## Variables management ####################################################
def vars_in_clause(self, clause): def var_names_in_clause(self, clause):
"""Return variables names from values in the given clause """Return the names of the variables from values in the given numeric clause
(DEBUG never used) (DEBUG never used)
""" """
return [self.get_var_indexed_name(var) for var in clause] return [self.get_var_indexed_name(var) for var in clause]
...@@ -426,7 +426,7 @@ class CLUnfolder(object): ...@@ -426,7 +426,7 @@ class CLUnfolder(object):
## Translation from names to num codes ##################################### ## Translation from names to num codes #####################################
# the translation depends on the shift direction ## The translation depends on the shift direction
def __forward_code(self, clause): def __forward_code(self, clause):
"""(deprecated, directly included in C++ module: forward_init_dynamic()) """(deprecated, directly included in C++ module: forward_init_dynamic())
...@@ -527,10 +527,14 @@ class CLUnfolder(object): ...@@ -527,10 +527,14 @@ class CLUnfolder(object):
"""Dynamics initialisations. """Dynamics initialisations.
Set dynamic constraints for a forward one step: X1 = f(X0) Set dynamic constraints for a forward one step: X1 = f(X0)
Numerically code a clause with the numeric code found in Numerically code clauses with the numeric codes found in
self.__var_code_table for a base variable x, self.__var_code_table for a base variable x,
and numeric_code + shift_step for x' variable integer coding increases and numeric_code + shift_step for x' variable integer coding increases
in futur steps in future steps.
__dynamic_constraints is a list of lists of numeric clauses (lists of ints)
Each sublist of __dynamic_constraints corresponds to a step in the unfolder;
the last step is the last element.
.. note:: Called by init_forward_unfolding() .. note:: Called by init_forward_unfolding()
...@@ -911,10 +915,9 @@ class CLUnfolder(object): ...@@ -911,10 +915,9 @@ class CLUnfolder(object):
## Whole initialisations ################################################### ## Whole initialisations ###################################################
def init_forward_unfolding(self): def init_forward_unfolding(self):
""" """Initialisation before generating constraints - forward trajectory
initialisation before generating constraints - forward trajectory
Called at the begining of squery_is_satisfied and squery_solve Called at the begining of squery_is_satisfied() and squery_solve()
""" """
self.__shift_direction = 'FORWARD' self.__shift_direction = 'FORWARD'
self.__current_step = 1 self.__current_step = 1
...@@ -935,8 +938,8 @@ class CLUnfolder(object): ...@@ -935,8 +938,8 @@ class CLUnfolder(object):
def init_backward_unfolding(self): def init_backward_unfolding(self):
"""Never used (and backward not implemented in __init_variant_constraints_0) """Initialisation before generating constraints - backward trajectory
initialisation before generating constraints - backward trajectory Never used (and backward not implemented in __init_variant_constraints_0)
""" """
self.__shift_direction = 'BACKWARD' self.__shift_direction = 'BACKWARD'
self.__current_step = 0 self.__current_step = 0
...@@ -1055,7 +1058,6 @@ class CLUnfolder(object): ...@@ -1055,7 +1058,6 @@ class CLUnfolder(object):
return tuple(RawSolution(solint, self) return tuple(RawSolution(solint, self)
for solint in solver.msolve_selected(max_sol, vvars)) for solint in solver.msolve_selected(max_sol, vvars))
# dynamic properties
def squery_is_satisfied(self, max_step): def squery_is_satisfied(self, max_step):
"""Ask the SAT solver if the query/unfolding is satisfiable in the given """Ask the SAT solver if the query/unfolding is satisfiable in the given
number of steps. number of steps.
......
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