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
19ade83b
Commit
19ade83b
authored
Feb 07, 2017
by
VIGNET Pierre
Browse files
Improve logging on not Debug mode; comprehension lists during the build of solver's clauses
parent
69661b04
Changes
4
Hide whitespace changes
Inline
Side-by-side
cadbiom/commons.py
View file @
19ade83b
...
...
@@ -14,7 +14,7 @@ DIR_DATA = 'data/'
# Logging
LOGGER_NAME
=
info
.
PACKAGE_NAME
LOG_LEVEL
=
logging
.
DEBUG
LOG_LEVEL
=
'debug'
LOG_LEVELS
=
{
'debug'
:
logging
.
DEBUG
,
'info'
:
logging
.
INFO
,
'error'
:
logging
.
ERROR
}
...
...
@@ -29,7 +29,7 @@ def logger(name=LOGGER_NAME, logfilename=None):
return
logging
.
getLogger
(
name
)
_logger
=
logging
.
getLogger
(
LOGGER_NAME
)
_logger
.
setLevel
(
LOG_LEVEL
)
_logger
.
setLevel
(
LOG_LEVEL
S
[
LOG_LEVEL
]
)
# log file
formatter
=
logging
.
Formatter
(
...
...
@@ -40,7 +40,7 @@ file_handler = RotatingFileHandler(
'.log'
,
'a'
,
100000000
,
1
)
file_handler
.
setLevel
(
LOG_LEVEL
)
file_handler
.
setLevel
(
LOG_LEVEL
S
[
LOG_LEVEL
]
)
file_handler
.
setFormatter
(
formatter
)
_logger
.
addHandler
(
file_handler
)
...
...
@@ -48,7 +48,7 @@ _logger.addHandler(file_handler)
stream_handler
=
logging
.
StreamHandler
()
formatter
=
logging
.
Formatter
(
'%(levelname)s: %(message)s'
)
stream_handler
.
setFormatter
(
formatter
)
stream_handler
.
setLevel
(
LOG_LEVEL
)
stream_handler
.
setLevel
(
LOG_LEVEL
S
[
LOG_LEVEL
]
)
_logger
.
addHandler
(
stream_handler
)
def
log_level
(
level
):
...
...
cadbiom/models/clause_constraints/mcl/CLUnfolder.py
View file @
19ade83b
...
...
@@ -48,6 +48,7 @@ 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
from
logging
import
DEBUG
LOGGER
=
cm
.
logger
()
...
...
@@ -797,50 +798,56 @@ class CLUnfolder(object):
return
lvar
# solver interface
def
__load_solver
(
self
,
solv
):
"""
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))
[
solv
.
add_clause
(
clause
)
for
clause
in
self
.
__final_constraints
]
# 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))
[
solv
.
add_clause
(
clause
)
for
lcl
in
self
.
__invariant_constraints
for
clause
in
lcl
]
# 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))
[
solv
.
add_clause
(
clause
)
for
clause
in
self
.
__variant_constraints
]
# 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))
[
solv
.
add_clause
(
clause
)
for
lcl
in
self
.
__dynamic_constraints
for
clause
in
lcl
]
# Debug:
#lvars = []
#for lcl in self.__dynamic_constraints:
# for clause in lcl:
# solv.add_clause(clause)
# lvars.append(self.vars_in_clause(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))
[
solv
.
add_clause
(
clause
)
for
clause
in
self
.
__initial_constraints
]
# LOGGING
if
LOGGER
.
getEffectiveLevel
()
==
DEBUG
:
# final
LOGGER
.
debug
(
"Load new solver !!"
)
LOGGER
.
debug
(
">> final: "
+
str
(
len
(
self
.
__final_constraints
)))
LOGGER
.
debug
(
str
(
self
.
__final_constraints
))
# trajectory invariant
LOGGER
.
debug
(
">> trajectory inv: "
+
str
(
len
(
self
.
__invariant_constraints
)))
LOGGER
.
debug
(
str
(
self
.
__invariant_constraints
))
# trajectory variant
LOGGER
.
debug
(
">> trajectory var: "
+
str
(
len
(
self
.
__variant_constraints
)))
LOGGER
.
debug
(
str
(
self
.
__variant_constraints
))
# dynamics
LOGGER
.
debug
(
">> dynamics: "
+
str
(
len
(
self
.
__dynamic_constraints
)))
LOGGER
.
debug
(
str
(
self
.
__dynamic_constraints
))
# initial
LOGGER
.
debug
(
">> initial: "
+
str
(
len
(
self
.
__initial_constraints
)))
LOGGER
.
debug
(
str
(
self
.
__initial_constraints
))
def
__constraints_satisfied
(
self
):
...
...
@@ -861,6 +868,7 @@ class CLUnfolder(object):
# Is problem satisfiable ?
return
solver
.
is_satisfiable
()
def
__msolve_constraints
(
self
,
max_sol
,
vvars
):
"""
@param max_sol: int - the max number of solution returned
...
...
@@ -869,15 +877,17 @@ 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
LOGGER
.
getEffectiveLevel
()
==
DEBUG
:
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
))
if
LOGGER
.
getEffectiveLevel
()
==
DEBUG
:
LOGGER
.
debug
(
"__msolve_constraints :: lintsol : "
+
str
(
lintsol
))
lsol
=
[]
for
solint
in
lintsol
:
sol
=
RawSolution
(
solint
,
self
)
...
...
@@ -919,7 +929,8 @@ class CLUnfolder(object):
@return: list of RawSolution objects
"""
LOGGER
.
debug
(
"squery_solve :: vvars : "
+
str
(
vvars
))
if
LOGGER
.
getEffectiveLevel
()
==
DEBUG
:
LOGGER
.
debug
(
"squery_solve :: vvars : "
+
str
(
vvars
))
# initialization
self
.
init_forward_unfolding
()
# horizon adjustment
...
...
cadbiom/models/clause_constraints/mcl/MCLQuery.py
View file @
19ade83b
...
...
@@ -44,6 +44,7 @@ Query internal representation
from
cadbiom.models.clause_constraints.mcl.MCLSolutions
import
MCLException
from
cadbiom
import
commons
as
cm
from
logging
import
DEBUG
LOGGER
=
cm
.
logger
()
...
...
@@ -67,10 +68,11 @@ class MCLSimpleQuery(object):
@param inv_prop: invariant property - None allowed
@param final_prop: final property - None is allowed
"""
LOGGER
.
debug
(
"MCLSimpleQuery params:: "
+
\
str
(
start_prop
)
+
'; '
+
\
str
(
inv_prop
)
+
'; '
+
\
str
(
final_prop
))
if
LOGGER
.
getEffectiveLevel
()
==
DEBUG
:
LOGGER
.
debug
(
"MCLSimpleQuery params:: "
+
\
str
(
start_prop
)
+
'; '
+
\
str
(
inv_prop
)
+
'; '
+
\
str
(
final_prop
))
self
.
start_prop
=
start_prop
# logical formula or None
self
.
inv_prop
=
inv_prop
# logical formula or None
self
.
variant_prop
=
[]
# list<logical formula>
...
...
script_mac.py
View file @
19ade83b
...
...
@@ -726,6 +726,6 @@ if __name__ == "__main__":
# get program args and launch associated command
args
=
parser
.
parse_args
()
# Set log level
cm
.
_logger
.
setLevel
(
cm
.
LOG_LEVELS
[
vars
(
args
)[
'verbose'
]])
LOGGER
.
setLevel
(
cm
.
LOG_LEVELS
[
vars
(
args
)[
'verbose'
]])
# launch associated command
args
.
func
(
args
)
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