CLUnfolder.py 43.9 KB
Newer Older
VIGNET Pierre's avatar
VIGNET Pierre committed
1
2
3
## Filename    : CLUnfolder.py
## Author(s)   : Michel Le Borgne
## Created     : 22 mars 2012
4
5
## Revision    :
## Source      :
VIGNET Pierre's avatar
VIGNET Pierre committed
6
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
##
## 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
36
37
##     35042 RENNES Cedex, FRANCE
##
VIGNET Pierre's avatar
VIGNET Pierre committed
38
39
40
41
42
43
##
## Contributor(s): Geoffroy Andrieux IRSET
##
"""
Main engine for constraint unfolding and solving
"""
VIGNET Pierre's avatar
VIGNET Pierre committed
44
45
#from pyCryptoMS import CryptoMS
from pycryptosat import Solver as CryptoMS
46
47
48
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
49
from cadbiom import commons as cm
VIGNET Pierre's avatar
VIGNET Pierre committed
50
51
52
53
54
55

# C++ API
from _cadbiom import shift_clause, shift_dynamic, forward_code, \
                     forward_init_dynamic

# Standard imports
56
from logging import DEBUG
VIGNET Pierre's avatar
VIGNET Pierre committed
57
import itertools as it
58
59

LOGGER = cm.logger()
VIGNET Pierre's avatar
VIGNET Pierre committed
60
61
62
63
64
65
66
67
68

class CLUnfolder(object):
    """
    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).
    During unfolding, clauses are shifted either to the future (forward) or
    to the past (backward). The shift operator is a simple addition
69
70
    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
71
    to add variables while generating a trajectory unfolding.
72
73

    Glossary
VIGNET Pierre's avatar
VIGNET Pierre committed
74
75
76
    ========
    - ground variables/ground dimacs code: variables at time 0/their encoding.
    - solution: a solution of the logical dynamic constraint from SAT solver
77
    - state vector: list of DIMACS code of original (not shifted) variables
VIGNET Pierre's avatar
VIGNET Pierre committed
78
79
80
      corresponding to a step.
    - trajectory: list of state_vectors
    """
81

VIGNET Pierre's avatar
VIGNET Pierre committed
82
83
    def __init__(self, sys):
        self.__dyn_sys = sys # symbolic clause dynamic system
84
85

        # shift_step equal to the total number of coded variables
VIGNET Pierre's avatar
VIGNET Pierre committed
86
87
88
89
90
91
        self.__shift_step_init = sys.get_var_number() # shift step of system
        self.__shift_step = self.__shift_step_init    #  current shift/step
        self.__locked = False
        self.__current_step = 1
        self.__steps_before_check = 0
        self.__include_aux_clauses = True
92

VIGNET Pierre's avatar
VIGNET Pierre committed
93
94
        # assign a DIMACS code number to each variable (invariant)
        self.__lit_cpt = self.__shift_step +1 # counter for aux. var. coding
95
        self.__var_code_table = dict()            # name -> DIMACS code
VIGNET Pierre's avatar
VIGNET Pierre committed
96
97
98
99
100
101
102
        self.__var_list = ['##']                  # DIMACS code -> name - != 0
        cpt = 1
        for svar in sys.base_var_set:
            self.__var_list.append(svar)
            self.__var_code_table[svar] = cpt
            cpt += 1
        assert(cpt == self.__shift_step + 1)
103

VIGNET Pierre's avatar
VIGNET Pierre committed
104
        # same tools for auxiliary variables from property compilation
105
        self.__aux_code_table = dict()            # name 2 code
VIGNET Pierre's avatar
VIGNET Pierre committed
106
        self.__aux_list = []                      # code to name
107
108

        # list  no_frontier place DIMACS codes
109
        self.__no_frontier_init = [[-self.__var_code_table[nfp]] for nfp in self.__dyn_sys.no_frontier]
110

VIGNET Pierre's avatar
VIGNET Pierre committed
111
        # ordered list of frontier place DIMACS codes for extraction (inv)
112
        self.__frontier = [self.__var_code_table[frp] for frp in self.__dyn_sys.frontier]
VIGNET Pierre's avatar
VIGNET Pierre committed
113
        self.__frontier.sort()
114
115
116
117
118
        # Convenient attribute for RawSolution.extract_frontier_values()
        # all frontiers and their opposite version
        # operations with sets are much faster
        self._frontiers_pos_and_neg = \
            frozenset(-frontier for frontier in self.__frontier) | frozenset(self.__frontier)
119

VIGNET Pierre's avatar
VIGNET Pierre committed
120
        # ordered list of input places DIMACS code for extraction (inv)
121
        self.__inputs = frozenset(self.__var_code_table[inp] for inp in self.__dyn_sys.inputs)
122

VIGNET Pierre's avatar
VIGNET Pierre committed
123
        # ordered list of free clocks DIMACS code for extraction (invariant)
124
125
126
127
128
        self.__free_clocks = frozenset(self.__var_code_table[fcl] for fcl in self.__dyn_sys.free_clocks)

        # Binding for a merged version of __inputs and __free_clocks
        # Convenient attribute for RawSolution.extract_frontier_values()
        self.__inputs_and_free_clocks = self.__inputs | self.__free_clocks
129

VIGNET Pierre's avatar
VIGNET Pierre committed
130
131
132
133
        # properties to be checked
        self.__initial_property = None            # string
        self.__dim_initial = None                 # list of dimacs clauses
        self.__final_property = None              # idem
134
        self.__dim_final = None
VIGNET Pierre's avatar
VIGNET Pierre committed
135
136
137
138
139
140
        self.__invariant_property = None          # idem
        self.__dim_invariant = None
        self.__variant_property = None            # list<logic formulas>
        self.__dim_variant = None                 # list<list<dimacs clauses>>
        # list of variant temporal constraints in Dimacs ground code
        self.__list_variant_constraints = None    # list<list<dimacs clauses>>
141
142

        # constraints - logical constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
143
        # result from unfolding of base constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
144
145
146
147
148
        # 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
149
        self.__dynamic_constraints = []        # DIMACS clauses: X' = f(X,H,I)
VIGNET Pierre's avatar
VIGNET Pierre committed
150
151
152
153
154
155
156
157

        # Simple temporal properties
        # SP(X0): Initial property/start property; Never change at each step.
        # IP(X): Invariant property
        # VP(X): Variant property;
        #   List of logical formulas of properties forced at each step
        # FP(X): Final property

