CLUnfolder.py 89.2 KB
Newer Older
VIGNET Pierre's avatar
VIGNET Pierre committed
1
# -*- coding: utf-8 -*-
VIGNET Pierre's avatar
VIGNET Pierre committed
2 3 4
## Filename    : CLUnfolder.py
## Author(s)   : Michel Le Borgne
## Created     : 22 mars 2012
5 6
## Revision    :
## Source      :
VIGNET Pierre's avatar
VIGNET Pierre committed
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
##
## Copyright 2012 : IRISA/IRSET
##
## This library is free software; you can redistribute it and/or modify it
## under the terms of the GNU General Public License as published
## by the Free Software Foundation; either version 2.1 of the License, or
## any later version.
##
## This library is distributed in the hope that it will be useful, but
## WITHOUT ANY WARRANTY, WITHOUT EVEN THE IMPLIED WARRANTY OF
## MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE.  The software and
## documentation provided here under is on an "as is" basis, and IRISA has
## no obligations to provide maintenance, support, updates, enhancements
## or modifications.
## In no event shall IRISA be liable to any party for direct, indirect,
## special, incidental or consequential damages, including lost profits,
## arising out of the use of this software and its documentation, even if
## IRISA have been advised of the possibility of such damage.  See
## the GNU General Public License for more details.
##
## You should have received a copy of the GNU General Public License
## along with this library; if not, write to the Free Software Foundation,
## Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA.
##
## The original code contained here was initially developed by:
##
##     Michel Le Borgne.
##     IRISA
##     Symbiose team
##     IRISA  Campus de Beaulieu
37 38
##     35042 RENNES Cedex, FRANCE
##
VIGNET Pierre's avatar
VIGNET Pierre committed
39 40 41
##
## Contributor(s): Geoffroy Andrieux IRSET
##
42 43 44 45 46 47 48 49 50 51 52 53 54
"""Main engine for constraints unfolding and solving.

Process from the intialization with a query to the finding of a solution.


MCLSimpleQuery (reminder):
    Object containing 2 main types of attributes describing properties:

        - Attributes in text format: These are logical formulas that are humanly
        readable.
            Ex: start_prop, inv_prop, final_prop, variant_prop
        - Attributes in DIMACS format: These are logical formulas encoded in
        the form of clauses containing numerical values.
55
            Ex: dim_start, dim_inv, dim_final, dim_variant
56

57 58 59 60 61 62 63
---

About shifting clauses and variables:

    Initialization of the dynamic system by __forward_init_dynamic() iterates on
    all literals of the system.
    If a literal is a t+1 literal, its value is shifted to the right or to the
VIGNET Pierre's avatar
VIGNET Pierre committed
64 65
    left depending on whether its sign is positive or negative
    (addition vs soustraction of the shift_step value which is the number of
66 67 68 69 70 71 72
    variables in the system).

    Otherwise, the literal is a t literal and its value stays untouched.

    t+1 and t literals are generated by CLDynSys object directly from the current
    model.

VIGNET Pierre's avatar
VIGNET Pierre committed
73 74 75
    Shifting a clause consists to iterates on all its literals and shift their
    values to the right or to the left depending on whether their values are
    positive or negative.
76

VIGNET Pierre's avatar
VIGNET Pierre committed
77 78
    *constraints unfolder attributes are shifted at every step and submitted to
    the solver.
VIGNET Pierre's avatar
VIGNET Pierre committed
79

80 81
---

82
init_with_query(query):
VIGNET Pierre's avatar
VIGNET Pierre committed
83
    Copy of the query attributes to temporary attributes of the CLUnfolder.
84 85 86 87 88 89

    Textual properties of query are compiled into numeric clauses in
    init_forward_unfolding(), just at the beginning of squery_is_satisfied()
    and squery_solve().

    ALL textual properties are susceptible to add new auxiliary variables in the
90 91
    system (increase shift_step). This is why any shift must be made after the
    initialization.
92 93 94 95 96 97 98 99 100 101 102 103 104


init_forward_unfolding():
    Organization of the initialization of the system (its clauses) for
    the current request and first variables shift.

    Initialized attributes:
        - __initial_constraints:
            Query data + negative values of all places that are not frontiers.
        - __final_constraints:
            Query data
        - __invariant_constraints:
            List of Query data
105
        - __precomputed_variant_constraints:
106 107
            Query data (automatic merge of textual and DIMACS forms)
        - __variant_constraints:
108 109 110 111 112
            Initialized with the first item of __precomputed_variant_constraints
        - __precomputed_dynamic_constraints:
            Initialized with the whole previously shifted system
            if the size of the system hasn't changed, and if no auxiliary
            clauses has been added meanwhile.
113 114 115

    Shifted attributes with __shift_step (nb of variables in the system):
        - __forward_init_dynamic(): __dynamic_constraints:
116
            Shift dynamic_system.clauses + dynamic_system.aux_clauses + init
117 118
        - __shift_final(): __final_constraints:
            Shift + replace __final_constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
119
        - __shift_invariant(): __invariant_constraints:
120 121 122 123
            Shift + append of the last element of __invariant_constraints

        PS: __variant_constraints si already initialized for the first step

VIGNET Pierre's avatar
VIGNET Pierre committed
124 125 126
    The following functions use the following methods to decompile textual
    properties or events (__compile_property(), __compile_event()) and to
    code them into DIMACS clauses constraints (__code_clause()).
127

128 129
    __code_clause() is susceptible to add new auxiliary numerical variables
    during this process if a variable is not found in __var_code_table and in
130 131 132
    __aux_code_table.

    - __init_initial_constraint_0, __init_final_constraint_0, __init_invariant_constraint_0
VIGNET Pierre's avatar
VIGNET Pierre committed
133
        Call __code_clause + __compile_property
134
    - __init_variant_constraints_0
VIGNET Pierre's avatar
VIGNET Pierre committed
135
        Call __code_clause + __compile_event
136 137


138 139 140 141 142 143 144 145 146 147 148
shift():
    Shift all clauses of the system to prepare it for the next step.

    Called at each step by:
        - squery_solve()
        - squery_is_satisfied()

    Modified attributes:
        - __shift_dynamic(): __dynamic_constraints:
            Shift + append of the last element of __dynamic_constraints
        - __shift_variant(): __variant_constraints:
149 150
            Shift clauses of the current step in __precomputed_variant_constraints,
            and append them to __variant_constraints.
151 152 153 154 155
        - __shift_invariant()
            ...
        - __shift_final()
            ...

156 157
        PS: __initial_constraints are left as this for now
        (shifted only with BACKWARD shift direction).
158

VIGNET Pierre's avatar
VIGNET Pierre committed
159
"""
160
from __future__ import print_function
161
from packaging import version
162

