diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py index a37c5d15557684637047606ac95abab6788d64f4..efc9fe6e95d79183b80d538c18c056a66209a479 100644 --- a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py +++ b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py @@ -154,9 +154,11 @@ shift(): """ from __future__ import print_function +from packaging import version #from pyCryptoMS import CryptoMS from pycryptosat import Solver as CryptoMS +from pycryptosat import __version__ as solver_version from cadbiom.models.biosignal.translators.gt_visitors import compile_cond, compile_event from cadbiom.models.clause_constraints.CLDynSys import Clause, Literal from cadbiom.models.clause_constraints.mcl.MCLSolutions import RawSolution, MCLException @@ -439,10 +441,10 @@ class CLUnfolder(object): """Disable solver statistics (never used)""" self.__stats = False - def _stats(self): + def stats(self): """Display solver statistics""" - print("\n NB Variables in solver:", self.__nb_vars) - print("NB Clauses in solver:", self.__nb_clauses) + LOGGER.info("NB Variables in solver:", self.__nb_vars) + LOGGER.info("NB Clauses in solver:", self.__nb_clauses) def set_include_aux_clauses(self, val): """Flag to include auxiliary clause to eliminate undesirable solutions. @@ -1375,6 +1377,24 @@ class CLUnfolder(object): LOGGER.debug(str(self.__initial_constraints)) + def __sync_stats(self, solver): + """Sync local data (nb vars, nb clauses) with solver state + if stats are activated (never besides in test environment). + + .. note:: Its the only way to set __nb_vars and __nb_clauses attributes. + """ + if version.parse(solver_version) < version.parse("5.6.9"): + if solver.nb_vars() > self.__nb_vars: + self.__nb_vars = solver.nb_vars() + else: + if solver.nb_vars > self.__nb_vars: + self.__nb_vars = solver.nb_vars + # Starting from pycryptosat 5.2, nb_clauses is private + # Starting from 5.6.9 the attribute is exposed + if solver.nb_clauses > self.__nb_clauses: + self.__nb_clauses = solver.nb_clauses + + def __constraints_satisfied(self): """Ask the SAT solver if the query/system is satisfiable in the given number of steps. @@ -1391,13 +1411,9 @@ class CLUnfolder(object): if self.__stats: # If stats are activated (never besides in test environment): - # sync local data (nb vars, nb clauses with solver state) - if solver.nb_vars() > self.__nb_vars: - self.__nb_vars = solver.nb_vars() + # sync local data (nb vars, nb clauses) with solver state + self.__sync_stats(solver) - # Starting from pycryptosat 5.2, nb_clauses() is a private attribute - #if solver.nb_clauses() > self.__nb_clauses: - # self.__nb_clauses = solver.nb_clauses() # Is the problem satisfiable ? return solver.is_satisfiable() @@ -1422,12 +1438,8 @@ class CLUnfolder(object): if self.__stats: # If stats are activated (never besides in test environment): - # sync local data (nb vars, nb clauses with solver state) - if solver.nb_vars() > self.__nb_vars: - self.__nb_vars = solver.nb_vars() - # Starting from pycryptosat 5.2, nb_clauses() is a private attribute - #if solver.nb_clauses() > self.__nb_clauses: - # self.__nb_clauses = solver.nb_clauses() + # sync local data (nb vars, nb clauses) with solver state + self.__sync_stats(solver) if LOGGER.getEffectiveLevel() == DEBUG: LOGGER.debug("__msolve_constraints :: vvars : %s", vvars)