VIGNET Pierre's avatar
VIGNET Pierre committed
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
        self.__initial_constraints = []        # DIMACS clauses: C(X_0)
        self.__final_constraints   = []        # idem: C(X_n)
        self.__invariant_constraints = []      # DIMACS clauses: C(X_i))
        self.__variant_constraints = []        # variant constraints along traj.
        self.__shift_direction = None          # forward or backward

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



    def reset(self):
        """
        Reset the unfolder before a new query
        """
        self.__initial_property = None
        self.__dim_initial = None
        self.__final_property = None
178
        self.__dim_final = None
VIGNET Pierre's avatar
VIGNET Pierre committed
179
180
181
182
183
184
        self.__invariant_property = None
        self.__dim_invariant = None
        self.__variant_property = None
        self.__dim_variant = None
        self.list_variant_constraints = None
        self.__steps_before_check = 0
185
        self.__shift_direction = None
VIGNET Pierre's avatar
VIGNET Pierre committed
186
        self.__locked = False
187

VIGNET Pierre's avatar
VIGNET Pierre committed
188
189
190
191
192
193
194
    def set_stats(self):
        """
        Enable solver statistics
        """
        self.__stats = True
        self.__nb_vars = 0
        self.__nb_clauses = 0
195

VIGNET Pierre's avatar
VIGNET Pierre committed
196
197
198
199
200
    def unset_stats(self):
        """
        disable solver statistics
        """
        self.__stats = False
201

VIGNET Pierre's avatar
VIGNET Pierre committed
202
203
    def _stats(self):
        """
204
        print solver statistics
VIGNET Pierre's avatar
VIGNET Pierre committed
205
206
207
        """
        print "\n NB Variables in solver: ", self.__nb_vars
        print "NB Clauses in solver: ", self.__nb_clauses
208

VIGNET Pierre's avatar
VIGNET Pierre committed
209
210
211
212
213
    def set_minimal_steps(self, nb_steps):
        """
        For reachability optimisation. number of shift before checking
        """
        self.__steps_before_check = nb_steps
214

VIGNET Pierre's avatar
VIGNET Pierre committed
215
216
217
218
219
220
221
    def set_include_aux_clauses(self, val):
        """
        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 = val
222

VIGNET Pierre's avatar
VIGNET Pierre committed
223
224
225
226
227
228
    # internal variable access for tests
    def get_dynamic_constraints(self):
        """
        For tests: returns coded dynamic constraints
        """
        return self.__dynamic_constraints
229

VIGNET Pierre's avatar
VIGNET Pierre committed
230
231
232
233
234
    def get_initial_constraints(self):
        """
        For tests: returns coded initial constraints
        """
        return self.__initial_constraints
235

VIGNET Pierre's avatar
VIGNET Pierre committed
236
237
238
239
240
    def get_invariant_constraints(self):
        """
        For tests: returns coded invariant constraints
        """
        return self.__invariant_constraints
241

VIGNET Pierre's avatar
VIGNET Pierre committed
242
243
244
245
246
    def get_variant_constraints(self):
        """
        For tests: returns coded variant constraints
        """
        return self.__variant_constraints
247

VIGNET Pierre's avatar
VIGNET Pierre committed
248
249
250
251
252
    def get_final_constraints(self):
        """
        For tests: returns coded final constraints
        """
        self.__final_constraints
253

VIGNET Pierre's avatar
VIGNET Pierre committed
254
255
256
257
258
259
    # variables management
    def var_dimacs_code(self, var_name):
        """
        returns dimacs code of (string) var_name variable
        """
        return self.__var_code_table[var_name]
260

VIGNET Pierre's avatar
VIGNET Pierre committed
261
262
263
264
265
    def get_system_var_number(self):
        """
        number of variables in the clause constraint dynamical system
        """
        return self.__dyn_sys.get_var_number()
266

VIGNET Pierre's avatar
VIGNET Pierre committed
267
268
269
270
271
    def get_var_number(self):
        """
        number of principal variables (properties excluded) in the unfolder
        """
        return len(self.__var_list) -1
272

VIGNET Pierre's avatar
VIGNET Pierre committed
273
274
275
    def get_var_name(self, var_num):
        """
        @param var_num: DIMACS literal coding of an initial variable
276
        @return: name of the variable
VIGNET Pierre's avatar
VIGNET Pierre committed
277
        """
278
        var_code = (abs(var_num) - 1) % self.__shift_step + 1
VIGNET Pierre's avatar
VIGNET Pierre committed
279
280
281
282
283
        if var_code <= self.__shift_step_init: # variable from initial system
            return self.__var_list[var_code]
        else: # auxiliary variable introduced by properties compilation
            return self.__aux_list[var_code - self.__shift_step_init -1]
            #raise MCLException("Not a DIMACS code of an initial variable")
284

VIGNET Pierre's avatar
VIGNET Pierre committed
285
286
287
288
289
    def get_var_indexed_name(self, var_num):
        """
        @param var_num: DIMACS literal coding
        @return: name of the variable with time index
        """
290
        varnum1 = abs(var_num)
VIGNET Pierre's avatar
VIGNET Pierre committed
291
292
293
294
295
296
297
        var_code = (varnum1 - 1) % self.__shift_step + 1
        var_step = (varnum1 - var_code)/self.__shift_step
        if var_code <= self.__shift_step_init:
            return self.__var_list[var_code] + '_%s'% var_step
        else:
            index = var_code - self.__shift_step_init -1
            return self.__aux_list[index] + '_%s'% var_step
298

VIGNET Pierre's avatar
VIGNET Pierre committed
299
300
    def get_frontier(self):
        """
301
        @return: the DIMACS code of the frontier variables
