src/abs/absEvaluate.c

Go to the documentation of this file.

#include "absInt.h"

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


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

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

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

static void EvaluateVariable(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
static void EvaluateIdentifier(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
static void EvaluateNot(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
static void EvaluateAnd(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
static void EvaluateFixedPoint(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
static void EvaluatePreImage(Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr);
static mdd_t * OverApproximatePreImageWithSubFSM(Abs_VerificationInfo_t *absInfo, mdd_t *lowerBound, mdd_t *upperBound, mdd_t *careSet);
static mdd_t * OverApproximatePreImageWithBddSubsetting(Abs_VerificationInfo_t *absInfo, mdd_t *lowerBound, mdd_t *upperBound, mdd_t *careSet);
static mdd_t * UnderApproximatePreImageWithBddSubsetting(Abs_VerificationInfo_t *absInfo, mdd_t *lowerBound, mdd_t *upperBound, mdd_t *careSet);

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


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

void
AbsSubFormulaVerify(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr)
{
  AbsStats_t *stats;
  mdd_manager *mddManager;
  mdd_t *oldTmpCareSet = NIL(mdd_t);
  
  long verbosity;

  stats = AbsVerificationInfoReadStats(absInfo);
  mddManager = AbsVerificationInfoReadMddManager(absInfo);

  /* 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:
      EvaluateFixedPoint(absInfo, vertexPtr);
      AbsStatsReadEvalFixedPoint(stats)++;
      break;
    case and_c: 
      EvaluateAnd(absInfo, vertexPtr);
      AbsStatsReadEvalAnd(stats)++;
      break;
    case not_c:
      EvaluateNot(absInfo, vertexPtr);
      AbsStatsReadEvalNot(stats)++;
      break;
    case preImage_c:
      EvaluatePreImage(absInfo, vertexPtr);
      AbsStatsReadEvalPreImage(stats)++;
      break;
    case identifier_c:
      EvaluateIdentifier(absInfo, vertexPtr);
      AbsStatsReadEvalIdentifier(stats)++;
      break;
    case variable_c:
      EvaluateVariable(absInfo, vertexPtr);
      AbsStatsReadEvalVariable(stats)++;
      break;
    default: fail("Encountered unknown type of vertex\n");
    }

  verbosity = AbsOptionsReadVerbosity(AbsVerificationInfoReadOptions(absInfo));

  /* Print the size of the care set */
  if (verbosity & ABS_VB_CARESZ) {
    (void) fprintf(vis_stdout, "ABS: Size of Care Set: ");
    (void) fprintf(vis_stdout, "%d Nodes.\n", 
                   mdd_size(AbsVerificationInfoReadCareSet(absInfo)));
  }

  /* Print the care set */
  if (verbosity & ABS_VB_CARE) {
    (void) fprintf(vis_stdout, "ABS: Care Set for Evaluation:\n");
    AbsBddPrintMinterms(AbsVerificationInfoReadCareSet(absInfo));
  }

  /* Print the contents of the vertex */
  if (verbosity & ABS_VB_VTXCNT) {
    AbsVertexPrint(vertexPtr, NIL(st_table), FALSE, verbosity);
  }

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

} /* End of AbsSubFormulaVerify */

void
AbsFormulaScheduleEvaluation(
  AbsVertexInfo_t *current,
  AbsVertexInfo_t *limit)
{
  /* We reached the final case */
  if (current == limit) {
    return;
  }
  else {
    AbsVertexInfo_t *parentPtr;
    lsList          parentList;
    lsGen           gen;

    /* Set the re-evaluation flag for the current vertex */
    AbsVertexSetServed(current, 0);

    /* Recur over the parents */
    parentList = AbsVertexReadParent(current);
    lsForEachItem(parentList, gen, parentPtr) {
      if (parentPtr != NIL(AbsVertexInfo_t)) {
        AbsFormulaScheduleEvaluation(parentPtr, limit);
      }
    }
  }

  return;
} /* End of AbsFormulaScheduleEvaluation */

mdd_t *
AbsComputeOptimalIterate(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr,
  mdd_t *lowerIterate,
  mdd_t *upperIterate)
{
  mdd_t *tmp;
  mdd_t *result;

  if (AbsOptionsReadMinimizeIterate(AbsVerificationInfoReadOptions(absInfo))
      && AbsVertexReadUseExtraCareSet(vertexPtr)) {

    /* 
     * For this computation we have three ingredients and a handfull of
     * choices. The ingredients are the sets newIterate, iterate and
     * careSet. The goal is to compute an interval delimited by two boolean
     * functions and then call the function bdd_between to try to obtain
     * the best bdd in size inside that interval. To compute the extremes
     * of the interval there are several choices. For example, the care set
     * can be used in the lower bound of the interval or in both
     * bounds. The bigger the interval the more choice the function
     * bdd_between has to minimize, however, this does not turn into a
     * better result. 
     *
     * Current Choice: [newIterate * iterate', newIterate]
     */
    tmp = mdd_and(lowerIterate, upperIterate, 0, 1);
    result = bdd_between(tmp, upperIterate);
    
    /* This line for debugging purposes, should be removed 
    (void) fprintf(vis_stdout, 
                   "newIterate : %d, Diff : %d, result %d\n",
                   mdd_size(upperIterate), mdd_size(tmp),
                   mdd_size(result)); */
    
    mdd_free(tmp);
  }
  else {
    result = mdd_dup(upperIterate);
  }

  return result;
} /* End of AbsComputeOptimalIterate */

boolean
AbsFixedPointIterate(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr,
  int iterateIndex)
{
  AbsVertexInfo_t *subFormula;
  boolean         keepIterating;
  boolean         globalApprox;
  int             stepCount;
  long            verbosity;
  mdd_t           *iterate;
  mdd_t           *newIterate;
  mdd_t           *careSet;
    
  /* Do not allow to iterate from the middle of a fixed point computation */
  assert(iterateIndex == array_n(AbsVertexReadRings(vertexPtr)) - 1);

  careSet = AbsVerificationInfoReadCareSet(absInfo);

  /* Check if the set of iterates has already converged */
  if (array_n(AbsVertexReadRings(vertexPtr)) > 1) {
    mdd_t *ring1 = AbsVertexFetchRing(vertexPtr, iterateIndex);
    mdd_t *ring2 = AbsVertexFetchRing(vertexPtr, iterateIndex - 1);
    if (AbsMddLEqualModCareSet(ring1, ring2, careSet)) {
      return FALSE;
    }
    iterate = AbsVertexFetchRing(vertexPtr, iterateIndex - 1);
  }
  else {
    iterate = AbsVertexFetchRing(vertexPtr, iterateIndex);
  }
  newIterate = AbsVertexFetchRing(vertexPtr, iterateIndex);

  /* Variable initialization */
  keepIterating = TRUE;
  stepCount = iterateIndex;
  verbosity = AbsOptionsReadVerbosity(AbsVerificationInfoReadOptions(absInfo));
  subFormula = AbsVertexReadLeftKid(vertexPtr);
  globalApprox = AbsVertexFetchSubApprox(vertexPtr, iterateIndex);
  
  /* Main loop for the fixed point computation */
  while (keepIterating) {
    mdd_t *best;
    
    /* 
     * Given newIterate, iterate and CareSet, if the use of extra care set is
     * enabled, choose the best candidate as the value of the iterate. 
     */
    best = AbsComputeOptimalIterate(absInfo, vertexPtr, iterate, newIterate);

    /* Print the iterates */
    if ((verbosity & ABS_VB_PITER) || (verbosity & ABS_VB_ITSIZ)) {
      (void) fprintf(vis_stdout, "ABS: New Iterate: ");
      if (verbosity & ABS_VB_ITSIZ) {
        (void) fprintf(vis_stdout, "%d -> %d\n", mdd_size(newIterate),
                       mdd_size(best));
      }
      else {
        (void) fprintf(vis_stdout, "\n");
      }
      if (verbosity & ABS_VB_PITER) {
        AbsBddPrintMinterms(newIterate);
      }
    }
    
    /* Store the value of the variable */
    AbsVertexSetSat(AbsVertexReadFpVar(vertexPtr), best);
    
    /* Mark the proper sub-formulas for re-evaluation */
    AbsFormulaScheduleEvaluation(AbsVertexReadFpVar(vertexPtr), vertexPtr);
    
    /* Evaluate the sub-formula */
    AbsSubFormulaVerify(absInfo, subFormula);
    mdd_free(best);
    iterate = newIterate;
    
    /* 
     * Compute the new iterate. Due to the fact that don't cares are being
     * used, it might be possible that the new iterate does not contain the
     * previous one, in that case the or is taken 
     */
    newIterate = mdd_or(iterate, AbsVertexReadSat(subFormula), 1, 1);
    
    assert(AbsMddLEqualModCareSet(iterate, newIterate, careSet));

    /* Set the rings and the approximation flags */
    AbsVertexInsertRing(vertexPtr, newIterate);
    AbsVertexInsertRingApprox(vertexPtr, FALSE);
    globalApprox = globalApprox || AbsVertexReadGlobalApprox(subFormula);
    AbsVertexInsertSubApprox(vertexPtr, globalApprox);

    keepIterating = !AbsMddEqualModCareSet(newIterate, iterate, careSet);
    
    stepCount++;
  } /* End of main while loop */

  return TRUE;
} /* End of AbsFixedPointIterate */

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

static void
EvaluateVariable(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr)
{
  /* Increase the number of times the result has been used */
  AbsVertexReadServed(vertexPtr)++;

  return;
} /* End of EvaluateVariable */

static void
EvaluateIdentifier(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr)
{
  if (AbsVertexReadServed(vertexPtr) == 0) {
    Ntk_Node_t     *node;
    Var_Variable_t *nodeVar;
    graph_t        *partition;
    vertex_t       *partitionVertex;
    Mvf_Function_t *nodeFunction;
    mdd_t          *result;
    char           *nodeNameString;
    char           *nodeValueString;
    int            nodeValue;

    /* Clean up of previous result */
    if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
      mdd_free(AbsVertexReadSat(vertexPtr));
      AbsVertexSetSat(vertexPtr, NIL(mdd_t));
    }

    /* Read the partition */
    partition = AbsVerificationInfoReadPartition(absInfo);
    
    assert(partition != NIL(graph_t));
    
    /* Obtain the name and the value being used */
    nodeNameString = AbsVertexReadName(vertexPtr);
    nodeValueString = AbsVertexReadValue(vertexPtr);
    
    /* Obtain the the node in the network and the variable attached to it */
    node = Ntk_NetworkFindNodeByName(AbsVerificationInfoReadNetwork(absInfo),
                                     nodeNameString);
    nodeVar = Ntk_NodeReadVariable(node);
    
    /* Obtain the real value of the multi-valued vairable */
    if (Var_VariableTestIsSymbolic(nodeVar)) {
      nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar,
                                                         nodeValueString);
    }
    else {
      nodeValue = atoi(nodeValueString);
    }
    
    /* Read the partition, find the vertex in the partition and its function */
    partitionVertex = Part_PartitionFindVertexByName(partition, 
                                                     nodeNameString);
    
    /* If the vertex is not represented in the partition must be built */
    if (partitionVertex == NIL(vertex_t)) { 
      Ntk_Node_t *tmpNode;
      lsGen      tmpGen;
      array_t    *mvfArray;
      array_t    *tmpRoots;
      st_table   *tmpLeaves;
      
      /* Initialize the variables */
      tmpRoots = array_alloc(Ntk_Node_t *, 0);
      tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash);
      
      /* Insert the parameters in the array and table */
      array_insert_last(Ntk_Node_t *, tmpRoots, node);
      Ntk_NetworkForEachCombInput(AbsVerificationInfoReadNetwork(absInfo),
                                  tmpGen, tmpNode) {
        st_insert(tmpLeaves, (char *) tmpNode, (char *) NTM_UNUSED);
      }
      
      /* Effectively build the mdd for the given vertex */
      mvfArray =  Ntm_NetworkBuildMvfs(AbsVerificationInfoReadNetwork(absInfo),
                                       tmpRoots, tmpLeaves, NIL(mdd_t));
      nodeFunction = array_fetch(Mvf_Function_t *, mvfArray, 0);
      array_free(tmpRoots);
      st_free_table(tmpLeaves);
      array_free(mvfArray);
      
      /* Store the result in the vertex */
      result = Mvf_FunctionReadComponent(nodeFunction, nodeValue);
      AbsVertexSetSat(vertexPtr, mdd_dup(result));
      Mvf_FunctionFree(nodeFunction);
    }
    else {
      /* Store the result in the vertex */
      nodeFunction = Part_VertexReadFunction(partitionVertex);
      result = Mvf_FunctionReadComponent(nodeFunction, nodeValue);
      AbsVertexSetSat(vertexPtr, mdd_dup(result));
    }
    
    /* Set the approximation flags */
    AbsVertexSetLocalApprox(vertexPtr, FALSE);
    AbsVertexSetGlobalApprox(vertexPtr, FALSE);
  }

  /* Increase the number of times the result has been used */
  AbsVertexReadServed(vertexPtr)++;
  
  return;
} /* End of EvaluateIdentifier */

static void
EvaluateNot(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr)
{
  if (AbsVertexReadServed(vertexPtr) == 0) {
    AbsVertexInfo_t *subFormula;
    
    /* Clean up of previous result */
    if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
      mdd_free(AbsVertexReadSat(vertexPtr));
      AbsVertexSetSat(vertexPtr, NIL(mdd_t));
    }

    /* Recursively evaluate the sub-formula */
    subFormula = AbsVertexReadLeftKid(vertexPtr);
    AbsSubFormulaVerify(absInfo, subFormula);

    /* Negate the result of the sub-formula */
    AbsVertexSetSat(vertexPtr, mdd_not(AbsVertexReadSat(subFormula)));

    /* Set the approximation flags */
    AbsVertexSetLocalApprox(vertexPtr, FALSE);
    AbsVertexSetGlobalApprox(vertexPtr, AbsVertexReadGlobalApprox(subFormula));
  }

  /* Increase the number of times the result has been used */
  AbsVertexReadServed(vertexPtr)++;

  return;
} /* End of EvaluateNot */

static void
EvaluateAnd(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr)
{
  if (AbsVertexReadServed(vertexPtr) == 0) {
    AbsVertexInfo_t *firstFormula;
    AbsVertexInfo_t *secondFormula;
    mdd_t *oldTmpCareSet;

    /* Clean up of previous result */
    if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
      mdd_free(AbsVertexReadSat(vertexPtr));
      AbsVertexSetSat(vertexPtr, NIL(mdd_t));
    }

    /* Obtain the subformulas to evaluate */
    firstFormula = AbsVertexReadLeftKid(vertexPtr);
    secondFormula = AbsVertexReadRightKid(vertexPtr);
  
    /* Recursively evaluate the first sub-formula */
    AbsSubFormulaVerify(absInfo, firstFormula);

    /* Store the temporary careset and set the new one */
    oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
    AbsVerificationInfoSetTmpCareSet(absInfo, 
                                     mdd_and(oldTmpCareSet, 
                                             AbsVertexReadSat(firstFormula), 
                                             1,1));

    /* Recursively evaluate the second sub-formula */
    AbsSubFormulaVerify(absInfo, secondFormula);

    /* Restore the temporary careset */
    mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
    AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
    
    /* Compute result, so far no approximation is required */
    AbsVertexSetSat(vertexPtr, mdd_and(AbsVertexReadSat(firstFormula),
                                       AbsVertexReadSat(secondFormula), 
                                       1, 1));

    /* Set the approximation flags */
    AbsVertexSetLocalApprox(vertexPtr, FALSE);
    AbsVertexSetGlobalApprox(vertexPtr, 
                             AbsVertexReadGlobalApprox(firstFormula) || 
                             AbsVertexReadGlobalApprox(secondFormula));
  }

  /* Increase the number of times the result has been used */
  AbsVertexReadServed(vertexPtr)++;

  return;
} /* End of EvaluateAnd */

