CLUnfolder.py 43.1 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
VIGNET Pierre's avatar
VIGNET Pierre committed
109
110
111
        self.__no_frontier_init = []
        for nfp in self.__dyn_sys.no_frontier:
            self.__no_frontier_init.append([- self.__var_code_table[nfp]])
112

VIGNET Pierre's avatar
VIGNET Pierre committed
113
114
115
116
117
        # ordered list of frontier place DIMACS codes for extraction (inv)
        self.__frontier = []
        for frp in self.__dyn_sys.frontier:
            self.__frontier.append(self.__var_code_table[frp])
        self.__frontier.sort()
118

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
131
132
133
134
        # properties to be checked
        self.__initial_property = None            # string
        self.__dim_initial = None                 # list of dimacs clauses
        self.__final_property = None              # idem
135
        self.__dim_final = None
VIGNET Pierre's avatar
VIGNET Pierre committed
136
137
138
139
140
141
        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>>
142
143

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

        # 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
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
        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
179
        self.__dim_final = None
VIGNET Pierre's avatar
VIGNET Pierre committed
180
181
182
183
184
185
        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
186
        self.__shift_direction = None
VIGNET Pierre's avatar
VIGNET Pierre committed
187
        self.__locked = False
188

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

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

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
216
217
218
219
220
221
222
    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
223

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

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

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

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

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

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

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
274
275
276
    def get_var_name(self, var_num):
        """
        @param var_num: DIMACS literal coding of an initial variable
277
        @return: name of the variable
VIGNET Pierre's avatar
VIGNET Pierre committed
278
        """
279
        if var_num < 0:
VIGNET Pierre's avatar
VIGNET Pierre committed
280
281
282
283
284
285
286
287
            varnum1 = -var_num
        else: varnum1 = var_num
        var_code = (varnum1 - 1) % self.__shift_step + 1
        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")
288

VIGNET Pierre's avatar
VIGNET Pierre committed
289
290
291
292
293
    def get_var_indexed_name(self, var_num):
        """
        @param var_num: DIMACS literal coding
        @return: name of the variable with time index
        """
294
        if var_num < 0:
VIGNET Pierre's avatar
VIGNET Pierre committed
295
296
297
298
299
300
301
302
303
            varnum1 = -var_num
        else: varnum1 = var_num
        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
304

VIGNET Pierre's avatar
VIGNET Pierre committed
305
306
    def get_frontier(self):
        """
307
        @return: the DIMACS code of the frontier variables
VIGNET Pierre's avatar
VIGNET Pierre committed
308
309
        """
        return self.__frontier
310

VIGNET Pierre's avatar
VIGNET Pierre committed
311
312
313
314
315
    def get_free_clocks(self):
        """
        @return: the DIMACS code of the free_clocks variables
        """
        return self.__free_clocks
316

VIGNET Pierre's avatar
VIGNET Pierre committed
317
318
319
320
321
    def get_inputs(self):
        """
        @return: the DIMACS code of the input variables
        """
        return self.__inputs
322

VIGNET Pierre's avatar
VIGNET Pierre committed
323
324
325
326
327
    def get_shift_direction(self):
        """
        @return: string "FORWARD" or "BACKWARD"
        """
        return self.__shift_direction
328

VIGNET Pierre's avatar
VIGNET Pierre committed
329
330
331
332
333
    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
334

VIGNET Pierre's avatar
VIGNET Pierre committed
335
336
337
338
339
    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
340

VIGNET Pierre's avatar
VIGNET Pierre committed
341
342
343
344
345
346
    def get_current_step(self):
        """
        @return: the current number of unfolding
        """
        return self.__current_step

347
348


VIGNET Pierre's avatar
VIGNET Pierre committed
349
350
351
352
353
354
355
356
357
358
    # 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
        """
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379

        # 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)

380

VIGNET Pierre's avatar
VIGNET Pierre committed
381
382
383
384
385
386
387
388
389
390
    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:
391
392
393
394
            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
395
            else:  # t+1 variable
396
397
398
                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
399
        return num_clause
400

VIGNET Pierre's avatar
VIGNET Pierre committed
401
402
    def __code_clause(self, clause):
        """
403
404
405
        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
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
        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
427

VIGNET Pierre's avatar
VIGNET Pierre committed
428
429
430
431
432
    # dynamics initialisations
    def __forward_init_dynamic(self):
        """
        set dynamic constraints for a forward one step: X1 = f(X0)
        """
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448

        # 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