VIGNET Pierre's avatar
VIGNET Pierre committed
302
303
        """
        return self.__frontier
304

305
306
307
308
309
310
311
312
313
314
315
    def get_frontiers_pos_and_neg(self):
        """
        Convenient attribute for RawSolution.extract_frontier_values()
        all frontiers and their opposite version
        operations with sets are much faster

        :return: Set of frontier positive and negative values.
        :rtype: <frozenset>
        """
        return self._frontiers_pos_and_neg

VIGNET Pierre's avatar
VIGNET Pierre committed
316
317
318
319
320
    def get_free_clocks(self):
        """
        @return: the DIMACS code of the free_clocks variables
        """
        return self.__free_clocks
321

VIGNET Pierre's avatar
VIGNET Pierre committed
322
323
324
325
326
    def get_inputs(self):
        """
        @return: the DIMACS code of the input variables
        """
        return self.__inputs
327

328
329
330
331
332
333
334
335
336
    def get_inputs_and_free_clocks(self):
        """Binding for a merged version of __inputs and __free_clocks
        Convenient attribute for RawSolution.extract_frontier_values()

        :return: the DIMACS code of the input and free_clocks variables
        :rtype: <frozenset>
        """
        return self.__inputs_and_free_clocks

VIGNET Pierre's avatar
VIGNET Pierre committed
337
338
339
340
341
    def get_shift_direction(self):
        """
        @return: string "FORWARD" or "BACKWARD"
        """
        return self.__shift_direction
342

VIGNET Pierre's avatar
VIGNET Pierre committed
343
344
345
346
347
    def get_shift_step(self):
        """
        @return: the shift step ss (if n is X_0 code, n+ss is X_1 code)
        """
        return self.__shift_step
348

VIGNET Pierre's avatar
VIGNET Pierre committed
349
350
351
352
353
    def get_shift_step_init(self):
        """
        @return: the shift step ss (if n is X_0 code, n+ss is X_1 code)
        """
        return self.__shift_step_init
354

VIGNET Pierre's avatar
VIGNET Pierre committed
355
356
357
358
359
360
    def get_current_step(self):
        """
        @return: the current number of unfolding
        """
        return self.__current_step

361
362


VIGNET Pierre's avatar
VIGNET Pierre committed
363
364
365
366
367
368
369
370
371
372
    # translation from names to num codes
    # the translation depends on the shift direction
    def __forward_code(self, clause):
        """
        numerically code a clause with the numeric code found in self.__var_code_table for
        a base variable x and numeric_code + shift_step for x'
        variable integer coding increases in futur steps
        @param clause: a Clause object
        @return: the DIMACS coding of the forward shifted clause
        """
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393

        # Old API
        # num_clause = []
        # for lit in clause.list_of_literals:
        #     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
        #print(forward_code(clause, self.__var_code_table, self.__shift_step))
        return forward_code(clause, self.__var_code_table, self.__shift_step)

394

VIGNET Pierre's avatar
VIGNET Pierre committed
395
396
397
398
399
400
401
402
403
404
    def __backward_code(self, clause):
        """
        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
        @param clause: a Clause object
        @return: the DIMACS coding of the backward shifted clause
        """
        num_clause = []
        for lit in clause.list_of_literals:
405
406
407
408
            if not lit.name[-1] == '`': # t 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
409
            else:  # t+1 variable
410
411
412
                num_clause.append(-self.__var_code_table[lit.name[:-1]] \
                if not lit.sign \
                else self.__var_code_table[lit.name[:-1]])
VIGNET Pierre's avatar
VIGNET Pierre committed
413
        return num_clause
414

VIGNET Pierre's avatar
VIGNET Pierre committed
415
416
    def __code_clause(self, clause):
        """
417
418
419
        numerically code a clause with the numeric code found in
        self.__var_code_table for variables in the dynamic system and
        self.__aux_code_table for other variables assume all variables
VIGNET Pierre's avatar
VIGNET Pierre committed
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
        are basic variables (t=0)
        @warning: MODIFIES SHIFT_STEP if auxiliary variables are present (numeric code)
        """
        num_clause = []
        for lit in clause.list_of_literals:
            name = lit.name
            if self.__var_code_table.has_key(name):
                var_cod = self.__var_code_table[name]
            elif self.__aux_code_table.has_key(name):
                var_cod = self.__aux_code_table[name]
            else: # create an auxiliary variable - modifies shift_step
                self.__shift_step += 1
                self.__aux_code_table[name] = self.__shift_step
                var_cod = self.__shift_step
                self.__aux_list.append(name)
            if lit.sign:
                lit_code = var_cod
            else:
                lit_code = - var_cod
            num_clause.append(lit_code)
        return num_clause
441

VIGNET Pierre's avatar
VIGNET Pierre committed
442
443
444
445
446
    # dynamics initialisations
    def __forward_init_dynamic(self):
        """
        set dynamic constraints for a forward one step: X1 = f(X0)
        """
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462

        # Old API
        # self.__dynamic_constraints = []

        # num_clause_list = \
        #     [self.__forward_code(clause)
        #      for clause in self.__dyn_sys.list_clauses]
        #
        # if self.__include_aux_clauses:
        #     num_clause_list += \
        #         [self.__forward_code(clause)
        #          for clause in self.__dyn_sys.aux_list_clauses]
        #
        # self.__dynamic_constraints.append(num_clause_list)

        # New API via C++ module
463
        # TODO: take a look at __backward_init_dynamic & __backward_code
VIGNET Pierre's avatar
VIGNET Pierre committed
464
        if self.__include_aux_clauses:
465
466
467
468
469
470
471
472
473
474
            self.__dynamic_constraints = \
                forward_init_dynamic(self.__dyn_sys.list_clauses,
                                     self.__var_code_table,
                                     self.__shift_step,
                                     self.__dyn_sys.aux_list_clauses)
        else:
            self.__dynamic_constraints = \
                forward_init_dynamic(self.__dyn_sys.list_clauses,
                                     self.__var_code_table,
                                     self.__shift_step)
475

VIGNET Pierre's avatar
VIGNET Pierre committed
476
477
478
479
480
    def __backward_init_dynamic(self):
        """
        set dynamic constraints for a forward one step: X0 = f(X1)
        """
        self.__dynamic_constraints = []
481
482
483
484
485

        num_clause_list = \
            [self.__backward_code(clause)
             for clause in self.__dyn_sys.list_clauses]

VIGNET Pierre's avatar
VIGNET Pierre committed
486
        if self.__include_aux_clauses:
487
488
489
490
            num_clause_list += \
                [self.__backward_code(clause)
                 for clause in self.__dyn_sys.aux_list_clauses]

VIGNET Pierre's avatar
VIGNET Pierre committed
491
        self.__dynamic_constraints.append(num_clause_list)
492

VIGNET Pierre's avatar
VIGNET Pierre committed
493
494
495
496
497
498
499
    # shifting: implementation of the shift operator
    def __shift_clause(self, ncl):
        """
        shift a clause one step
        @param ncl: DIMACS clause
        @warning: lock the unfolder
        """
500
        self.__locked = True  # shift_step must be frozen
VIGNET Pierre's avatar
VIGNET Pierre committed
501
502
503
504
505
506
507
508
509
510

        # Old API
        # Less efficient with abs()
        # return [(abs(lit) + self.__shift_step) * (-1 if lit < 0 else 1) for lit in ncl]
        # More efficient with ternary assignment
        # return [(lit + self.__shift_step) if lit > 0 else (lit - self.__shift_step)
        #         for lit in ncl]

        # New API via C++ module
        return shift_clause(ncl, self.__shift_step)
511

VIGNET Pierre's avatar
VIGNET Pierre committed
512
513
514
515
    def __m_shift_clause(self, ncl, nb_steps):
        """
        shift a clause many step
        @param ncl: DIMACS clause
