MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

CLUnfolder.py 75.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

    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
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
        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.
271
272
        # Note: "future" literals are already in self.dynamic_system.clauses
        # and maybe in self.dynamic_system.aux_clauses
273
274
275
        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)
VIGNET Pierre's avatar
VIGNET Pierre committed
294
295
296
297
        self.__no_frontier_init = [
            [-self.__var_code_table[not_front_name]]
            for not_front_name in self.dynamic_system.no_frontiers
        ]
298

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

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

331
        # DIMACS codes of the free_clocks variables/places for extraction (invariant)
332
        self.__free_clocks = frozenset(self.__var_code_table[fcl] for fcl in self.dynamic_system.free_clocks)
333
334

        # Binding for a merged version of __inputs and __free_clocks
335
        # Convenient attribute for RawSolution.extract_act_input_clock_seq()
336
337
        # DIMACS codes of the input and free_clocks variables
        self.inputs_and_free_clocks = self.__inputs | self.__free_clocks
338

339
340
        # Properties to be checked
        self.reset()
341

342
        # Logical constraints:
343
        # Result from unfolding of base constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
344
345
346
347
348
        # 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
349
        self.__dynamic_constraints = []        # DIMACS clauses: X' = f(X,H,I)
350
        self.__precomputed_dynamic_constraints = []
VIGNET Pierre's avatar
VIGNET Pierre committed
351

352
        # Simple temporal properties:
VIGNET Pierre's avatar
VIGNET Pierre committed
353
354
        # SP(X0): Initial property/start property; Never change at each step.
        # IP(X): Invariant property
355
        # VP(X): Variant property
VIGNET Pierre's avatar
VIGNET Pierre committed
356
        #   List of logical formulas of properties forced at each step
357
        #   It's the trajectory of events of a solution.
VIGNET Pierre's avatar
VIGNET Pierre committed
358
359
        # FP(X): Final property

VIGNET Pierre's avatar
VIGNET Pierre committed
360
361
362
363
364
        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
365
366
367
368
369
370
371
372

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


    def reset(self):
373
374
        """Reset the unfolder before a new query

375
        Reset only properties and dimacs clauses from the current query;
376
        AND __precomputed_variant_constraints.
377

378
379
380
381
        => __initial_constraints, __final_constraints, __invariant_constraints,
        __variant_constraints and __dynamic_constraints ARE NOT reset here
        (see init_forward_unfolding())

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

398
399
        # If this function is called from the constructor,
        # the following variables are just redefined here.
400
401
402

        # For reachability optimisation. Number of shifts before checking
        # the final property
VIGNET Pierre's avatar
VIGNET Pierre committed
403
        self.__steps_before_check = 0
VIGNET Pierre's avatar
VIGNET Pierre committed
404
        self.__shift_direction = None     # FORWARD or BACKWARD
VIGNET Pierre's avatar
VIGNET Pierre committed
405
        self.__locked = False
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
431
432
433
434
435
436
    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))
437
        if query.dim_variant:
438
439
            # Handle empty steps:
            # Ex: [[], [[4]], [[6], [7]], []]
440
            g = (step for step in query.dim_variant if step)
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
            [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):
458
459
        """Initialise the unfolder with the given query

460
        Following attributes are used from the query:
461
            start_prop, dim_start, inv_prop, dim_inv, final_prop, dim_final,
462
            variant_prop, dim_variant, steps_before_check
463
464

        Textual properties of query are compiled into numeric clauses in
465
466
        init_forward_unfolding(), just at the beginning of squery_is_satisfied()
        and squery_solve().
467
        This compilation step is costly due to ANTLR performances...
468
469

        .. warning:: ALL textual properties are susceptible to add new auxiliary
470
471
472
473
474
475
476
477
478
479
480
481
            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>
