src/abs/absRefine.c

Go to the documentation of this file.

#include "absInt.h"

static char rcsid[] UNUSED = "$Id: absRefine.c,v 1.24 2002/09/19 05:25:01 fabio Exp $";


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static mdd_t * RefineVariable(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet);
static mdd_t * RefineIdentifier(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet);
static mdd_t * RefineNot(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet);
static mdd_t * RefineAnd(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet);
static mdd_t * RefineFixedPoint(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet);
static mdd_t * RefineFixedPointIterate(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet, int iterateNumber);
static mdd_t * RefinePreImage(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, mdd_t *goalSet);
static boolean RestoreContainment(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
static int PruneIterateVector(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
static mdd_t * SuccessTest(mdd_t *sat, mdd_t *goalSet, boolean polarity);

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

mdd_t *
AbsSubFormulaRefine(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr,
  mdd_t *goalSet)
{
  AbsStats_t *stats;
  mdd_manager *mddManager;
  mdd_t *oldTmpCareSet = NIL(mdd_t);
  mdd_t      *realGoalSet;
  mdd_t      *result;
  long       verbosity;

  verbosity = AbsOptionsReadVerbosity(AbsVerificationInfoReadOptions(absInfo));
  stats = AbsVerificationInfoReadStats(absInfo);
  mddManager = AbsVerificationInfoReadMddManager(absInfo);

  if (verbosity & ABS_VB_REFINE) {
    (void) fprintf(vis_stdout, "ABS: Beginning Refinement of Vertex(%3d)\n",
                   AbsVertexReadId(vertexPtr));
  }

  /* If the goal set is empty, do not refine */
  if (mdd_is_tautology(goalSet, 0)) {

    if (verbosity & ABS_VB_GOALSZ) {
      (void) fprintf(vis_stdout, 
                     "ABS: Empty Goal in Refinement of Vertex(%3d)\n",
                     AbsVertexReadId(vertexPtr));
    }

    /* Set the refine flag */
    AbsVertexSetTrueRefine(vertexPtr, TRUE);

    return mdd_dup(goalSet);
  }

  realGoalSet = SuccessTest(AbsVertexReadSat(vertexPtr), goalSet, 
                            AbsVertexReadPolarity(vertexPtr));

  /* If the vertex is refined already do not try to refine it */
  if (mdd_is_tautology(realGoalSet, 0) || 
      !AbsVertexReadGlobalApprox(vertexPtr)) {

    if (verbosity & ABS_VB_GOALSZ) {
      (void) fprintf(vis_stdout, 
                     "ABS: Quick (%d,%d) Refinement of Vertex(%3d)\n",
                     mdd_is_tautology(realGoalSet, 0)? 1: 0,
                     AbsVertexReadGlobalApprox(vertexPtr)? 0: 1,
                     AbsVertexReadId(vertexPtr));
    }

    AbsVertexSetTrueRefine(vertexPtr, TRUE);
    return realGoalSet;
  }

  if (verbosity & ABS_VB_GOALSZ) {
    (void) fprintf(vis_stdout, "ABS: Received Goal Set-> ");
    (void) fprintf(vis_stdout, "%d Nodes\n",
                   mdd_size(realGoalSet));
    if (verbosity & ABS_VB_GLCUBE) {
      AbsBddPrintMinterms(realGoalSet);
    }
  }

  mdd_free(realGoalSet);

  /* If the current vertex has more than one parent, the temporary care set
   * must be reset (because it depends on the path that led to this vertex) */
  if (lsLength(vertexPtr->parent) > 1) {
    oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
    AbsVerificationInfoSetTmpCareSet(absInfo, mdd_one(mddManager));
  }

  switch (AbsVertexReadType(vertexPtr)) {
    case fixedPoint_c:
      result = RefineFixedPoint(absInfo, vertexPtr, goalSet);
      AbsStatsReadRefineFixedPoint(stats)++;
      break;
    case and_c: 
      result = RefineAnd(absInfo, vertexPtr, goalSet);
      AbsStatsReadRefineAnd(stats)++;
      break;
    case not_c:
      result = RefineNot(absInfo, vertexPtr, goalSet);
      AbsStatsReadRefineNot(stats)++;
      break;
    case preImage_c:
      result = RefinePreImage(absInfo, vertexPtr, goalSet);
      AbsStatsReadRefinePreImage(stats)++;
      break;
    case identifier_c:
      result = RefineIdentifier(absInfo, vertexPtr, goalSet);
      AbsStatsReadRefineIdentifier(stats)++;
      break;
    case variable_c:
      result = RefineVariable(absInfo, vertexPtr, goalSet);
      AbsStatsReadRefineVariable(stats)++;
      break;
    default: fail("Encountered unknown type of vertex\n");
    }

  if (verbosity & ABS_VB_REFINE) {
    (void) fprintf(vis_stdout, 
                   "ABS: Done Refining Vertex(%3d).\n",
                   AbsVertexReadId(vertexPtr));
  }

  if (verbosity & ABS_VB_GOALSZ) {
    (void) fprintf(vis_stdout, "ABS: Returned Goal Set-> ");
    (void) fprintf(vis_stdout, "%d Nodes\n",
                   mdd_size(result));
    if (verbosity & ABS_VB_GLCUBE) {
      AbsBddPrintMinterms(result);
    }
  }

  if (verbosity  & ABS_VB_REFVTX) {
    AbsVertexPrint(vertexPtr, NIL(st_table), FALSE, verbosity);
  }

  if (lsLength(vertexPtr->parent) > 1) {
    /* Restore the old temporary careset */
    mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
    AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
  }

  return result;
} /* End of AbsSubFormulaRefine */

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

static mdd_t *
RefineVariable(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr,
  mdd_t *goalSet)
{
  /* Set the current goalSet. If the pointer is non-empty, that means that the
     variable belongs to a different pointer from the one being considered,
     therefore, only the first goal set is of interest to us.*/
  if (AbsVertexReadGoalSet(vertexPtr) == NIL(mdd_t)) {
    AbsVertexSetGoalSet(vertexPtr, mdd_dup(goalSet));
  }

  /* Set the validity of the refinement */
  AbsVertexSetTrueRefine(vertexPtr, !AbsVertexReadGlobalApprox(vertexPtr));

  return mdd_dup(goalSet);
} /* End of RefineVariable */

static mdd_t *
RefineIdentifier(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr,
  mdd_t *goalSet)
{
  /* Set the refinement flags */
  AbsVertexSetTrueRefine(vertexPtr, TRUE);

  /*
   * If the polarity of this vertex is negative, we need to add states to
   * the satisfying set.  Since we already have the exact set, the states not
   * in it are the returned goal.  If the polarity is positive, we need to
   * remove states.  The states of the incoming goal that are in the
   * satisfying set are the returned goal.
   */
  if (AbsVertexReadPolarity(vertexPtr)) {
    return mdd_and(goalSet, AbsVertexReadSat(vertexPtr), 1, 1);
  } else {
    return mdd_and(goalSet, AbsVertexReadSat(vertexPtr), 1, 0);
  }
} /* End of RefineIdentifier */

static mdd_t *
RefineNot(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr,
  mdd_t *goalSet)
{
  AbsVertexInfo_t *subFormula;
  mdd_t *result;

  /* The not vertex has a trivial propagation equation */
  subFormula = AbsVertexReadLeftKid(vertexPtr);

  /* Go ahead and re-evaluate */
  mdd_free(AbsVertexReadSat(vertexPtr));

  /* Refine recursively */
  result = AbsSubFormulaRefine(absInfo, subFormula, goalSet);

  /* Set the set sat */
  AbsVertexSetSat(vertexPtr, mdd_not(AbsVertexReadSat(subFormula)));
  
  /* Set the approximation flags */
  AbsVertexSetLocalApprox(vertexPtr, FALSE);
  AbsVertexSetGlobalApprox(vertexPtr, AbsVertexReadGlobalApprox(subFormula));

  /* Set the trueRefine flag */
  AbsVertexSetTrueRefine(vertexPtr, AbsVertexReadTrueRefine(subFormula));

  assert(mdd_lequal(result, goalSet, 1, 1));

  return result;
} /* End of RefineNot */

static mdd_t *
RefineAnd(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr,
  mdd_t *goalSet)
{
  AbsVertexInfo_t *firstFormula;
  AbsVertexInfo_t *secondFormula;
  mdd_t           *kidFirstResult;
  mdd_t           *conjunction;
  mdd_t           *result;
  mdd_t           *oldTmpCareSet;

  /* Delete the old sat */
  mdd_free(AbsVertexReadSat(vertexPtr));

  /* Obtain the Sub-formulas  */
  firstFormula = AbsVertexReadLeftKid(vertexPtr);
  secondFormula = AbsVertexReadRightKid(vertexPtr);

  kidFirstResult = AbsSubFormulaRefine(absInfo, firstFormula, goalSet);
  
  /* Store the temporary careset and set the new one */
  oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
  AbsVerificationInfoSetTmpCareSet(absInfo, 
                                   mdd_and(oldTmpCareSet, 
                                           AbsVertexReadSat(firstFormula), 
                                           1,1));
  
  if (AbsVertexReadPolarity(vertexPtr)) {
    /* 
     * Positive polarity: The goal set is given to one sub-formula first for
     * refinement, and the left-overs are given to the second sub-formula.
     */
    result = AbsSubFormulaRefine(absInfo, secondFormula, kidFirstResult);
    mdd_free(kidFirstResult);
  }
  else { /* Vertex with negative polarity */
    mdd_t *kidSecondResult;
    mdd_t *reducedGoalSet;

    reducedGoalSet = mdd_and(goalSet, AbsVertexReadSat(firstFormula), 1, 1);
    kidSecondResult = AbsSubFormulaRefine(absInfo, secondFormula,
                                          reducedGoalSet);
    result = mdd_or(kidFirstResult, kidSecondResult, 1, 1);

    mdd_free(reducedGoalSet);
    mdd_free(kidFirstResult);
    mdd_free(kidSecondResult);
  }

  /* Restore the temporary careset */
  mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
  AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
  
  /* Re-evaluate the vertex just in case there has been some refinement */
  conjunction = mdd_and(AbsVertexReadSat(firstFormula),
                        AbsVertexReadSat(secondFormula), 1, 1);
  
  /* Store the new Sat value */
  AbsVertexSetSat(vertexPtr, conjunction);
  
  /* Set the approximation flags */
  AbsVertexSetLocalApprox(vertexPtr, FALSE);
  AbsVertexSetGlobalApprox(vertexPtr,
                           AbsVertexReadGlobalApprox(firstFormula) || 
                           AbsVertexReadGlobalApprox(secondFormula));

  /* Set the refinement flags */
  AbsVertexSetTrueRefine(vertexPtr, AbsVertexReadTrueRefine(firstFormula) &&
                         AbsVertexReadTrueRefine(secondFormula));

  assert(mdd_lequal(result, goalSet, 1, 1));

  return result;
} /* End of RefineAnd */

static mdd_t *
RefineFixedPoint(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr,
  mdd_t *goalSet)
{
  boolean newIterates;
  mdd_t   *currentGoalSet;
  mdd_t   *result;
  mdd_t   *oldTmpCareSet;
  mdd_t   *newTmpCareSet;
  mdd_t   *oneMdd;
  int     numIterates;

  /* Variable initialization */
  numIterates = array_n(AbsVertexReadRings(vertexPtr)) - 1;
  newIterates = TRUE;

  /* Delete the previous result */
  if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
    mdd_free(AbsVertexReadSat(vertexPtr));
  }

  /* Set the new care set */
  oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
  newTmpCareSet = mdd_one(AbsVerificationInfoReadMddManager(absInfo));
  AbsVerificationInfoSetTmpCareSet(absInfo, newTmpCareSet);

  oneMdd = mdd_one(AbsVerificationInfoReadMddManager(absInfo));
  currentGoalSet = mdd_dup(oneMdd);
  /* While the fixed point has not been approximated exactly */
  while (newIterates && AbsVertexReadGlobalApprox(vertexPtr)
         && !mdd_is_tautology(currentGoalSet, 0)) {
    mdd_t *newGoalSet;
    boolean pruneIterates;

    newGoalSet = RefineFixedPointIterate(absInfo, vertexPtr, currentGoalSet,
                                         numIterates);

    /* Release unnecessary functions */
    mdd_free(newGoalSet);
    mdd_free(currentGoalSet);

    /* Restore the inclusion property in the fixed point iterates */
    pruneIterates = RestoreContainment(absInfo, vertexPtr);

    /* Remove redundant iterates */
    if (pruneIterates) {
      numIterates = PruneIterateVector(absInfo, vertexPtr);
    }

    /* Sanity check of the refinement process */
    assert(AbsIteratesSanityCheck(absInfo, vertexPtr));

    /* Check if further iteration is required */
    newIterates = AbsFixedPointIterate(absInfo, vertexPtr, numIterates);
    numIterates = array_n(AbsVertexReadRings(vertexPtr)) - 1;

    currentGoalSet = SuccessTest(AbsVertexFetchRing(vertexPtr, numIterates),
                                 oneMdd, AbsVertexReadPolarity(vertexPtr));
  } /* End of while loop */

  mdd_free(oneMdd);

  /* Restore the old temporary careset */
  mdd_free(newTmpCareSet);
  AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);

  AbsVertexSetSat(vertexPtr, 
                  mdd_dup(AbsVertexFetchRing(vertexPtr, numIterates)));

  AbsVertexSetLocalApprox(vertexPtr, FALSE);
  AbsVertexSetGlobalApprox(vertexPtr, 
                           AbsVertexFetchSubApprox(vertexPtr, numIterates));

  result = mdd_and(currentGoalSet, goalSet, 1, 1);
  mdd_free(currentGoalSet);
  return result;
} /* End of RefineFixedPoint */