VIGNET Pierre's avatar
VIGNET Pierre committed
163 164
#from pyCryptoMS import CryptoMS
from pycryptosat import Solver as CryptoMS
165
from pycryptosat import __version__ as solver_version
166 167 168
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
169
from cadbiom import commons as cm
VIGNET Pierre's avatar
VIGNET Pierre committed
170 171

# C++ API
172
from _cadbiom import shift_clause, shift_dimacs_clauses, forward_code, \
VIGNET Pierre's avatar
VIGNET Pierre committed
173 174 175
                     forward_init_dynamic

# Standard imports
176
from logging import DEBUG
VIGNET Pierre's avatar
VIGNET Pierre committed
177
import itertools as it
178 179

LOGGER = cm.logger()
VIGNET Pierre's avatar
VIGNET Pierre committed
180 181 182

class CLUnfolder(object):
    """
183 184 185 186 187 188 189 190 191
    When loading a model in a MCLAnalyser object, a CLUnfolder is generated which
    implies the compilation of the dynamical system into a clause constraint
    dynamical system and the DIMACS coding of all the variables.
    This coding cannot be changed later.
    The unfolding of constraints is performed efficiently on the numeric form
    of the clause constraints. The CLUnfolder provide various method to convert
    variable names to DIMACS code and back, to extract the frontier of a model
    and to extract informations from raw solutions.

VIGNET Pierre's avatar
VIGNET Pierre committed
192 193 194 195
    Dynamic constraints unfolding management
    ========================================
    Each variable is coded as an integer (in var_code_table and var_list).
    Each clause is represented as a list of signed integers (DIMACS coding).
VIGNET Pierre's avatar
VIGNET Pierre committed
196

VIGNET Pierre's avatar
VIGNET Pierre committed
197 198
    During unfolding, clauses are shifted either to the future (forward) or
    to the past (backward). The shift operator is a simple addition
199 200
    of self.__shift_step. The shift direction depends only on initializations.
    self.__shift_step depends on the number of variables so it is impossible
VIGNET Pierre's avatar
VIGNET Pierre committed
201
    to add variables while generating a trajectory unfolding.
202 203

    Glossary
VIGNET Pierre's avatar
VIGNET Pierre committed
204
    ========
205
    - ground variables/ground DIMACS code: variables at time t=0 (not shifted).
VIGNET Pierre's avatar
VIGNET Pierre committed
206
    - solution: a solution of the logical dynamic constraint from SAT solver
207
    - state vector: list of DIMACS code of original (not shifted) variables
VIGNET Pierre's avatar
VIGNET Pierre committed
208 209
      corresponding to a step.
    - trajectory: list of state_vectors
210 211 212

    Some attributes (Please read the constructor comments for much more information):

VIGNET Pierre's avatar
VIGNET Pierre committed
213 214 215 216
    - __*_property: Logical formulas in text format from the current query.
    - __dimacs_*: Clauses in DIMACS format from the current query.
    - __*_constraints: CLUnfolder attributes for unfolding and shift;
      initialized from the query attributes.
217

VIGNET Pierre's avatar
VIGNET Pierre committed
218
    """
219

220
    def __init__(self, dynamic_system, debug=False):
221 222
        """
        :param dynamic_system: Describe a dynamic system in clause form.
VIGNET Pierre's avatar
VIGNET Pierre committed
223 224 225 226
        :key debug: (Optional) Used to activate debug mode in the Unfolder.
            i.e. `__var_list` attribute will be ordered, and initializations of
            the unfolder will be reproductible.
            Default: False.
227
        :type dynamic_system: <CLDynSys>
VIGNET Pierre's avatar
VIGNET Pierre committed
228
        :type debug: <boolean>
229
        """
