diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py index 182209938532d756fb1ab91ddade36c63743e553..c70777ea07c70c73b995ecb35390479d11b5ffff 100644 --- a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py +++ b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py @@ -483,15 +483,19 @@ class CLUnfolder(object): @return: the DIMACS coding of the backward shifted clause """ num_clause = [] - for lit in clause.list_of_literals: - if not lit.name[-1] == '`': # t variable - num_clause.append(-(self.__var_code_table[lit.name] + self.__shift_step) \ - if not lit.sign \ - else (self.__var_code_table[lit.name] + self.__shift_step)) - else: # t+1 variable - num_clause.append(-self.__var_code_table[lit.name[:-1]] \ - if not lit.sign \ - else self.__var_code_table[lit.name[:-1]]) + for lit in clause.literals: + if lit.name[-1] == '`': # t+1 variable + num_clause.append( + -self.__var_code_table[lit.name[:-1]] \ + if not lit.sign \ + else self.__var_code_table[lit.name[:-1]] + ) + else: # t variable, base variable + num_clause.append( + -(self.__var_code_table[lit.name] + self.__shift_step) \ + if not lit.sign \ + else (self.__var_code_table[lit.name] + self.__shift_step) + ) return num_clause def __code_clause(self, clause):