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

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


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

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

57
58
59
60
61
62
63
---

About shifting clauses and variables:

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

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

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

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

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

80
81
---

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

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

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


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

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

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

        PS: __variant_constraints si already initialized for the first step

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

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

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


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

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

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

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
163
164
#from pyCryptoMS import CryptoMS
from pycryptosat import Solver as CryptoMS
165
from pycryptosat import __version__ as solver_version
166
167
168
from cadbiom.models.biosignal.translators.gt_visitors import compile_cond, compile_event
from cadbiom.models.clause_constraints.CLDynSys import Clause, Literal
from cadbiom.models.clause_constraints.mcl.MCLSolutions import RawSolution, MCLException
169
from cadbiom import commons as cm
VIGNET Pierre's avatar
VIGNET Pierre committed
170
171

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

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

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

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

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

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

    Glossary
VIGNET Pierre's avatar
VIGNET Pierre committed
204
    ========
205
    - ground variables/ground DIMACS code: variables at time t=0 (not shifted).
VIGNET Pierre's avatar
VIGNET Pierre committed
206
    - solution: a solution of the logical dynamic constraint from SAT solver
207
    - state vector: list of DIMACS code of original (not shifted) variables
VIGNET Pierre's avatar
VIGNET Pierre committed
208
209
      corresponding to a step.
    - trajectory: list of state_vectors
210
211
212
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
        """
        :param dynamic_system: Describe a dynamic system in clause form.
VIGNET Pierre's avatar
VIGNET Pierre committed
224
225
226
227
        :key debug: (Optional) Used to activate debug mode in the Unfolder.
            i.e. `__var_list` attribute will be ordered, and initializations of
            the unfolder will be reproductible.
            Default: False.
228
        :type dynamic_system: <CLDynSys>
VIGNET Pierre's avatar
VIGNET Pierre committed
229
        :type debug: <boolean>
230
        """
231
        self.dynamic_system = dynamic_system # symbolic clause dynamic system
232

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

237
        # 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
238
        self.shift_step_init = dynamic_system.get_var_number()
239
        self.__shift_step = self.shift_step_init
240

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

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

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

272
273
274
275
276
277
        # 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.
278
279
        # Note: "future" literals are already in self.dynamic_system.clauses
        # and maybe in self.dynamic_system.aux_clauses
280
281
282
        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)
283

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

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

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

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

        # Frontiers:
        # Ordered list of DIMACS codes of the frontier variables/places
VIGNET Pierre's avatar
VIGNET Pierre committed
321
322
323
324
        self.frontier_values = [
            self.__var_code_table[front_name]
            for front_name in self.dynamic_system.frontiers
        ]
325
        self.frontier_values.sort()
VIGNET Pierre's avatar
VIGNET Pierre committed
326
327
        ## TODO: Utiliser une liste triée est-il utile ici ?
        ## si non passer utiliser un frozenset et supprimer les casts partout
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
        ## 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)
346
347
348
349
        self.frontiers_pos_and_neg = \
            self.frontiers_negative_values | frozenset(self.frontier_values)

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

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

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

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

363
        # Logical constraints:
364
        # Result from unfolding of base constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
365
366
367
368
369
        # 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
370
        self.__dynamic_constraints = []        # DIMACS clauses: X' = f(X,H,I)
371
        self.__precomputed_dynamic_constraints = []
VIGNET Pierre's avatar
VIGNET Pierre committed
372

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

VIGNET Pierre's avatar
VIGNET Pierre committed
381
382
383
384
385
        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
386
387
388
389
390
391
392
393

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


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

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

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

403
        This function is called from the constructor and during
VIGNET Pierre's avatar
VIGNET Pierre committed
404
405
406
407
408
        :meth:`MCLAnalyser.sq_is_satisfiable()
        <cadbiom.models.clause_constraints.mcl.MCLAnalyser.MCLAnalyser.sq_is_satisfiable>`
        and :meth:`MCLAnalyser.sq_is_satisfiable()
        <cadbiom.models.clause_constraints.mcl.MCLAnalyser.MCLAnalyser.sq_solutions>`
        following the call of :meth:`init_with_query`.
