CLUnfolder.py 76.5 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
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)
230
        # This number can change if auxiliary clauses are added.
VIGNET Pierre's avatar
VIGNET Pierre committed
231

232
        # 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
233
        self.shift_step_init = dynamic_system.get_var_number()
234
        self.__shift_step = self.shift_step_init
235

236
        # About unfolder lock and shift_step:
VIGNET Pierre's avatar
VIGNET Pierre committed
237
        # shift_step must be frozen in order to avoid problems during the
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.
241
        # See __shift_clause() and __shift_ground_clause()
VIGNET Pierre's avatar
VIGNET Pierre committed
242
        self.__locked = False
243
244
245
        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
246
        self.__steps_before_check = 0
247

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

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

267
268
269
270
271
272
        # 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.
273
274
        # Note: "future" literals are already in self.dynamic_system.clauses
        # and maybe in self.dynamic_system.aux_clauses
275
276
277
        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)
278

279
        assert len(self.__var_code_table) == 2 * self.__shift_step
280

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

288
289
290
291
        # 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
292
        self.__aux_list = []                      # code to name
293

294
295
        # 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
296
297
298
299
        self.__no_frontier_init = [
            [-self.__var_code_table[not_front_name]]
            for not_front_name in self.dynamic_system.no_frontiers
        ]
300

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

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

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

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

341
342
        # Properties to be checked
        self.reset()
343

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

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

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

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


    def reset(self):
375
376
        """Reset the unfolder before a new query

377
        Reset only properties and dimacs clauses from the current query;
378
        AND __precomputed_variant_constraints.
379

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

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

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

        # For reachability optimisation. Number of shifts before checking
        # the final property
VIGNET Pierre's avatar
VIGNET Pierre committed
405
        self.__steps_before_check = 0
VIGNET Pierre's avatar
VIGNET Pierre committed
406
        self.__shift_direction = None     # FORWARD or BACKWARD
VIGNET Pierre's avatar
VIGNET Pierre committed
407
        self.__locked = False
408
        self.__lit_cpt = self.shift_step_init + 1
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
437
438
439
    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))
440
        if query.dim_variant:
441
            # Handle empty steps:
442
            # Ex: [[[12], [1]], [[58], [47]], [[104], [93]]
443
            g = (step for step in query.dim_variant if step)
444
445
446
447
448
449
450
451
452
453
454
            [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(
455
            "%s variable(s) is/are not in the initial system.\n"
456
457
458
459
460
            "Insertion of auxiliary variables is not allowed here."
            % out_of_range_values
        )

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

463
        Following attributes are used from the query:
464
            start_prop, dim_start, inv_prop, dim_inv, final_prop, dim_final,
465
            variant_prop, dim_variant, steps_before_check
466
467

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

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

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

495
496
        self.__final_property = query.final_prop # logical formula in text
        self.__dimacs_final = query.dim_final
497

498
499
        self.__invariant_property = query.inv_prop # logical formula in text
        self.__dimacs_invariant = query.dim_inv
500
501

        # It's the trajectory of events of a solution.
502
        self.__variant_property = query.variant_prop # logical formula in text
503
        self.__dimacs_variant = query.dim_variant
504

505
506
507
        # For reachability optimisation. Number of shifts before checking
        # the final property (default 0)
        self.__steps_before_check = query.steps_before_check
508

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

VIGNET Pierre's avatar
VIGNET Pierre committed
515
    def unset_stats(self):
516
        """Disable solver statistics (never used)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
517
        self.__stats = False
518

519
    def stats(self):
520
        """Display solver statistics"""
521
522
        LOGGER.info("NB Variables in solver:", self.__nb_vars)
        LOGGER.info("NB Clauses in solver:", self.__nb_clauses)
523

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

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

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

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

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

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

560
561
    @property
    def final_constraints(self):
562
        """For tests: returns coded final constraints"""
563
        return self.__final_constraints
564

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

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

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

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

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
595
    def get_var_name(self, var_num):
596
597
        """Get name of the variable

598
        .. seealso:: Explanations on :meth:`get_var_indexed_name`
599

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

VIGNET Pierre's avatar
VIGNET Pierre committed
613
    def get_var_indexed_name(self, var_num):
614
615
616
617
618
        """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
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
662
663
664
        :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"
665

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

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

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

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

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

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

713

714
    ## Translation from names to num codes #####################################
