MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Commit 861f0f18 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

Add Logging of clauses passed to the solver

parent 560322d7
......@@ -47,6 +47,9 @@ from cadbiom.models.biosignal.translators.gt_visitors import compile_cond, compi
from cadbiom.models.clause_constraints.CLDynSys import Clause, Literal
from cadbiom.models.clause_constraints.mcl.MCLSolutions import RawSolution, MCLException
from cadbiom import commons as cm
LOGGER = cm.logger()
class CLUnfolder(object):
"""
......@@ -801,26 +804,42 @@ class CLUnfolder(object):
add all the current clauses in solver solv
"""
# final
LOGGER.debug("Load new solver !!")
LOGGER.debug(">> final: " + str(len(self.__final_constraints)))
LOGGER.debug(str(self.__final_constraints))
for clause in self.__final_constraints:
solv.add_clause(clause)
# LOGGER.debug(str(clause))
# trajectory invariant
LOGGER.debug(">> trajectory inv: " + str(len(self.__invariant_constraints)))
LOGGER.debug(str(self.__invariant_constraints))
for lcl in self.__invariant_constraints:
for clause in lcl:
solv.add_clause(clause)
# LOGGER.debug(str(clause))
# trajectory variant
LOGGER.debug(">> trajectory var: " + str(len(self.__variant_constraints)))
LOGGER.debug(str(self.__variant_constraints))
for clause in self.__variant_constraints:
solv.add_clause(clause)
# LOGGER.debug(str(clause))
# dynamics
LOGGER.debug(">> dynamics: " + str(len(self.__dynamic_constraints)))
LOGGER.debug(str(self.__dynamic_constraints))
lvars = []
for lcl in self.__dynamic_constraints:
for clause in lcl:
solv.add_clause(clause)
lvars.append(self.vars_in_clause(clause))
# LOGGER.debug(str(clause))
# initial
LOGGER.debug(">> initial: " + str(len(self.__initial_constraints)))
LOGGER.debug(str(self.__initial_constraints))
for clause in self.__initial_constraints:
solv.add_clause(clause)
# LOGGER.debug(str(clause))
......@@ -828,13 +847,18 @@ class CLUnfolder(object):
"""
@return: boolean
"""
LOGGER.debug("__constraints_satisfied ?")
solver = CryptoMS()
# Load Solver and all clauses
self.__load_solver(solver)
# If stats are activated (never besides in test environment):
# sync local data (nb vars, nb clauses with solver state)
if self.__stats:
if solver.nb_vars() > self.__nb_vars:
self.__nb_vars = solver.nb_vars()
if solver.nb_clauses() > self.__nb_clauses:
self.__nb_clauses = solver.nb_clauses()
# Is problem satisfiable ?
return solver.is_satisfiable()
def __msolve_constraints(self, max_sol, vvars):
......@@ -845,12 +869,15 @@ class CLUnfolder(object):
"""
solver = CryptoMS()
self.__load_solver(solver)
LOGGER.debug("__msolve_constraints :: vvars : " + str(vvars))
LOGGER.debug("__msolve_constraints :: max_sol : " + str(max_sol))
if self.__stats:
if solver.nb_vars() > self.__nb_vars:
self.__nb_vars = solver.nb_vars()
if solver.nb_clauses() > self.__nb_clauses:
self.__nb_clauses = solver.nb_clauses()
lintsol = solver.msolve_selected(max_sol, vvars)
LOGGER.debug("__msolve_constraints :: lintsol : " + str(lintsol))
lsol = []
for solint in lintsol:
sol = RawSolution(solint, self)
......@@ -892,6 +919,7 @@ class CLUnfolder(object):
@return: list of RawSolution objects
"""
LOGGER.debug("squery_solve :: vvars : " + str(vvars))
# initialization
self.init_forward_unfolding()
# horizon adjustment
......
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