CLUnfolder.py 74.6 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
116
117
118

    Shifted attributes with __shift_step (nb of variables in the system):
        - __forward_init_dynamic(): __dynamic_constraints:
            Shift dynamic_system.list_clauses + dynamic_system.aux_list_clauses + init
        - __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
206
    ========
    - ground variables/ground dimacs code: variables at time 0/their encoding.
    - 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
213
214
215


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

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

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

221
    def __init__(self, dynamic_system, debug=False):
222
223
224
225
        """
        :param dynamic_system: Describe a dynamic system in clause form.
        :type dynamic_system: <CLDynSys>
        """
226
        self.dynamic_system = dynamic_system # symbolic clause dynamic system
227

VIGNET Pierre's avatar
VIGNET Pierre committed
228
        # shift_step equals to the total number of coded variables of the system
229
        # (including inputs, entities, clocks/events, auxiliary variables)
VIGNET Pierre's avatar
VIGNET Pierre committed
230

231
        # 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
232
        self.shift_step_init = dynamic_system.get_var_number()
233
234
        self.__shift_step = self.shift_step_init  # current shift/step

235
        # About unfolder lock and shift_step:
VIGNET Pierre's avatar
VIGNET Pierre committed
236
        # shift_step must be frozen in order to avoid problems during the
237
238
239
240
        # unflatten() step of RawSolutions.
        # => Each step MUST have the same number of variables.
        # Thus, we lock the Unfolder by turning self.__locked to True.
        # See __shift_clause() and __m_shift_clause()
VIGNET Pierre's avatar
VIGNET Pierre committed
241
        self.__locked = False
242
243
244
        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
245
        self.__steps_before_check = 0
246

VIGNET Pierre's avatar
VIGNET Pierre committed
247
        # assign a DIMACS code number to each variable (invariant)
248
249
        # 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
250
        # (including inputs, entities, clocks/events, auxiliary variables).
251
252
        self.__var_code_table = dict()     # Mapping: name -> DIMACS code (!= 0)
        self.__var_list = ['##']           # Mapping: DIMACS code (!= 0) -> name
253
254

        # Fix order of variables names with a list:
255
256
        # - indexes of __var_list are the values of the variables at these indexes
        # - values begin from 1 (0 is a blacklisted value)
257
258
259
260
        if debug:
            base_var_set = sorted(list(dynamic_system.base_var_set))
        else:
            base_var_set = list(dynamic_system.base_var_set)
261
        self.__var_list += base_var_set
262
        # keys: are the names of the variables, values: their values
263
264
265
266
267
268
269
270
271
272
273
274
275
        self.__var_code_table = \
            {var_name: var_num for var_num, var_name in enumerate(base_var_set, 1)}
        # 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.
        # Note: "future" literals are already in self.dynamic_system.list_clauses
        # and maybe in self.dynamic_system.aux_list_clauses
        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)
276

277
        assert len(self.__var_code_table) == 2 * self.__shift_step
278

279
280
281
282
        # 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
283
        self.__include_aux_clauses_changed = False
284
        self.__lit_cpt = self.__shift_step + 1    # counter for aux. var. coding
285

286
287
288
289
        # Same mapping tools for auxiliary variables introduced by properties
        # compilation
        # Cf __code_clause()
        self.__aux_code_table = dict()            # name to code
VIGNET Pierre's avatar
VIGNET Pierre committed
290
        self.__aux_list = []                      # code to name
291

292
293
        # ordered list of DIMACS codes of the simple variables/places
        # Disable all variables of places (entities) in the model (except frontiers)
294
        self.__no_frontier_init = [[-self.__var_code_table[nfp]] for nfp in self.dynamic_system.no_frontiers]
295

296
        # ordered list of DIMACS codes of the frontier variables/places
297
298
        self.frontier_values = [self.__var_code_table[frp] for frp in self.dynamic_system.frontiers]
        self.frontier_values.sort()
VIGNET Pierre's avatar
VIGNET Pierre committed
299
300
        ## TODO: Utiliser une liste triée est-il utile ici ?
        ## si non passer utiliser un frozenset et supprimer les casts partout
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
        ## 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)
319
320
321
322
        self.frontiers_pos_and_neg = \
            self.frontiers_negative_values | frozenset(self.frontier_values)

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

325
        # DIMACS codes of the free_clocks variables/places for extraction (invariant)