VIGNET Pierre's avatar
VIGNET Pierre committed
715
    ## The translation depends on the shift direction
VIGNET Pierre's avatar
VIGNET Pierre committed
716
    def __forward_code(self, clause):
717
718
719
        """Deprecated, directly included in C++ module

        .. seelalso:: :meth:`forward_init_dynamic`
720

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

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

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

751

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

VIGNET Pierre's avatar
VIGNET Pierre committed
778
    def __code_clause(self, clause):
779
780
        """Numerically code a clause

781
782
783
784
        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).
785

786
787
788
789
        .. 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.
790
791
792
793
794
795

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

821
    ## Dynamic initialisations #################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
822
    def __forward_init_dynamic(self):
823
824
        """Dynamics initialisations.
        Set dynamic constraints for a forward one step: X1 = f(X0)
825

VIGNET Pierre's avatar
VIGNET Pierre committed
826
        Numerically code clauses with the numeric codes found in
827
        self.__var_code_table for a base variable x,
VIGNET Pierre's avatar
VIGNET Pierre committed
828
        and numeric_code +/- shift_step (according to the sign) for x' variable.
VIGNET Pierre's avatar
VIGNET Pierre committed
829
830
831
832

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

834
        .. seealso:: :meth:`__forward_code`
835

836
        .. note:: Called by :meth:`init_forward_unfolding`
837

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

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

865
866
        .. note:: Called by init_backward_unfolding()
        """
867
868
        num_clause_list = \
            [self.__backward_code(clause)
869
             for clause in self.dynamic_system.clauses]
870

VIGNET Pierre's avatar
VIGNET Pierre committed
871
        if self.__include_aux_clauses:
872
873
            num_clause_list += \
                [self.__backward_code(clause)
874
                 for clause in self.dynamic_system.aux_clauses]
875

876
        self.__dynamic_constraints = [num_clause_list]
877

878
    ## Shifting variables: implementation of the shift operator ################
879
    def __shift_clause(self, numeric_clause):
880
881
        """Shift a clause for the current __shift_step

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

884
885
886
        Basically, `shift_step` is added to positive variables and subtracted
        from negative variables in `numeric_clause`.

887
        About unfolder lock and shift_step:
888
889
890
891
892
        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.

893
        @param numeric_clause: DIMACS clause
VIGNET Pierre's avatar
VIGNET Pierre committed
894
895
        @warning: lock the unfolder
        """
896
897
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True
VIGNET Pierre's avatar
VIGNET Pierre committed
898
899
900

        # Old API
        # Less efficient with abs()
901
902
        # return [(abs(lit) + self.__shift_step) * (-1 if lit < 0 else 1)
        #         for lit in numeric_clause]
VIGNET Pierre's avatar
VIGNET Pierre committed
903
904
        # More efficient with ternary assignment
        # return [(lit + self.__shift_step) if lit > 0 else (lit - self.__shift_step)
905
        #         for lit in numeric_clause]
VIGNET Pierre's avatar
VIGNET Pierre committed
906
907

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

910
    def __shift_ground_clause(self, numeric_clause, nb_steps):
911
912
        """Shift a clause for the given step number

913
914
915
916
917
        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
918
        reloaded/forced trajectory and is composed of ground variables.
919
920

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

926
927
        Called by: __shift_variant()

928
        @param numeric_clause: DIMACS clause
929
        @param nb_steps: number of shifts asked
VIGNET Pierre's avatar
VIGNET Pierre committed
930
931
        @warning: lock the unfolder
        """
932
933
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True
934

935
936
937
        shift_offset = self.__shift_step * nb_steps
        return [(lit + shift_offset) if lit > 0 else (lit - shift_offset)
                for lit in numeric_clause]
938

VIGNET Pierre's avatar
VIGNET Pierre committed
939
    def __shift_dynamic(self):
940
941
942
943
        """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
944

945
946
        .. note:: Called by shift()
        """
947
948
949
950
951
952
953

        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(
954
                "shift_dynamic:: OPTI DO NOT SHIFT; "
955
956
957
958
959
960
961
                "Reload dynamic constraints; step: %s",
                self.__current_step
            )
            return

        # System has not been shifted for this step until now
        LOGGER.info(
962
                "shift_dynamic:: SHIFT; "
963
964
965
966
967
                "Set dynamic constraints; step: %s; dyn consts len: %s",
                self.__current_step,
                len(self.__dynamic_constraints)
            )

VIGNET Pierre's avatar