static void
EvaluateFixedPoint(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr)
{
  if (AbsVertexReadServed(vertexPtr) == 0) {
    mdd_manager *mddManager;
    mdd_t       *oldTmpCareSet;
    mdd_t       *newTmpCareSet;

    if (AbsVertexReadRings(vertexPtr) != NIL(array_t)) {
      mdd_t *ringUnit;
      int i;

      arrayForEachItem(mdd_t *, AbsVertexReadRings(vertexPtr), i, ringUnit) {
        mdd_free(ringUnit);
      }
      array_free(AbsVertexReadRings(vertexPtr));
      array_free(AbsVertexReadRingApprox(vertexPtr));
      array_free(AbsVertexReadSubApprox(vertexPtr));
      mdd_free(AbsVertexReadSat(vertexPtr));
    }

    /* Re-allocation of the temporary structures */
    AbsVertexSetRings(vertexPtr, array_alloc(mdd_t *, 0));
    AbsVertexSetRingApprox(vertexPtr, array_alloc(boolean, 0));
    AbsVertexSetSubApprox(vertexPtr, array_alloc(boolean, 0));
    
    /* Initial values of the fixed point */
    mddManager = AbsVerificationInfoReadMddManager(absInfo);
    AbsVertexInsertRing(vertexPtr, mdd_zero(mddManager));
    AbsVertexInsertRingApprox(vertexPtr, FALSE);
    AbsVertexInsertSubApprox(vertexPtr, FALSE);

    /* Reset the temporary careset to the mdd one */
    oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
    newTmpCareSet = mdd_one(mddManager);
    AbsVerificationInfoSetTmpCareSet(absInfo, newTmpCareSet);

    /* Effectively iterate the body */
    AbsFixedPointIterate(absInfo, vertexPtr, 0);

    /* Restore the old temporary careset */
    mdd_free(newTmpCareSet);
    AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
    
    /* Set the last result as the set sat*/
    AbsVertexSetSat(vertexPtr, 
                    mdd_dup(AbsVertexFetchRing(vertexPtr,
                                        array_n(AbsVertexReadRings(vertexPtr))
                                               - 1)));

    /* Set the approximation flags */
    AbsVertexSetLocalApprox(vertexPtr, FALSE);
    AbsVertexSetGlobalApprox(vertexPtr, 
                             AbsVertexFetchSubApprox(vertexPtr,
                               array_n(AbsVertexReadSubApprox(vertexPtr)) - 1));
  }

  /* Increase the number of times the result has been used */
  AbsVertexReadServed(vertexPtr)++;

  return;
}

 /* End of EvaluateFixedPoint */

