Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
VIGNET Pierre
cadbiom
Commits
477ef5c0
Commit
477ef5c0
authored
Dec 12, 2019
by
VIGNET Pierre
Browse files
[lib] Cleaning stats management; Sync with new solver (nb_clauses)
parent
c7b8fae5
Changes
1
Hide whitespace changes
Inline
Side-by-side
library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py
View file @
477ef5c0
...
...
@@ -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
)
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment