From b2c20ecd89c78be4dc72ee1e96259f027c00fd83 Mon Sep 17 00:00:00 2001
From: VIGNET Pierre <pierre.vignet@irisa.fr>
Date: Thu, 12 Dec 2019 21:04:04 +0100
Subject: [PATCH] [lib] Add few todos.. sorry
---
.../models/clause_constraints/mcl/CLUnfolder.py | 12 ++++++++++++
1 file changed, 12 insertions(+)
diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
index efc9fe6..12d31bb 100644
--- a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
+++ b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
@@ -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)
--
GitLab