Commit 42c57f9f authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] CLU: Fix typos

parent d76de0f6
...@@ -282,6 +282,10 @@ class CLUnfolder(object): ...@@ -282,6 +282,10 @@ class CLUnfolder(object):
# If A->B has clock h, an aux constraint added is h included in h when A # If A->B has clock h, an aux constraint added is h included in h when A
# Must be set to False for inhibitors computations # Must be set to False for inhibitors computations
self.__include_aux_clauses = True self.__include_aux_clauses = True
# Flag used to know if the set of auxiliary clauses has changed between
# 2 initializations of the Unfolder by a query
# (i.e. properties of the queries are different).
# Cf init_forward_unfolding()
self.__include_aux_clauses_changed = False self.__include_aux_clauses_changed = False
self.__lit_cpt = self.shift_step_init + 1 # counter for aux. var. coding self.__lit_cpt = self.shift_step_init + 1 # counter for aux. var. coding
...@@ -858,7 +862,6 @@ class CLUnfolder(object): ...@@ -858,7 +862,6 @@ class CLUnfolder(object):
in the next step. in the next step.
""" """
# New API via C++ module # New API via C++ module
# TODO: take a look at __backward_init_dynamic & __backward_code
if self.__include_aux_clauses: if self.__include_aux_clauses:
# Auxiliary clauses are supported (default) # Auxiliary clauses are supported (default)
self.__dynamic_constraints = \ self.__dynamic_constraints = \
...@@ -1287,7 +1290,7 @@ class CLUnfolder(object): ...@@ -1287,7 +1290,7 @@ class CLUnfolder(object):
:Example: :Example:
[[[12], [1]], [[58], [47]], [[104], [93]] [[[12], [1]], [[58], [47]], [[104], [93]]]
t0 t1 t2 t0 t1 t2
.. note:: __invariant_property and __dimacs_invariant should contain .. note:: __invariant_property and __dimacs_invariant should contain
...@@ -1343,8 +1346,10 @@ class CLUnfolder(object): ...@@ -1343,8 +1346,10 @@ class CLUnfolder(object):
- initilised with the first item of - initilised with the first item of
self.__precomputed_variant_constraints self.__precomputed_variant_constraints
""" """
# coding of variant properties self.__variant_constraints = list()
# Take __variant_property in priority on __dimacs_variant
# Coding of variant properties
# Take __variant_property in priority over __dimacs_variant
if self.__variant_property: if self.__variant_property:
self.__precomputed_variant_constraints = list() self.__precomputed_variant_constraints = list()
...@@ -1620,7 +1625,7 @@ class CLUnfolder(object): ...@@ -1620,7 +1625,7 @@ class CLUnfolder(object):
lintsol = solver.msolve_selected(max_sol, vvars) lintsol = solver.msolve_selected(max_sol, vvars)
LOGGER.info("__msolve_constraints :: max_sol : %s", max_sol) LOGGER.info("__msolve_constraints :: max_sol : %s", max_sol)
LOGGER.info("__msolve_constraints :: lintsol : %s", [len(sol) for sol in lintsol]) LOGGER.info("__msolve_constraints :: sol size : %s", [len(sol) for sol in lintsol])
# Make a RawSolution for each solution (tuple of literals) # Make a RawSolution for each solution (tuple of literals)
return [RawSolution(solint, self) for solint in lintsol] return [RawSolution(solint, self) for solint in lintsol]
......
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