326
        self.__free_clocks = frozenset(self.__var_code_table[fcl] for fcl in self.dynamic_system.free_clocks)
327
328

        # Binding for a merged version of __inputs and __free_clocks
329
        # Convenient attribute for RawSolution.extract_act_input_clock_seq()
330
331
        # DIMACS codes of the input and free_clocks variables
        self.inputs_and_free_clocks = self.__inputs | self.__free_clocks
332

333
334
        # Properties to be checked
        self.reset()
335

336
        # Logical constraints:
337
        # Result from unfolding of base constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
338
339
340
341
342
        # 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
343
        self.__dynamic_constraints = []        # DIMACS clauses: X' = f(X,H,I)
344
        self.__precomputed_dynamic_constraints = []
VIGNET Pierre's avatar
VIGNET Pierre committed
345

346
        # Simple temporal properties:
VIGNET Pierre's avatar
VIGNET Pierre committed
347
348
        # SP(X0): Initial property/start property; Never change at each step.
        # IP(X): Invariant property
349
        # VP(X): Variant property
VIGNET Pierre's avatar
VIGNET Pierre committed
350
        #   List of logical formulas of properties forced at each step
351
        #   It's the trajectory of events of a solution.
VIGNET Pierre's avatar
VIGNET Pierre committed
352
353
        # FP(X): Final property

VIGNET Pierre's avatar
VIGNET Pierre committed
354
355
356
357
358
        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
359
360
361
362
363
364
365
366

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


    def reset(self):
367
368
        """Reset the unfolder before a new query

369
        Reset only properties and dimacs clauses from the current query;
370
        AND __precomputed_variant_constraints.
371

372
373
374
375
        => __initial_constraints, __final_constraints, __invariant_constraints,
        __variant_constraints and __dynamic_constraints ARE NOT reset here
        (see init_forward_unfolding())

376
        This function is called from the constructor and during
377
378
        MCLAnalyser.sq_is_satisfiable() and MCLAnalyser.sq_solutions()
        following the call of init_with_query().
VIGNET Pierre's avatar
VIGNET Pierre committed
379
        """
380
        # Properties to be checked
VIGNET Pierre's avatar
VIGNET Pierre committed
381
382
383
384
385
386
387
388
        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
389
        # list of variant temporal constraints in DIMACS ground code
390
        self.__precomputed_variant_constraints = None  # list<list<DIMACS clauses>>
391

392
393
        # If this function is called from the constructor,
        # the following variables are just redefined here.
394
395
396

        # For reachability optimisation. Number of shifts before checking
        # the final property
VIGNET Pierre's avatar
VIGNET Pierre committed
397
        self.__steps_before_check = 0
VIGNET Pierre's avatar
VIGNET Pierre committed
398
        self.__shift_direction = None     # FORWARD or BACKWARD
VIGNET Pierre's avatar
VIGNET Pierre committed
399
        self.__locked = False
400

401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
    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
        will be raised.

        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):
            # System will be modified; Auxiliary clauses will be added
            # Do not reload cached constraints
            self.__include_aux_clauses_changed = True

        # 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))
431
        if query.dim_variant:
432
433
            # Handle empty steps:
            # Ex: [[], [[4]], [[6], [7]], []]