static void
EvaluatePreImage(
  Abs_VerificationInfo_t *absInfo,
  AbsVertexInfo_t *vertexPtr)
{
  AbsOptions_t *options;
  AbsStats_t   *stats;
  long         verbosity;

  /* Variable initialization */
  options = AbsVerificationInfoReadOptions(absInfo);
  verbosity = AbsOptionsReadVerbosity(options);
  stats = AbsVerificationInfoReadStats(absInfo);

  if (AbsVertexReadServed(vertexPtr) == 0) {
    AbsVertexInfo_t *subFormula;
    mdd_manager     *mddManager;
    mdd_t           *result;
    mdd_t           *careSet;
    mdd_t           *oldTmpCareSet;
    mdd_t           *minimizedSet;

    /* Variable initialization */
    mddManager = AbsVerificationInfoReadMddManager(absInfo);
    subFormula = AbsVertexReadLeftKid(vertexPtr);

    /* 
     * Compute the care set as the conjunction of the given one and the
     * temporary one 
     */
    careSet = mdd_and(AbsVerificationInfoReadCareSet(absInfo),
                      AbsVerificationInfoReadTmpCareSet(absInfo), 1, 1);

    /* Clean up */
    if (AbsVertexReadSat(vertexPtr) != NIL(mdd_t)) {
      mdd_free(AbsVertexReadSat(vertexPtr));
      AbsVertexSetSat(vertexPtr, NIL(mdd_t));
    }
    
    /* Reset the temporary careset to the mdd one */
    oldTmpCareSet = AbsVerificationInfoReadTmpCareSet(absInfo);
    AbsVerificationInfoSetTmpCareSet(absInfo, mdd_one(mddManager));

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

    /* Restore the old temporary careset */
    mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo));
    AbsVerificationInfoSetTmpCareSet(absInfo, oldTmpCareSet);
    
    /* Check for trivial cases */
    if (mdd_is_tautology(AbsVertexReadSat(subFormula), 0) ||
        mdd_is_tautology(AbsVertexReadSat(subFormula), 1)) {
      AbsVertexSetSat(vertexPtr, mdd_dup(AbsVertexReadSat(subFormula)));
      AbsVertexSetLocalApprox(vertexPtr, FALSE);
      AbsVertexSetGlobalApprox(vertexPtr, 
                               AbsVertexReadGlobalApprox(subFormula));
      mdd_free(careSet);
      return;
    }

    /* if (AbsOptionsReadMinimizeIterate(options)){ */
    if (FALSE){
      minimizedSet = bdd_minimize(AbsVertexReadSat(subFormula),
                                  AbsVerificationInfoReadCareSet(absInfo));
    }
    else {
      minimizedSet = mdd_dup(AbsVertexReadSat(subFormula));
    }
      
    /* Look up in the cache if the result has been previously computed */
    if (AbsVertexReadSolutions(vertexPtr) != NIL(st_table)) {
      mdd_t   *unit;
      boolean localFlag;
      boolean exactness;
      
      exactness = AbsOptionsReadExact(options);
      if (AbsEvalCacheLookup(AbsVertexReadSolutions(vertexPtr),
                             minimizedSet, careSet, !exactness,
                             &unit, &localFlag)) {

        /* Set the sat */
        AbsVertexSetSat(vertexPtr, mdd_dup(unit));

        /* Set the approximation flags */
        AbsVertexSetLocalApprox(vertexPtr, localFlag & !exactness);
        AbsVertexSetGlobalApprox(vertexPtr, 
                                 AbsVertexReadGlobalApprox(subFormula) || 
                                 AbsVertexReadLocalApprox(vertexPtr));
        /* Increase the number of times the result has been used */
        AbsVertexReadServed(vertexPtr)++;
        
        mdd_free(careSet);
        mdd_free(minimizedSet);
        return;
      }
    }
    else {
      /* Initialize the cache */
      AbsVertexSetSolutions(vertexPtr, st_init_table(st_ptrcmp, st_ptrhash));
    }

    /* Effectively compute preImage */
    if (!AbsOptionsReadExact(options)) {
      if (AbsVertexReadPolarity(vertexPtr)) {
        if (AbsOptionsReadPartApprox(options)) {
          result = OverApproximatePreImageWithSubFSM(absInfo, minimizedSet, 
                                                     minimizedSet, careSet);
        }
        else {
          result = OverApproximatePreImageWithBddSubsetting(absInfo, 
                                                            minimizedSet, 
                                                            minimizedSet, 
                                                            careSet);
        }
        AbsVertexSetLocalApprox(vertexPtr, TRUE);
      }
      else {
        result = UnderApproximatePreImageWithBddSubsetting(absInfo, 
                                                           minimizedSet, 
                                                           minimizedSet,
                                                           careSet);
        AbsVertexSetLocalApprox(vertexPtr, TRUE);
      }
      AbsStatsReadApproxPreImage(AbsVerificationInfoReadStats(absInfo))++;
    }
    else {
      Fsm_Fsm_t       *system;
      Img_ImageInfo_t *imageInfo;
      long            cpuTime;

      system = AbsVerificationInfoReadFsm(absInfo);
      imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 0);
      cpuTime = util_cpu_time();
      result = Img_ImageInfoComputeBwdWithDomainVars(imageInfo, minimizedSet,
                                                     minimizedSet,careSet);
      AbsStatsReadPreImageCpuTime(stats)+= util_cpu_time() - cpuTime;

      AbsStatsReadExactPreImage(stats)++;
      AbsVertexSetLocalApprox(vertexPtr, FALSE);
    }
    AbsVertexSetSat(vertexPtr, result);

    /* Set the value in the cache */
    AbsEvalCacheInsert(AbsVertexReadSolutions(vertexPtr),
                       minimizedSet, AbsVertexReadSat(vertexPtr), careSet,
                       AbsVertexReadLocalApprox(vertexPtr), FALSE);
    AbsStatsReadPreImageCacheEntries(stats)++;
    mdd_free(minimizedSet);

    /* Set the approximation flags */
    AbsVertexSetGlobalApprox(vertexPtr, 
                             AbsVertexReadGlobalApprox(subFormula) || 
                             AbsVertexReadLocalApprox(vertexPtr));

    /* Print the number of states in the on set of Sat */
    if (verbosity & ABS_VB_TSAT) {
      Fsm_Fsm_t *globalSystem;
      array_t *domainVars;
      mdd_t *intersection;
      
      intersection = mdd_and(AbsVertexReadSat(vertexPtr), careSet, 1, 1);
      
      globalSystem = AbsVerificationInfoReadFsm(absInfo);
      domainVars = Fsm_FsmReadPresentStateVars(globalSystem);
      (void) fprintf(vis_stdout, "ABS: %.0f States satisfy the EX formula.\n",
                     mdd_count_onset(AbsVerificationInfoReadMddManager(absInfo),
                                     intersection, domainVars));
      mdd_free(intersection);
    }
    mdd_free(careSet);
  }
  

  /* Increase the number of times the result has been used */
  AbsVertexReadServed(vertexPtr)++;

  return;
} /* End of EvaluatePreImage */