449
        # TODO: take a look at __backward_init_dynamic & __backward_code
VIGNET Pierre's avatar
VIGNET Pierre committed
450
        if self.__include_aux_clauses:
451
452
453
454
455
456
457
458
459
460
            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)
461

VIGNET Pierre's avatar
VIGNET Pierre committed
462
463
464
465
466
    def __backward_init_dynamic(self):
        """
        set dynamic constraints for a forward one step: X0 = f(X1)
        """
        self.__dynamic_constraints = []
467
468
469
470
471

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

VIGNET Pierre's avatar
VIGNET Pierre committed
472
        if self.__include_aux_clauses:
473
474
475
476
            num_clause_list += \
                [self.__backward_code(clause)
                 for clause in self.__dyn_sys.aux_list_clauses]

VIGNET Pierre's avatar
VIGNET Pierre committed
477
        self.__dynamic_constraints.append(num_clause_list)
478

VIGNET Pierre's avatar
VIGNET Pierre committed
479
480
481
482
483
484
485
    # shifting: implementation of the shift operator
    def __shift_clause(self, ncl):
        """
        shift a clause one step
        @param ncl: DIMACS clause
        @warning: lock the unfolder
        """
486
        self.__locked = True  # shift_step must be frozen
VIGNET Pierre's avatar
VIGNET Pierre committed
487
488
489
490
491
492
493
494
495
496

        # 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)
497

VIGNET Pierre's avatar
VIGNET Pierre committed
498
499
500
501
    def __m_shift_clause(self, ncl, nb_steps):
        """
        shift a clause many step
        @param ncl: DIMACS clause
502
        @param nb_steps: number of shifts
VIGNET Pierre's avatar
VIGNET Pierre committed
503
504
        @warning: lock the unfolder
        """
505
506
        self.__locked = True  # shift_step must be frozen

507
508
        return [(lit + self.__shift_step * nb_steps) if lit > 0
                else (lit - self.__shift_step * nb_steps) for lit in ncl]
509

VIGNET Pierre's avatar
VIGNET Pierre committed
510
511
512
    def __shift_dynamic(self):
        """
        Shift clauses representing the dynamics X' = f(X,I,C)
513
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
514
515
516
517
518
519
520
521
522
523
524
525
526
527

        # 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
            )
        )
528

VIGNET Pierre's avatar
VIGNET Pierre committed
529
530
531
532
    def __shift_initial(self):
        """
        Shift initialisation condition
        """
533
534
535
536

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

VIGNET Pierre's avatar
VIGNET Pierre committed
538
539
540
541
    def __shift_final(self):
        """
        Shift final property
        """
542
543
544
545
546

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

547

VIGNET Pierre's avatar
VIGNET Pierre committed
548
549
550
551
552
    def __shift_invariant(self):
        """
        Shift invariant property
        """
        if not self.__invariant_constraints == []:
VIGNET Pierre's avatar
VIGNET Pierre committed
553
554
555
556
557
558
559
560
561
562
563
564
565
566

            # 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
                )
            )
567

VIGNET Pierre's avatar
VIGNET Pierre committed
568
569
570
    def __shift_variant(self):
        """
        shift variant property - depends on unfolding direction
571
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
572
573
574
575
576
577
578
579
580
581
582
583
584
585
        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)
586
587


VIGNET Pierre's avatar
VIGNET Pierre committed
588
589
590
591
592
593
594
595
596
597
598
599
600
601
    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
602

VIGNET Pierre's avatar
VIGNET Pierre committed
603
604
605
606
607
608
609
610
611
    # 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
612
613
            raise MCLException("Trying to compile property while unfolder is locked")

VIGNET Pierre's avatar
VIGNET Pierre committed
614
        # syntax analyser and type checker
VIGNET Pierre's avatar
VIGNET Pierre committed
615
616
617
618
        # property_text, symb_t, reporter
        tree_prop = compile_cond(property_text,
                                 self.__dyn_sys.symb_tab,
                                 self.__dyn_sys.report)
619
620
        # avoid name collisions of aux var
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
621
622
623
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
624

VIGNET Pierre's avatar
VIGNET Pierre committed
625
        # coding of properties
626

VIGNET Pierre's avatar
VIGNET Pierre committed
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
    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)
642
643
        # avoid name collisions of aux var
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
644
645
646
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
647

