bdd.c

Go to the documentation of this file.

extern "C" {

#include "tarski.h"

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


bdd_manager *bddMgr=0;
st_table *nodeToBdd= ( st_table * ) 0;  // mapping from forumla nodes to bdds
st_table *indexToName= ( st_table * ) 0;  // mapping from forumla nodes to bdds

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

bdd_t *
nodeComputeBdd(
  F aNode )
{
  if (aNode.raw == NIL( Fnode ) ) {
    return NIL( bdd_t );
  }
  assert( node_test_is_boolean( aNode.raw ) );

  bdd_t *leftBdd;
  bdd_t *rightBdd;
  bdd_t *result;
  int aId;

  if ( nodeToBdd == NIL( st_table ) ) {
    nodeToBdd = st_init_table( (int (*)()) node_cmp, (int (*)()) node_hash );
  }
  if ( indexToName == NIL( st_table ) ) {
    indexToName = st_init_table( (int (*)()) st_numcmp, (int (*)()) st_numhash );
  }
  if ( bddMgr == NIL( bdd_manager ) ) {
    bddMgr = bdd_start( 0 );
    bdd_dynamic_reordering( bddMgr, BDD_REORDER_SIFT); // turn on variable reordering
    bdd_set_gc_mode(bddMgr, 0); // turn on garbage collection
  }
  if ( st_lookup( nodeToBdd, (char *) aNode.raw, (char **) & result ) ) {
    return bdd_dup( result );
  }
  if ( ( aNode.type() == BooleanPI_c ) ||
       ( aNode.type() == BooleanReg_c ) ) {
    aId = bdd_num_vars( bddMgr );
    result = bdd_get_variable( bddMgr, aId );
    st_insert( indexToName, (char *) aId, (char *) aNode.lchild() );
  }
  else {
    F leftNode;
    leftNode.raw = aNode.lchild();
    F rightNode;
    rightNode.raw = aNode.rchild();
    leftBdd = nodeComputeBdd( leftNode );
    rightBdd = nodeComputeBdd( rightNode );
    switch ( aNode.type() ) {
      case And_c: result = bdd_and( leftBdd, rightBdd, 1, 1 ); break;
      case Or_c: result = bdd_or( leftBdd, rightBdd, 1, 1 ); break;
      case Iff_c: result = bdd_xnor( leftBdd, rightBdd ); break;
      case Not_c: result = bdd_not( leftBdd ); break;
      case TRUE_c: result = bdd_one( bddMgr ); break;
      case FALSE_c: result = bdd_zero( bddMgr ); break;
      default: printf("Bad type of node in nodeComputeBdd\n"); assert(0);
    }
    if ( leftBdd != NIL(bdd_t) ) bdd_free( leftBdd );
    if ( rightBdd != NIL(bdd_t) ) bdd_free( rightBdd );
  }
  printf("nodeComputeBdd is returning a bdd of size %d\n", bdd_size( result ) );
  st_insert( nodeToBdd, (char *) aNode.raw, (char *) result );
  return bdd_dup( result );
}


int
test_bdd()
{

  F fs = build_fs();
  return 1;

  st_table *fsSupport = nodeGetSupport( fs );
  st_generator *stGen;
  Fnode *aRawNode;

  cube aCube;
  aCube.nodeToValue = fsSupport;
  int i;
  for ( i = 0 ; i < 100; i++ ) {
    st_foreach_item( fsSupport, stGen, ( char ** ) & aRawNode, ( char ** ) 0 ) {
      int val = rand() % 2;
      st_insert( fsSupport, (char *) aRawNode, (char *) ( val ) );
      // printf("%s is getting %d\n", (char *) aRawNode->lchild, val );
    }
    printf("Eval fs on aCube yields %d\n", fs( aCube ) );
  }

  return 0;

}


int 
bdd_print_dot(
  bdd_t *aBdd 
)
{
  printf("digraph  G {\nsize=\"7.5,10\";\n");

  st_table *processedTable = st_init_table( (int (*)()) bdd_cmp, (int (*)()) bdd_hash );

  bdd_print_recur( aBdd, processedTable );
  printf("\n}\n");

  return 1;
}



int 
bdd_print_recur(
 bdd_t *aBdd,
  st_table *processedTable
)
{
  if ( st_lookup( processedTable, (char *) aBdd, 0 ) ) {
    return 1;
  }
  int is_complemented;
  bdd_node *aNode = bdd_get_node( ( bdd_t * ) aBdd, & is_complemented);
  if ( is_complemented ) {
    aNode = (bdd_node *) ( (unsigned int) aNode ^ (unsigned int) 0x1 );
  }
  if ( bdd_is_tautology( aBdd, 0 ) ) { 
    printf("%u  [shape=polygon,sides=4,label=FALSE]\n", (unsigned int) aNode );
    st_insert( processedTable, (char *) aBdd, (char *) 0 );
    return 1;
  }
  if ( bdd_is_tautology( aBdd, 1 ) ) { 
    printf("%u  [shape=polygon,sides=4,label=TRUE]\n", (unsigned int) aNode );
    st_insert( processedTable, (char *) aBdd, (char *) 0 );
    return 1;
  }
 
  char *label;
  int index = bdd_top_var_id( aBdd );
  st_lookup( indexToName, (char *) index, (char **) & label );
  printf("%u [shape=ellipse,sides=4,label=\"%s\"]\n", (unsigned int) aNode, label );
  
  bdd_t *lBdd = bdd_else( aBdd );
  bdd_t *rBdd = bdd_then( aBdd );

  bdd_node *lNode = bdd_get_node( ( bdd_t * ) lBdd, & is_complemented);
  if ( is_complemented ) {
    lNode = (bdd_node *) ( (unsigned int) lNode ^ (unsigned int) 0x1 );
  }
  bdd_node *rNode = bdd_get_node( ( bdd_t * ) rBdd, & is_complemented);
  if ( is_complemented ) {
    rNode = (bdd_node *) ( (unsigned int) rNode ^ (unsigned int) 0x1 );
  }
  printf("%u -> %u [style=dotted];\n", (unsigned int) aNode, (unsigned int) lNode );
  printf("%u -> %u [style=solid];\n", (unsigned int) aNode, (unsigned int) rNode );

  bdd_print_recur( lBdd, processedTable );
  bdd_print_recur( rBdd, processedTable );

  st_insert( processedTable, (char *) aBdd, (char *) 0 );

  return 1;
}

  


int
bdd_cmp(
  char *aBdd,
  char *bBdd
)
{
  int is_complemented;
  bdd_node *aNode = bdd_get_node( ( bdd_t * ) aBdd, & is_complemented);
  if ( is_complemented ) {
    aNode = (bdd_node *) ( (unsigned int) aNode ^ (unsigned int) 0x1 );
  }
  bdd_node *bNode = bdd_get_node( ( bdd_t * ) bBdd, & is_complemented);
  if ( is_complemented ) {
    bNode = (bdd_node *) ( (unsigned int) bNode ^ (unsigned int) 0x1 );
  }
  int result = st_numcmp( (char*) aNode, (char*) bNode );
  return result;
                                                                                                 
}




int
bdd_hash(
  char *aBdd,
  int modulus
)
{
  int is_complemented;
  bdd_node *aNode = bdd_get_node( ( bdd_t *) aBdd, & is_complemented);
  if ( is_complemented ) {
    aNode = (bdd_node *) ( (unsigned int) aNode ^ (unsigned int) 0x1) ;
  }
  int result = st_numhash(  ( char *) aNode, modulus );
  return result;
}



cube::cube(){
  nodeToValue = st_init_table( (int (*)()) node_cmp, (int (*)()) node_hash );
}


cube::~cube(){
  // st_free_table( nodeToValue ); // problem - this frees the cube right away
                                   // even when we pass in something to a function
}


int 
cube::operator[]( F aNode ) {
  int result=-1;
  st_lookup( nodeToValue, ( char * ) aNode.raw, ( char **) & result );
  if ( result == -1 ) {
    printf("Failed to find node in cube support\n");
    assert(0);
  }
  assert( ( result == 1 ) || (result == 0 ) );
  return result;
}


void
cube::insert( F aNode, int value )
{
  assert( ( value == 1 ) || ( value == 0 ) );
  st_insert( nodeToValue, (char *) aNode.raw, (char *) value );
  return;
}


int 
F::operator()(
  cube aCube
)
{
  int leftValue, rightValue;
  F lchildWrapped;
  F rchildWrapped;
  lchildWrapped.raw = this->lchild();
  rchildWrapped.raw = this->rchild();
  assert( node_test_is_boolean( this->raw ) );

  if ( ( this->type() == BooleanPI_c ) ||
       ( this->type() == BooleanReg_c ) ) {
    return aCube[ *this ];
  }
  else if (  this->type() == TRUE_c ) {
    return 1;
  }
  else if (  this->type() == FALSE_c ) {
    return 0;
  }
  else {
    leftValue = lchildWrapped( aCube );
    if ( this->type() != Not_c ) {
      rightValue = rchildWrapped( aCube );
    }
    switch( this->type() ) {
      case Not_c: return !leftValue; break;
      case And_c: return leftValue && rightValue; break;
      case Or_c: return leftValue || rightValue; break;
      case Iff_c: return (leftValue==rightValue); break;
      default: printf("Panic, unknown type in eval op, bailing\n"); assert(0);
    }
  }
  assert(0);
  return -1; // never get here
}
    
} // extern "C"

---