Commit 56e194b4 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] Remove nb_clauses() call from the solver object

=> Not supported anymore since it is a private attribute of the C++ class
This feature is only used during tests so, not very important (?)
parent 9cf5b885
......@@ -942,7 +942,6 @@ class CLUnfolder(object):
"""
@return: boolean
"""
LOGGER.debug("__constraints_satisfied ?")
solver = CryptoMS()
# Load Solver and all clauses
self.__load_solver(solver)
......@@ -951,8 +950,10 @@ class CLUnfolder(object):
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()
# 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 problem satisfiable ?
return solver.is_satisfiable()
......@@ -969,8 +970,9 @@ class CLUnfolder(object):
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()
# Starting from pycryptosat 5.2, nb_clauses() is a private attribute
#if solver.nb_clauses() > self.__nb_clauses:
# self.__nb_clauses = solver.nb_clauses()
if LOGGER.getEffectiveLevel() == DEBUG:
LOGGER.debug("__msolve_constraints :: vvars : " + str(vvars))
......
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