Commit d2fc94e0 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] CLUnfolder: fix typos

parent 1b0e10ee
......@@ -594,6 +594,8 @@ class CLUnfolder(object):
def __shift_clause(self, ncl):
"""Shift a clause for the current __shift_step
(no used anymore, replaced by direct use of C++ code)
self.shift_step must be frozen in order to avoid problems during the
unflatten() step of RawSolutions.
=> Each step MUST have the same number of variables.
......@@ -692,12 +694,6 @@ class CLUnfolder(object):
- init_backward_unfolding()
"""
if self.__invariant_constraints:
# Old API
# self.__invariant_constraints.append(
# [self.__shift_clause(clause)
# for clause in self.__invariant_constraints[-1]]
# )
# New API via C++ module
self.__invariant_constraints.append(
shift_dynamic(
......@@ -1014,7 +1010,12 @@ class CLUnfolder(object):
def __constraints_satisfied(self):
"""Test if the system loaded in the solver is satisfiable
"""Ask the SAT solver if the query/system is satisfiable in the given
number of steps.
.. warning:: vvars (frontier values) are not tested. Thus the satisfiability
is not tested for interesting variables like in squery_solve().
:return: True if the problem is satisfiable, False otherwise.
:rtype: <boolean>
"""
......@@ -1075,7 +1076,7 @@ class CLUnfolder(object):
for solint in solver.msolve_selected(max_sol, vvars))
def squery_is_satisfied(self, max_step):
"""Ask the SAT solver if the query/unfolding is satisfiable in the given
"""Ask the SAT solver if the query/system is satisfiable in the given
number of steps.
If __invariant_property is set and __final_property is not set,
......
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