Commit b2c20ecd authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] Add few todos.. sorry

parent 477ef5c0
......@@ -74,6 +74,8 @@ About shifting clauses and variables:
to the right or to the left depending on whether their values are positive
or negative.
*constraints attributes are shifted at every step and submitted to the solver.
---
init_with_query(query):
......@@ -1291,12 +1293,15 @@ class CLUnfolder(object):
self.__aux_list = [] # idem
# Init properties to generate all variable num codes
## Similar code with init_backward_unfolding, move this into a function
## => could help to recall init state of a query
self.__init_initial_constraint_0()
self.__init_final_constraint_0()
self.__init_invariant_constraint_0()
self.__init_variant_constraints_0()
# Now shifting is possible
## TODO: check shift_direction too (not urgent, backward is not usable)
if old_shift_step != self.__shift_step \
or self.__include_aux_clauses_changed \
or not self.__dynamic_constraints:
......@@ -1307,6 +1312,7 @@ class CLUnfolder(object):
self.__forward_init_dynamic()
self.__precomputed_dynamic_constraints = []
else:
# Optimization for __dynamic_constraints
# Main settings of the unfolder haven't changed and the system
# was initialized before.
LOGGER.info("init_forward_unfolding:: Reload dynamic constraints")
......@@ -1346,6 +1352,12 @@ class CLUnfolder(object):
.. note:: Called by:
- __constraints_satisfied()
- __msolve_constraints()
.. todo::
Avoid to reload the solver everytime just for a few changed variables.
Ex: __initial_constraints is changed only because of
__initial_property and __dimacs_initial changes.
Ex: __dynamic_constraints is huge and stays the same.
"""
# New API via C++ module
solv.add_clauses(self.__final_constraints)
......
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