230
        self.dynamic_system = dynamic_system # symbolic clause dynamic system
231

VIGNET Pierre's avatar
VIGNET Pierre committed
232
        # shift_step equals to the total number of coded variables of the system
233
        # (including inputs, entities, clocks/events, auxiliary variables)
234
        # This number can change if auxiliary clauses are added.
VIGNET Pierre's avatar
VIGNET Pierre committed
235

236
        # shift_step_init: the shift step ss (if n is X_0 code, n+ss is X_1 code)
VIGNET Pierre's avatar
VIGNET Pierre committed
237
        self.shift_step_init = dynamic_system.get_var_number()
238
        self.__shift_step = self.shift_step_init
239

240
        # About unfolder lock and shift_step:
VIGNET Pierre's avatar
VIGNET Pierre committed
241
        # shift_step must be frozen in order to avoid problems during the
242 243 244
        # unflatten() step of RawSolutions.
        # => Each step MUST have the same number of variables.
        # Thus, we lock the Unfolder by turning self.__locked to True.
245
        # See __shift_clause() and __shift_ground_clause()
VIGNET Pierre's avatar
VIGNET Pierre committed
246
        self.__locked = False
247 248 249
        self.__current_step = 1                   # current number of unfolding
        # For reachability optimisation. Number of shifts before checking
        # the final property
VIGNET Pierre's avatar
VIGNET Pierre committed
250
        self.__steps_before_check = 0
251

VIGNET Pierre's avatar
VIGNET Pierre committed
252
        # assign a DIMACS code number to each variable (invariant)
253 254
        # Create mappings between names and values of the variables of the system
        # dynamic_system.base_var_set : Set of ALL variables of the dynamic system
255
        # (including inputs, entities, clocks/events, auxiliary variables).
256 257
        self.__var_code_table = dict()     # Mapping: name -> DIMACS code (!= 0)
        self.__var_list = ['##']           # Mapping: DIMACS code (!= 0) -> name
258 259

        # Fix order of variables names with a list:
260 261
        # - indexes of __var_list are the values of the variables at these indexes
        # - values begin from 1 (0 is a blacklisted value)
262 263 264 265
        if debug:
            base_var_set = sorted(list(dynamic_system.base_var_set))
        else:
            base_var_set = list(dynamic_system.base_var_set)
266
        self.__var_list += base_var_set
267
        # keys: are the names of the variables, values: their values
268 269
        self.__var_code_table = \
            {var_name: var_num for var_num, var_name in enumerate(base_var_set, 1)}
270

271 272 273 274 275 276
        # Optimization: for forward_init_dynamic() and forward_code() (mostly
        # implemented in C.
        # Precompute __var_code_table with the literal names in "future" format;
        # i.e with a last char '`' at the end.
        # Thus it is easy to search them directly in the dict (in O(1)),
        # instead of slicing them.
277 278
        # Note: "future" literals are already in self.dynamic_system.clauses
        # and maybe in self.dynamic_system.aux_clauses
279 280 281
        temp_var_code_table = \
            {var_name + "`": var_num for var_name, var_num in self.__var_code_table.iteritems()}
        self.__var_code_table.update(temp_var_code_table)
282

283
        assert len(self.__var_code_table) == 2 * self.__shift_step
284

285 286 287 288
        # Include auxiliary clause to eliminate undesirable solutions
        # If A->B has clock h, an aux constraint added is h included in h when A
        # Must be set to False for inhibitors computations
        self.__include_aux_clauses = True
VIGNET Pierre's avatar
VIGNET Pierre committed
289 290 291 292
        # Flag used to know if the set of auxiliary clauses has changed between
        # 2 initializations of the Unfolder by a query
        # (i.e. properties of the queries are different).
        # Cf init_forward_unfolding()
293
        self.__include_aux_clauses_changed = False
294
        self.__lit_cpt = self.shift_step_init + 1  # counter for aux. var. coding
295

VIGNET Pierre's avatar
VIGNET Pierre committed
296 297
        # Same mapping tools but for auxiliary variables introduced by properties
        # compilation. Cf __code_clause()
298
        self.__aux_code_table = dict()            # name to code
VIGNET Pierre's avatar
VIGNET Pierre committed
299
        self.__aux_list = []                      # code to name
300

301 302 303 304 305
        # No frontier init:
        # Set of DIMACS codes of the simple variables/places that are not frontiers
        # Used to disable all variables of places in the model (except frontiers)
        self.no_frontier_values = frozenset(
            self.__var_code_table[not_front_name]
VIGNET Pierre's avatar
VIGNET Pierre committed
306
            for not_front_name in self.dynamic_system.no_frontiers
307 308 309 310 311 312 313 314 315 316 317 318 319
        )
        # Used in __prune_initial_no_frontier_constraint_0() in order to
        # compute values of literals that are specified in user constraints.
        # These literals should not be blindly disabled by default in __no_frontier_init
        self.initial_values = set()
        # Ordered list of DIMACS codes of the places that are not frontiers
        # => Clauses of negatives values
        # Ex: [[-1], [-2], ...]
        # The values are usually a subset of no_frontier_values
        self.__no_frontier_init = list()

        # Frontiers:
        # Ordered list of DIMACS codes of the frontier variables/places