516
        @param nb_steps: number of shifts
VIGNET Pierre's avatar
VIGNET Pierre committed
517
518
        @warning: lock the unfolder
        """
519
520
        self.__locked = True  # shift_step must be frozen

521
522
        return [(lit + self.__shift_step * nb_steps) if lit > 0
                else (lit - self.__shift_step * nb_steps) for lit in ncl]
523

VIGNET Pierre's avatar
VIGNET Pierre committed
524
525
526
    def __shift_dynamic(self):
        """
        Shift clauses representing the dynamics X' = f(X,I,C)
527
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
528
529
530
531
532
533
534
535
536
537
538
539
540
541

        # Old API
        # self.__dynamic_constraints.append(
        #   [self.__shift_clause(clause)
        #    for clause in self.__dynamic_constraints[-1]]
        # )

        # New API via C++ module
        self.__dynamic_constraints.append(
            shift_dynamic(
                self.__dynamic_constraints[-1],
                self.__shift_step
            )
        )
542

VIGNET Pierre's avatar
VIGNET Pierre committed
543
544
545
546
    def __shift_initial(self):
        """
        Shift initialisation condition
        """
547
548
549
550

        self.__initial_constraints = \
            [self.__shift_clause(clause)
             for clause in self.__initial_constraints]
551

VIGNET Pierre's avatar
VIGNET Pierre committed
552
553
554
555
    def __shift_final(self):
        """
        Shift final property
        """
556
557
558
559
560

        self.__final_constraints = \
            [self.__shift_clause(clause)
             for clause in self.__final_constraints]

561

VIGNET Pierre's avatar
VIGNET Pierre committed
562
563
564
565
566
    def __shift_invariant(self):
        """
        Shift invariant property
        """
        if not self.__invariant_constraints == []:
VIGNET Pierre's avatar
VIGNET Pierre committed
567
568
569
570
571
572
573
574
575
576
577
578
579
580

            # Old API
            # self.__invariant_constraints.append(
            #     [self.__shift_clause(clause)
            #      for clause in self.__invariant_constraints[-1]]
            # )

            # New API via C++ module
            self.__invariant_constraints.append(
                shift_dynamic(
                    self.__invariant_constraints[-1],
                    self.__shift_step
                )
            )
581

VIGNET Pierre's avatar
VIGNET Pierre committed
582
583
584
    def __shift_variant(self):
        """
        shift variant property - depends on unfolding direction
585
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
586
587
588
589
590
591
592
593
594
595
596
597
598
599
        if not self.__list_variant_constraints:
            return
        if self.__shift_direction == "FORWARD":
            index = self.__current_step # constraint t0 already included
            current_constraint = self.__list_variant_constraints[index]
            # shift constraint at current step and add to var_constraints
            for clause in current_constraint:
                s_clause = self.__m_shift_clause(clause, index)
                self.__variant_constraints.append(s_clause)
                return
        elif self.__shift_direction == 'BACKWARD':
            raise MCLException("Not yet implemented")
        else:
            raise MCLException("Shift incoherent data: "+self.__shift_direction)
600
601


VIGNET Pierre's avatar
VIGNET Pierre committed
602
603
604
605
606
607
608
609
610
611
612
613
614
615
    def shift(self):
        """
        assume shift direction is set - shift one step
        """
        self.__shift_dynamic()
        self.__shift_invariant()
        self.__shift_variant()
        if self.__shift_direction == 'FORWARD':
            self.__shift_final()
        elif self.__shift_direction == 'BACKWARD':
            self.__shift_initial()
        else:
            raise MCLException("Shift incoherent data: "+self.__shift_direction)
        self.__current_step += 1
616

VIGNET Pierre's avatar
VIGNET Pierre committed
617
618
619
620
621
622
623
624
625
    # coding of properties
    def __compile_property(self, property_text):
        """
        compile a property (logical formula) into clauses
        type checking uses the symbol table of dyn_sys
        error reporting through the dyn_sys reporter
        MODIFIES __lit_cpt for numbering of auxiliary variables (not coding)
        """
        if self.__locked:
VIGNET Pierre's avatar
VIGNET Pierre committed
626
627
            raise MCLException("Trying to compile property while unfolder is locked")

VIGNET Pierre's avatar
VIGNET Pierre committed
628
        # syntax analyser and type checker
VIGNET Pierre's avatar
VIGNET Pierre committed
629
630
631
632
        # property_text, symb_t, reporter
        tree_prop = compile_cond(property_text,
                                 self.__dyn_sys.symb_tab,
                                 self.__dyn_sys.report)
633
634
        # avoid name collisions of aux var
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
635
636
637
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
638

VIGNET Pierre's avatar
VIGNET Pierre committed
639
        # coding of properties
640

VIGNET Pierre's avatar
VIGNET Pierre committed
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
    def __compile_event(self, property_text):
        """
        compile an event (biosignal expression) into clauses
        type checking uses the symbol table of dyn_sys
        error reporting through the dyn_sys reporter
        MODIFIES __lit_cpt for numbering of auxiliary variables (not coding)
        """
        if self.__locked:
            mess = "Trying to compile property while unfolder is locked"
            raise MCLException(mess)
        reporter = self.__dyn_sys.report
        symb_t = self.__dyn_sys.symb_tab
        # syntax analyser and type checker
        (tree_prop, ste, fcl) = compile_event(property_text, symb_t,
                                              True,  reporter)
656
657
        # avoid name collisions of aux var
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
658
659
660
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
661

VIGNET Pierre's avatar
VIGNET Pierre committed
662
663
    def set_initial_property(self, property_text):
        """