static mdd_t *
RefineFixedPointIterate(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr,
  mdd_t *goalSet,
  int iterateNumber)
{
  AbsVertexInfo_t *varFormula;
  AbsVertexInfo_t *subFormula;
  boolean         trueRefine;
  mdd_t           *careSet;
  mdd_t           *variableValue;
  mdd_t           *result;
  mdd_t           *previousGoal;
  mdd_t           *refinedGoal;
  mdd_t           *newIterate;
  mdd_t           *oldIterate;
  mdd_t           *subFormulaSat;
  int             saveExact;

  assert(iterateNumber != 0);

  /* Variable initialization */
  varFormula = AbsVertexReadFpVar(vertexPtr);
  subFormula = AbsVertexReadLeftKid(vertexPtr);
  careSet = AbsVerificationInfoReadCareSet(absInfo);
  oldIterate = AbsVertexFetchRing(vertexPtr, iterateNumber);

  /* Propagate the goalSet for refinement */
  variableValue = AbsVertexFetchRing(vertexPtr, iterateNumber - 1);

  AbsVertexSetSat(varFormula, variableValue);

  AbsVertexSetGlobalApprox(varFormula,
                           AbsVertexFetchSubApprox(vertexPtr,
                                                   iterateNumber - 1));

  /* Schedule the formula for Re-evaluation */
  AbsFormulaScheduleEvaluation(varFormula, vertexPtr);

  /* Evaluate the sub-formula again */
  AbsSubFormulaVerify(absInfo, subFormula);

  /* Set the goal to empty to detect if the refinement reaches it */
  if (AbsVertexReadGoalSet(varFormula) != NIL(mdd_t)) {
    mdd_free(AbsVertexReadGoalSet(varFormula));
    AbsVertexSetGoalSet(varFormula, NIL(mdd_t));
  }

  /* Refine the sub-formula for this iterate */
  result = AbsSubFormulaRefine(absInfo, subFormula, goalSet);

  /* Read the trueRefine from the subFormula */
  trueRefine = AbsVertexReadTrueRefine(subFormula);

  /* If The refinement does not need a recursive step, return. The return may
   * be for three different reasons:
   *   a) The local refinement that was just done, succeeded completely.
   *   b) The goalset in varFormula is NIL, which means, the refinement
          process failed somewhere earlier in the process, and therefore, the
          false result was computed without the refinement of the variable.
       c) trueRefine is TRUE. Which means, that even though the approximate
          flag in the vertex is TRUE, meaning that there has been an
          approximation, the refinement is still solid
   */
  if (mdd_is_tautology(result, 0) || trueRefine || 
      AbsVertexReadGoalSet(varFormula) == NIL(mdd_t)) {

    subFormulaSat = AbsVertexReadSat(subFormula);
    if (AbsVertexReadPolarity(vertexPtr)) {
      if (AbsMddLEqualModCareSet(subFormulaSat, oldIterate, careSet)) {
        newIterate = mdd_dup(subFormulaSat);
      }
      else {
        newIterate = mdd_and(subFormulaSat, oldIterate, 1, 1);
      }
    }
    else {
      if (AbsMddLEqualModCareSet(oldIterate, subFormulaSat, careSet)) {
        newIterate = mdd_dup(subFormulaSat);
      }
      else {
        newIterate = mdd_or(subFormulaSat, oldIterate, 1, 1);
      }
    }

    mdd_free(oldIterate);
    array_insert(mdd_t *, AbsVertexReadRings(vertexPtr), iterateNumber,
                 newIterate);

    /* Set the new approx flag */
    array_insert(boolean, AbsVertexReadSubApprox(vertexPtr), iterateNumber,
                 AbsVertexReadGlobalApprox(subFormula));

    AbsVertexSetTrueRefine(vertexPtr, trueRefine);

    return result;
  }

  /* Recursive call to refine the previous iterate */
  previousGoal = mdd_dup(AbsVertexReadGoalSet(varFormula));
  refinedGoal = RefineFixedPointIterate(absInfo, vertexPtr, previousGoal,
                                        iterateNumber - 1);

  trueRefine = AbsVertexReadTrueRefine(vertexPtr);

  /* 
   * Due to the refinement of the previous iterate, convergence might have
   * been reached
   */
  if (iterateNumber > 1) {
    mdd_t *ring1 = AbsVertexFetchRing(vertexPtr, iterateNumber - 1);
    mdd_t *ring2 = AbsVertexFetchRing(vertexPtr, iterateNumber - 2);
    if (AbsMddLEqualModCareSet(ring1, ring2, careSet)) {
      mdd_free(previousGoal);
      mdd_free(refinedGoal);
      mdd_free(oldIterate);
      mdd_free(result);

      array_insert(mdd_t *, AbsVertexReadRings(vertexPtr), iterateNumber,
                   mdd_dup(AbsVertexFetchRing(vertexPtr, iterateNumber - 1)));

      AbsVertexSetTrueRefine(vertexPtr, trueRefine);

      /* Set the new approx flag */
      array_insert(boolean, AbsVertexReadSubApprox(vertexPtr), iterateNumber, 
                   AbsVertexReadGlobalApprox(subFormula));

      return SuccessTest(AbsVertexFetchRing(vertexPtr, iterateNumber),
                         goalSet, AbsVertexReadPolarity(vertexPtr));
    }
  }

  mdd_free(previousGoal);
  mdd_free(refinedGoal);

  /* Evaluate the sub-formula exactly */
  variableValue = AbsVertexFetchRing(vertexPtr, iterateNumber - 1);

  AbsVertexSetSat(varFormula, variableValue);
  mdd_free(result);

  AbsVertexSetGlobalApprox(varFormula, 
                           AbsVertexFetchSubApprox(vertexPtr, 
                                                   iterateNumber - 1));

  /* Schedule the formula for Re-evaluation */
  AbsFormulaScheduleEvaluation(varFormula, vertexPtr);

  /* Evaluate the sub-formula this time exactly */
  saveExact = AbsOptionsReadExact(AbsVerificationInfoReadOptions(absInfo));
  AbsOptionsSetExact(AbsVerificationInfoReadOptions(absInfo), TRUE);
  AbsSubFormulaVerify(absInfo, subFormula);
  AbsOptionsSetExact(AbsVerificationInfoReadOptions(absInfo), saveExact);

  /* Enforce monotonicity of the approximants */
  subFormulaSat = AbsVertexReadSat(subFormula);
  if (AbsVertexReadPolarity(vertexPtr)) {
    if (AbsMddLEqualModCareSet(subFormulaSat, oldIterate, careSet)) {
      newIterate = mdd_dup(subFormulaSat);
    }
    else {
      newIterate = mdd_and(subFormulaSat, oldIterate, 1, 1);
    }
  }
  else {
    if (AbsMddLEqualModCareSet(oldIterate, subFormulaSat, careSet)) {
      newIterate = mdd_dup(subFormulaSat);
    }
    else {
      newIterate = mdd_or(subFormulaSat, oldIterate, 1, 1);
    }
  }

  /* Set the new approx flag */
  array_insert(boolean, AbsVertexReadSubApprox(vertexPtr), iterateNumber, 
               AbsVertexReadGlobalApprox(subFormula));

  /* Recompute the goal set and the iterate */
  result = SuccessTest(newIterate, goalSet,
                       AbsVertexReadPolarity(vertexPtr));

  /* Some basic sanity check */
  assert(AbsVertexReadPolarity(vertexPtr)?
         AbsMddLEqualModCareSet(newIterate, oldIterate, careSet):
         AbsMddLEqualModCareSet(oldIterate, newIterate, careSet));

  /* Store the new iterate */
  mdd_free(oldIterate);
  array_insert(mdd_t *, AbsVertexReadRings(vertexPtr), iterateNumber, 
               newIterate);

  /* Set the new approx flag */
  array_insert(boolean, AbsVertexReadSubApprox(vertexPtr), iterateNumber, 
               AbsVertexReadGlobalApprox(subFormula));

  AbsVertexSetTrueRefine(vertexPtr, trueRefine);

  return result;
} /* End of RefineFixedPointIterate */