VIGNET Pierre's avatar
VIGNET Pierre committed
320 321 322 323
        self.frontier_values = [
            self.__var_code_table[front_name]
            for front_name in self.dynamic_system.frontiers
        ]
324
        self.frontier_values.sort()
VIGNET Pierre's avatar
VIGNET Pierre committed
325 326
        ## TODO: Utiliser une liste triée est-il utile ici ?
        ## si non passer utiliser un frozenset et supprimer les casts partout
327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344
        ## Cf RawSolution.frontier_pos_and_neg_values BACKWARD, encore utilisé avec index
        ## Cf TestCLUnfolder.test_frontier indexable mais peut etre contourné

        # Precompute convenient attributes for:
        # frontiers_pos_and_neg:
        #     - RawSolution.frontier_pos_and_neg_values
        #     (set operation with solution variables)
        # frontiers_negative_values:
        #     - MCLQuery.from_frontier_sol_new_timing
        #     - MCLQuery.frontiers_negative_values
        #     - MCLAnalyser.__solve_with_inact_fsolution
        #     - TestCLUnfolder.test_prune
        #
        # Set of frontier positive and negative values
        # (all frontiers and their opposite version).
        # => operations with sets are much faster
        self.frontiers_negative_values = \
            frozenset(-frontier for frontier in self.frontier_values)
345 346 347 348
        self.frontiers_pos_and_neg = \
            self.frontiers_negative_values | frozenset(self.frontier_values)

        # DIMACS codes of the input variables/places for extraction (inv)
349
        self.__inputs = frozenset(self.__var_code_table[inp] for inp in self.dynamic_system.inputs)
350

351
        # DIMACS codes of the free_clocks variables/places for extraction (invariant)
352
        self.__free_clocks = frozenset(self.__var_code_table[fcl] for fcl in self.dynamic_system.free_clocks)
353 354

        # Binding for a merged version of __inputs and __free_clocks
355
        # Convenient attribute for RawSolution.extract_act_input_clock_seq()
356 357
        # DIMACS codes of the input and free_clocks variables
        self.inputs_and_free_clocks = self.__inputs | self.__free_clocks
358

359 360
        # Properties to be checked
        self.reset()
361

362
        # Logical constraints:
363
        # Result from unfolding of base constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
364 365 366 367 368
        # Boolean vectors signification:
        # X: Current state of places (activated/unactivated)
        # X': Future state of places
        # H: Current 'free' events (present/not present) => ?
        # I: Current inputs => ?
VIGNET Pierre's avatar
VIGNET Pierre committed
369
        self.__dynamic_constraints = []        # DIMACS clauses: X' = f(X,H,I)
370
        self.__precomputed_dynamic_constraints = []
VIGNET Pierre's avatar
VIGNET Pierre committed
371

372
        # Simple temporal properties:
VIGNET Pierre's avatar
VIGNET Pierre committed
373 374
        # SP(X0): Initial property/start property; Never change at each step.
        # IP(X): Invariant property
375
        # VP(X): Variant property
VIGNET Pierre's avatar
VIGNET Pierre committed
376
        #   List of logical formulas of properties forced at each step
377
        #   It's the trajectory of events of a solution.
VIGNET Pierre's avatar
VIGNET Pierre committed
378 379
        # FP(X): Final property

VIGNET Pierre's avatar
VIGNET Pierre committed
380 381 382 383 384
        self.__initial_constraints = []    # DIMACS clauses: C(X_0) <list <list <int>>>
        self.__final_constraints   = []    # idem: C(X_n)
        self.__invariant_constraints = []  # DIMACS clauses: C(X_i))
        self.__variant_constraints = []    # variant constraints along trajectory
        self.__shift_direction = None      # FORWARD or BACKWARD
VIGNET Pierre's avatar
VIGNET Pierre committed
385 386 387 388 389 390 391 392

        # statistics on solver
        self.__stats = False
        self.__nb_vars = 0
        self.__nb_clauses = 0


    def reset(self):
393 394
        """Reset the unfolder before a new query

395
        Reset only properties and dimacs clauses from the current query;
VIGNET Pierre's avatar
VIGNET Pierre committed
396
        AND `__precomputed_variant_constraints`.
397

VIGNET Pierre's avatar
VIGNET Pierre committed
398 399 400
        `__initial_constraints`, `__final_constraints`, `__invariant_constraints`,
        `__variant_constraints` and `__dynamic_constraints` ARE NOT reset here
        (see :meth:`init_forward_unfolding`).
401

402
        This function is called from the constructor and during
VIGNET Pierre's avatar
VIGNET Pierre committed
403 404 405 406 407
        :meth:`MCLAnalyser.sq_is_satisfiable()
        <cadbiom.models.clause_constraints.mcl.MCLAnalyser.MCLAnalyser.sq_is_satisfiable>`
        and :meth:`MCLAnalyser.sq_is_satisfiable()
        <cadbiom.models.clause_constraints.mcl.MCLAnalyser.MCLAnalyser.sq_solutions>`
        following the call of :meth:`init_with_query`.
VIGNET Pierre's avatar
VIGNET Pierre committed
408
        """