664
        @param property_text: string - litteral boolean expression
VIGNET Pierre's avatar
VIGNET Pierre committed
665
666
        """
        self.__initial_property = property_text
667

VIGNET Pierre's avatar
VIGNET Pierre committed
668
669
670
    def set_dim_initial_property(self, dimacs_clause_list):
        """
        set initial property with a DIMACS representation
671
        @param dimacs_clause_list:
VIGNET Pierre's avatar
VIGNET Pierre committed
672
673
        """
        self.__dim_initial = dimacs_clause_list
674

VIGNET Pierre's avatar
VIGNET Pierre committed
675
676
677
678
679
680
    def __init_initial_constraint_0(self, no_frontier_init=True):
        """
        if initial property is set, generate constraints clauses in numeric form
        base variable form - we have to wait until all variables are num coded
        before shifting anything!!
        """
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
# OLD
#        self.__initial_constraints = []
#        if no_frontier_init:
#            # initialize no frontier places to False
#            for nfp in self.__no_frontier_init:
#                self.__initial_constraints.append(nfp)
#        if self.__initial_property:
#            # compile initial property
#            l_clauses = self.__compile_property(self.__initial_property)
#            # compile numeric form
#            for clause in l_clauses:
#                self.__initial_constraints.append(self.__code_clause(clause))
#        # dimacs aux initial properties
#        dim_init = self.__dim_initial
#        if dim_init:
#            self.__initial_constraints = self.__initial_constraints + dim_init

        self.__initial_constraints = list()

        # initialize no frontier places to False
VIGNET Pierre's avatar
VIGNET Pierre committed
701
        if no_frontier_init:
702
703
            self.__initial_constraints += [elem for elem in self.__no_frontier_init]

VIGNET Pierre's avatar
VIGNET Pierre committed
704
705
706
        if self.__initial_property:
            # compile initial property
            # compile numeric form
707
708
            self.__initial_constraints += [self.__code_clause(clause) for clause in self.__compile_property(self.__initial_property)]

VIGNET Pierre's avatar
VIGNET Pierre committed
709
        # dimacs aux initial properties
710
711
        if self.__dim_initial:
            self.__initial_constraints += self.__dim_initial
712

VIGNET Pierre's avatar
VIGNET Pierre committed
713
714
    def set_final_property(self, property_text):
        """
715
        @param property_text: string - litteral boolean expression
VIGNET Pierre's avatar
VIGNET Pierre committed
716
717
        """
        self.__final_property = property_text
718

VIGNET Pierre's avatar
VIGNET Pierre committed
719
720
721
    def set_dim_final_property(self, dimacs_clause_list):
        """
        set final property with a DIMACS representation
722
723
        @param dimacs_clause_list:
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
724
        self.__dim_final = dimacs_clause_list
725

VIGNET Pierre's avatar
VIGNET Pierre committed
726
727
728
729
730
731
    def __init_final_constraint_0(self):
        """
        if final property is set, generate constraints clauses in numeric form
        base variable used - we have to wait until all variables are num coded
        before shifting anything!!
        """
732

VIGNET Pierre's avatar
VIGNET Pierre committed
733
734
735
        self.__final_constraints = []
        if self.__final_property:
            # compile initial (X0) property
VIGNET Pierre's avatar
VIGNET Pierre committed
736
            # ex: Px => [$Px$]
VIGNET Pierre's avatar
VIGNET Pierre committed
737
738
            l_clauses = self.__compile_property(self.__final_property)
            # compile numeric form
VIGNET Pierre's avatar
VIGNET Pierre committed
739
            # ex: [$Px$] => self.__final_constraints = [[7]]
VIGNET Pierre's avatar
VIGNET Pierre committed
740
741
742
743
744
            for clause in l_clauses:
                self.__final_constraints.append(self.__code_clause(clause))
        dim_fin = self.__dim_final
        if dim_fin:
            self.__final_constraints = self.__final_constraints + dim_fin
745

VIGNET Pierre's avatar
VIGNET Pierre committed
746
747
    def set_current_property(self, property_text):
        """
748
        @param property_text: string - litteral boolean expression
VIGNET Pierre's avatar
VIGNET Pierre committed
749
        """
750

VIGNET Pierre's avatar
VIGNET Pierre committed
751
        self.__invariant_property = property_text
752

VIGNET Pierre's avatar
VIGNET Pierre committed
753
754
755
756
757
    def set_dim_current_property(self, dimacs_clause_list):
        """
        set final property with a DIMACS representation
        @param dimacs_clause_list:
        """
758

VIGNET Pierre's avatar
VIGNET Pierre committed
759
        self.__dim_invariant = dimacs_clause_list
760

VIGNET Pierre's avatar
VIGNET Pierre committed
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
    def __init_invariant_constraint_0(self):
        """
        if trajectory property is set, generate constraints clauses in numeric form
        base variable used - we have to wait until all variables are num coded
        before shifting anything!!
        """
        self.__invariant_constraints = []
        if self.__invariant_property:
            # compile initial (X0) property
            l_clauses = self.__compile_property(self.__invariant_property)
            # compile numeric form
            init_const = []
            for clause in l_clauses:
                init_const.append(self.__code_clause(clause))
            self.__invariant_constraints.append(init_const)
        d_inv = self.__dim_invariant
        if d_inv:
            self.__invariant_constraints = self.__invariant_constraints + d_inv
779

VIGNET Pierre's avatar
VIGNET Pierre committed
780
781
782
783
784
785
786
    def set_variant_property(self, var_prop):
        """
        @param var_prop: a list of logical formulas representing time varying
        constraints. Each constraint uses ground (not shifted) variables.
        The order of the list of constraints is always time increasing.
        """
        self.__variant_property = var_prop
787