static mdd_t *
RefinePreImage(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr,
  mdd_t *goalSet)
{
  AbsStats_t      *stats;
  AbsVertexInfo_t *subFormula;
  Img_ImageInfo_t *imageInfo;
  Fsm_Fsm_t       *system;
  mdd_t           *careSet;
  mdd_t           *result;
  mdd_t           *subResult;
  mdd_t           *newGoalSet;
  mdd_t           *oldTmpCareSet;
  mdd_t           *preImage;

  /* Variable initialization */
  system = AbsVerificationInfoReadFsm(absInfo);
  subFormula = AbsVertexReadLeftKid(vertexPtr);
  subResult = AbsVertexReadSat(subFormula);
  stats = AbsVerificationInfoReadStats(absInfo);
  imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 1);
  careSet = mdd_and(AbsVerificationInfoReadCareSet(absInfo),
                    AbsVerificationInfoReadTmpCareSet(absInfo), 1, 1);

  /* Propagate the goal set */
  newGoalSet = AbsImageReadOrCompute(absInfo, imageInfo, goalSet, subResult);

  /* Store the new care set */
  oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
  AbsVerificationInfoSetTmpCareSet(absInfo, 
                        mdd_one(AbsVerificationInfoReadMddManager(absInfo)));

  /* Refine recursively */
  result = AbsSubFormulaRefine(absInfo, subFormula, newGoalSet);

  /* Restore the old temporary careset */
  mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
  AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);

  if (!mdd_equal(result, newGoalSet) || 
      !AbsVertexReadGlobalApprox(subFormula)) {
    mdd_free(AbsVertexReadSat(vertexPtr));
    
    if (AbsVertexReadSolutions(vertexPtr) == NIL(st_table)) {
      /* Initialize the cache */
      AbsVertexSetSolutions(vertexPtr, st_init_table(st_ptrcmp, st_ptrhash));
    }
    
    preImage = NIL(mdd_t);
    if (AbsEvalCacheLookup(AbsVertexReadSolutions(vertexPtr),
                           AbsVertexReadSat(subFormula), careSet, FALSE,
                           &preImage, 0)) {
      
      /* Set the sat */
      AbsVertexSetSat(vertexPtr, mdd_dup(preImage));
    }
    else {
      long cpuTime;
      
      subResult = AbsVertexReadSat(subFormula);
      
      cpuTime = util_cpu_time();
      AbsVertexSetSat(vertexPtr, 
                      Img_ImageInfoComputeBwdWithDomainVars(imageInfo, 
                                                            subResult,
                                                            subResult,
                                                            careSet));
      AbsStatsReadPreImageCpuTime(stats)+= util_cpu_time() - cpuTime;
      
      AbsStatsReadExactPreImage(stats)++;
      
      /* Insert the result in the cache */
      AbsEvalCacheInsert(AbsVertexReadSolutions(vertexPtr),
                         AbsVertexReadSat(subFormula),
                         AbsVertexReadSat(vertexPtr), careSet,
                         FALSE, FALSE);
      
    }
    /* Set the new approximation flags */
    AbsVertexSetLocalApprox(vertexPtr, FALSE);
    AbsVertexSetGlobalApprox(vertexPtr, 
                             AbsVertexReadGlobalApprox(subFormula));
  } /* If !mdd_equal || !GlobalApprox(subFormula) */
  mdd_free(careSet);
  mdd_free(newGoalSet);
  mdd_free(result);

  result = SuccessTest(AbsVertexReadSat(vertexPtr), goalSet,
                       AbsVertexReadPolarity(vertexPtr));

  AbsVertexSetTrueRefine(vertexPtr, 
                         AbsVertexReadTrueRefine(subFormula));

  return result;
} /* End of RefinePreImage */

