From 477ef5c045a5b2120df3d22f740afa65d9c3ad37 Mon Sep 17 00:00:00 2001
From: VIGNET Pierre <pierre.vignet@irisa.fr>
Date: Thu, 12 Dec 2019 20:35:30 +0100
Subject: [PATCH] [lib] Cleaning stats management; Sync with new solver
(nb_clauses)
---
.../clause_constraints/mcl/CLUnfolder.py | 42 ++++++++++++-------
1 file changed, 27 insertions(+), 15 deletions(-)
diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
index a37c5d1..efc9fe6 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)
--
GitLab