VIGNET Pierre's avatar
VIGNET Pierre committed
788
789
    def set_dim_variant_property(self, dim_var_prop):
        """
790
791
        @param dim_var_prop: a list list of dimacs clauses representing time
        varying constraints. Each constraint uses ground (not shifted)
VIGNET Pierre's avatar
VIGNET Pierre committed
792
793
794
        variable codes.
        """
        self.__dim_variant = dim_var_prop
795

VIGNET Pierre's avatar
VIGNET Pierre committed
796
797
    def __init_variant_constraints_0(self):
        """
798
        if variant_property is set, compile each property into clauses and
VIGNET Pierre's avatar
VIGNET Pierre committed
799
800
801
802
803
804
805
806
807
808
809
810
811
812
        encode these clauses. Clauses already in dimacs form are added.
        The two variant constraint forms must be compatible (same length)
        """
        # coding of variant properties
        if self.__variant_property:
            self.__list_variant_constraints = []
            for prop in self.__variant_property:
                # compile initial (X0) property
                l_clauses = self.__compile_event(prop)
                # encode the clauses
                dim_cl = []
                for clause in l_clauses:
                    dim_cl.append(self.__code_clause(clause))
                self.__list_variant_constraints.append(dim_cl)
813

VIGNET Pierre's avatar
VIGNET Pierre committed
814
815
            # add variant properties in dimacs form
            if self.__dim_variant:
816
                vp_length = len(self.__variant_property)
VIGNET Pierre's avatar
VIGNET Pierre committed
817
818
819
                if vp_length != len(self.__dim_variant):
                    mess = "Incoherent variant properties"
                    raise MCLException(mess)
820

VIGNET Pierre's avatar
VIGNET Pierre committed
821
822
823
                for i in range(vp_length):
                    c_var = self.__list_variant_constraints[i]
                    c_var = c_var + self.__dim_variant[i]
824
                    self.__list_variant_constraints[i] = c_var
VIGNET Pierre's avatar
VIGNET Pierre committed
825
826
827
828
829
830
831
832
833
834
835
836
        else:
            if self.__dim_variant:
                self.__list_variant_constraints = self.__dim_variant
        # initialisation
        if self.__list_variant_constraints:
            if self.__shift_direction == "FORWARD":
                self.__variant_constraints = self.__list_variant_constraints[0]
            elif  self.__shift_direction == "BACKWARD":
                raise MCLException("Not yet implemented")
            else:
                raise MCLException("Shift incoherent data: "
                                   + self.__shift_direction)
837

VIGNET Pierre's avatar
VIGNET Pierre committed
838
839
840
841
842
843
844
845
846
847
    # whole initialisations
    def init_forward_unfolding(self):
        """
        initialisation before generating constraints - forward trajectory
        """
        self.__shift_direction = 'FORWARD'
        self.__current_step = 1
        self.__shift_step = self.__shift_step_init  # back to basic!
        self.__aux_code_table = dict()              # flush auxiliary variables
        self.__aux_list = []                        # idem
848

VIGNET Pierre's avatar
VIGNET Pierre committed
849
850
851
852
853
        # init properties to generate all variable num codes
        self.__init_initial_constraint_0()
        self.__init_final_constraint_0()
        self.__init_invariant_constraint_0()
        self.__init_variant_constraints_0()
854

VIGNET Pierre's avatar
VIGNET Pierre committed
855
856
857
858
        # now shifting is possible
        self.__forward_init_dynamic()
        self.__shift_final()
        self.__shift_invariant()
859
860


VIGNET Pierre's avatar
VIGNET Pierre committed
861
862
863
864
865
866
867
868
869
    def init_backward_unfolding(self):
        """
        initialisation before generating constraints - backward trajectory
        """
        self.__shift_direction = 'BACKWARD'
        self.__current_step = 0
        self.__shift_step = self.__shift_step_init  # back to basic!
        self.__aux_code_table = dict()              # flush auxiliary variables
        self.__aux_list = []                        # idem
870

VIGNET Pierre's avatar
VIGNET Pierre committed
871
872
873
874
875
        # init properties to generate all variable num codes
        self.__init_initial_constraint_0()
        self.__init_final_constraint_0()
        self.__init_invariant_constraint_0()
        self.__init_variant_constraints_0()
876

VIGNET Pierre's avatar
VIGNET Pierre committed
877
878
879
880
        # now shifting is possible
        self.__backward_init_dynamic()
        self.__shift_initial()
        self.__shift_invariant()
881