VIGNET Pierre's avatar
VIGNET Pierre committed
648
649
    def set_initial_property(self, property_text):
        """
650
        @param property_text: string - litteral boolean expression
VIGNET Pierre's avatar
VIGNET Pierre committed
651
652
        """
        self.__initial_property = property_text
653

VIGNET Pierre's avatar
VIGNET Pierre committed
654
655
656
    def set_dim_initial_property(self, dimacs_clause_list):
        """
        set initial property with a DIMACS representation
657
        @param dimacs_clause_list:
VIGNET Pierre's avatar
VIGNET Pierre committed
658
659
        """
        self.__dim_initial = dimacs_clause_list
660

VIGNET Pierre's avatar
VIGNET Pierre committed
661
662
663
664
665
666
    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!!
        """
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
# 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
687
        if no_frontier_init:
688
689
            self.__initial_constraints += [elem for elem in self.__no_frontier_init]

VIGNET Pierre's avatar
VIGNET Pierre committed
690
691
692
        if self.__initial_property:
            # compile initial property
            # compile numeric form
693
694
            self.__initial_constraints += [self.__code_clause(clause) for clause in self.__compile_property(self.__initial_property)]

VIGNET Pierre's avatar
VIGNET Pierre committed
695
        # dimacs aux initial properties
696
697
        if self.__dim_initial:
            self.__initial_constraints += self.__dim_initial
698

VIGNET Pierre's avatar
VIGNET Pierre committed
699
700
    def set_final_property(self, property_text):
        """
701
        @param property_text: string - litteral boolean expression
VIGNET Pierre's avatar
VIGNET Pierre committed
702
703
        """
        self.__final_property = property_text
704

VIGNET Pierre's avatar
VIGNET Pierre committed
705
706
707
    def set_dim_final_property(self, dimacs_clause_list):
        """
        set final property with a DIMACS representation
708
709
        @param dimacs_clause_list:
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
710
        self.__dim_final = dimacs_clause_list
711

VIGNET Pierre's avatar
VIGNET Pierre committed
712
713
714
715
716
717
    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!!
        """
718

VIGNET Pierre's avatar
VIGNET Pierre committed
719
720
721
        self.__final_constraints = []
        if self.__final_property:
            # compile initial (X0) property
VIGNET Pierre's avatar
VIGNET Pierre committed
722
            # ex: Px => [$Px$]
VIGNET Pierre's avatar
VIGNET Pierre committed
723
724
            l_clauses = self.__compile_property(self.__final_property)
            # compile numeric form
VIGNET Pierre's avatar
VIGNET Pierre committed
725
            # ex: [$Px$] => self.__final_constraints = [[7]]
VIGNET Pierre's avatar
VIGNET Pierre committed
726
727
728
729
730
            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
731

VIGNET Pierre's avatar
VIGNET Pierre committed
732
733
    def set_current_property(self, property_text):
        """
734
        @param property_text: string - litteral boolean expression
VIGNET Pierre's avatar
VIGNET Pierre committed
735
        """
736

VIGNET Pierre's avatar
VIGNET Pierre committed
737
        self.__invariant_property = property_text
738

VIGNET Pierre's avatar
VIGNET Pierre committed
739
740
741
742
743
    def set_dim_current_property(self, dimacs_clause_list):
        """
        set final property with a DIMACS representation
        @param dimacs_clause_list:
        """
744

VIGNET Pierre's avatar
VIGNET Pierre committed
745
        self.__dim_invariant = dimacs_clause_list
746

VIGNET Pierre's avatar
VIGNET Pierre committed
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
    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
765

VIGNET Pierre's avatar
VIGNET Pierre committed
766
767
768
769
770
771
772
    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
773

VIGNET Pierre's avatar
VIGNET Pierre committed
774
775
    def set_dim_variant_property(self, dim_var_prop):
        """
776
777
        @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
778
779
780
        variable codes.
        """
        self.__dim_variant = dim_var_prop
781

VIGNET Pierre's avatar
VIGNET Pierre committed
782
783
    def __init_variant_constraints_0(self):
        """
784
        if variant_property is set, compile each property into clauses and
VIGNET Pierre's avatar
VIGNET Pierre committed
785
786
787
788
789
790
791
792
793
794
795
796
797
798
        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)
799

VIGNET Pierre's avatar
VIGNET Pierre committed
800
801
            # add variant properties in dimacs form
            if self.__dim_variant:
802
                vp_length = len(self.__variant_property)
VIGNET Pierre's avatar
VIGNET Pierre committed
803
804
805
                if vp_length != len(self.__dim_variant):
                    mess = "Incoherent variant properties"
                    raise MCLException(mess)
806

VIGNET Pierre's avatar
VIGNET Pierre committed
807
808
809
                for i in range(vp_length):
                    c_var = self.__list_variant_constraints[i]
                    c_var = c_var + self.__dim_variant[i]
810
                    self.__list_variant_constraints[i] = c_var
VIGNET Pierre's avatar
VIGNET Pierre committed
811
812
813
814
815
816
817
818
819
820
821
822
        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)
823

VIGNET Pierre's avatar
VIGNET Pierre committed
824
825
826
827
828
829
830
831
832
833
    # 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
834

VIGNET Pierre's avatar
VIGNET Pierre committed
835
836
837
838
839
        # 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()
840

VIGNET Pierre's avatar
VIGNET Pierre committed
841
842
843
844
        # now shifting is possible
        self.__forward_init_dynamic()
        self.__shift_final()
        self.__shift_invariant()
845
846


VIGNET Pierre's avatar
VIGNET Pierre committed
847
848
849
850
851
852
853
854
855
    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
856

VIGNET Pierre's avatar
VIGNET Pierre committed
857
858
859
860
861
        # 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()
862

VIGNET Pierre's avatar
VIGNET Pierre committed
863
864
865
866
        # now shifting is possible
        self.__backward_init_dynamic()
        self.__shift_initial()
        self.__shift_invariant()
867

VIGNET Pierre's avatar
VIGNET Pierre committed
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
    # 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
883
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899

        # 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
900
        # final
VIGNET Pierre's avatar
VIGNET Pierre committed
901
        #[solv.add_clause(clause) for clause in self.__final_constraints]
902

VIGNET Pierre's avatar
VIGNET Pierre committed
903
        # trajectory invariant
VIGNET Pierre's avatar
VIGNET Pierre committed
904
905
        #[solv.add_clause(clause) for lcl in self.__invariant_constraints
        # for clause in lcl]
906

VIGNET Pierre's avatar
VIGNET Pierre committed
907
        # trajectory variant
VIGNET Pierre's avatar
VIGNET Pierre committed
908
        #[solv.add_clause(clause) for clause in self.__variant_constraints]
909

VIGNET Pierre's avatar
VIGNET Pierre committed
910
        # dynamics
VIGNET Pierre's avatar
VIGNET Pierre committed
911
912
        #[solv.add_clause(clause) for lcl in self.__dynamic_constraints
        # for clause in lcl]
913

914
        # initial
VIGNET Pierre's avatar
VIGNET Pierre committed
915
        #[solv.add_clause(clause) for clause in self.__initial_constraints]
VIGNET Pierre's avatar
VIGNET Pierre committed
916

917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
        # 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))
939
940


VIGNET Pierre's avatar
VIGNET Pierre committed
941
942
943
944
945
    def __constraints_satisfied(self):
        """
        @return: boolean
        """
        solver = CryptoMS()
946
        # Load Solver and all clauses
VIGNET Pierre's avatar
VIGNET Pierre committed
947
        self.__load_solver(solver)
948
949
        # 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
950
        if self.__stats:
951
            if solver.nb_vars() > self.__nb_vars:
VIGNET Pierre's avatar
VIGNET Pierre committed
952
                self.__nb_vars = solver.nb_vars()
953
954
955
956

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

960

VIGNET Pierre's avatar
VIGNET Pierre committed
961
962
963
964
965
966
967
968
    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)
969

VIGNET Pierre's avatar
VIGNET Pierre committed
970
        if self.__stats:
971
            if solver.nb_vars() > self.__nb_vars:
VIGNET Pierre's avatar
VIGNET Pierre committed
972
                self.__nb_vars = solver.nb_vars()
973
974
975
            # Starting from pycryptosat 5.2, nb_clauses() is a private attribute
            #if solver.nb_clauses() > self.__nb_clauses:
            #    self.__nb_clauses = solver.nb_clauses()
976

977
        if LOGGER.getEffectiveLevel() == DEBUG:
978
979
980
            LOGGER.debug("__msolve_constraints :: vvars : " + str(vvars))
            LOGGER.debug("__msolve_constraints :: max_sol : " + str(max_sol))
            lintsol = solver.msolve_selected(max_sol, vvars)