409
        # Properties to be checked
VIGNET Pierre's avatar
VIGNET Pierre committed
410 411 412 413 414 415 416 417
        self.__initial_property = None    # logical formula - literal boolean expression
        self.__dimacs_initial = None      # list of DIMACS clauses
        self.__final_property = None      # logical formula
        self.__dimacs_final = None        # list of DIMACS clauses
        self.__invariant_property = None  # logical formula
        self.__dimacs_invariant = None    # list of DIMACS clauses
        self.__variant_property = None    # list<logic formulas>
        self.__dimacs_variant = None      # list<list<DIMACS clauses>>
VIGNET Pierre's avatar
VIGNET Pierre committed
418
        # list of variant temporal constraints in DIMACS ground code
419
        self.__precomputed_variant_constraints = None  # list<list<DIMACS clauses>>
420

421 422 423 424 425 426
        # Note: temp_initial_values is used in:
        # __init_initial_constraint_0()
        # __init_invariant_constraint_0()
        # See __prune_initial_no_frontier_constraint_0()
        self.temp_initial_values = set()

427 428
        # If this function is called from the constructor,
        # the following variables are just redefined here.
429 430 431

        # For reachability optimisation. Number of shifts before checking
        # the final property
VIGNET Pierre's avatar
VIGNET Pierre committed
432
        self.__steps_before_check = 0
VIGNET Pierre's avatar
VIGNET Pierre committed
433
        self.__shift_direction = None     # FORWARD or BACKWARD
VIGNET Pierre's avatar
VIGNET Pierre committed
434
        self.__locked = False
435
        self.__lit_cpt = self.shift_step_init + 1
436

437 438 439 440 441 442 443 444
    def check_query(self, query):
        """Check textual and DIMACS properties of the given query

        If textual properties have changed since the last initialization of the
        CLUnfolder, new auxiliary variables will be added to the dynamic system.

        Also check if values of literals are in the limits of the dynamical
        system (shift_step_init). If it's not the case, a ValueError exception
445 446 447 448 449 450 451 452 453 454
        will be raised. Indeed, literals **can't** be used without a proper init.

        .. TODO:: Keep in mind that adding auxiliary variables is possible in
            the future.
            Il faut remplir __aux_code_table, __aux_list, jusqu'à la valeur
            du litéral inconnu dans le système et incrémenter les
            variables en conséquence.
            S'inspirer de __code_clause()

        .. TODO:: We do not test if the textual events of query.variant_prop
455
            involve events that are not in the model...
456 457 458 459 460 461 462 463 464 465 466 467 468

        Called by:
            :meth:`init_with_query`

        :param query: Query built with start, invariant, final, variant properties
            in textual and/or DIMACS forms.
        :type query: <MCLSimpleQuery>
        """
        # Check textual properties
        if (self.__initial_property != query.start_prop
            or self.__final_property != query.final_prop
            or self.__invariant_property != query.inv_prop
            or self.__variant_property != query.variant_prop):
469 470 471
            # Properties have changed:
            # The system will be modified; Auxiliary clauses will be added.
            # Do not reload cached constraints. Cf init_forward_unfolding()
472
            self.__include_aux_clauses_changed = True
473 474 475
            ## TODO: à repasser dans init_with_query ?
            # Ne pas faire ce test systématiquement implique que les propriétés
            # texte ne sont jamais modifiées entre chaque requete.
476

477 478 479 480 481 482
        # Check literals
        if query.dim_inv:
            # Check dimacs invariant: Initial state only (will be shifted later)
            # Ex: [[12]]
            assert len(query.dim_inv) == 1

483 484 485 486
        # Check values of literals
        values = set(it.chain(*query.dim_start))
        values.update(it.chain(*query.dim_final))
        values.update(it.chain(*query.dim_inv))
487
        if query.dim_variant:
488
            # Handle empty steps:
489
            # Ex: [[[12], [1]], [[58], [47]], []]
490
            g = (step for step in query.dim_variant if step)
491 492 493 494 495 496 497 498 499
            [values.update(it.chain(*step)) for step in g]

        # Get all values that are not in the initial dynamic system
        out_of_range_values = {val for val in values if abs(val) > self.shift_step_init}
        if not out_of_range_values:
            return

        # The literal comes from an auxilary clause; not from the dynamic model.
        raise ValueError(
500
            "%s variable(s) is/are not in the initial system.\n"
501 502 503 504
            "Insertion of literals from auxiliary clauses is not allowed here.\n"
            "Since the auxiliary clauses are reset here, this literal is suspect\n"
            "and its use dangerous because its value is not reproductible\n"
            "(the value can refer to a different constraint from one run to another)."
505 506 507 508
            % out_of_range_values
        )

    def init_with_query(self, query, check_query=True):