VIGNET Pierre's avatar
VIGNET Pierre committed
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
    # for debug
    def vars_in_clause(self, clause):
        """
        DEBUG
        """
        lvar = []
        for var in clause:
            lvar.append(self.get_var_indexed_name(var))
        return lvar


    # solver interface
    def __load_solver(self, solv):
        """
        add all the current clauses in solver solv
897
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913

        # New API via C++ module
        solv.add_clauses(self.__final_constraints)
        solv.add_clauses(it.chain(*self.__invariant_constraints))
        solv.add_clauses(self.__variant_constraints)
        solv.add_clauses(it.chain(*self.__dynamic_constraints))
        solv.add_clauses(self.__initial_constraints)

        # Less efficient alternative
        # solv.add_clauses([clause for lcl in self.__invariant_constraints
        #                   for clause in lcl])
        # solv.add_clauses([clause for lcl in self.__dynamic_constraints
        #                   for clause in lcl])

        # Old API
        # Clauses are added one by one
VIGNET Pierre's avatar
VIGNET Pierre committed
914
        # final
VIGNET Pierre's avatar
VIGNET Pierre committed
915
        #[solv.add_clause(clause) for clause in self.__final_constraints]
916

VIGNET Pierre's avatar
VIGNET Pierre committed
917
        # trajectory invariant
VIGNET Pierre's avatar
VIGNET Pierre committed
918
919
        #[solv.add_clause(clause) for lcl in self.__invariant_constraints
        # for clause in lcl]
920

VIGNET Pierre's avatar
VIGNET Pierre committed
921
        # trajectory variant
VIGNET Pierre's avatar
VIGNET Pierre committed
922
        #[solv.add_clause(clause) for clause in self.__variant_constraints]
923

VIGNET Pierre's avatar
VIGNET Pierre committed
924
        # dynamics
VIGNET Pierre's avatar
VIGNET Pierre committed
925
926
        #[solv.add_clause(clause) for lcl in self.__dynamic_constraints
        # for clause in lcl]
927

928
        # initial
VIGNET Pierre's avatar
VIGNET Pierre committed
929
        #[solv.add_clause(clause) for clause in self.__initial_constraints]
VIGNET Pierre's avatar
VIGNET Pierre committed
930

931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
        # LOGGING
        if LOGGER.getEffectiveLevel() == DEBUG:
            # final
            LOGGER.debug("Load new solver !!")
            LOGGER.debug(">> final: " + str(len(self.__final_constraints)))
            LOGGER.debug(str(self.__final_constraints))

            # trajectory invariant
            LOGGER.debug(">> trajectory inv: " + str(len(self.__invariant_constraints)))
            LOGGER.debug(str(self.__invariant_constraints))

            # trajectory variant
            LOGGER.debug(">> trajectory var: " + str(len(self.__variant_constraints)))
            LOGGER.debug(str(self.__variant_constraints))

            # dynamics
            LOGGER.debug(">> dynamics: " + str(len(self.__dynamic_constraints)))
            LOGGER.debug(str(self.__dynamic_constraints))

            # initial
            LOGGER.debug(">> initial: " + str(len(self.__initial_constraints)))
            LOGGER.debug(str(self.__initial_constraints))
953
954


VIGNET Pierre's avatar
VIGNET Pierre committed
955
956
957
958
959
    def __constraints_satisfied(self):
        """
        @return: boolean
        """
        solver = CryptoMS()
960
        # Load Solver and all clauses
VIGNET Pierre's avatar
VIGNET Pierre committed
961
        self.__load_solver(solver)
962
963
        # If stats are activated (never besides in test environment):
        # sync local data (nb vars, nb clauses with solver state)
VIGNET Pierre's avatar
VIGNET Pierre committed
964
        if self.__stats:
965
            if solver.nb_vars() > self.__nb_vars:
VIGNET Pierre's avatar
VIGNET Pierre committed
966
                self.__nb_vars = solver.nb_vars()
967
968
969
970

            # Starting from pycryptosat 5.2, nb_clauses() is a private attribute
            #if solver.nb_clauses() > self.__nb_clauses:
            #    self.__nb_clauses = solver.nb_clauses()
971
        # Is problem satisfiable ?
VIGNET Pierre's avatar
VIGNET Pierre committed
972
        return solver.is_satisfiable()
973

974

VIGNET Pierre's avatar
VIGNET Pierre committed
975
976
977
978
979
980
981
982
    def __msolve_constraints(self, max_sol, vvars):
        """
        @param max_sol: int - the max number of solution returned
        @param vvars: variables for which the solver must find different solutions(dimacs code)
        @return: a list of RawSolution
        """
        solver = CryptoMS()
        self.__load_solver(solver)
983

VIGNET Pierre's avatar
VIGNET Pierre committed
984
        if self.__stats:
985
            if solver.nb_vars() > self.__nb_vars:
VIGNET Pierre's avatar
VIGNET Pierre committed
986
                self.__nb_vars = solver.nb_vars()
987
988
989
            # Starting from pycryptosat 5.2, nb_clauses() is a private attribute
            #if solver.nb_clauses() > self.__nb_clauses:
            #    self.__nb_clauses = solver.nb_clauses()
990

991
        if LOGGER.getEffectiveLevel() == DEBUG:
992
993
994
            LOGGER.debug("__msolve_constraints :: vvars : " + str(vvars))
            LOGGER.debug("__msolve_constraints :: max_sol : " + str(max_sol))
            lintsol = solver.msolve_selected(max_sol, vvars)
995
            LOGGER.debug("__msolve_constraints :: lintsol : " + str(lintsol))
996
            return [RawSolution(solint, self) for solint in lintsol]
997

998
999
        return [RawSolution(solint, self)
                for solint in solver.msolve_selected(max_sol, vvars)]
VIGNET Pierre's avatar
VIGNET Pierre committed
1000
1001
1002
1003
1004

    # dynamic properties
    def squery_is_satisfied(self, max_step):
        """
        Ask the SAT solver
1005
        @param max_step: int - the horizon
VIGNET Pierre's avatar
VIGNET Pierre committed
1006
1007
1008
1009
1010
1011
1012
        """
        # initialization
        self.init_forward_unfolding()
        # horizon adjustment
        if self.__list_variant_constraints:
            max_step = min(max_step, len(self.__list_variant_constraints)-1)
        # loop
1013
        if self.__invariant_property and not self.__final_property :
VIGNET Pierre's avatar
VIGNET Pierre committed
1014
1015
            while self.__current_step <= max_step:
                self.shift()
1016
            return self.__constraints_satisfied()
VIGNET Pierre's avatar
VIGNET Pierre committed
1017
1018
1019
1020
1021
        else :
            while self.__current_step <= max_step:
                if self.__constraints_satisfied():
                    return True
                self.shift()
1022
1023
1024
1025
            return self.__constraints_satisfied()



VIGNET Pierre's avatar
VIGNET Pierre committed
1026
1027
1028
1029
1030
1031
    def squery_solve(self, vvars, max_step, max_sol):
        """
        Assert a query is loaded (start_condition, inv_condition, final_condition)
        @param vvars: variables on which different solutions must differ
        @param max_step: bounded horizon for computations
        @param max_sol: max number of solutions to be computed
1032
1033

        @return: list of RawSolution objects
VIGNET Pierre's avatar
VIGNET Pierre committed
1034
        """
1035
1036
        if LOGGER.getEffectiveLevel() == DEBUG:
            LOGGER.debug("squery_solve :: vvars : " + str(vvars))
VIGNET Pierre's avatar
VIGNET Pierre committed
1037
1038
1039
1040
1041
1042
1043
1044
1045
        # initialization
        self.init_forward_unfolding()
        # horizon adjustment
        if self.__list_variant_constraints:
            max_step = min(max_step, len(self.__list_variant_constraints)-1)
        # loop
        if self.__invariant_property and not self.__final_property :
            while self.__current_step <= max_step:
                self.shift()
VIGNET Pierre's avatar
VIGNET Pierre committed
1046
1047
1048
            # return l_rawsol
            return self.__msolve_constraints(max_sol, vvars)

VIGNET Pierre's avatar
VIGNET Pierre committed
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
        else : # reachability
            l_rawsol = []
            # check and correct for incoherent data on step number
            if self.__steps_before_check > max_step:
                self.__steps_before_check = max_step - 1
            # shift without checking (optimization)
            while self.__current_step <= self.__steps_before_check:
                self.shift()
            # search for solutions at each step
            while self.__current_step <= max_step:
                lsol = self.__msolve_constraints(max_sol, vvars)
                if len(lsol)>0:
                    l_rawsol = l_rawsol + lsol
                self.shift()
            return l_rawsol
1064

VIGNET Pierre's avatar
VIGNET Pierre committed
1065
1066
1067
1068
1069
1070

###############################################################################
class CLPropertyVisitor(object):
    """
    SigExpression on states and events into a set of clauses
    Type checking must be done.