static boolean
RestoreContainment(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr)
{
  mdd_t *iterateMdd;
  mdd_t *iterateMddPrevious;
  mdd_t *product;
  boolean convergence;
  int numIterates;
  int index;

  convergence = FALSE;
  numIterates = array_n(AbsVertexReadRings(vertexPtr)) - 1;

  if (AbsVertexReadPolarity(vertexPtr)) {
    iterateMddPrevious = AbsVertexFetchRing(vertexPtr, numIterates);
    
    for(index = numIterates - 1; index >= 0; index--) {
      iterateMdd = iterateMddPrevious;
      iterateMddPrevious = AbsVertexFetchRing(vertexPtr, index);
      
      if (!AbsMddLEqualModCareSet(iterateMddPrevious, iterateMdd,
                                  AbsVerificationInfoReadCareSet(absInfo))) {
        product = mdd_and(iterateMddPrevious, iterateMdd, 1, 1);
        
        /* Add here don't care minimization */
        
        mdd_free(iterateMddPrevious);
        array_insert(mdd_t *, AbsVertexReadRings(vertexPtr), index, product);
        iterateMddPrevious = product;
      }

      if (index != numIterates - 1 &&
          AbsMddLEqualModCareSet(iterateMdd, iterateMddPrevious,
                                 AbsVerificationInfoReadCareSet(absInfo))) {
        convergence = TRUE;
      }
    }
  }
  else {
    iterateMdd = AbsVertexFetchRing(vertexPtr, 0);

    for(index = 1; index <= numIterates; index++) {
      iterateMddPrevious = iterateMdd;
      iterateMdd = AbsVertexFetchRing(vertexPtr, index);

      if (!AbsMddLEqualModCareSet(iterateMddPrevious, iterateMdd,
                                  AbsVerificationInfoReadCareSet(absInfo))) {
        product = mdd_or(iterateMddPrevious, iterateMdd, 1, 1);
        
        /* Add here don't care minimization */

        mdd_free(iterateMdd);
        array_insert(mdd_t *, AbsVertexReadRings(vertexPtr), index, product);
        iterateMdd = product;
      }
      
      if (index != numIterates &&
          AbsMddLEqualModCareSet(iterateMdd, iterateMddPrevious,
                                 AbsVerificationInfoReadCareSet(absInfo))) {
        convergence = TRUE;
      }
    }
  }

  return convergence;
} /* End of RestoreContainment */

