src/restr/restrCProj.c

Go to the documentation of this file.

#include "restrInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

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


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


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


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

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

bdd_node *
RestrMinimizeFsmByCProj(
  bdd_manager   *ddManager,
  bdd_node      *equivRel,
  bdd_node      *originalTR,
  bdd_node      *initBdd,
  bdd_node      **xVars,
  bdd_node      **yVars,
  bdd_node      **uVars,
  bdd_node      **vVars,
  bdd_node      **piVars,
  int           nVars,
  int           nPi,
  array_t       **outBdds,
  bdd_node      **newInit)

{
  bdd_node *resultYV, *temp, *temp1, *temp2;
  bdd_node *result, *resultXU;
  bdd_node *xCube, *yCube;
  bdd_node *oneInitState;
  array_t *newOutBdds;
  int i;

  /* Select one state from the set of initial states. This is redundant in case
     of circuits described in blif format.*/
  oneInitState = bdd_bdd_pick_one_minterm(ddManager,initBdd,xVars,nVars);
  bdd_ref(oneInitState);

  temp = bdd_bdd_swap_variables(ddManager,oneInitState,xVars,vVars,nVars);
  bdd_ref(temp);
  bdd_recursive_deref(ddManager,oneInitState);

  /* Select a representative for each equivalence class. The vVars encode the
   * representative for each class. resultYV has yVars and vVars in its
   * support. equivRel is a function of yVars and vVars.
   */
  resultYV = bdd_bdd_cprojection(ddManager, equivRel, temp);
  bdd_ref(resultYV);
  bdd_recursive_deref(ddManager,temp);

  temp = bdd_bdd_swap_variables(ddManager,resultYV,yVars,xVars,nVars);
  bdd_ref(temp);
  resultXU = bdd_bdd_swap_variables(ddManager,temp,vVars,uVars,nVars);
  bdd_ref(resultXU);
  bdd_recursive_deref(ddManager, temp);

  /* Change the initBdd accordingly
   * initBdd^{new} = [\exists_x (initBdd(x) * result(x,u))]_{u=x}
   */
  xCube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars);
  bdd_ref(xCube);
  bdd_ref(temp1 = bdd_bdd_and_abstract(ddManager,initBdd,resultXU,
                                       xCube));
  bdd_ref(*newInit = bdd_bdd_swap_variables(ddManager,temp1,uVars,
                                            xVars,nVars));
  bdd_recursive_deref(ddManager,temp1);

  /* compute the new TR.
   * TR^{new}(x,w,y) = 
   *    [\exists_{xy}(result(x,u) * TR(x,w,y) * result(y,v))]_{u=x,v=y}
   * result is the new restructured/minimized TR.
   */
  bdd_ref(yCube = bdd_bdd_compute_cube(ddManager,yVars,NIL(int),nVars));
  bdd_ref(temp = bdd_bdd_and_abstract(ddManager,resultYV,originalTR,yCube));
  bdd_recursive_deref(ddManager,resultYV);
  bdd_recursive_deref(ddManager,yCube);

  bdd_ref(result = bdd_bdd_and_abstract(ddManager,temp,resultXU,xCube));
  bdd_recursive_deref(ddManager,temp);

  bdd_ref(temp = bdd_bdd_swap_variables(ddManager,result,uVars,
                                        xVars,nVars));
  bdd_recursive_deref(ddManager,result);
  bdd_ref(result = bdd_bdd_swap_variables(ddManager,temp,vVars,
                                          yVars,nVars));
  bdd_recursive_deref(ddManager,temp);

  /* Change the outputs accordingly
   * lambda^{new}_i(x,w) = [\exists_x (lambda_i(x,w) * result(x,u))]_{u=x}
   *
   * lambda_i(x,w) is the ith primary output.
   */
  newOutBdds = array_alloc(bdd_node *,0);
  arrayForEachItem(bdd_node *,*outBdds,i,temp) {
    temp1 = bdd_bdd_and_abstract(ddManager,temp,resultXU,xCube);
    bdd_ref(temp1);
    temp2 = bdd_bdd_swap_variables(ddManager,temp1,uVars,xVars,nVars);
    bdd_ref(temp2);
    bdd_recursive_deref(ddManager,temp1);
    array_insert_last(bdd_node *,newOutBdds,temp2);
  }
  bdd_recursive_deref(ddManager, xCube);
  bdd_recursive_deref(ddManager,resultXU);

#ifdef RESTR_DIAG
  {
    int flag1,flag2;

    (void) fprintf(vis_stdout,"Old transition relation ...\n");
    flag1 = RestrTestIsDeterministic(ddManager,originalTR,initBdd,
                                     xVars,yVars,nVars);
    (void) fprintf(vis_stdout,"New transition relation ...\n");
    flag2 = RestrTestIsDeterministic(ddManager,result,*newInit,
                                     xVars,yVars,nVars);
  }
#endif
  
  /* Delete the old array */
  arrayForEachItem(bdd_node *,*outBdds,i,temp) {
    bdd_recursive_deref(ddManager,temp);
  }
  array_free(*outBdds);
  *outBdds = newOutBdds;
  
  return result;

}

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