1071
1072
    """

VIGNET Pierre's avatar
VIGNET Pierre committed
1073
1074
1075
1076
    def __init__(self, aux_cpt=0):
        self.cpt = aux_cpt         # for auxiliary variable naming
        self.clauses = []          # generated clauses
        self.top = True            # root of the formula?
1077

VIGNET Pierre's avatar
VIGNET Pierre committed
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
    def visit_sig_ident(self, tnode):
        """
        ident -> literal
        """
        name = tnode.name
        new_lit = Literal(name, True)
        if self.top:
            self.clauses.append(Clause([new_lit]))
            return None
        return new_lit
1088

VIGNET Pierre's avatar
VIGNET Pierre committed
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
    def visit_sig_not(self, node):
        """
        translate a not
        """
        top = self.top
        self.top = False
        # compile operand to nl <=> formula
        newl = node.operand.accept(self)
        notnl = newl.lit_not()
        if top: # we are at the root
            self.clauses.append(Clause([notnl]))
            return None
        return notnl # if we are not at the root
1102

VIGNET Pierre's avatar
VIGNET Pierre committed
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
    def visit_sig_sync(self, binnode):
        """
        translate a binary (or/and) expression
        """
        top = self.top
        self.top = False
        # the internal nodes will be affected with the name '_lit'
        name = '_lit'+str(self.cpt)
        self.cpt += 1
        newl = Literal(name, True)
        notnl = Literal(name, False)
        # recursive visits
        operator = binnode.operator
        nl1 = binnode.left_h.accept(self)
        notnl1 = nl1.lit_not()
        nl2 = binnode.right_h.accept(self)
        notnl2 = nl2.lit_not()
        # clauses generation
        if operator == 'and':   # x = lh and rh
1122
1123
1124
1125
1126
            self.clauses.extend([
                Clause([nl1, notnl]),           # not x or not lh
                Clause([nl2, notnl]),           # not x or not rh
                Clause([notnl1, notnl2, newl])  # x or not lh or not rh
            ])
VIGNET Pierre's avatar
VIGNET Pierre committed
1127
1128

        if operator == 'or':    # x = lh or rh
1129
1130
1131
1132
1133
            self.clauses.extend([
                Clause([notnl1, newl]),         # x or not lh
                Clause([notnl2, newl]),         # x or not rh
                Clause([nl1, nl2, notnl])       # not x or not lh or not rh
            ])
VIGNET Pierre's avatar
VIGNET Pierre committed
1134

1135
1136
1137
#        self.clauses.append(cl1)
#        self.clauses.append(cl2)
#        self.clauses.append(cl3)
VIGNET Pierre's avatar
VIGNET Pierre committed
1138
1139
1140
1141
        if top:
            self.clauses.append(Clause([newl]))
            return None
        return newl
1142

VIGNET Pierre's avatar
VIGNET Pierre committed
1143
1144
1145
1146
1147
1148
1149
1150
1151
    def visit_sig_const(self, exp):
        """
        translate a constant expression
        """
        top = self.top
        if top:
            if exp.is_const_false():
                raise TypeError("No constant False property allowed")
            else: # always present or satisfied
1152
                return None
VIGNET Pierre's avatar
VIGNET Pierre committed
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
        # the internal nodes will be affected with the name '_lit'
        name = '_lit'+str(self.cpt)
        self.cpt += 1
        newl = Literal(name, True)

        # clause generation
        if exp.value:
            clause = newl  # x = True
        else:
            clause = newl.lit_not()
        self.clauses.append(Clause([clause]))
        return newl

    # time operators
    def visit_sig_default(self, exp):
        """
        default translation
        """
        top = self.top
        self.top = False
        # the internal nodes will be affected the name '_lit'
        name = '_lit'+str(self.cpt)
        self.cpt += 1
        newl = Literal(name, True)
        notnl = Literal(name, False)
        # recursive visits
        nl1 = exp.left_h.accept(self)
        notnl1 = nl1.lit_not()
        nl2 = exp.right_h.accept(self)
        notnl2 = nl2.lit_not()
        # clause generation: x = lh or rh
        cl1 = Clause([notnl1, newl])        # x or not lh
        cl2 = Clause([notnl2, newl])        # x or not rh
        cl3 = Clause([nl1, nl2, notnl])     # not x or not lh or not rh
1187

VIGNET Pierre's avatar
VIGNET Pierre committed
1188
1189
1190
1191
1192
1193
1194
        self.clauses.append(cl1)
        self.clauses.append(cl2)
        self.clauses.append(cl3)
        if top:
            self.clauses.append(Clause([newl]))
            return None
        return newl
1195

VIGNET Pierre's avatar
VIGNET Pierre committed
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
    def visit_sig_when(self, exp):
        """
        when translation
        """
        top = self.top
        self.top = False
        # the internal nodes will be affected the name '_lit'
        name = '_lit'+str(self.cpt)
        self.cpt += 1
        newl = Literal(name, True)
        notnl = Literal(name, False)
        # recursive visits
        nl1 = exp.left_h.accept(self)
        notnl1 = nl1.lit_not()
        nl2 = exp.right_h.accept(self)
        notnl2 = nl2.lit_not()
        # clause generation: x = lh and rh
        cl1 = Clause([nl1, notnl])           # not x or not lh
        cl2 = Clause([nl2, notnl])           # not x or not rh
        cl3 = Clause([notnl1, notnl2, newl]) # x or not lh or not rh

        self.clauses.append(cl1)
        self.clauses.append(cl2)
        self.clauses.append(cl3)
        if top:
            self.clauses.append(Clause([newl]))
            return None
        return newl
1224