static int
PruneIterateVector(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr)
{
  array_t *newRings;
  array_t *newRingApprox;
  array_t *newSubApprox;
  mdd_t   *current;
  mdd_t   *previous;
  mdd_t   *careSet;
  int     numIterates;
  int     index;

  /* Read the care Set */
  careSet = AbsVerificationInfoReadCareSet(absInfo);
  
  /* Read the number of iterates initially in the vertex */
  numIterates = array_n(AbsVertexReadRings(vertexPtr)) - 1;
  assert(numIterates > 0);
  
  /* If there are only two iterates, no pruning is needed */
  if (numIterates < 2) {
    return numIterates;
  }

  /* Allocate the new arrays to store the new iterates */
  newRings = array_alloc(mdd_t *, 0);
  newRingApprox = array_alloc(boolean, 0);
  newSubApprox = array_alloc(boolean, 0);

  /* Initial values for the loop */
  index = 1;
  previous = AbsVertexFetchRing(vertexPtr, index - 1);
  current = AbsVertexFetchRing(vertexPtr, index);
  array_insert_last(mdd_t *, newRings, mdd_dup(previous));
  array_insert_last(boolean, newRingApprox,
                    AbsVertexFetchRingApprox(vertexPtr, index - 1));
  array_insert_last(boolean, newSubApprox,
                    AbsVertexFetchSubApprox(vertexPtr, index - 1));

  /* Traverse the set of iterates */
  while (index < numIterates && 
         !AbsMddLEqualModCareSet(current, previous, careSet)) {
    array_insert_last(mdd_t *, newRings, mdd_dup(current));
    array_insert_last(boolean, newRingApprox,
                      AbsVertexFetchRingApprox(vertexPtr, index));
    array_insert_last(boolean, newSubApprox,
                      AbsVertexFetchSubApprox(vertexPtr, index));
    index++;
    previous = current;
    current = AbsVertexFetchRing(vertexPtr, index);
  }

  /* Insert the last two elements of the array */
  array_insert_last(mdd_t *, newRings, mdd_dup(current));
  array_insert_last(boolean, newRingApprox, 
                    AbsVertexFetchRingApprox(vertexPtr, index));
  array_insert_last(boolean, newSubApprox,
                    AbsVertexFetchSubApprox(vertexPtr, index));

  /* Free the arrays stored in the vertex and store the new ones */
  arrayForEachItem(mdd_t *, AbsVertexReadRings(vertexPtr), index, current) {
    mdd_free(current);
  }
  array_free(AbsVertexReadRings(vertexPtr));
  array_free(AbsVertexReadRingApprox(vertexPtr));
  array_free(AbsVertexReadSubApprox(vertexPtr));
  
  /* Store the new results */
  AbsVertexSetRings(vertexPtr, newRings);
  AbsVertexSetRingApprox(vertexPtr, newRingApprox);
  AbsVertexSetSubApprox(vertexPtr, newSubApprox);
  
  assert(array_n(newRings) == array_n(newRingApprox));
  assert(array_n(newRings) == array_n(newSubApprox));

  return array_n(newRings) - 1;
} /* End of PruneIterateVector */

static mdd_t *
SuccessTest(
  mdd_t *sat,
  mdd_t *goalSet,
  boolean polarity)
{
  mdd_t *result;

  if (polarity) {
    result = mdd_and(goalSet, sat, 1, 1);
  }
  else {
    result = mdd_and(goalSet, sat, 1, 0);
  }

  return result;
} /* End of SuccessTest */