static mdd_t *
OverApproximatePreImageWithSubFSM(
  Abs_VerificationInfo_t *absInfo,
  mdd_t *lowerBound,
  mdd_t *upperBound,
  mdd_t *careSet)
{
  Fsm_Fsm_t       *system;
  Img_ImageInfo_t *imageInfo;
  mdd_t           *result;
  long            cpuTime;

  /* Initialize some variables */
  system = AbsVerificationInfoReadApproxFsm(absInfo);

  if (system == NIL(Fsm_Fsm_t)) {
    system = AbsVerificationInfoReadFsm(absInfo);
  }

  /* Obtain the image info */
  imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 0);

  cpuTime = util_cpu_time();
  result = Img_ImageInfoComputeBwdWithDomainVars(imageInfo, lowerBound,
                                                 upperBound, careSet);
  AbsStatsReadAppPreCpuTime(AbsVerificationInfoReadStats(absInfo))+= 
    util_cpu_time() - cpuTime;

  return result;
} /* End of OverApproximatePreImageWithSubFSM */


static mdd_t *
OverApproximatePreImageWithBddSubsetting(
  Abs_VerificationInfo_t *absInfo,
  mdd_t *lowerBound,
  mdd_t *upperBound,
  mdd_t *careSet)
{
  Fsm_Fsm_t       *system;
  Img_ImageInfo_t *imageInfo;
  mdd_t           *superSet;
  mdd_t           *result;
  long            cpuTime;

  /* Initialize some variables */
  system = AbsVerificationInfoReadFsm(absInfo);

  /* Compute the subset of the restriction set */
  superSet = bdd_approx_remap_ua(lowerBound,BDD_OVER_APPROX,
                          AbsVerificationInfoReadNumStateVars(absInfo), 
                          0,1);
  
  /* Obtain the image info */
  imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 0);

  cpuTime = util_cpu_time();
  result = Img_ImageInfoComputeBwdWithDomainVars(imageInfo, superSet,
                                                 superSet, careSet);
  AbsStatsReadAppPreCpuTime(AbsVerificationInfoReadStats(absInfo))+= 
    util_cpu_time() - cpuTime;

  mdd_free(superSet);

  return result;
} /* End of OverApproximatePreImageWithBddSubsetting */

static mdd_t *
UnderApproximatePreImageWithBddSubsetting(
  Abs_VerificationInfo_t *absInfo,
  mdd_t *lowerBound,
  mdd_t *upperBound,
  mdd_t *careSet)
{
  Fsm_Fsm_t       *system;
  Img_ImageInfo_t *imageInfo;
  mdd_t           *subSet;
  mdd_t           *result;
  long            cpuTime;

  /* Initialize some variables */
  system = AbsVerificationInfoReadFsm(absInfo);

  /* Compute the subset of the restriction set */
  subSet = bdd_approx_remap_ua(lowerBound, BDD_UNDER_APPROX,
                      AbsVerificationInfoReadNumStateVars(absInfo),
                      0,1);

  /* Obtain the image info */
  imageInfo = Fsm_FsmReadOrCreateImageInfo(system, 1, 0);

  cpuTime = util_cpu_time();
  result = Img_ImageInfoComputeBwdWithDomainVars(imageInfo, subSet, subSet, 
                                                 careSet);
  AbsStatsReadAppPreCpuTime(AbsVerificationInfoReadStats(absInfo))+= 
    util_cpu_time() - cpuTime;

  mdd_free(subSet);

  return result;
} /* End of UnderApproximatePreImageWithBddSubsetting */