509 510
        """Initialise the unfolder with the given query

511
        Following attributes are used from the query:
512
            start_prop, dim_start, inv_prop, dim_inv, final_prop, dim_final,
513
            variant_prop, dim_variant, steps_before_check
514 515

        Textual properties of query are compiled into numeric clauses in
516 517
        init_forward_unfolding(), just at the beginning of squery_is_satisfied()
        and squery_solve().
518
        This compilation step is costly due to ANTLR performances...
519 520

        .. warning:: ALL textual properties are susceptible to add new auxiliary
521 522 523 524 525 526 527 528 529
            variables in the system (increase shift_step). Thus, the system
            will be rebuilt.

        :param query: Query built with start, invariant, final, variant properties
            in textual and/or DIMACS forms.
        :key check_query: Check textual and DIMACS properties of the given query.

            .. warning:: This option should be disable for performance reasons;
                or if you know what you are doing.
530 531 532 533
                You will assume in particular that:
                - textual properties are not modified
                - values of literals in DIMACS properties are already described
                  in the model (new literals are not allowed).
534 535 536

        :type query: <MCLSimpleQuery>
        :type check_query: <boolean>
537
        """
538 539 540
        if check_query:
            self.check_query(query)

541 542
        # Reset the unfolder before a new query
        self.reset()
543
        # Init with query properties and clauses
544 545
        self.__initial_property = query.start_prop # logical formula in text
        self.__dimacs_initial = query.dim_start
546

547 548
        self.__final_property = query.final_prop # logical formula in text
        self.__dimacs_final = query.dim_final
549

550 551
        self.__invariant_property = query.inv_prop # logical formula in text
        self.__dimacs_invariant = query.dim_inv
552 553

        # It's the trajectory of events of a solution.
554
        self.__variant_property = query.variant_prop # logical formula in text
555
        self.__dimacs_variant = query.dim_variant
556

557 558 559
        # For reachability optimisation. Number of shifts before checking
        # the final property (default 0)
        self.__steps_before_check = query.steps_before_check
560

VIGNET Pierre's avatar
VIGNET Pierre committed
561
    def set_stats(self):
562
        """Enable solver statistics (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
563 564 565
        self.__stats = True
        self.__nb_vars = 0
        self.__nb_clauses = 0
566

VIGNET Pierre's avatar
VIGNET Pierre committed
567
    def unset_stats(self):
568
        """Disable solver statistics (never used)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
569
        self.__stats = False
570

571
    def stats(self):
572
        """Display solver statistics"""
573 574
        LOGGER.info("NB Variables in solver:", self.__nb_vars)
        LOGGER.info("NB Clauses in solver:", self.__nb_clauses)
575

VIGNET Pierre's avatar
VIGNET Pierre committed
576
    def set_include_aux_clauses(self, val):
577 578
        """Flag to include auxiliary clause to eliminate undesirable solutions.

579
        If A->B has clock h, an aux constraint added is h included in h when A
580 581 582 583
        Must be set to False for inhibitors computations.

        .. warning:: This function impacts the shift_step number.

VIGNET Pierre's avatar
VIGNET Pierre committed
584
        Tested by:
585 586
            - __forward_init_dynamic
            - __backward_init_dynamic
VIGNET Pierre's avatar
VIGNET Pierre committed
587 588
        """
        self.__include_aux_clauses = val
589
        self.__include_aux_clauses_changed = True
590

591
    ## Internal variable access for tests (never used) #########################
592 593
    @property
    def dynamic_constraints(self):
594
        """For tests: returns coded dynamic constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
595
        return self.__dynamic_constraints
596

597 598
    @property
    def initial_constraints(self):
599
        """For tests: returns coded initial constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
600
        return self.__initial_constraints
601

602 603
    @property
    def invariant_constraints(self):
604
        """For tests: returns coded invariant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
605
        return self.__invariant_constraints
606

607 608
    @property
    def variant_constraints(self):
609
        """For tests: returns coded variant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
610
        return self.__variant_constraints
611

612 613
    @property
    def final_constraints(self):
614
        """For tests: returns coded final constraints"""
615
        return self.__final_constraints
616

617
    ## Variables management ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
618 619
    def var_names_in_clause(self, clause):
        """Return the names of the variables from values in the given numeric clause
620 621 622 623
        (DEBUG never used)
        """
        return [self.get_var_indexed_name(var) for var in clause]

VIGNET Pierre's avatar
VIGNET Pierre committed
624
    def var_dimacs_code(self, var_name):
625
        """Returns DIMACS code of var_name (string) variable (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
626
        return self.__var_code_table[var_name]
627

VIGNET Pierre's avatar
VIGNET Pierre committed
628
    def get_system_var_number(self):
629 630
        """Get number of variables in the clause constraint dynamical system
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
631 632 633

        .. note:: This number should be equal to the number of variables
            in self.get_var_number()
VIGNET Pierre's avatar
VIGNET Pierre committed
634
        """
635
        return self.dynamic_system.get_var_number()
636

VIGNET Pierre's avatar
VIGNET Pierre committed
637
    def get_var_number(self):
638 639
        """Get number of principal variables (properties excluded) in the unfolder
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
640 641 642

        .. note:: This number should be equal to the number of variables
            in self.get_system_var_number()
VIGNET Pierre's avatar
VIGNET Pierre committed
643
        """
644 645
        # Remove the blacklisted first item (##) for variables naming
        return len(self.__var_list) - 1
646

VIGNET Pierre's avatar
VIGNET Pierre committed
647
    def get_var_name(self, var_num):
648 649
        """Get name of the variable