434
            g = (step for step in query.dim_variant if step)
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
            [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.
        # Since the auxiliary clauses are reset here, this literal is suspect
        # and its use dangerous because its value is not reproductible.
        raise ValueError(
            "%s variable is not in the initial system.\n"
            "Insertion of auxiliary variables is not allowed here."
            % out_of_range_values
        )

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

454
        Following attributes are used from the query:
455
            start_prop, dim_start, inv_prop, dim_inv, final_prop, dim_final,
456
            variant_prop, dim_variant, steps_before_check
457
458

        Textual properties of query are compiled into numeric clauses in
459
460
        init_forward_unfolding(), just at the beginning of squery_is_satisfied()
        and squery_solve().
461
        This compilation step is costly due to ANTLR performances...
462
463

        .. warning:: ALL textual properties are susceptible to add new auxiliary
464
465
466
467
468
469
470
471
472
473
474
475
            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.

        :type query: <MCLSimpleQuery>
        :type check_query: <boolean>
476
        """
477
478
479
        if check_query:
            self.check_query(query)

480
481
        # Reset the unfolder before a new query
        self.reset()
482
        # Init with query properties and clauses
483
484
        self.__initial_property = query.start_prop # logical formula in text
        self.__dimacs_initial = query.dim_start
485

486
487
        self.__final_property = query.final_prop # logical formula in text
        self.__dimacs_final = query.dim_final
488

489
490
        self.__invariant_property = query.inv_prop # logical formula in text
        self.__dimacs_invariant = query.dim_inv
491
492

        # It's the trajectory of events of a solution.
493
        self.__variant_property = query.variant_prop # logical formula in text
494
        self.__dimacs_variant = query.dim_variant
495

496
497
498
        # For reachability optimisation. Number of shifts before checking
        # the final property (default 0)
        self.__steps_before_check = query.steps_before_check
499

VIGNET Pierre's avatar
VIGNET Pierre committed
500
    def set_stats(self):
501
        """Enable solver statistics (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
502
503
504
        self.__stats = True
        self.__nb_vars = 0
        self.__nb_clauses = 0
505

VIGNET Pierre's avatar
VIGNET Pierre committed
506
    def unset_stats(self):
507
        """Disable solver statistics (never used)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
508
        self.__stats = False
509

510
    def stats(self):
511
        """Display solver statistics"""
512
513
        LOGGER.info("NB Variables in solver:", self.__nb_vars)
        LOGGER.info("NB Clauses in solver:", self.__nb_clauses)
514

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

518
        If A->B has clock h, an aux constraint added is h included in h when A
519
520
521
522
523
524
525
        Must be set to False for inhibitors computations.

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

        Tested in by:
            - __forward_init_dynamic
            - __backward_init_dynamic
VIGNET Pierre's avatar
VIGNET Pierre committed
526
527
        """
        self.__include_aux_clauses = val
528
        self.__include_aux_clauses_changed = True
529

530
    ## Internal variable access for tests (never used) #########################
531
532
    @property
    def dynamic_constraints(self):
533
        """For tests: returns coded dynamic constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
534
        return self.__dynamic_constraints
535

536
537
    @property
    def initial_constraints(self):
538
        """For tests: returns coded initial constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
539
        return self.__initial_constraints
540

541
542
    @property
    def invariant_constraints(self):
543
        """For tests: returns coded invariant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
544
        return self.__invariant_constraints
545

546
547
    @property
    def variant_constraints(self):
548
        """For tests: returns coded variant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
549
        return self.__variant_constraints
550

551
552
    @property
    def final_constraints(self):
553
        """For tests: returns coded final constraints"""
554
        return self.__final_constraints
555

556
    ## Variables management ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
557
558
    def var_names_in_clause(self, clause):
        """Return the names of the variables from values in the given numeric clause
559
560
561
562
        (DEBUG never used)
        """
        return [self.get_var_indexed_name(var) for var in clause]

VIGNET Pierre's avatar
VIGNET Pierre committed
563
    def var_dimacs_code(self, var_name):
564
        """Returns DIMACS code of var_name (string) variable (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
565
        return self.__var_code_table[var_name]
566

VIGNET Pierre's avatar
VIGNET Pierre committed
567
    def get_system_var_number(self):
568
569
        """Get number of variables in the clause constraint dynamical system
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
570
571
572

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

VIGNET Pierre's avatar
VIGNET Pierre committed
576
    def get_var_number(self):
577
578
        """Get number of principal variables (properties excluded) in the unfolder
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
579
580
581

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

VIGNET Pierre's avatar
VIGNET Pierre committed
586
    def get_var_name(self, var_num):
587
588
589
590
        """Get name of the variable

        .. seealso:: Explanations on get_var_indexed_name()

VIGNET Pierre's avatar
VIGNET Pierre committed
591
        @param var_num: DIMACS literal coding of an initial variable
592
        @return: name of the variable
VIGNET Pierre's avatar
VIGNET Pierre committed
593
        """
594
        # Get the original var_code without shifts
595
        var_code = (abs(var_num) - 1) % self.__shift_step + 1
596
        if var_code <= self.shift_step_init:
597
598
            # 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
599
            return self.__var_list[var_code]
600
601
602
        else:
            # auxiliary variable introduced by properties compilation
            return self.__aux_list[var_code - self.shift_step_init -1]
VIGNET Pierre's avatar
VIGNET Pierre committed
603
            #raise MCLException("Not a DIMACS code of an initial variable")
604

VIGNET Pierre's avatar
VIGNET Pierre committed
605
    def get_var_indexed_name(self, var_num):
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
        """Get name of the variable with the time index appended

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

            :Example:
                __shift_step = 2 (current step of the unfolding)
                shift_step_init = 2 (number of variables in the system)
                __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"

VIGNET Pierre's avatar
VIGNET Pierre committed
628
        @param var_num: DIMACS literal coding
629
        @return: name of the variable with the time index appended
VIGNET Pierre's avatar
VIGNET Pierre committed
630
        """
631
        varnum1 = abs(var_num)
632
        # Get the original var_code without shifts
VIGNET Pierre's avatar
VIGNET Pierre committed
633
        var_code = (varnum1 - 1) % self.__shift_step + 1
634
        var_step = (varnum1 - var_code) / self.__shift_step
635
        if var_code <= self.shift_step_init:
636
637
            # 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
638
639
            return self.__var_list[var_code] + '_%s'% var_step
        else:
640
641
            # Auxiliary variable introduced by properties compilation
            index = var_code - self.shift_step_init - 1
VIGNET Pierre's avatar
VIGNET Pierre committed
642
            return self.__aux_list[index] + '_%s'% var_step
643

644
645
    @property
    def free_clocks(self):
646
        """Get the DIMACS codes of the free_clocks variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
647
        return self.__free_clocks
648

649
650
    @property
    def inputs(self):
651
        """Get the DIMACS codes of the input variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
652
        return self.__inputs
653

654
655
    @property
    def shift_direction(self):
VIGNET Pierre's avatar
VIGNET Pierre committed
656
657
658
659
        """
        @return: string "FORWARD" or "BACKWARD"
        """
        return self.__shift_direction
660

661
662
    @property
    def shift_step(self):
VIGNET Pierre's avatar
VIGNET Pierre committed
663
664
665
666
        """
        @return: the shift step ss (if n is X_0 code, n+ss is X_1 code)
        """
        return self.__shift_step
667

668
669
    @property
    def current_step(self):
VIGNET Pierre's avatar
VIGNET Pierre committed
670
671
672
673
674
        """
        @return: the current number of unfolding
        """
        return self.__current_step

675

676
    ## Translation from names to num codes #####################################
VIGNET Pierre's avatar
VIGNET Pierre committed
677
    ## The translation depends on the shift direction
VIGNET Pierre's avatar
VIGNET Pierre committed
678
    def __forward_code(self, clause):
679
680
        """(deprecated, directly included in C++ module: forward_init_dynamic())

VIGNET Pierre's avatar
VIGNET Pierre committed
681
        Numerically code a clause with the numeric codes found in
682
        self.__var_code_table for a base variable x,
VIGNET Pierre's avatar
VIGNET Pierre committed
683
        and numeric_code +/- shift_step (according to the sign) for x' variable.
684
685

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

VIGNET Pierre's avatar
VIGNET Pierre committed
689
690
691
        @param clause: a Clause object
        @return: the DIMACS coding of the forward shifted clause
        """
692
693
        # Old API
        # num_clause = []
694
        # for lit in clause.literals:
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
        #     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)

711

VIGNET Pierre's avatar
VIGNET Pierre committed
712
    def __backward_code(self, clause):
713
714
715
716
717
718
        """(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
719
720
721
722
        @param clause: a Clause object
        @return: the DIMACS coding of the backward shifted clause
        """
        num_clause = []
723
724
725
726
727
728
729
730
731
732
733
734
735
        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
736
        return num_clause
737

VIGNET Pierre's avatar
VIGNET Pierre committed
738
    def __code_clause(self, clause):
739
740
741
742
743
        """Numerically code a clause

        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;
744
        assume all variables are basic variables (t=0) (not shifted).
745

746
747
748
749
        @warning: This function MODIFIES SHIFT_STEP because we add a variable
            in the system if a variable is not found in __var_code_table or in
            __aux_code_table.
            A new auxiliary variable will be created in __aux_code_table.
750
751
752
753
754
755

        :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
756
757
        """
        num_clause = []
758
        for lit in clause.literals:
759
            # Get variable value with the given name
VIGNET Pierre's avatar
VIGNET Pierre committed
760
            name = lit.name
761
            if name in self.__var_code_table:
VIGNET Pierre's avatar
VIGNET Pierre committed
762
                var_cod = self.__var_code_table[name]
763
            elif name in self.__aux_code_table:
VIGNET Pierre's avatar
VIGNET Pierre committed
764
                var_cod = self.__aux_code_table[name]
765
766
            else:
                # Create an auxiliary variable - modifies shift_step (nb of variables)
VIGNET Pierre's avatar
VIGNET Pierre committed
767
                self.__shift_step += 1
768
                # Mapping name to value code
VIGNET Pierre's avatar
VIGNET Pierre committed
769
                self.__aux_code_table[name] = self.__shift_step
770
                # Mapping value code to name
VIGNET Pierre's avatar
VIGNET Pierre committed
771
                self.__aux_list.append(name)
772
                # Define var_cod
773
774
775
776
777
                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
778
779
            num_clause.append(lit_code)
        return num_clause
780

781
    ## Dynamic initialisations #################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
782
    def __forward_init_dynamic(self):
783
784
        """Dynamics initialisations.
        Set dynamic constraints for a forward one step: X1 = f(X0)
785

VIGNET Pierre's avatar
VIGNET Pierre committed
786
        Numerically code clauses with the numeric codes found in
787
        self.__var_code_table for a base variable x,
VIGNET Pierre's avatar
VIGNET Pierre committed
788
        and numeric_code +/- shift_step (according to the sign) for x' variable.
VIGNET Pierre's avatar
VIGNET Pierre committed
789
790
791
792

        __dynamic_constraints is a list of lists of numeric clauses (lists of ints)
        Each sublist of __dynamic_constraints corresponds to a step in the unfolder;
        the last step is the last element.
793

794
795
        .. seealso:: __forward_code()

796
        .. note:: Called by init_forward_unfolding()
797

798
        .. note:: Future variables x' are noted "name`" in Literal names.
VIGNET Pierre's avatar
VIGNET Pierre committed
799
800
            The absolute value of these variables will increase by shift_step
            in the next step.
801
        """
802
        # New API via C++ module
803
        # TODO: take a look at __backward_init_dynamic & __backward_code
VIGNET Pierre's avatar
VIGNET Pierre committed
804
        if self.__include_aux_clauses:
805
            # Auxiliary clauses are supported (default)
806
            self.__dynamic_constraints = \
807
                forward_init_dynamic(self.dynamic_system.list_clauses,
808
809
                                     self.__var_code_table,
                                     self.__shift_step,
810
                                     self.dynamic_system.aux_list_clauses)
811
812
        else:
            self.__dynamic_constraints = \
813
                forward_init_dynamic(self.dynamic_system.list_clauses,
814
815
                                     self.__var_code_table,
                                     self.__shift_step)
816

817
818
819
820
        # __dynamic_constraints is initialized and
        # has now taken into account the auxiliary clauses flag
        self.__include_aux_clauses_changed = False

VIGNET Pierre's avatar
VIGNET Pierre committed
821
    def __backward_init_dynamic(self):
822
823
        """Dynamics initialisations. (never used, backward is partially implemented)
        Set dynamic constraints for a forward one step: X0 = f(X1)
824

825
826
        .. note:: Called by init_backward_unfolding()
        """
827
828
        num_clause_list = \
            [self.__backward_code(clause)
829
             for clause in self.dynamic_system.list_clauses]
830

VIGNET Pierre's avatar
VIGNET Pierre committed
831
        if self.__include_aux_clauses:
832
833
            num_clause_list += \
                [self.__backward_code(clause)
834
                 for clause in self.dynamic_system.aux_list_clauses]
835

836
        self.__dynamic_constraints = [num_clause_list]
837

838
    ## Shifting variables: implementation of the shift operator ################
839
    def __shift_clause(self, numeric_clause):
840
841
        """Shift a clause for the current __shift_step

VIGNET Pierre's avatar
VIGNET Pierre committed
842
843
        (no used anymore, replaced by direct use of C++ code)

844
845
846
        Basically, `shift_step` is added to positive variables and subtracted
        from negative variables in `numeric_clause`.

847
        About unfolder lock and shift_step:
848
849
850
851
852
        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.
        Thus, we lock the Unfolder by turning self.__locked to True.

853
        @param numeric_clause: DIMACS clause
VIGNET Pierre's avatar
VIGNET Pierre committed
854
855
        @warning: lock the unfolder
        """
856
857
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True
VIGNET Pierre's avatar
VIGNET Pierre committed
858
859
860

        # Old API
        # Less efficient with abs()
861
862
        # return [(abs(lit) + self.__shift_step) * (-1 if lit < 0 else 1)
        #         for lit in numeric_clause]
VIGNET Pierre's avatar
VIGNET Pierre committed
863
864
        # More efficient with ternary assignment
        # return [(lit + self.__shift_step) if lit > 0 else (lit - self.__shift_step)
865
        #         for lit in numeric_clause]
VIGNET Pierre's avatar
VIGNET Pierre committed
866
867

        # New API via C++ module
868
        return shift_clause(numeric_clause, self.__shift_step)
869

870
    def __m_shift_clause(self, numeric_clause, nb_steps):
871
872
        """Shift a clause for the given step number

873
874
875
876
877
878
879
880
        Each literal will be shifted by (nb_steps * __shift_step).

        Why ?
        Such function is used for clauses that are not already shifted during
        previous steps. It is the case of variant_constraints which come from a
        reloaded/forced trajectory.

        About unfolder lock and shift_step:
881
882
883
884
885
        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.
        Thus, we lock the Unfolder by turning self.__locked to True.

886
887
        Called by: __shift_variant()

888
        @param numeric_clause: DIMACS clause
889
        @param nb_steps: number of shifts asked
VIGNET Pierre's avatar
VIGNET Pierre committed
890
891
        @warning: lock the unfolder
        """
892
893
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True
894

895
        return [(lit + self.__shift_step * nb_steps) if lit > 0
896
                else (lit - self.__shift_step * nb_steps) for lit in numeric_clause]
897

VIGNET Pierre's avatar
VIGNET Pierre committed
898
    def __shift_dynamic(self):
899
900
901
902
        """Shift clauses representing the dynamics X' = f(X,I,C)

        Shift the last item of self.__dynamic_constraints and append the result
        to self.__dynamic_constraints.
VIGNET Pierre's avatar
VIGNET Pierre committed
903

904
905
        .. note:: Called by shift()
        """
906
907
908
909
910
911
912

        if len(self.__precomputed_dynamic_constraints) > self.__current_step:
            # Recall the saved state of the system for the next step
            self.__dynamic_constraints.append(
                self.__precomputed_dynamic_constraints[self.__current_step]
            )
            LOGGER.info(
913
                "shift_dynamic:: OPTI DO NOT SHIFT; "
914
915
916
917
918
919
920
                "Reload dynamic constraints; step: %s",
                self.__current_step
            )
            return

        # System has not been shifted for this step until now
        LOGGER.info(
921
                "shift_dynamic:: SHIFT; "
922
923
924
925
926
                "Set dynamic constraints; step: %s; dyn consts len: %s",
                self.__current_step,
                len(self.__dynamic_constraints)
            )

VIGNET Pierre's avatar
VIGNET Pierre committed
927
928
929
930
931
932
933
        # Old API
        # self.__dynamic_constraints.append(
        #   [self.__shift_clause(clause)
        #    for clause in self.__dynamic_constraints[-1]]
        # )

        # New API via C++ module
934
935
        # __dynamic_constraints:
        # List of lists of DIMACS encoded clauses (lists of ints)
VIGNET Pierre's avatar
VIGNET Pierre committed
936
        self.__dynamic_constraints.append(
937
            shift_dimacs_clauses(
938
                self.__dynamic_constraints[-1], # <list <list <int>>>
VIGNET Pierre's avatar
VIGNET Pierre committed
939
940
941
                self.__shift_step
            )
        )
942

VIGNET Pierre's avatar
VIGNET Pierre committed
943
    def __shift_initial(self):
944
        """Shift initialisation condition
945

946
947
        Shift + replace __initial_constraints

948
949
950
951
        .. note:: Called by:
            - shift()
            - init_backward_unfolding()
        """
952
        self.__initial_constraints = \
953
            shift_dimacs_clauses(
954
955
956
                self.__initial_constraints,
                self.__shift_step
            )
957

VIGNET Pierre's avatar
VIGNET Pierre committed
958
    def __shift_final(self):
959
        """Shift final property
960

961
962
        Shift + replace __final_constraints

963
964
965
966
        .. note:: Called by:
            - shift()
            - init_forward_unfolding()
        """
967
        self.__final_constraints = \
968
            shift_dimacs_clauses(
969
970
971
                self.__final_constraints,
                self.__shift_step
            )
972

VIGNET Pierre's avatar
VIGNET Pierre committed