source: vis_dev/vis-2.3/src/abs/absRefine.c @ 97

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

vis2.3
File size: 33.3 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [absRefine.c]
4
5  PackageName [abs]
6
7  Synopsis [Abstraction Refinement procedures for the mu-calculus model
8  checker.]
9
10  Author      [Abelardo Pardo <abel@vlsi.colorado.edu>]
11
12  Copyright   [This file was created at the University of Colorado at Boulder.
13  The University of Colorado at Boulder makes no warranty about the suitability
14  of this software for any purpose.  It is presented on an AS IS basis.]
15
16******************************************************************************/
17
18#include "absInt.h"
19
20static char rcsid[] UNUSED = "$Id: absRefine.c,v 1.24 2002/09/19 05:25:01 fabio Exp $";
21
22
23/*---------------------------------------------------------------------------*/
24/* Macro declarations                                                        */
25/*---------------------------------------------------------------------------*/
26
27/*---------------------------------------------------------------------------*/
28/* Variable declarations                                                     */
29/*---------------------------------------------------------------------------*/
30
31/**AutomaticStart*************************************************************/
32
33/*---------------------------------------------------------------------------*/
34/* Static function prototypes                                                */
35/*---------------------------------------------------------------------------*/
36
37static mdd_t * RefineVariable(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet);
38static mdd_t * RefineIdentifier(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet);
39static mdd_t * RefineNot(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet);
40static mdd_t * RefineAnd(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet);
41static mdd_t * RefineFixedPoint(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet);
42static mdd_t * RefineFixedPointIterate(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet, int iterateNumber);
43static mdd_t * RefinePreImage(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet);
44static boolean RestoreContainment(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
45static int PruneIterateVector(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
46static mdd_t * SuccessTest(mdd_t *sat, mdd_t *goalSet, boolean polarity);
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           [Refine a given sub-formula]
63
64  Description [This function just checks for some trivial cases and then calls
65  the appropriate refinement function depending on the type of the formula]
66
67  SideEffects        []
68
69  SeeAlso [RefineAnd, RefineFixedPoint, RefineNot, RefinePreImage,
70  RefineIdentifier, RefineVariable]
71
72******************************************************************************/
73mdd_t *
74AbsSubFormulaRefine(
75  Abs_VerificationInfo_t *absInfo,
76  AbsVertexInfo_t *vertexPtr,
77  mdd_t *goalSet)
78{
79  AbsStats_t *stats;
80  mdd_manager *mddManager;
81  mdd_t *oldTmpCareSet = NIL(mdd_t);
82  mdd_t      *realGoalSet;
83  mdd_t      *result;
84  long       verbosity;
85
86  verbosity = AbsOptionsReadVerbosity(AbsVerificationInfoReadOptions(absInfo));
87  stats = AbsVerificationInfoReadStats(absInfo);
88  mddManager = AbsVerificationInfoReadMddManager(absInfo);
89
90  if (verbosity & ABS_VB_REFINE) {
91    (void) fprintf(vis_stdout, "ABS: Beginning Refinement of Vertex(%3d)\n",
92                   AbsVertexReadId(vertexPtr));
93  }
94
95  /* If the goal set is empty, do not refine */
96  if (mdd_is_tautology(goalSet, 0)) {
97
98    if (verbosity & ABS_VB_GOALSZ) {
99      (void) fprintf(vis_stdout, 
100                     "ABS: Empty Goal in Refinement of Vertex(%3d)\n",
101                     AbsVertexReadId(vertexPtr));
102    }
103
104    /* Set the refine flag */
105    AbsVertexSetTrueRefine(vertexPtr, TRUE);
106
107    return mdd_dup(goalSet);
108  }
109
110  realGoalSet = SuccessTest(AbsVertexReadSat(vertexPtr), goalSet, 
111                            AbsVertexReadPolarity(vertexPtr));
112
113  /* If the vertex is refined already do not try to refine it */
114  if (mdd_is_tautology(realGoalSet, 0) || 
115      !AbsVertexReadGlobalApprox(vertexPtr)) {
116
117    if (verbosity & ABS_VB_GOALSZ) {
118      (void) fprintf(vis_stdout, 
119                     "ABS: Quick (%d,%d) Refinement of Vertex(%3d)\n",
120                     mdd_is_tautology(realGoalSet, 0)? 1: 0,
121                     AbsVertexReadGlobalApprox(vertexPtr)? 0: 1,
122                     AbsVertexReadId(vertexPtr));
123    }
124
125    AbsVertexSetTrueRefine(vertexPtr, TRUE);
126    return realGoalSet;
127  }
128
129  if (verbosity & ABS_VB_GOALSZ) {
130    (void) fprintf(vis_stdout, "ABS: Received Goal Set-> ");
131    (void) fprintf(vis_stdout, "%d Nodes\n",
132                   mdd_size(realGoalSet));
133    if (verbosity & ABS_VB_GLCUBE) {
134      AbsBddPrintMinterms(realGoalSet);
135    }
136  }
137
138  mdd_free(realGoalSet);
139
140  /* If the current vertex has more than one parent, the temporary care set
141   * must be reset (because it depends on the path that led to this vertex) */
142  if (lsLength(vertexPtr->parent) > 1) {
143    oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
144    AbsVerificationInfoSetTmpCareSet(absInfo, mdd_one(mddManager));
145  }
146
147  switch (AbsVertexReadType(vertexPtr)) {
148    case fixedPoint_c:
149      result = RefineFixedPoint(absInfo, vertexPtr, goalSet);
150      AbsStatsReadRefineFixedPoint(stats)++;
151      break;
152    case and_c: 
153      result = RefineAnd(absInfo, vertexPtr, goalSet);
154      AbsStatsReadRefineAnd(stats)++;
155      break;
156    case not_c:
157      result = RefineNot(absInfo, vertexPtr, goalSet);
158      AbsStatsReadRefineNot(stats)++;
159      break;
160    case preImage_c:
161      result = RefinePreImage(absInfo, vertexPtr, goalSet);
162      AbsStatsReadRefinePreImage(stats)++;
163      break;
164    case identifier_c:
165      result = RefineIdentifier(absInfo, vertexPtr, goalSet);
166      AbsStatsReadRefineIdentifier(stats)++;
167      break;
168    case variable_c:
169      result = RefineVariable(absInfo, vertexPtr, goalSet);
170      AbsStatsReadRefineVariable(stats)++;
171      break;
172    default: fail("Encountered unknown type of vertex\n");
173    }
174
175  if (verbosity & ABS_VB_REFINE) {
176    (void) fprintf(vis_stdout, 
177                   "ABS: Done Refining Vertex(%3d).\n",
178                   AbsVertexReadId(vertexPtr));
179  }
180
181  if (verbosity & ABS_VB_GOALSZ) {
182    (void) fprintf(vis_stdout, "ABS: Returned Goal Set-> ");
183    (void) fprintf(vis_stdout, "%d Nodes\n",
184                   mdd_size(result));
185    if (verbosity & ABS_VB_GLCUBE) {
186      AbsBddPrintMinterms(result);
187    }
188  }
189
190  if (verbosity  & ABS_VB_REFVTX) {
191    AbsVertexPrint(vertexPtr, NIL(st_table), FALSE, verbosity);
192  }
193
194  if (lsLength(vertexPtr->parent) > 1) {
195    /* Restore the old temporary careset */
196    mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
197    AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
198  }
199
200  return result;
201} /* End of AbsSubFormulaRefine */
202
203/*---------------------------------------------------------------------------*/
204/* Definition of static functions                                            */
205/*---------------------------------------------------------------------------*/
206
207/**Function********************************************************************
208
209  Synopsis           [Function to refine the sat set of a variable vertex.]
210
211  Description [The variable vertex reads the value of sat from the environment,
212  therefore no approximation is done here. The function just reads if the
213  goalSet is included in the current sat. This function returns
214  trueVerification_c if the vertex has been successfully refined,
215  falseVerification_c if the vertex has been refined until the exact
216  computation has been performed but the refinement failed, and
217  inconclusiveVerification_c if the vertex has been refined to the extent of
218  the computational limits and still failed.]
219
220  SideEffects        []
221
222  SeeAlso            [AbsSubFormulaRefine]
223
224******************************************************************************/
225static mdd_t *
226RefineVariable(
227  Abs_VerificationInfo_t *absInfo,
228  AbsVertexInfo_t *vertexPtr,
229  mdd_t *goalSet)
230{
231  /* Set the current goalSet. If the pointer is non-empty, that means that the
232     variable belongs to a different pointer from the one being considered,
233     therefore, only the first goal set is of interest to us.*/
234  if (AbsVertexReadGoalSet(vertexPtr) == NIL(mdd_t)) {
235    AbsVertexSetGoalSet(vertexPtr, mdd_dup(goalSet));
236  }
237
238  /* Set the validity of the refinement */
239  AbsVertexSetTrueRefine(vertexPtr, !AbsVertexReadGlobalApprox(vertexPtr));
240
241  return mdd_dup(goalSet);
242} /* End of RefineVariable */
243
244/**Function********************************************************************
245
246  Synopsis           [Function to refine an atomic formula]
247
248  SideEffects        []
249
250  SeeAlso            [AbsSubFormulaRefine]
251
252******************************************************************************/
253static mdd_t *
254RefineIdentifier(
255  Abs_VerificationInfo_t *absInfo,
256  AbsVertexInfo_t *vertexPtr,
257  mdd_t *goalSet)
258{
259  /* Set the refinement flags */
260  AbsVertexSetTrueRefine(vertexPtr, TRUE);
261
262  /*
263   * If the polarity of this vertex is negative, we need to add states to
264   * the satisfying set.  Since we already have the exact set, the states not
265   * in it are the returned goal.  If the polarity is positive, we need to
266   * remove states.  The states of the incoming goal that are in the
267   * satisfying set are the returned goal.
268   */
269  if (AbsVertexReadPolarity(vertexPtr)) {
270    return mdd_and(goalSet, AbsVertexReadSat(vertexPtr), 1, 1);
271  } else {
272    return mdd_and(goalSet, AbsVertexReadSat(vertexPtr), 1, 0);
273  }
274} /* End of RefineIdentifier */
275
276/**Function********************************************************************
277
278  Synopsis           [Formula to refine a negation formula]
279
280  SideEffects        []
281
282  SeeAlso            [AbsSubFormulaRefine]
283
284******************************************************************************/
285static mdd_t *
286RefineNot(
287  Abs_VerificationInfo_t *absInfo,
288  AbsVertexInfo_t *vertexPtr,
289  mdd_t *goalSet)
290{
291  AbsVertexInfo_t *subFormula;
292  mdd_t *result;
293
294  /* The not vertex has a trivial propagation equation */
295  subFormula = AbsVertexReadLeftKid(vertexPtr);
296
297  /* Go ahead and re-evaluate */
298  mdd_free(AbsVertexReadSat(vertexPtr));
299
300  /* Refine recursively */
301  result = AbsSubFormulaRefine(absInfo, subFormula, goalSet);
302
303  /* Set the set sat */
304  AbsVertexSetSat(vertexPtr, mdd_not(AbsVertexReadSat(subFormula)));
305 
306  /* Set the approximation flags */
307  AbsVertexSetLocalApprox(vertexPtr, FALSE);
308  AbsVertexSetGlobalApprox(vertexPtr, AbsVertexReadGlobalApprox(subFormula));
309
310  /* Set the trueRefine flag */
311  AbsVertexSetTrueRefine(vertexPtr, AbsVertexReadTrueRefine(subFormula));
312
313  assert(mdd_lequal(result, goalSet, 1, 1));
314
315  return result;
316} /* End of RefineNot */
317
318/**Function********************************************************************
319
320  Synopsis           [Function to refine a conjunction formula]
321
322  SideEffects        []
323
324  SeeAlso            [AbsSubFormulaRefine]
325
326******************************************************************************/
327static mdd_t *
328RefineAnd(
329  Abs_VerificationInfo_t *absInfo,
330  AbsVertexInfo_t *vertexPtr,
331  mdd_t *goalSet)
332{
333  AbsVertexInfo_t *firstFormula;
334  AbsVertexInfo_t *secondFormula;
335  mdd_t           *kidFirstResult;
336  mdd_t           *conjunction;
337  mdd_t           *result;
338  mdd_t           *oldTmpCareSet;
339
340  /* Delete the old sat */
341  mdd_free(AbsVertexReadSat(vertexPtr));
342
343  /* Obtain the Sub-formulas  */
344  firstFormula = AbsVertexReadLeftKid(vertexPtr);
345  secondFormula = AbsVertexReadRightKid(vertexPtr);
346
347  kidFirstResult = AbsSubFormulaRefine(absInfo, firstFormula, goalSet);
348 
349  /* Store the temporary careset and set the new one */
350  oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
351  AbsVerificationInfoSetTmpCareSet(absInfo, 
352                                   mdd_and(oldTmpCareSet, 
353                                           AbsVertexReadSat(firstFormula), 
354                                           1,1));
355 
356  if (AbsVertexReadPolarity(vertexPtr)) {
357    /*
358     * Positive polarity: The goal set is given to one sub-formula first for
359     * refinement, and the left-overs are given to the second sub-formula.
360     */
361    result = AbsSubFormulaRefine(absInfo, secondFormula, kidFirstResult);
362    mdd_free(kidFirstResult);
363  }
364  else { /* Vertex with negative polarity */
365    mdd_t *kidSecondResult;
366    mdd_t *reducedGoalSet;
367
368    reducedGoalSet = mdd_and(goalSet, AbsVertexReadSat(firstFormula), 1, 1);
369    kidSecondResult = AbsSubFormulaRefine(absInfo, secondFormula,
370                                          reducedGoalSet);
371    result = mdd_or(kidFirstResult, kidSecondResult, 1, 1);
372
373    mdd_free(reducedGoalSet);
374    mdd_free(kidFirstResult);
375    mdd_free(kidSecondResult);
376  }
377
378  /* Restore the temporary careset */
379  mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
380  AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
381 
382  /* Re-evaluate the vertex just in case there has been some refinement */
383  conjunction = mdd_and(AbsVertexReadSat(firstFormula),
384                        AbsVertexReadSat(secondFormula), 1, 1);
385 
386  /* Store the new Sat value */
387  AbsVertexSetSat(vertexPtr, conjunction);
388 
389  /* Set the approximation flags */
390  AbsVertexSetLocalApprox(vertexPtr, FALSE);
391  AbsVertexSetGlobalApprox(vertexPtr,
392                           AbsVertexReadGlobalApprox(firstFormula) || 
393                           AbsVertexReadGlobalApprox(secondFormula));
394
395  /* Set the refinement flags */
396  AbsVertexSetTrueRefine(vertexPtr, AbsVertexReadTrueRefine(firstFormula) &&
397                         AbsVertexReadTrueRefine(secondFormula));
398
399  assert(mdd_lequal(result, goalSet, 1, 1));
400
401  return result;
402} /* End of RefineAnd */
403
404/**Function********************************************************************
405
406  Synopsis           [Function to refine the fix-point sub-formulas]
407
408  Description [The function calls several additional procedures to perform the
409  refinement]
410
411  SideEffects        []
412
413  SeeAlso [AbsSubFormulaRefine, AbsFixedPointIterate, RefineFixedPointIterate,
414  PruneIterateVector, RestoreContainment]
415
416******************************************************************************/
417static mdd_t *
418RefineFixedPoint(
419  Abs_VerificationInfo_t *absInfo,
420  AbsVertexInfo_t *vertexPtr,
421  mdd_t *goalSet)
422{
423  boolean newIterates;
424  mdd_t   *currentGoalSet;
425  mdd_t   *result;
426  mdd_t   *oldTmpCareSet;
427  mdd_t   *newTmpCareSet;
428  mdd_t   *oneMdd;
429  int     numIterates;
430
431  /* Variable initialization */
432  numIterates = array_n(AbsVertexReadRings(vertexPtr)) - 1;
433  newIterates = TRUE;
434
435  /* Delete the previous result */
436  if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
437    mdd_free(AbsVertexReadSat(vertexPtr));
438  }
439
440  /* Set the new care set */
441  oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
442  newTmpCareSet = mdd_one(AbsVerificationInfoReadMddManager(absInfo));
443  AbsVerificationInfoSetTmpCareSet(absInfo, newTmpCareSet);
444
445  oneMdd = mdd_one(AbsVerificationInfoReadMddManager(absInfo));
446  currentGoalSet = mdd_dup(oneMdd);
447  /* While the fixed point has not been approximated exactly */
448  while (newIterates && AbsVertexReadGlobalApprox(vertexPtr)
449         && !mdd_is_tautology(currentGoalSet, 0)) {
450    mdd_t *newGoalSet;
451    boolean pruneIterates;
452
453    newGoalSet = RefineFixedPointIterate(absInfo, vertexPtr, currentGoalSet,
454                                         numIterates);
455
456    /* Release unnecessary functions */
457    mdd_free(newGoalSet);
458    mdd_free(currentGoalSet);
459
460    /* Restore the inclusion property in the fixed point iterates */
461    pruneIterates = RestoreContainment(absInfo, vertexPtr);
462
463    /* Remove redundant iterates */
464    if (pruneIterates) {
465      numIterates = PruneIterateVector(absInfo, vertexPtr);
466    }
467
468    /* Sanity check of the refinement process */
469    assert(AbsIteratesSanityCheck(absInfo, vertexPtr));
470
471    /* Check if further iteration is required */
472    newIterates = AbsFixedPointIterate(absInfo, vertexPtr, numIterates);
473    numIterates = array_n(AbsVertexReadRings(vertexPtr)) - 1;
474
475    currentGoalSet = SuccessTest(AbsVertexFetchRing(vertexPtr, numIterates),
476                                 oneMdd, AbsVertexReadPolarity(vertexPtr));
477  } /* End of while loop */
478
479  mdd_free(oneMdd);
480
481  /* Restore the old temporary careset */
482  mdd_free(newTmpCareSet);
483  AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
484
485  AbsVertexSetSat(vertexPtr, 
486                  mdd_dup(AbsVertexFetchRing(vertexPtr, numIterates)));
487
488  AbsVertexSetLocalApprox(vertexPtr, FALSE);
489  AbsVertexSetGlobalApprox(vertexPtr, 
490                           AbsVertexFetchSubApprox(vertexPtr, numIterates));
491
492  result = mdd_and(currentGoalSet, goalSet, 1, 1);
493  mdd_free(currentGoalSet);
494  return result;
495} /* End of RefineFixedPoint */
496
497/**Function********************************************************************
498
499  Synopsis           [Apply the refinement procedure to one of the iterations
500  of the fix-point]
501
502  SideEffects        []
503
504  SeeAlso            [AbsSubFormulaRefine]
505
506******************************************************************************/
507static mdd_t *
508RefineFixedPointIterate(
509  Abs_VerificationInfo_t *absInfo,
510  AbsVertexInfo_t *vertexPtr,
511  mdd_t *goalSet,
512  int iterateNumber)
513{
514  AbsVertexInfo_t *varFormula;
515  AbsVertexInfo_t *subFormula;
516  boolean         trueRefine;
517  mdd_t           *careSet;
518  mdd_t           *variableValue;
519  mdd_t           *result;
520  mdd_t           *previousGoal;
521  mdd_t           *refinedGoal;
522  mdd_t           *newIterate;
523  mdd_t           *oldIterate;
524  mdd_t           *subFormulaSat;
525  int             saveExact;
526
527  assert(iterateNumber != 0);
528
529  /* Variable initialization */
530  varFormula = AbsVertexReadFpVar(vertexPtr);
531  subFormula = AbsVertexReadLeftKid(vertexPtr);
532  careSet = AbsVerificationInfoReadCareSet(absInfo);
533  oldIterate = AbsVertexFetchRing(vertexPtr, iterateNumber);
534
535  /* Propagate the goalSet for refinement */
536  variableValue = AbsVertexFetchRing(vertexPtr, iterateNumber - 1);
537
538  AbsVertexSetSat(varFormula, variableValue);
539
540  AbsVertexSetGlobalApprox(varFormula,
541                           AbsVertexFetchSubApprox(vertexPtr,
542                                                   iterateNumber - 1));
543
544  /* Schedule the formula for Re-evaluation */
545  AbsFormulaScheduleEvaluation(varFormula, vertexPtr);
546
547  /* Evaluate the sub-formula again */
548  AbsSubFormulaVerify(absInfo, subFormula);
549
550  /* Set the goal to empty to detect if the refinement reaches it */
551  if (AbsVertexReadGoalSet(varFormula) != NIL(mdd_t)) {
552    mdd_free(AbsVertexReadGoalSet(varFormula));
553    AbsVertexSetGoalSet(varFormula, NIL(mdd_t));
554  }
555
556  /* Refine the sub-formula for this iterate */
557  result = AbsSubFormulaRefine(absInfo, subFormula, goalSet);
558
559  /* Read the trueRefine from the subFormula */
560  trueRefine = AbsVertexReadTrueRefine(subFormula);
561
562  /* If The refinement does not need a recursive step, return. The return may
563   * be for three different reasons:
564   *   a) The local refinement that was just done, succeeded completely.
565   *   b) The goalset in varFormula is NIL, which means, the refinement
566          process failed somewhere earlier in the process, and therefore, the
567          false result was computed without the refinement of the variable.
568       c) trueRefine is TRUE. Which means, that even though the approximate
569          flag in the vertex is TRUE, meaning that there has been an
570          approximation, the refinement is still solid
571   */
572  if (mdd_is_tautology(result, 0) || trueRefine || 
573      AbsVertexReadGoalSet(varFormula) == NIL(mdd_t)) {
574
575    subFormulaSat = AbsVertexReadSat(subFormula);
576    if (AbsVertexReadPolarity(vertexPtr)) {
577      if (AbsMddLEqualModCareSet(subFormulaSat, oldIterate, careSet)) {
578        newIterate = mdd_dup(subFormulaSat);
579      }
580      else {
581        newIterate = mdd_and(subFormulaSat, oldIterate, 1, 1);
582      }
583    }
584    else {
585      if (AbsMddLEqualModCareSet(oldIterate, subFormulaSat, careSet)) {
586        newIterate = mdd_dup(subFormulaSat);
587      }
588      else {
589        newIterate = mdd_or(subFormulaSat, oldIterate, 1, 1);
590      }
591    }
592
593    mdd_free(oldIterate);
594    array_insert(mdd_t *, AbsVertexReadRings(vertexPtr), iterateNumber,
595                 newIterate);
596
597    /* Set the new approx flag */
598    array_insert(boolean, AbsVertexReadSubApprox(vertexPtr), iterateNumber,
599                 AbsVertexReadGlobalApprox(subFormula));
600
601    AbsVertexSetTrueRefine(vertexPtr, trueRefine);
602
603    return result;
604  }
605
606  /* Recursive call to refine the previous iterate */
607  previousGoal = mdd_dup(AbsVertexReadGoalSet(varFormula));
608  refinedGoal = RefineFixedPointIterate(absInfo, vertexPtr, previousGoal,
609                                        iterateNumber - 1);
610
611  trueRefine = AbsVertexReadTrueRefine(vertexPtr);
612
613  /*
614   * Due to the refinement of the previous iterate, convergence might have
615   * been reached
616   */
617  if (iterateNumber > 1) {
618    mdd_t *ring1 = AbsVertexFetchRing(vertexPtr, iterateNumber - 1);
619    mdd_t *ring2 = AbsVertexFetchRing(vertexPtr, iterateNumber - 2);
620    if (AbsMddLEqualModCareSet(ring1, ring2, careSet)) {
621      mdd_free(previousGoal);
622      mdd_free(refinedGoal);
623      mdd_free(oldIterate);
624      mdd_free(result);
625
626      array_insert(mdd_t *, AbsVertexReadRings(vertexPtr), iterateNumber,
627                   mdd_dup(AbsVertexFetchRing(vertexPtr, iterateNumber - 1)));
628
629      AbsVertexSetTrueRefine(vertexPtr, trueRefine);
630
631      /* Set the new approx flag */
632      array_insert(boolean, AbsVertexReadSubApprox(vertexPtr), iterateNumber, 
633                   AbsVertexReadGlobalApprox(subFormula));
634
635      return SuccessTest(AbsVertexFetchRing(vertexPtr, iterateNumber),
636                         goalSet, AbsVertexReadPolarity(vertexPtr));
637    }
638  }
639
640  mdd_free(previousGoal);
641  mdd_free(refinedGoal);
642
643  /* Evaluate the sub-formula exactly */
644  variableValue = AbsVertexFetchRing(vertexPtr, iterateNumber - 1);
645
646  AbsVertexSetSat(varFormula, variableValue);
647  mdd_free(result);
648
649  AbsVertexSetGlobalApprox(varFormula, 
650                           AbsVertexFetchSubApprox(vertexPtr, 
651                                                   iterateNumber - 1));
652
653  /* Schedule the formula for Re-evaluation */
654  AbsFormulaScheduleEvaluation(varFormula, vertexPtr);
655
656  /* Evaluate the sub-formula this time exactly */
657  saveExact = AbsOptionsReadExact(AbsVerificationInfoReadOptions(absInfo));
658  AbsOptionsSetExact(AbsVerificationInfoReadOptions(absInfo), TRUE);
659  AbsSubFormulaVerify(absInfo, subFormula);
660  AbsOptionsSetExact(AbsVerificationInfoReadOptions(absInfo), saveExact);
661
662  /* Enforce monotonicity of the approximants */
663  subFormulaSat = AbsVertexReadSat(subFormula);
664  if (AbsVertexReadPolarity(vertexPtr)) {
665    if (AbsMddLEqualModCareSet(subFormulaSat, oldIterate, careSet)) {
666      newIterate = mdd_dup(subFormulaSat);
667    }
668    else {
669      newIterate = mdd_and(subFormulaSat, oldIterate, 1, 1);
670    }
671  }
672  else {
673    if (AbsMddLEqualModCareSet(oldIterate, subFormulaSat, careSet)) {
674      newIterate = mdd_dup(subFormulaSat);
675    }
676    else {
677      newIterate = mdd_or(subFormulaSat, oldIterate, 1, 1);
678    }
679  }
680
681  /* Set the new approx flag */
682  array_insert(boolean, AbsVertexReadSubApprox(vertexPtr), iterateNumber, 
683               AbsVertexReadGlobalApprox(subFormula));
684
685  /* Recompute the goal set and the iterate */
686  result = SuccessTest(newIterate, goalSet,
687                       AbsVertexReadPolarity(vertexPtr));
688
689  /* Some basic sanity check */
690  assert(AbsVertexReadPolarity(vertexPtr)?
691         AbsMddLEqualModCareSet(newIterate, oldIterate, careSet):
692         AbsMddLEqualModCareSet(oldIterate, newIterate, careSet));
693
694  /* Store the new iterate */
695  mdd_free(oldIterate);
696  array_insert(mdd_t *, AbsVertexReadRings(vertexPtr), iterateNumber, 
697               newIterate);
698
699  /* Set the new approx flag */
700  array_insert(boolean, AbsVertexReadSubApprox(vertexPtr), iterateNumber, 
701               AbsVertexReadGlobalApprox(subFormula));
702
703  AbsVertexSetTrueRefine(vertexPtr, trueRefine);
704
705  return result;
706} /* End of RefineFixedPointIterate */
707
708/**Function********************************************************************
709
710  Synopsis           [Function to refine the pre-image sub-formula]
711
712  SideEffects        []
713
714  SeeAlso            [AbsSubFormulaRefine]
715
716******************************************************************************/
717static mdd_t *
718RefinePreImage(
719  Abs_VerificationInfo_t *absInfo,
720  AbsVertexInfo_t *vertexPtr,
721  mdd_t *goalSet)
722{
723  AbsStats_t      *stats;
724  AbsVertexInfo_t *subFormula;
725  Img_ImageInfo_t *imageInfo;
726  Fsm_Fsm_t       *system;
727  mdd_t           *careSet;
728  mdd_t           *result;
729  mdd_t           *subResult;
730  mdd_t           *newGoalSet;
731  mdd_t           *oldTmpCareSet;
732  mdd_t           *preImage;
733
734  /* Variable initialization */
735  system = AbsVerificationInfoReadFsm(absInfo);
736  subFormula = AbsVertexReadLeftKid(vertexPtr);
737  subResult = AbsVertexReadSat(subFormula);
738  stats = AbsVerificationInfoReadStats(absInfo);
739  imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 1);
740  careSet = mdd_and(AbsVerificationInfoReadCareSet(absInfo),
741                    AbsVerificationInfoReadTmpCareSet(absInfo), 1, 1);
742
743  /* Propagate the goal set */
744  newGoalSet = AbsImageReadOrCompute(absInfo, imageInfo, goalSet, subResult);
745
746  /* Store the new care set */
747  oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
748  AbsVerificationInfoSetTmpCareSet(absInfo, 
749                        mdd_one(AbsVerificationInfoReadMddManager(absInfo)));
750
751  /* Refine recursively */
752  result = AbsSubFormulaRefine(absInfo, subFormula, newGoalSet);
753
754  /* Restore the old temporary careset */
755  mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
756  AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
757
758  if (!mdd_equal(result, newGoalSet) || 
759      !AbsVertexReadGlobalApprox(subFormula)) {
760    mdd_free(AbsVertexReadSat(vertexPtr));
761   
762    if (AbsVertexReadSolutions(vertexPtr) == NIL(st_table)) {
763      /* Initialize the cache */
764      AbsVertexSetSolutions(vertexPtr, st_init_table(st_ptrcmp, st_ptrhash));
765    }
766   
767    preImage = NIL(mdd_t);
768    if (AbsEvalCacheLookup(AbsVertexReadSolutions(vertexPtr),
769                           AbsVertexReadSat(subFormula), careSet, FALSE,
770                           &preImage, 0)) {
771     
772      /* Set the sat */
773      AbsVertexSetSat(vertexPtr, mdd_dup(preImage));
774    }
775    else {
776      long cpuTime;
777     
778      subResult = AbsVertexReadSat(subFormula);
779     
780      cpuTime = util_cpu_time();
781      AbsVertexSetSat(vertexPtr, 
782                      Img_ImageInfoComputeBwdWithDomainVars(imageInfo, 
783                                                            subResult,
784                                                            subResult,
785                                                            careSet));
786      AbsStatsReadPreImageCpuTime(stats)+= util_cpu_time() - cpuTime;
787     
788      AbsStatsReadExactPreImage(stats)++;
789     
790      /* Insert the result in the cache */
791      AbsEvalCacheInsert(AbsVertexReadSolutions(vertexPtr),
792                         AbsVertexReadSat(subFormula),
793                         AbsVertexReadSat(vertexPtr), careSet,
794                         FALSE, FALSE);
795     
796    }
797    /* Set the new approximation flags */
798    AbsVertexSetLocalApprox(vertexPtr, FALSE);
799    AbsVertexSetGlobalApprox(vertexPtr, 
800                             AbsVertexReadGlobalApprox(subFormula));
801  } /* If !mdd_equal || !GlobalApprox(subFormula) */
802  mdd_free(careSet);
803  mdd_free(newGoalSet);
804  mdd_free(result);
805
806  result = SuccessTest(AbsVertexReadSat(vertexPtr), goalSet,
807                       AbsVertexReadPolarity(vertexPtr));
808
809  AbsVertexSetTrueRefine(vertexPtr, 
810                         AbsVertexReadTrueRefine(subFormula));
811
812  return result;
813} /* End of RefinePreImage */
814
815/**Function********************************************************************
816
817  Synopsis [Function to restore the containment relation between the iterations
818  of a fix-point]
819
820  Description [After the refinement procedure has gone through the iterations
821  of the fix-point, it is possible that the containment relation is no longer
822  satisfied. This function looks at the polarity of the formula inside the
823  fix-point and restores the containment relation to the iterations. This
824  process can be seen as the propagation of certain refinements in the middle
825  of the chain of iterations to the rest of the chain]
826
827  SideEffects        []
828
829  SeeAlso            [AbsSubFormulaRefine]
830
831******************************************************************************/
832static boolean
833RestoreContainment(
834  Abs_VerificationInfo_t *absInfo,
835  AbsVertexInfo_t *vertexPtr)
836{
837  mdd_t *iterateMdd;
838  mdd_t *iterateMddPrevious;
839  mdd_t *product;
840  boolean convergence;
841  int numIterates;
842  int index;
843
844  convergence = FALSE;
845  numIterates = array_n(AbsVertexReadRings(vertexPtr)) - 1;
846
847  if (AbsVertexReadPolarity(vertexPtr)) {
848    iterateMddPrevious = AbsVertexFetchRing(vertexPtr, numIterates);
849   
850    for(index = numIterates - 1; index >= 0; index--) {
851      iterateMdd = iterateMddPrevious;
852      iterateMddPrevious = AbsVertexFetchRing(vertexPtr, index);
853     
854      if (!AbsMddLEqualModCareSet(iterateMddPrevious, iterateMdd,
855                                  AbsVerificationInfoReadCareSet(absInfo))) {
856        product = mdd_and(iterateMddPrevious, iterateMdd, 1, 1);
857       
858        /* Add here don't care minimization */
859       
860        mdd_free(iterateMddPrevious);
861        array_insert(mdd_t *, AbsVertexReadRings(vertexPtr), index, product);
862        iterateMddPrevious = product;
863      }
864
865      if (index != numIterates - 1 &&
866          AbsMddLEqualModCareSet(iterateMdd, iterateMddPrevious,
867                                 AbsVerificationInfoReadCareSet(absInfo))) {
868        convergence = TRUE;
869      }
870    }
871  }
872  else {
873    iterateMdd = AbsVertexFetchRing(vertexPtr, 0);
874
875    for(index = 1; index <= numIterates; index++) {
876      iterateMddPrevious = iterateMdd;
877      iterateMdd = AbsVertexFetchRing(vertexPtr, index);
878
879      if (!AbsMddLEqualModCareSet(iterateMddPrevious, iterateMdd,
880                                  AbsVerificationInfoReadCareSet(absInfo))) {
881        product = mdd_or(iterateMddPrevious, iterateMdd, 1, 1);
882       
883        /* Add here don't care minimization */
884
885        mdd_free(iterateMdd);
886        array_insert(mdd_t *, AbsVertexReadRings(vertexPtr), index, product);
887        iterateMdd = product;
888      }
889     
890      if (index != numIterates &&
891          AbsMddLEqualModCareSet(iterateMdd, iterateMddPrevious,
892                                 AbsVerificationInfoReadCareSet(absInfo))) {
893        convergence = TRUE;
894      }
895    }
896  }
897
898  return convergence;
899} /* End of RestoreContainment */
900
901/**Function********************************************************************
902
903  Synopsis [Detect early convergence in the iterations of a fix-point]
904
905  Description [After the refinement process has modified the iterations of the
906  fix-point and the containment relation has been restored, it could happen
907  that two iterations in the middle of the chain are identical. This is an
908  early termination condition and the sequence of iterations needs to be
909  pruned]
910
911  SideEffects        []
912
913  SeeAlso            [AbsSubFormulaRefine]
914
915******************************************************************************/
916static int
917PruneIterateVector(
918  Abs_VerificationInfo_t *absInfo,
919  AbsVertexInfo_t *vertexPtr)
920{
921  array_t *newRings;
922  array_t *newRingApprox;
923  array_t *newSubApprox;
924  mdd_t   *current;
925  mdd_t   *previous;
926  mdd_t   *careSet;
927  int     numIterates;
928  int     index;
929
930  /* Read the care Set */
931  careSet = AbsVerificationInfoReadCareSet(absInfo);
932 
933  /* Read the number of iterates initially in the vertex */
934  numIterates = array_n(AbsVertexReadRings(vertexPtr)) - 1;
935  assert(numIterates > 0);
936 
937  /* If there are only two iterates, no pruning is needed */
938  if (numIterates < 2) {
939    return numIterates;
940  }
941
942  /* Allocate the new arrays to store the new iterates */
943  newRings = array_alloc(mdd_t *, 0);
944  newRingApprox = array_alloc(boolean, 0);
945  newSubApprox = array_alloc(boolean, 0);
946
947  /* Initial values for the loop */
948  index = 1;
949  previous = AbsVertexFetchRing(vertexPtr, index - 1);
950  current = AbsVertexFetchRing(vertexPtr, index);
951  array_insert_last(mdd_t *, newRings, mdd_dup(previous));
952  array_insert_last(boolean, newRingApprox,
953                    AbsVertexFetchRingApprox(vertexPtr, index - 1));
954  array_insert_last(boolean, newSubApprox,
955                    AbsVertexFetchSubApprox(vertexPtr, index - 1));
956
957  /* Traverse the set of iterates */
958  while (index < numIterates && 
959         !AbsMddLEqualModCareSet(current, previous, careSet)) {
960    array_insert_last(mdd_t *, newRings, mdd_dup(current));
961    array_insert_last(boolean, newRingApprox,
962                      AbsVertexFetchRingApprox(vertexPtr, index));
963    array_insert_last(boolean, newSubApprox,
964                      AbsVertexFetchSubApprox(vertexPtr, index));
965    index++;
966    previous = current;
967    current = AbsVertexFetchRing(vertexPtr, index);
968  }
969
970  /* Insert the last two elements of the array */
971  array_insert_last(mdd_t *, newRings, mdd_dup(current));
972  array_insert_last(boolean, newRingApprox, 
973                    AbsVertexFetchRingApprox(vertexPtr, index));
974  array_insert_last(boolean, newSubApprox,
975                    AbsVertexFetchSubApprox(vertexPtr, index));
976
977  /* Free the arrays stored in the vertex and store the new ones */
978  arrayForEachItem(mdd_t *, AbsVertexReadRings(vertexPtr), index, current) {
979    mdd_free(current);
980  }
981  array_free(AbsVertexReadRings(vertexPtr));
982  array_free(AbsVertexReadRingApprox(vertexPtr));
983  array_free(AbsVertexReadSubApprox(vertexPtr));
984 
985  /* Store the new results */
986  AbsVertexSetRings(vertexPtr, newRings);
987  AbsVertexSetRingApprox(vertexPtr, newRingApprox);
988  AbsVertexSetSubApprox(vertexPtr, newSubApprox);
989 
990  assert(array_n(newRings) == array_n(newRingApprox));
991  assert(array_n(newRings) == array_n(newSubApprox));
992
993  return array_n(newRings) - 1;
994} /* End of PruneIterateVector */
995
996/**Function********************************************************************
997
998  Synopsis [Test if the function SAT is contained/excluded from the goal set
999  depending on the polarity]
1000
1001  SideEffects        []
1002
1003  SeeAlso            [AbsSubFormulaRefine]
1004
1005******************************************************************************/
1006static mdd_t *
1007SuccessTest(
1008  mdd_t *sat,
1009  mdd_t *goalSet,
1010  boolean polarity)
1011{
1012  mdd_t *result;
1013
1014  if (polarity) {
1015    result = mdd_and(goalSet, sat, 1, 1);
1016  }
1017  else {
1018    result = mdd_and(goalSet, sat, 1, 0);
1019  }
1020
1021  return result;
1022} /* End of SuccessTest */
Note: See TracBrowser for help on using the repository browser.