650
        .. seealso:: Explanations on :meth:`get_var_indexed_name`
651

VIGNET Pierre's avatar
VIGNET Pierre committed
652
        @param var_num: DIMACS literal coding of an initial variable
653
        @return: name of the variable
VIGNET Pierre's avatar
VIGNET Pierre committed
654
        """
655
        # Get the original var_code without shifts
656
        var_code = (abs(var_num) - 1) % self.__shift_step + 1
657
        if var_code <= self.shift_step_init:
658 659
            # Variable num is less than the number of the variables in the system
            # => variable from the initial system
VIGNET Pierre's avatar
VIGNET Pierre committed
660
            return self.__var_list[var_code]
661
        else:
662 663
            # Auxiliary variable introduced by properties compilation
            return self.__aux_list[var_code - self.shift_step_init - 1]
664

VIGNET Pierre's avatar
VIGNET Pierre committed
665
    def get_var_indexed_name(self, var_num):
666 667 668 669 670
        """Get name of the variable with the time index appended

        .. note:: time index is the number of steps since the begining of the
            simulation.

VIGNET Pierre's avatar
VIGNET Pierre committed
671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716
        :Example - Only standard variables:

            __shift_step = 2 (number of variables in the system)
            shift_step_init = 2 (number of variables in the system at the initial state)
            __var_list = ["##", "n1", "n2"]

            Virtual list of indexes in the state vector of a solution:
            [0, 1, 2, 3, 4, 5, 6, 7, 8, ...]
             #|n1,n2|n1,n2|n1,n2|n1,n2|
               ti=0  ti=1  ti=2  ti=3

            Given var_num = 7:
            index of var_name in __var_list: ((7-1) % 2) + 1 = 1
            var_name = "n1"
            time index: (7 - 1) / 2 = 3

            => return: "n1_3"

        :Example - With an auxiliary variable:

            __shift_step = 2 (There is 1 auxiliary variable)
            shift_step_init = 1
            __var_list = ["##", "n1"]
            __aux_list = ["_lit0"]

            Virtual list of indexes in the state vector of a solution:
            [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, ...]
             #|n1,_lit0|n1,_lit0|n1,_lit0|
               ti=0     ti=1     ti=2

            If the index is > shift_step_init, then it is an auxiliary
            variable. In order to get the index in __aux_list we have to
            substract:
                - `1` because on the contrary of __var_list,  __aux_list begins at index 0
                - `shift_step_init` because value of the first aux variable
                follows the last value of __var_list

            Given var_num = 6
            var_code of var_name: ((6-1) % 2) + 1 = 2
            2 > shift_step_init
            index of var_name in __aux_list:
                var_code - shift_step_init - 1
                2 -1 -1 = 0
            var_name = "_lit0"

            => return: "_lit0_2"
717

VIGNET Pierre's avatar
VIGNET Pierre committed
718
        @param var_num: DIMACS literal coding
719
        @return: name of the variable with the time index appended
VIGNET Pierre's avatar
VIGNET Pierre committed
720
        """
721
        varnum1 = abs(var_num)
722
        # Get the original var_code without shifts
VIGNET Pierre's avatar
VIGNET Pierre committed
723
        var_code = (varnum1 - 1) % self.__shift_step + 1
724
        var_step = (varnum1 - var_code) / self.__shift_step
725
        if var_code <= self.shift_step_init:
726 727
            # Variable num is less than the number of the variables in the system
            # => variable from the initial system
VIGNET Pierre's avatar
VIGNET Pierre committed
728 729
            return self.__var_list[var_code] + '_%s'% var_step
        else:
730 731
            # Auxiliary variable introduced by properties compilation
            index = var_code - self.shift_step_init - 1
VIGNET Pierre's avatar
VIGNET Pierre committed
732
            return self.__aux_list[index] + '_%s'% var_step
733

734 735
    @property
    def free_clocks(self):
736
        """Get the DIMACS codes of the free_clocks variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
737
        return self.__free_clocks
738

739 740
    @property
    def inputs(self):
741
        """Get the DIMACS codes of the input variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
742
        return self.__inputs
743

744 745
    @property
    def shift_direction(self):
VIGNET Pierre's avatar
VIGNET Pierre committed
746 747 748 749
        """
        @return: string "FORWARD" or "BACKWARD"
        """
        return self.__shift_direction
750

751 752
    @property
    def shift_step(self):
VIGNET Pierre's avatar
VIGNET Pierre committed
753 754 755 756
        """
        @return: the shift step ss (if n is X_0 code, n+ss is X_1 code)
        """
        return self.__shift_step
757

758 759
    @property
    def current_step(self):
VIGNET Pierre's avatar
VIGNET Pierre committed
760 761 762 763 764
        """
        @return: the current number of unfolding
        """
        return self.__current_step

765

766
    ## Translation from names to num codes #####################################
VIGNET Pierre's avatar
VIGNET Pierre committed
767
    ## The translation depends on the shift direction
VIGNET Pierre's avatar
VIGNET Pierre committed
768
    def __forward_code(self, clause):
769 770 771
        """Deprecated, directly included in C++ module

        .. seelalso:: :meth:`forward_init_dynamic`
772