VIGNET Pierre's avatar
VIGNET Pierre committed
409
        """
410
        # Properties to be checked
VIGNET Pierre's avatar
VIGNET Pierre committed
411
412
413
414
415
416
417
418
        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
419
        # list of variant temporal constraints in DIMACS ground code
420
        self.__precomputed_variant_constraints = None  # list<list<DIMACS clauses>>
421

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

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

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

438
439
440
441
442
443
444
445
    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
446
447
448
449
450
451
452
453
454
455
456
        will be raised. Indeed, literals **can't** be used without a proper init.

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

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

        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):
470
471
472
            # Properties have changed:
            # The system will be modified; Auxiliary clauses will be added.
            # Do not reload cached constraints. Cf init_forward_unfolding()
473
474
            self.__include_aux_clauses_changed = True

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

481
482
483
484
        # 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))
485
        if query.dim_variant:
486
            # Handle empty steps:
487
            # Ex: [[[12], [1]], [[58], [47]], []]
488
            g = (step for step in query.dim_variant if step)
489
490
491
492
493
494
495
496
497
            [values.update(it.chain(*step)) for step in g]

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

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

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

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

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

        .. warning:: ALL textual properties are susceptible to add new auxiliary
519
520
521
522
523
524
525
526
527
528
529
530
            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>
531
        """
532
533
534
        if check_query:
            self.check_query(query)

535
536
        # Reset the unfolder before a new query
        self.reset()
537
        # Init with query properties and clauses
538
539
        self.__initial_property = query.start_prop # logical formula in text
        self.__dimacs_initial = query.dim_start
540

541
542
        self.__final_property = query.final_prop # logical formula in text
        self.__dimacs_final = query.dim_final
543

544
545
        self.__invariant_property = query.inv_prop # logical formula in text
        self.__dimacs_invariant = query.dim_inv
546
547

        # It's the trajectory of events of a solution.
548
        self.__variant_property = query.variant_prop # logical formula in text
549
        self.__dimacs_variant = query.dim_variant
550

551
552
553
        # For reachability optimisation. Number of shifts before checking
        # the final property (default 0)
        self.__steps_before_check = query.steps_before_check
554

VIGNET Pierre's avatar
VIGNET Pierre committed
555
    def set_stats(self):
556
        """Enable solver statistics (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
557
558
559
        self.__stats = True
        self.__nb_vars = 0
        self.__nb_clauses = 0
560

VIGNET Pierre's avatar
VIGNET Pierre committed
561
    def unset_stats(self):
562
        """Disable solver statistics (never used)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
563
        self.__stats = False
564

565
    def stats(self):
566
        """Display solver statistics"""
567
568
        LOGGER.info("NB Variables in solver:", self.__nb_vars)
        LOGGER.info("NB Clauses in solver:", self.__nb_clauses)
569

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

573
        If A->B has clock h, an aux constraint added is h included in h when A
574
575
576
577
        Must be set to False for inhibitors computations.

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

VIGNET Pierre's avatar
VIGNET Pierre committed
578
        Tested by:
579
580
            - __forward_init_dynamic
            - __backward_init_dynamic
VIGNET Pierre's avatar
VIGNET Pierre committed
581
582
        """
        self.__include_aux_clauses = val
583
        self.__include_aux_clauses_changed = True
584

585
    ## Internal variable access for tests (never used) #########################
586
587
    @property
    def dynamic_constraints(self):
588
        """For tests: returns coded dynamic constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
589
        return self.__dynamic_constraints
590

591
592
    @property
    def initial_constraints(self):
593
        """For tests: returns coded initial constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
594
        return self.__initial_constraints
595

596
597
    @property
    def invariant_constraints(self):
598
        """For tests: returns coded invariant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
599
        return self.__invariant_constraints
600

601
602
    @property
    def variant_constraints(self):
603
        """For tests: returns coded variant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
604
        return self.__variant_constraints
605

606
607
    @property
    def final_constraints(self):
608
        """For tests: returns coded final constraints"""
609
        return self.__final_constraints
610

611
    ## Variables management ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
612
613
    def var_names_in_clause(self, clause):
        """Return the names of the variables from values in the given numeric clause
