source: vis_dev/vis-2.3/src/bmc/bmcAutSat.c @ 17

Last change on this file since 17 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 22.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [bmcAutSat.c]
4
5  PackageName [bmc]
6 
7  Synopsis    [Automaton for BMC]
8
9  Author      [Mohammad Awedh]
10
11  Copyright   [This file was created at the University of Colorado at
12  Boulder.  The University of Colorado at Boulder makes no warranty
13  about the suitability of this software for any purpose.  It is
14  presented on an AS IS basis.]
15******************************************************************************/
16
17#include "bmc.h"
18#include "bmcInt.h"
19
20static char rcsid[] UNUSED = "$Id: bmcAutSat.c,v 1.10 2005/04/16 18:02:25 awedh Exp $";
21
22/*---------------------------------------------------------------------------*/
23/* Constant declarations                                                     */
24/*---------------------------------------------------------------------------*/
25
26/*---------------------------------------------------------------------------*/
27/* Type declarations                                                         */
28/*---------------------------------------------------------------------------*/
29
30
31/*---------------------------------------------------------------------------*/
32/* Structure declarations                                                    */
33/*---------------------------------------------------------------------------*/
34
35
36/*---------------------------------------------------------------------------*/
37/* Variable declarations                                                     */
38/*---------------------------------------------------------------------------*/
39
40
41/**AutomaticStart*************************************************************/
42
43/*---------------------------------------------------------------------------*/
44/* Static function prototypes                                                */
45/*---------------------------------------------------------------------------*/
46
47
48/**AutomaticEnd***************************************************************/
49
50
51/*---------------------------------------------------------------------------*/
52/* Definition of exported functions                                          */
53/*---------------------------------------------------------------------------*/
54
55
56/*---------------------------------------------------------------------------*/
57/* Definition of internal functions                                          */
58/*---------------------------------------------------------------------------*/
59
60/**Function********************************************************************
61
62 Synopsis [Verify the general LTL formula passes by applying the
63   termination criteria that are described in the paper "Proving More
64   Properties with Bounded Model Checking"]
65
66  Description [Check for the termination on the composition of the
67  automaton that describes the negation of the LTL formula and the
68  model.  We apply the termination criteria as described in the paper
69  "Proving More Properties with Bounded Model Checking".]
70
71  Return value:
72        -1 error in running BMC
73         0 no action
74         1 (m+n-1) <= options->maxK.  If no counterexample of length up to (m+n-1),
75                                      the property passes
76         2 (m+n-1) >  options->maxK   The property is undecided if no counterexample
77                                      of length <= options->maxK.
78         3 Pass by early termination
79 
80  SideEffects []
81
82  SeeAlso     []
83
84******************************************************************************/
85int
86BmcAutLtlCheckForTermination(
87  Ntk_Network_t            *network,
88  array_t                  *constraintArray,
89  BmcCheckForTermination_t *terminationStatus,
90  st_table                 *nodeToMvfAigTable,
91  st_table                 *CoiTable,
92  BmcOption_t              *options)
93{
94 
95  BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
96  FILE            *cnfFile;
97  array_t         *result = NIL(array_t);
98  array_t         *unitClause = array_alloc(int, 0);
99  array_t         *orClause;
100
101  long            startTime, endTime;
102  int             k = terminationStatus->k;
103  int             returnStatus = 0;
104  Ltl_Automaton_t *automaton = terminationStatus->automaton;
105
106  /*
107    If checkLevel == 0 -->  check for beta' only and if UNSAT, m=k and chekLevel =1
108    If checkLevel == 1 -->  check for beta  only and if UNSAT, checkLevel = 2.
109    If checkLevel == 2 -->  check for alpha only and if UNSAT, n=k and checkLevel = 3.
110    If gama is UNSAT up to (m+n-1) and checkLvel = 3, formula passes.
111    checkLevel = 4 if (m+n-1) > maxK;
112   */ 
113  startTime = util_cpu_ctime();
114 
115  /* ===========================
116     Early termination condition
117     =========================== */
118  if (options->earlyTermination) {
119    if (options->verbosityLevel == BmcVerbosityMax_c) {
120      (void) fprintf(vis_stdout, "\nChecking the early termination at k= %d\n", k);
121    }
122    /*
123      Create clauses database
124    */
125    cnfClauses = BmcCnfClausesAlloc();
126
127    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
128    if (cnfFile == NIL(FILE)) {
129      (void)fprintf(vis_stderr,
130                    "** bmc error: Cannot create CNF output file %s\n",
131                    options->satInFile);
132      return -1;
133    }
134    BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k, BMC_INITIAL_STATES,
135                                                cnfClauses, nodeToMvfAigTable, CoiTable);
136    BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
137    (void) fclose(cnfFile);
138    BmcCnfClausesFree(cnfClauses);
139         
140    result = BmcCheckSAT(options);
141    if(options->satSolverError){
142      return -1;
143    }
144    if(result == NIL(array_t)) {
145      (void) fprintf(vis_stdout, "# BMC: by early ermination\n");
146      return 3;
147    }
148  } /* Early termination */
149   if((!automaton->fairSets) &&
150     (terminationStatus->checkLevel == 0)) {
151    /*
152      All the automaton states are fair states. So, beta' and beta are always UNSAT.
153    */
154    terminationStatus->m = 0;
155     (void) fprintf(vis_stdout,"Value of m = %d\n", terminationStatus->m);
156    terminationStatus->checkLevel = 2;
157  }
158  /*
159    beta''(k)
160  */
161  if(terminationStatus->checkLevel == 0){ 
162    int i;
163    /*
164      Create clauses database
165    */
166    cnfClauses = BmcCnfClausesAlloc();
167    if (options->verbosityLevel == BmcVerbosityMax_c) {
168      (void) fprintf(vis_stdout, "# BMC: Check Beta'' \n");
169    }
170    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
171    if (cnfFile == NIL(FILE)) {
172      (void)fprintf(vis_stderr,
173                    "** bmc error: Cannot create CNF output file %s\n",
174                    options->satInFile);
175      return -1;
176    }
177    BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k+1, BMC_NO_INITIAL_STATES,
178                                                cnfClauses, nodeToMvfAigTable, CoiTable);
179    for(i=1; i<=k+1; i++){
180      if(constraintArray != NIL(array_t)){
181        Ctlsp_Formula_t *formula;
182        int              j;
183       
184        arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
185          array_insert(int, unitClause, 0,
186                       - BmcGenerateCnfForLtl(network, formula, i, i, -1, cnfClauses)
187                       );
188          BmcCnfInsertClause(cnfClauses, unitClause);
189        }
190      }
191      array_insert(int, unitClause, 0,
192                   - BmcAutGenerateCnfForBddOffSet(automaton->fairSets, i, i, cnfClauses, NIL(st_table))
193                   );
194      BmcCnfInsertClause(cnfClauses, unitClause);
195    }
196       if(constraintArray != NIL(array_t)){
197      Ctlsp_Formula_t *formula;
198      int              j;
199
200      orClause   = array_alloc(int, 0);
201     
202      arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
203        array_insert_last(int, orClause,
204                          BmcGenerateCnfForLtl(network, formula, k+1, k+1, -1, cnfClauses)
205                          );
206      }
207      array_insert_last(int, orClause, 
208                        BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
209                        );
210      BmcCnfInsertClause(cnfClauses, orClause);
211      array_free(orClause);
212    } else {
213      array_insert(int, unitClause, 0, 
214                   BmcAutGenerateCnfForBddOffSet(automaton->fairSets, 0, 0, cnfClauses, NIL(st_table))
215                   );
216      BmcCnfInsertClause(cnfClauses, unitClause);
217    }
218    BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
219    (void) fclose(cnfFile);
220   
221    result = BmcCheckSAT(options);
222   
223    if(options->satSolverError){
224      return -1;
225    }
226    if(result == NIL(array_t)) {
227      terminationStatus->m = k;
228      (void)fprintf(vis_stderr,"m = %d\n", terminationStatus->m);
229      terminationStatus->checkLevel = 1;
230    }
231    BmcCnfClausesFree(cnfClauses);
232  } /* Check for Beta' */
233 
234  /*
235    beta'(k)
236  */
237  if(terminationStatus->checkLevel == 0){
238    int i;
239    /*
240      Create clauses database
241    */
242    cnfClauses = BmcCnfClausesAlloc();
243    if (options->verbosityLevel == BmcVerbosityMax_c) {
244      (void) fprintf(vis_stdout, "# BMC: Check Beta' \n");
245    }
246    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
247    if (cnfFile == NIL(FILE)) {
248      (void)fprintf(vis_stderr,
249                    "** bmc error: Cannot create CNF output file %s\n",
250                    options->satInFile);
251      return -1;
252    }
253    BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k+1, BMC_NO_INITIAL_STATES,
254                                                cnfClauses, nodeToMvfAigTable, CoiTable);
255    for(i=0; i<=k; i++){
256      if(constraintArray != NIL(array_t)){
257        Ctlsp_Formula_t *formula;
258        int              j;
259       
260        arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
261          array_insert(int, unitClause, 0,
262                       - BmcGenerateCnfForLtl(network, formula, i, i, -1, cnfClauses)
263                       );
264          BmcCnfInsertClause(cnfClauses, unitClause);
265        }
266      }
267      array_insert(int, unitClause, 0,
268                   - BmcAutGenerateCnfForBddOffSet(automaton->fairSets, i, i, cnfClauses, NIL(st_table))
269                   );
270      BmcCnfInsertClause(cnfClauses, unitClause);
271    }
272    if(constraintArray != NIL(array_t)){
273      Ctlsp_Formula_t *formula;
274      int              j;
275
276      orClause   = array_alloc(int, 0);
277     
278      arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
279        array_insert_last(int, orClause,
280                          BmcGenerateCnfForLtl(network, formula, k+1, k+1, -1, cnfClauses)
281                          );
282      }
283      array_insert_last(int, orClause, 
284                        BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
285                        );
286      BmcCnfInsertClause(cnfClauses, orClause);
287      array_free(orClause);
288    } else {
289      array_insert(int, unitClause, 0, 
290                   BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
291                   );
292      BmcCnfInsertClause(cnfClauses, unitClause);
293    }
294   
295    BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
296    (void) fclose(cnfFile);
297   
298    result = BmcCheckSAT(options);
299   
300    if(options->satSolverError){
301      return -1;
302    }
303    if(result == NIL(array_t)) {
304      terminationStatus->m = k;
305      (void)fprintf(vis_stdout,"Value of m = %d\n", terminationStatus->m);
306      terminationStatus->checkLevel = 1;
307    }
308    BmcCnfClausesFree(cnfClauses);
309  } /* Check for Beta' */
310 
311  /*
312    Check for Beta.
313  */
314  if(terminationStatus->checkLevel == 1){
315    cnfClauses = BmcCnfClausesAlloc();
316    {/* To print a witness */
317      /*  lsGen               lsGen;
318      vertex_t            *vtx;
319      Ltl_AutomatonNode_t *state;
320      int i;
321     
322      foreach_vertex(automaton->G, lsGen, vtx) {
323        state = (Ltl_AutomatonNode_t *) vtx->user_data;
324        state->cnfIndex = ALLOC(int, k+2);
325        for(i=0; i<=k+1; i++){
326          state->cnfIndex[i] = BmcAutGenerateCnfForBddOffSet(state->Encode, i,
327                                                             i, cnfClauses, NIL(st_table));
328        }
329        } */
330    }/* To print a witness */
331    if (options->verbosityLevel == BmcVerbosityMax_c) {
332      (void) fprintf(vis_stdout, "# BMC: Check Beta\n");
333    }
334   
335    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
336    if (cnfFile == NIL(FILE)) {
337      (void)fprintf(vis_stderr,
338                    "** bmc error: Cannot create CNF output file %s\n",
339                    options->satInFile);
340      return -1;
341    }
342    /*
343      Generate a simple path of length k+1.
344    */
345    BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k+1, BMC_NO_INITIAL_STATES,
346                                                cnfClauses, nodeToMvfAigTable,
347                                                   CoiTable);
348
349    if(constraintArray != NIL(array_t)){
350      Ctlsp_Formula_t *formula;
351      int              j;
352     
353      arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
354        array_insert(int, unitClause, 0,
355                     - BmcGenerateCnfForLtl(network, formula, k, k, -1, cnfClauses)
356                     );
357        BmcCnfInsertClause(cnfClauses, unitClause);
358      }
359    }
360   
361    array_insert(int, unitClause, 0, 
362                 - BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k, k, cnfClauses, NIL(st_table))
363                 );
364    BmcCnfInsertClause(cnfClauses, unitClause);
365
366   if(constraintArray != NIL(array_t)){
367      Ctlsp_Formula_t *formula;
368      int              j;
369
370      orClause   = array_alloc(int, 0);
371     
372      arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
373        array_insert_last(int, orClause,
374                          BmcGenerateCnfForLtl(network, formula, k+1, k+1, -1, cnfClauses)
375                          );
376      }
377      array_insert_last(int, orClause, 
378                        BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
379                        );
380      BmcCnfInsertClause(cnfClauses, orClause);
381      array_free(orClause);
382    } else { 
383      array_insert(int, unitClause, 0, 
384                   BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
385                   );
386      BmcCnfInsertClause(cnfClauses, unitClause);
387    }
388   
389    BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
390    (void) fclose(cnfFile);
391   
392    result = BmcCheckSAT(options);
393   
394    if(options->satSolverError){
395      return -1;
396    }
397    if(result == NIL(array_t)) {
398      terminationStatus->checkLevel = 2;
399    }
400    BmcCnfClausesFree(cnfClauses);
401  } /* Check Beta*/
402 
403  if(terminationStatus->checkLevel == 2){ /* we check Alpha if Beta is unsatisfiable */
404
405    if (options->verbosityLevel == BmcVerbosityMax_c) {
406      (void) fprintf(vis_stdout, "# BMC: Check Alpha \n");
407    }
408   
409    cnfClauses = BmcCnfClausesAlloc();
410     
411    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
412    if (cnfFile == NIL(FILE)) {
413      (void)fprintf(vis_stderr,
414                    "** bmc error: Cannot create CNF output file %s\n",
415                    options->satInFile);
416      return -1;
417    }
418   
419    BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k, BMC_INITIAL_STATES,
420                                                cnfClauses, nodeToMvfAigTable, CoiTable);
421    if(automaton->fairSets){
422
423      if(constraintArray != NIL(array_t)){
424        Ctlsp_Formula_t *formula;
425        int              j;
426       
427        orClause   = array_alloc(int, 0);
428       
429        arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
430          array_insert_last(int, orClause,
431                            BmcGenerateCnfForLtl(network, formula, k, k, -1, cnfClauses)
432                            );
433        }
434        array_insert_last(int, orClause, 
435                          BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k, k, cnfClauses, NIL(st_table))
436                          );
437        BmcCnfInsertClause(cnfClauses, orClause);
438        array_free(orClause);
439      } else {
440       
441        array_insert(int, unitClause, 0, 
442                     BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k, k, cnfClauses, NIL(st_table))
443                     );
444        BmcCnfInsertClause(cnfClauses, unitClause);
445      }
446    }
447    BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
448    (void) fclose(cnfFile);
449   
450    result = BmcCheckSAT(options);
451    BmcCnfClausesFree(cnfClauses);
452    if(options->satSolverError){
453      return -1;
454    }
455    if(result == NIL(array_t)) {
456      terminationStatus->n = k;
457      terminationStatus->checkLevel = 3;
458      (void)fprintf(vis_stderr,"m=%d  n=%d\n",terminationStatus->m,terminationStatus->n);
459      if ((terminationStatus->m+terminationStatus->n-1) <= options->maxK){
460        terminationStatus->k = terminationStatus->m+terminationStatus->n-1;
461        if(k==0){
462          /*
463            By induction, the property passes.
464          */
465          terminationStatus->k = 0;
466        }
467        returnStatus = 1;
468      } else {
469        terminationStatus->checkLevel = 4;
470        returnStatus = 2;
471      }
472    }
473  }/* Chek for Alpha */
474 
475  array_free(unitClause);
476
477  if (options->verbosityLevel != BmcVerbosityNone_c) {
478    endTime = util_cpu_ctime();
479    fprintf(vis_stdout, "-- Check for termination time time = %10g\n",
480            (double)(endTime - startTime) / 1000.0);
481  }
482
483  return returnStatus;
484 
485} /* BmcAutLtlCheckForTermination */
486
487
488/**Function********************************************************************
489
490  Synopsis [Generate CNF clauses that describe a path in the automaton.]
491
492  Description [Generate CNF clauses for a path in the automaton
493  starting from "fromState" and ending at "toState". If "initialState"
494  = BMC_INITIAL_STATES, the the path starts from an initial state.]
495
496  SideEffects []
497
498  SeeAlso     []
499
500******************************************************************************/
501void
502BmcAutCnfGenerateClausesForPath(
503  Ltl_Automaton_t *automaton,
504  int             fromState,
505  int             toState,
506  int             initialState,
507  BmcCnfClauses_t *cnfClauses)
508{
509  int          k;
510  array_t      *unitClause = array_alloc(int, 1);
511
512  if(initialState){
513    array_insert(int, unitClause, 0, 
514                 BmcAutGenerateCnfForBddOffSet(automaton->initialStates, 0, 0, cnfClauses, automaton->nsPsTable)
515                 );
516    BmcCnfInsertClause(cnfClauses, unitClause);
517  }
518  for(k=fromState; k<toState; k++){
519    array_insert(int, unitClause, 0, 
520    BmcAutGenerateCnfForBddOffSet(automaton->transitionRelation, k, k+1, cnfClauses, automaton->nsPsTable)
521                      );
522    BmcCnfInsertClause(cnfClauses, unitClause);
523  }
524  array_free(unitClause);
525 
526} /* BmcAutCnfGenerateClausesForPath() */
527
528
529/**Function********************************************************************
530
531  Synopsis [Generate CNF clauses for a simple path in the composite
532  model]
533
534  Description [This function generates CNF clauses for a simple path
535  from state "fromState" to state "toState" in the composition of
536  network and automaton.  A simple path is a path along which every
537  state in the path is distinct.  If Si and Sj in the path then Si !=
538  Sj.
539
540  If the value of "initialState" is BMC_INITIAL_STATES, then the path
541  is an initialized path.  Otherwise "initialState" is
542  BMC_NO_INITIAL_STATES.]
543
544  SideEffects []
545
546  SeeAlso     []
547
548******************************************************************************/
549void
550BmcAutCnfGenerateClausesForSimpleCompositePath(
551   Ntk_Network_t   *network,
552   Ltl_Automaton_t *automaton,
553   int             fromState,
554   int             toState,
555   int             initialState,
556   BmcCnfClauses_t *cnfClauses,
557   st_table        *nodeToMvfAigTable,
558   st_table        *CoiTable)
559{
560  int state;
561 
562  /*
563    Generate clauses for a path from fromState to toState in the original model.
564  */
565  BmcCnfGenerateClausesForPath(network, fromState, toState, initialState, cnfClauses, nodeToMvfAigTable, CoiTable);
566  /*
567    Generate clauses for a path from fromState to toState in the Automaton.
568  */
569  BmcAutCnfGenerateClausesForPath(automaton, fromState, toState, initialState, cnfClauses);
570 
571  /*
572    Restrict the above path to be simpe path.
573  */
574  for(state= fromState + 1; state < toState; state++){
575    BmcCnfNoLoopToAnyPreviouseCompositeStates(network, automaton, fromState, state,
576                                              cnfClauses, nodeToMvfAigTable, CoiTable);
577  }
578
579  return;
580} /* BmcAutCnfGenerateClausesForSimpleCompositePath */
581
582
583/**Function********************************************************************
584
585  Synopsis [Generate CNF clauses for no loop from last state to any of
586  the previouse states of the path]
587
588  Description [Generate CNF clauses for no loop from last state
589  "toState" to any of the previous states starting from
590  "fromState". It generates the CNF clauses such that the last state
591  of the path is not equal to any previous states.]
592
593  SideEffects []
594
595  SeeAlso     []
596
597******************************************************************************/
598void
599BmcCnfNoLoopToAnyPreviouseCompositeStates(
600   Ntk_Network_t   *network,
601   Ltl_Automaton_t *automaton,
602   int             fromState,
603   int             toState,
604   BmcCnfClauses_t *cnfClauses,
605   st_table        *nodeToMvfAigTable,
606   st_table        *CoiTable)
607{
608  mAig_Manager_t     *manager   = Ntk_NetworkReadMAigManager(network);
609  bdd_manager        *bddManager = bdd_get_manager(automaton->transitionRelation);
610 
611  Ntk_Node_t         *latch;
612  MvfAig_Function_t  *latchMvfAig;
613  bAigEdge_t         *latchBAig;
614  array_t            *orClause;
615  int                currentIndex, nextIndex, andIndex1, andIndex2; 
616  int                i, k, mvfSize, bddID;
617   
618  st_generator       *stGen;
619
620  /*
621    Generates CNF clauses to constrain that the toState is not equal
622    to any previouse states starting from fromState.
623   
624    Assume there are two state varaibles a and b. To check if Si !=
625    Sj, we must generate clauses for the formula ( ai != aj + bi !=
626    bj).
627  */
628  for(k=fromState; k < toState; k++){
629    orClause = array_alloc(int,0);
630    st_foreach_item(CoiTable, stGen, &latch, NULL) {
631     
632 
633      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
634      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
635        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
636        array_free(latchMvfAig);
637        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
638      } 
639      mvfSize   = array_n(latchMvfAig);
640      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
641     
642      for(i=0; i< mvfSize; i++){
643        latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
644      }
645
646      for (i=0; i< mvfSize; i++){
647        currentIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], k       ,cnfClauses);
648        nextIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], toState ,cnfClauses);     
649        andIndex1 = cnfClauses->cnfGlobalIndex++;
650        BmcCnfGenerateClausesForAND(currentIndex, -nextIndex, andIndex1, cnfClauses);
651        andIndex2 = cnfClauses->cnfGlobalIndex++;
652        BmcCnfGenerateClausesForAND(-currentIndex, nextIndex, andIndex2, cnfClauses);
653
654        array_insert_last(int, orClause, andIndex1);
655        array_insert_last(int, orClause, andIndex2);
656      }
657      FREE(latchBAig);
658    }/* For each latch loop*/
659    st_foreach_item(automaton->psNsTable, stGen, &bddID, NULL) {
660      currentIndex = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(bdd_bdd_ith_var(bddManager, bddID)),
661                                                 k, cnfClauses);
662      nextIndex    = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(bdd_bdd_ith_var(bddManager, bddID)),
663                                                 toState, cnfClauses);
664                                                 
665      andIndex1 = cnfClauses->cnfGlobalIndex++;
666      BmcCnfGenerateClausesForAND(currentIndex, -nextIndex, andIndex1, cnfClauses);
667      andIndex2 = cnfClauses->cnfGlobalIndex++;
668      BmcCnfGenerateClausesForAND(-currentIndex, nextIndex, andIndex2, cnfClauses);
669     
670      array_insert_last(int, orClause, andIndex1);
671      array_insert_last(int, orClause, andIndex2);
672    }
673    BmcCnfInsertClause(cnfClauses, orClause);
674    array_free(orClause);
675  } /* foreach k*/
676  return;
677} /* BmcCnfNoLoopToAnyPreviouseCompositeStates */
Note: See TracBrowser for help on using the repository browser.