VIGNET Pierre's avatar
VIGNET Pierre committed
773
        Numerically code a clause with the numeric codes found in
774
        self.__var_code_table for a base variable x,
VIGNET Pierre's avatar
VIGNET Pierre committed
775
        and numeric_code +/- shift_step (according to the sign) for x' variable.
776

777
        .. note:: Future variables x' are noted "name`" in Literal names.
VIGNET Pierre's avatar
VIGNET Pierre committed
778 779
            The absolute value of these variables will increase by shift_step
            in the next step.
780

781 782
        :param clause: A Clause object
        :return: The DIMACS coding of the forward shifted clause
VIGNET Pierre's avatar
VIGNET Pierre committed
783
        """
784 785
        # Old API
        # num_clause = []
786
        # for lit in clause.literals:
787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802
        #     if lit.name[-1] == '`': # t+1 variable
        #         num_clause.append(
        #             -(self.__var_code_table[lit.name[:-1]] + self.__shift_step) \
        #             if not lit.sign \
        #             else (self.__var_code_table[lit.name[:-1]] + self.__shift_step)
        #         )
        #     else: # t variable
        #         num_clause.append(
        #             -self.__var_code_table[lit.name] \
        #             if not lit.sign else self.__var_code_table[lit.name]
        #         )
        # return num_clause

        # New API via C++ module
        return forward_code(clause, self.__var_code_table, self.__shift_step)

803

VIGNET Pierre's avatar
VIGNET Pierre committed
804
    def __backward_code(self, clause):
805 806 807 808 809 810
        """(never used, backward is partially implemented)

        numerically code a clause with the numeric code found in
        self.__var_code_table + shift_step for a base variable x,
        and numeric_code for x' variable integer coding increases in past steps

VIGNET Pierre's avatar
VIGNET Pierre committed
811 812 813 814
        @param clause: a Clause object
        @return: the DIMACS coding of the backward shifted clause
        """
        num_clause = []
815 816 817 818 819 820 821 822 823 824 825 826 827
        for lit in clause.literals:
            if lit.name[-1] == '`': # t+1 variable
                num_clause.append(
                    -self.__var_code_table[lit.name[:-1]] \
                    if not lit.sign \
                    else self.__var_code_table[lit.name[:-1]]
                )
            else: # t variable, base variable
                num_clause.append(
                    -(self.__var_code_table[lit.name] + self.__shift_step) \
                    if not lit.sign \
                    else (self.__var_code_table[lit.name] + self.__shift_step)
                )
VIGNET Pierre's avatar
VIGNET Pierre committed
828
        return num_clause
829

VIGNET Pierre's avatar
VIGNET Pierre committed
830
    def __code_clause(self, clause):
831 832
        """Numerically code a clause

833 834 835 836
        The numerical values are found in:
            - self.__var_code_table for variables in the dynamic system,
            - or in self.__aux_code_table for other auxiliary variables;
        We assume all variables are ground variables (not shifted).
837

838 839 840 841
        .. warning:: This function MODIFIES SHIFT_STEP because we add a variable
            in the system if a variable is found neither in __var_code_table nor
            in __aux_code_table.
            Thus, a new auxiliary variable will be created.
842 843 844 845 846 847

        :param clause:
        :return: List of numerical values corresponding to the literals
            in the given clause.
        :type clause: <Clause>
        :rtype: <list <int>>
VIGNET Pierre's avatar
VIGNET Pierre committed
848 849
        """
        num_clause = []
850
        for lit in clause.literals:
851
            # Get variable value with the given name
VIGNET Pierre's avatar
VIGNET Pierre committed
852
            name = lit.name
853
            if name in self.__var_code_table:
VIGNET Pierre's avatar
VIGNET Pierre committed
854
                var_cod = self.__var_code_table[name]
855
            elif name in self.__aux_code_table:
VIGNET Pierre's avatar
VIGNET Pierre committed
856
                var_cod = self.__aux_code_table[name]
857 858
            else:
                # Create an auxiliary variable - modifies shift_step (nb of variables)
VIGNET Pierre's avatar
VIGNET Pierre committed
859
                self.__shift_step += 1
860
                # Mapping name to value code
VIGNET Pierre's avatar
VIGNET Pierre committed
861
                self.__aux_code_table[name] = self.__shift_step
862
                # Mapping value code to name
VIGNET Pierre's avatar
VIGNET Pierre committed
863
                self.__aux_list.append(name)
864
                # Define var_cod
865 866 867 868 869
                var_cod = self.__shift_step

            # Add the sign to the value
            lit_code = var_cod if lit.sign else -var_cod

VIGNET Pierre's avatar
VIGNET Pierre committed
870 871
            num_clause.append(lit_code)
        return num_clause
872

873
    ## Dynamic initialisations #################################################
874
    ## TODO: move near init_forward_unfolding
VIGNET Pierre's avatar
VIGNET Pierre committed
875
    def __forward_init_dynamic(self):
876 877
        """Dynamics initialisations.
        Set dynamic constraints for a forward one step: X1 = f(X0)
878

VIGNET Pierre's avatar
VIGNET Pierre committed
879
        Numerically code clauses with the numeric codes found in
880
        self.__var_code_table for a base variable x,