482
        """
483
484
485
        if check_query:
            self.check_query(query)

486
487
        # Reset the unfolder before a new query
        self.reset()
488
        # Init with query properties and clauses
489
490
        self.__initial_property = query.start_prop # logical formula in text
        self.__dimacs_initial = query.dim_start
491

492
493
        self.__final_property = query.final_prop # logical formula in text
        self.__dimacs_final = query.dim_final
494

495
496
        self.__invariant_property = query.inv_prop # logical formula in text
        self.__dimacs_invariant = query.dim_inv
497
498

        # It's the trajectory of events of a solution.
499
        self.__variant_property = query.variant_prop # logical formula in text
500
        self.__dimacs_variant = query.dim_variant
501

502
503
504
        # For reachability optimisation. Number of shifts before checking
        # the final property (default 0)
        self.__steps_before_check = query.steps_before_check
505

VIGNET Pierre's avatar
VIGNET Pierre committed
506
    def set_stats(self):
507
        """Enable solver statistics (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
508
509
510
        self.__stats = True
        self.__nb_vars = 0
        self.__nb_clauses = 0
511

VIGNET Pierre's avatar
VIGNET Pierre committed
512
    def unset_stats(self):
513
        """Disable solver statistics (never used)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
514
        self.__stats = False
515

516
    def stats(self):
517
        """Display solver statistics"""
518
519
        LOGGER.info("NB Variables in solver:", self.__nb_vars)
        LOGGER.info("NB Clauses in solver:", self.__nb_clauses)
520

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

524
        If A->B has clock h, an aux constraint added is h included in h when A
525
526
527
528
529
530
531
        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
532
533
        """
        self.__include_aux_clauses = val
534
        self.__include_aux_clauses_changed = True
535

536
    ## Internal variable access for tests (never used) #########################
537
538
    @property
    def dynamic_constraints(self):
539
        """For tests: returns coded dynamic constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
540
        return self.__dynamic_constraints
541

542
543
    @property
    def initial_constraints(self):
544
        """For tests: returns coded initial constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
545
        return self.__initial_constraints
546

547
548
    @property
    def invariant_constraints(self):
549
        """For tests: returns coded invariant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
550
        return self.__invariant_constraints
551

552
553
    @property
    def variant_constraints(self):
554
        """For tests: returns coded variant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
555
        return self.__variant_constraints
556

557
558
    @property
    def final_constraints(self):
559
        """For tests: returns coded final constraints"""
560
        return self.__final_constraints
561

562
    ## Variables management ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
563
564
    def var_names_in_clause(self, clause):
        """Return the names of the variables from values in the given numeric clause
565
566
567
568
        (DEBUG never used)
        """
        return [self.get_var_indexed_name(var) for var in clause]

VIGNET Pierre's avatar
VIGNET Pierre committed
569
    def var_dimacs_code(self, var_name):
570
        """Returns DIMACS code of var_name (string) variable (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
571
        return self.__var_code_table[var_name]
572

VIGNET Pierre's avatar
VIGNET Pierre committed
573
    def get_system_var_number(self):
574
575
        """Get number of variables in the clause constraint dynamical system
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
576
577
578

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

VIGNET Pierre's avatar
VIGNET Pierre committed
582
    def get_var_number(self):
583
584
        """Get number of principal variables (properties excluded) in the unfolder
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
585
586
587

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

VIGNET Pierre's avatar
VIGNET Pierre committed
592
    def get_var_name(self, var_num):
593
594
        """Get name of the variable

595
        .. seealso:: Explanations are on :meth:`get_var_indexed_name`
596

VIGNET Pierre's avatar
VIGNET Pierre committed
597
        @param var_num: DIMACS literal coding of an initial variable
598
        @return: name of the variable
VIGNET Pierre's avatar
VIGNET Pierre committed
599
        """
600
        # Get the original var_code without shifts
601
        var_code = (abs(var_num) - 1) % self.__shift_step + 1
602
        if var_code <= self.shift_step_init:
603
604
            # 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
605
            return self.__var_list[var_code]
606
        else:
607
608
            # Auxiliary variable introduced by properties compilation
            return self.__aux_list[var_code - self.shift_step_init - 1]
609

VIGNET Pierre's avatar
VIGNET Pierre committed
610
    def get_var_indexed_name(self, var_num):
611
612
613
614
615
        """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
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
        :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"
662

VIGNET Pierre's avatar
VIGNET Pierre committed
663
        @param var_num: DIMACS literal coding
664
        @return: name of the variable with the time index appended
VIGNET Pierre's avatar
VIGNET Pierre committed
665
        """
666
        varnum1 = abs(var_num)
667
        # Get the original var_code without shifts
VIGNET Pierre's avatar
VIGNET Pierre committed
668
        var_code = (varnum1 - 1) % self.__shift_step + 1
669
        var_step = (varnum1 - var_code) / self.__shift_step
670
        if var_code <= self.shift_step_init:
671
672
            # 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
673
674
            return self.__var_list[var_code] + '_%s'% var_step
        else:
675
676
            # Auxiliary variable introduced by properties compilation
            index = var_code - self.shift_step_init - 1
VIGNET Pierre's avatar
VIGNET Pierre committed
677
            return self.__aux_list[index] + '_%s'% var_step
678

679
680
    @property
    def free_clocks(self):
681
        """Get the DIMACS codes of the free_clocks variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
682
        return self.__free_clocks
683

684
685
    @property
    def inputs(self):
686
        """Get the DIMACS codes of the input variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
687
        return self.__inputs
688

689
690
    @property
    def shift_direction(self):
VIGNET Pierre's avatar
VIGNET Pierre committed
691
692
693
694
        """
        @return: string "FORWARD" or "BACKWARD"
        """
        return self.__shift_direction
695

696
697
    @property
    def shift_step(self):
VIGNET Pierre's avatar
VIGNET Pierre committed
698
699
700
701
        """
        @return: the shift step ss (if n is X_0 code, n+ss is X_1 code)
        """
        return self.__shift_step
702

703
704
    @property
    def current_step(self):
VIGNET Pierre's avatar
VIGNET Pierre committed
705
706
707
708
709
        """
        @return: the current number of unfolding
        """
        return self.__current_step

710

711
    ## Translation from names to num codes #####################################
VIGNET Pierre's avatar
VIGNET Pierre committed
712
    ## The translation depends on the shift direction
VIGNET Pierre's avatar
VIGNET Pierre committed
713
    def __forward_code(self, clause):
714
715
        """(deprecated, directly included in C++ module: forward_init_dynamic())

VIGNET Pierre's avatar
VIGNET Pierre committed
716
        Numerically code a clause with the numeric codes found in
717
        self.__var_code_table for a base variable x,
VIGNET Pierre's avatar
VIGNET Pierre committed
718
        and numeric_code +/- shift_step (according to the sign) for x' variable.
719
720

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

VIGNET Pierre's avatar
VIGNET Pierre committed
724
725
726
        @param clause: a Clause object
        @return: the DIMACS coding of the forward shifted clause
        """
727
728
        # Old API
        # num_clause = []
729
        # for lit in clause.literals:
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
        #     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)

746

VIGNET Pierre's avatar
VIGNET Pierre committed
747
    def __backward_code(self, clause):
748
749
750
751
752
753
        """(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
754
755
756
757
        @param clause: a Clause object
        @return: the DIMACS coding of the backward shifted clause
        """
        num_clause = []
758
759
760
761
762
763
764
765
766
767
768
769
770
        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
771
        return num_clause
772

VIGNET Pierre's avatar
VIGNET Pierre committed
773
    def __code_clause(self, clause):
774
775
776
777
778
        """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;
779
        assume all variables are basic variables (t=0) (not shifted).
780

781
782
783
784
        @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.
785
786
787
788
789
790

        :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
791
792
        """
        num_clause = []
793
        for lit in clause.literals:
794
            # Get variable value with the given name
VIGNET Pierre's avatar
VIGNET Pierre committed
795
            name = lit.name
796
            if name in self.__var_code_table:
VIGNET Pierre's avatar
VIGNET Pierre committed
797
                var_cod = self.__var_code_table[name]
798
            elif name in self.__aux_code_table:
VIGNET Pierre's avatar
VIGNET Pierre committed
799
                var_cod = self.__aux_code_table[name]
800
801
            else:
                # Create an auxiliary variable - modifies shift_step (nb of variables)
VIGNET Pierre's avatar
VIGNET Pierre committed
802
                self.__shift_step += 1
803
                # Mapping name to value code
VIGNET Pierre's avatar
VIGNET Pierre committed
804
                self.__aux_code_table[name] = self.__shift_step
805
                # Mapping value code to name
VIGNET Pierre's avatar
VIGNET Pierre committed
806
                self.__aux_list.append(name)
807
                # Define var_cod
808
809
810
811
812
                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
813
814
            num_clause.append(lit_code)
        return num_clause
815

816
    ## Dynamic initialisations #################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
817
    def __forward_init_dynamic(self):
818
819
        """Dynamics initialisations.
        Set dynamic constraints for a forward one step: X1 = f(X0)
820

VIGNET Pierre's avatar
VIGNET Pierre committed
821
        Numerically code clauses with the numeric codes found in
822
        self.__var_code_table for a base variable x,
VIGNET Pierre's avatar
VIGNET Pierre committed
823
        and numeric_code +/- shift_step (according to the sign) for x' variable.
VIGNET Pierre's avatar
VIGNET Pierre committed
824
825
826
827

        __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.
828

829
830
        .. seealso:: __forward_code()

831
        .. note:: Called by init_forward_unfolding()
832

833
        .. note:: Future variables x' are noted "name`" in Literal names.
VIGNET Pierre's avatar
VIGNET Pierre committed
834
835
            The absolute value of these variables will increase by shift_step
            in the next step.
836
        """
837
        # New API via C++ module
838
        # TODO: take a look at __backward_init_dynamic & __backward_code
VIGNET Pierre's avatar
VIGNET Pierre committed
839
        if self.__include_aux_clauses:
840
            # Auxiliary clauses are supported (default)
841
            self.__dynamic_constraints = \
842
                forward_init_dynamic(self.dynamic_system.clauses,
843
844
                                     self.__var_code_table,
                                     self.__shift_step,
845
                                     self.dynamic_system.aux_clauses)
846
847
        else:
            self.__dynamic_constraints = \
848
                forward_init_dynamic(self.dynamic_system.clauses,
849
850
                                     self.__var_code_table,
                                     self.__shift_step)
851

852
853
854
855
        # __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
856
    def __backward_init_dynamic(self):
857
858
        """Dynamics initialisations. (never used, backward is partially implemented)
        Set dynamic constraints for a forward one step: X0 = f(X1)
859

860
861
        .. note:: Called by init_backward_unfolding()
        """
862
863
        num_clause_list = \
            [self.__backward_code(clause)
864
             for clause in self.dynamic_system.clauses]
865

VIGNET Pierre's avatar
VIGNET Pierre committed
866
        if self.__include_aux_clauses:
867
868
            num_clause_list += \
                [self.__backward_code(clause)
869
                 for clause in self.dynamic_system.aux_clauses]
870

871
        self.__dynamic_constraints = [num_clause_list]
872

873
    ## Shifting variables: implementation of the shift operator ################
874
    def __shift_clause(self, numeric_clause):
875
876
        """Shift a clause for the current __shift_step

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

879
880
881
        Basically, `shift_step` is added to positive variables and subtracted
        from negative variables in `numeric_clause`.

882
        About unfolder lock and shift_step:
883
884
885
886
887
        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.

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

        # Old API
        # Less efficient with abs()
896
897
        # return [(abs(lit) + self.__shift_step) * (-1 if lit < 0 else 1)
        #         for lit in numeric_clause]
VIGNET Pierre's avatar
VIGNET Pierre committed
898
899
        # More efficient with ternary assignment
        # return [(lit + self.__shift_step) if lit > 0 else (lit - self.__shift_step)
900
        #         for lit in numeric_clause]
VIGNET Pierre's avatar
VIGNET Pierre committed
901
902

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

905
    def __m_shift_clause(self, numeric_clause, nb_steps):
906
907
        """Shift a clause for the given step number

908
909
910
911
912
913
914
915
        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:
916
917
918
919
920
        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.

921
922
        Called by: __shift_variant()

923
        @param numeric_clause: DIMACS clause
924
        @param nb_steps: number of shifts asked
VIGNET Pierre's avatar
VIGNET Pierre committed
925
926
        @warning: lock the unfolder
        """
927
928
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True
929

930
        return [(lit + self.__shift_step * nb_steps) if lit > 0
931
                else (lit - self.__shift_step * nb_steps) for lit in numeric_clause]
932

VIGNET Pierre's avatar
VIGNET Pierre committed
933
    def __shift_dynamic(self):
934
935
936
937
        """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
938

939
940
        .. note:: Called by shift()
        """
941
942
943
944
945
946
947

        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(
948
                "shift_dynamic:: OPTI DO NOT SHIFT; "
949
950
951
952
953
954
955
                "Reload dynamic constraints; step: %s",
                self.__current_step
            )
            return

        # System has not been shifted for this step until now
        LOGGER.info(
956
                "shift_dynamic:: SHIFT; "
957
958
959
960
961
                "Set dynamic constraints; step: %s; dyn consts len: %s",
                self.__current_step,
                len(self.__dynamic_constraints)
            )

VIGNET Pierre's avatar
VIGNET Pierre committed
962
963
964
965
966
967
968
        # Old API
        # self.__dynamic_constraints.append(
        #   [self.__shift_clause(clause)
        #    for clause in self.__dynamic_constraints[-1]]
        # )

        # New API via C++ module
969
970
        # __dynamic_constraints:
        # List of lists of DIMACS encoded clauses (lists of ints)
VIGNET Pierre's avatar
VIGNET Pierre committed
971
        self.__dynamic_constraints.append(
972
            shift_dimacs_clauses(
973
                self.__dynamic_constraints[-1], # <list <list <int>>>
VIGNET Pierre's avatar
VIGNET Pierre committed
974
975
976
                self.__shift_step
            )
        )
977

VIGNET Pierre's avatar
VIGNET Pierre committed
978
    def __shift_initial(self):
979
        """Shift initialisation condition
980

981
982
        Shift + replace __initial_constraints

983
984
985
986
        .. note:: Called by:
            - shift()
            - init_backward_unfolding()
        """
987
        self.__initial_constraints = \