981
            LOGGER.debug("__msolve_constraints :: lintsol : " + str(lintsol))
982
            return [RawSolution(solint, self) for solint in lintsol]
983

984
985
        return [RawSolution(solint, self)
                for solint in solver.msolve_selected(max_sol, vvars)]
VIGNET Pierre's avatar
VIGNET Pierre committed
986
987
988
989
990

    # dynamic properties
    def squery_is_satisfied(self, max_step):
        """
        Ask the SAT solver
991
        @param max_step: int - the horizon
VIGNET Pierre's avatar
VIGNET Pierre committed
992
993
994
995
996
997
998
        """
        # initialization
        self.init_forward_unfolding()
        # horizon adjustment
        if self.__list_variant_constraints:
            max_step = min(max_step, len(self.__list_variant_constraints)-1)
        # loop
999
        if self.__invariant_property and not self.__final_property :
VIGNET Pierre's avatar
VIGNET Pierre committed
1000
1001
            while self.__current_step <= max_step:
                self.shift()
1002
            return self.__constraints_satisfied()
VIGNET Pierre's avatar
VIGNET Pierre committed
1003
1004
1005
1006
1007
        else :
            while self.__current_step <= max_step:
                if self.__constraints_satisfied():
                    return True
                self.shift()
1008
1009
1010
1011
            return self.__constraints_satisfied()



VIGNET Pierre's avatar
VIGNET Pierre committed
1012
1013
1014
1015
1016
1017
    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
1018
1019

        @return: list of RawSolution objects
VIGNET Pierre's avatar
VIGNET Pierre committed
1020
        """
1021
1022
        if LOGGER.getEffectiveLevel() == DEBUG:
            LOGGER.debug("squery_solve :: vvars : " + str(vvars))
VIGNET Pierre's avatar
VIGNET Pierre committed
1023
1024
1025
1026
1027
1028
1029
1030
1031
        # 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
1032
1033
1034
            # return l_rawsol
            return self.__msolve_constraints(max_sol, vvars)

VIGNET Pierre's avatar
VIGNET Pierre committed
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
        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
1050

VIGNET Pierre's avatar
VIGNET Pierre committed
1051
1052
1053
1054
1055
1056

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

VIGNET Pierre's avatar
VIGNET Pierre committed
1059
1060
1061
1062
    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?
1063

VIGNET Pierre's avatar
VIGNET Pierre committed
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
    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
1074

VIGNET Pierre's avatar
VIGNET Pierre committed
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
    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
1088

VIGNET Pierre's avatar
VIGNET Pierre committed
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
    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
1108
1109
1110
            self.clauses.append(Clause([nl1, notnl]))           # not x or not lh
            self.clauses.append(Clause([nl2, notnl]))           # not x or not rh
            self.clauses.append(Clause([notnl1, notnl2, newl])) # x or not lh or not rh
VIGNET Pierre's avatar
VIGNET Pierre committed
1111
1112

        if operator == 'or':    # x = lh or rh
1113
1114
1115
            self.clauses.append(Clause([notnl1, newl]))        # x or not lh
            self.clauses.append(Clause([notnl2, newl]))        # x or not rh
            self.clauses.append(Clause([nl1, nl2, notnl]))     # not x or not lh or not rh
VIGNET Pierre's avatar
VIGNET Pierre committed
1116

1117
1118
1119
#        self.clauses.append(cl1)
#        self.clauses.append(cl2)
#        self.clauses.append(cl3)
VIGNET Pierre's avatar
VIGNET Pierre committed
1120
1121
1122
1123
        if top:
            self.clauses.append(Clause([newl]))
            return None
        return newl
1124

VIGNET Pierre's avatar
VIGNET Pierre committed
1125
1126
1127
1128
1129
1130
1131
1132
1133
    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
1134
                return None
VIGNET Pierre's avatar
VIGNET Pierre committed
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
        # 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
1169

VIGNET Pierre's avatar
VIGNET Pierre committed
1170
1171
1172
1173
1174
1175
1176
        self.clauses.append(cl1)
        self.clauses.append(cl2)
        self.clauses.append(cl3)
        if top:
            self.clauses.append(Clause([newl]))
            return None
        return newl
1177

VIGNET Pierre's avatar
VIGNET Pierre committed
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
    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
1206