614
615
616
617
        (DEBUG never used)
        """
        return [self.get_var_indexed_name(var) for var in clause]

VIGNET Pierre's avatar
VIGNET Pierre committed
618
    def var_dimacs_code(self, var_name):
619
        """Returns DIMACS code of var_name (string) variable (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
620
        return self.__var_code_table[var_name]
621

VIGNET Pierre's avatar
VIGNET Pierre committed
622
    def get_system_var_number(self):
623
624
        """Get number of variables in the clause constraint dynamical system
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
625
626
627

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

VIGNET Pierre's avatar
VIGNET Pierre committed
631
    def get_var_number(self):
632
633
        """Get number of principal variables (properties excluded) in the unfolder
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
634
635
636

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

VIGNET Pierre's avatar
VIGNET Pierre committed
641
    def get_var_name(self, var_num):
642
643
        """Get name of the variable

644
        .. seealso:: Explanations on :meth:`get_var_indexed_name`
645

VIGNET Pierre's avatar
VIGNET Pierre committed
646
        @param var_num: DIMACS literal coding of an initial variable
647
        @return: name of the variable
VIGNET Pierre's avatar
VIGNET Pierre committed
648
        """
649
        # Get the original var_code without shifts
650
        var_code = (abs(var_num) - 1) % self.__shift_step + 1
651
        if var_code <= self.shift_step_init:
652
653
            # 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
654
            return self.__var_list[var_code]
655
        else:
656
657
            # Auxiliary variable introduced by properties compilation
            return self.__aux_list[var_code - self.shift_step_init - 1]
658

VIGNET Pierre's avatar
VIGNET Pierre committed
659
    def get_var_indexed_name(self, var_num):
660
661
662
663
664
        """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
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
        :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"
711

VIGNET Pierre's avatar
VIGNET Pierre committed
712
        @param var_num: DIMACS literal coding
713
        @return: name of the variable with the time index appended
VIGNET Pierre's avatar
VIGNET Pierre committed
714
        """
715
        varnum1 = abs(var_num)
716
        # Get the original var_code without shifts
VIGNET Pierre's avatar
VIGNET Pierre committed
717
        var_code = (varnum1 - 1) % self.__shift_step + 1
718
        var_step = (varnum1 - var_code) / self.__shift_step
719
        if var_code <= self.shift_step_init:
720
721
            # 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
722
723
            return self.__var_list[var_code] + '_%s'% var_step
        else:
724
725
            # Auxiliary variable introduced by properties compilation
            index = var_code - self.shift_step_init - 1
VIGNET Pierre's avatar
VIGNET Pierre committed
726
            return self.__aux_list[index] + '_%s'% var_step
727

728
729
    @property
    def free_clocks(self):
730
        """Get the DIMACS codes of the free_clocks variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
731
        return self.__free_clocks
732

733
734
    @property
    def inputs(self):
735
        """Get the DIMACS codes of the input variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
736
        return self.__inputs
737

738
739
    @property
    def shift_direction(self):
VIGNET Pierre's avatar
VIGNET Pierre committed
740
741
742
743
        """
        @return: string "FORWARD" or "BACKWARD"
        """
        return self.__shift_direction
744

745
746
    @property
    def shift_step(self):
VIGNET Pierre's avatar
VIGNET Pierre committed
747
748
749
750
        """
        @return: the shift step ss (if n is X_0 code, n+ss is X_1 code)
        """
        return self.__shift_step
751

752
753
    @property
    def current_step(self):
VIGNET Pierre's avatar
VIGNET Pierre committed
754
755
756
757
758
        """
        @return: the current number of unfolding
        """
        return self.__current_step

759

760
    ## Translation from names to num codes #####################################
VIGNET Pierre's avatar
VIGNET Pierre committed
761
    ## The translation depends on the shift direction
VIGNET Pierre's avatar
VIGNET Pierre committed
762
    def __forward_code(self, clause):
763
764
765
        """Deprecated, directly included in C++ module

        .. seelalso:: :meth:`forward_init_dynamic`
766

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

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

775
776
        :param clause: A Clause object
        :return: The DIMACS coding of the forward shifted clause
VIGNET Pierre's avatar
VIGNET Pierre committed
777
        """
778
779
        # Old API
        # num_clause = []
780
        # for lit in clause.literals:
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
        #     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)

797

VIGNET Pierre's avatar
VIGNET Pierre committed
798
    def __backward_code(self, clause):
799
800
801
802
803
804
        """(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
805
806
807
808
        @param clause: a Clause object
        @return: the DIMACS coding of the backward shifted clause
        """
        num_clause = []
809
810
811
812
813
814
815
816
817
818
819
820
821
        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
822
        return num_clause
823

VIGNET Pierre's avatar
VIGNET Pierre committed
824
    def __code_clause(self, clause):
825
826
        """Numerically code a clause

827
828
829
830
        The numerical values are found in:
            - self.__var_code_table for variables in the dynamic system,
            - or in self.__aux_code_table for other auxiliary variables;
        We assume all variables are ground variables (not shifted).
831

832
833
834
835
        .. warning:: This function MODIFIES SHIFT_STEP because we add a variable
            in the system if a variable is found neither in __var_code_table nor
            in __aux_code_table.
            Thus, a new auxiliary variable will be created.
836
837
838
839
840
841

        :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
842
843
        """
        num_clause = []
844
        for lit in clause.literals:
845
            # Get variable value with the given name
VIGNET Pierre's avatar
VIGNET Pierre committed
846
            name = lit.name
847
            if name in self.__var_code_table:
VIGNET Pierre's avatar
VIGNET Pierre committed
848
                var_cod = self.__var_code_table[name]
849
            elif name in self.__aux_code_table:
VIGNET Pierre's avatar
VIGNET Pierre committed
850
                var_cod = self.__aux_code_table[name]
851
852
            else:
                # Create an auxiliary variable - modifies shift_step (nb of variables)
VIGNET Pierre's avatar
VIGNET Pierre committed
853
                self.__shift_step += 1
854
                # Mapping name to value code
VIGNET Pierre's avatar
VIGNET Pierre committed
855
                self.__aux_code_table[name] = self.__shift_step
856
                # Mapping value code to name
VIGNET Pierre's avatar
VIGNET Pierre committed
857
                self.__aux_list.append(name)
858
                # Define var_cod
859
860
861
862
863
                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
864
865
            num_clause.append(lit_code)
        return num_clause
866

867
    ## Dynamic initialisations #################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
868
    def __forward_init_dynamic(self):
869
870
        """Dynamics initialisations.
        Set dynamic constraints for a forward one step: X1 = f(X0)
871

VIGNET Pierre's avatar
VIGNET Pierre committed
872
        Numerically code clauses with the numeric codes found in
873
        self.__var_code_table for a base variable x,
VIGNET Pierre's avatar
VIGNET Pierre committed
874
        and numeric_code +/- shift_step (according to the sign) for x' variable.
VIGNET Pierre's avatar
VIGNET Pierre committed
875
876
877
878

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

880
        .. seealso:: :meth:`__forward_code`
881

882
        .. note:: Called by :meth:`init_forward_unfolding`
883

884
        .. note:: Future variables x' are noted "name`" in Literal names.
VIGNET Pierre's avatar
VIGNET Pierre committed
885
886
            The absolute value of these variables will increase by shift_step
            in the next step.
887
        """
888
        # New API via C++ module
VIGNET Pierre's avatar
VIGNET Pierre committed
889
        if self.__include_aux_clauses:
890
            # Auxiliary clauses are supported (default)
891
            self.__dynamic_constraints = \
892
                forward_init_dynamic(self.dynamic_system.clauses,
893
894
                                     self.__var_code_table,
                                     self.__shift_step,
895
                                     self.dynamic_system.aux_clauses)
896
897
        else:
            self.__dynamic_constraints = \
898
                forward_init_dynamic(self.dynamic_system.clauses,
899
900
                                     self.__var_code_table,
                                     self.__shift_step)
901

902
903
904
905
        # __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
906
    def __backward_init_dynamic(self):
907
908
        """Dynamics initialisations. (never used, backward is partially implemented)
        Set dynamic constraints for a forward one step: X0 = f(X1)
909

910
911
        .. note:: Called by init_backward_unfolding()
        """
912
913
        num_clause_list = \
            [self.__backward_code(clause)
914
             for clause in self.dynamic_system.clauses]
915

VIGNET Pierre's avatar
VIGNET Pierre committed
916
        if self.__include_aux_clauses:
917
918
            num_clause_list += \
                [self.__backward_code(clause)
919
                 for clause in self.dynamic_system.aux_clauses]
920

921
        self.__dynamic_constraints = [num_clause_list]
922

923
    ## Shifting variables: implementation of the shift operator ################
924
    def __shift_clause(self, numeric_clause):
925
926
        """Shift a clause for the current __shift_step

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

929
930
931
        Basically, `shift_step` is added to positive variables and subtracted
        from negative variables in `numeric_clause`.

932
        About unfolder lock and shift_step:
933
934
935
936
937
        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.

938
        @param numeric_clause: DIMACS clause
VIGNET Pierre's avatar
VIGNET Pierre committed
939
940
        @warning: lock the unfolder
        """
941
942
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True
VIGNET Pierre's avatar
VIGNET Pierre committed
943
944
945

        # Old API
        # Less efficient with abs()
946
947
        # return [(abs(lit) + self.__shift_step) * (-1 if lit < 0 else 1)
        #         for lit in numeric_clause]
VIGNET Pierre's avatar
VIGNET Pierre committed
948
949
        # More efficient with ternary assignment
        # return [(lit + self.__shift_step) if lit > 0 else (lit - self.__shift_step)
950
        #         for lit in numeric_clause]
VIGNET Pierre's avatar
VIGNET Pierre committed
951
952

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

955
    def __shift_ground_clause(self, numeric_clause, nb_steps):
956
957
        """Shift a clause for the given step number

958
959
960
961
962
        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
963
        reloaded/forced trajectory and is composed of ground variables.
964
965

        About unfolder lock and shift_step:
966
967
        self.shift_step must be frozen in order to avoid problems during the
        unflatten() step of RawSolutions.
968
        => Indeed, each step MUST have the same number of variables.
969
970
        Thus, we lock the Unfolder by turning self.__locked to True.

971
972
        Called by: __shift_variant()