src/puresat/puresatAig.c

Go to the documentation of this file.

#include "maigInt.h"
#include "baig.h"
#include "ntk.h"
#include "puresatInt.h"
/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

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


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


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

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

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


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


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

void
PureSat_unconnectOutput(
   bAig_Manager_t *manager,
   bAigEdge_t from,
   bAigEdge_t to)
{
   bAigEdge_t cur, *pfan, *newfan;
   int i, nfan,find=0;

  from = bAig_NonInvertedEdge(from);
  to = bAig_NonInvertedEdge(to);

  pfan = (bAigEdge_t *)fanout(from);
  nfan = nFanout(from);
  newfan = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*(nfan));
  for(i=0; i<nfan; i++) {
    cur = pfan[i];
    cur = cur >> 1;
    cur = bAig_NonInvertedEdge(cur);
    if(cur == to) {
      find = 1;
      memcpy(newfan, pfan, sizeof(bAigEdge_t)*i);
      memcpy(&(newfan[i]), &(pfan[i+1]), sizeof(bAigEdge_t)*(nfan-i-1));
      newfan[nfan-1] = 0;

      fanout(from) = (bAigEdge_t)newfan;


      free(pfan);
      nFanout(from) = nfan-1;
      break;
    }
  }
  assert(find);
}


void
PureSat_connectOutput(
   bAig_Manager_t *manager,
   bAigEdge_t from,
   bAigEdge_t to,
   int inputIndex)
{
  bAigEdge_t *pfan;
  bAigEdge_t nfan;

  to = bAig_NonInvertedEdge(to);
  pfan = (bAigEdge_t *)fanout(from);
  nfan = nFanout(from);
  if(nfan == 0) pfan = malloc((sizeof(bAigEdge_t)*2));
  else          pfan = realloc(pfan, sizeof(bAigEdge_t)*(nfan+2));
  to += bAig_IsInverted(from);
  to = to << 1;
  to += inputIndex;
  pfan[nfan++] = to;
  pfan[nfan] = 0;
  fanout(from) = (bAigEdge_t)pfan;
  nFanout(from) = nfan;
}


bAigEdge_t
PureSat_HashTableLookup(
  bAig_Manager_t *manager,
  bAigEdge_t  node1,
  bAigEdge_t  node2)
{
  bAigEdge_t key = HashTableFunction(node1, node2);
  bAigEdge_t node;

  node = manager->HashTableArray[manager->class_][key];
  if  (node == bAig_NULL) {
    return bAig_NULL;
  }
  else{
    while ( (rightChild(bAig_NonInvertedEdge(node)) != node2) ||
            (leftChild(bAig_NonInvertedEdge(node))  != node1)) {

      if (next(bAig_NonInvertedEdge(node)) == bAig_NULL){
        return(bAig_NULL);
      }
      node = next(bAig_NonInvertedEdge(node)); /* Get the next Node */
    } /* While loop */
    return(node);

  } /* If Then Else */

} /* End of HashTableLookup() */


int
PureSat_HashTableAdd(
  bAig_Manager_t   *manager,
  bAigEdge_t  nodeIndexParent,
  bAigEdge_t  nodeIndex1,
  bAigEdge_t  nodeIndex2)
{
  bAigEdge_t key = HashTableFunction(nodeIndex1, nodeIndex2);
  bAigEdge_t nodeIndex;
  bAigEdge_t node;

  nodeIndex = manager->HashTableArray[manager->class_][key];
  if  (nodeIndex == bAig_NULL) {
    manager->HashTableArray[manager->class_][key] = nodeIndexParent;
    return TRUE;
  }
  else{
    node = nodeIndex;
    nodeIndex = next(bAig_NonInvertedEdge(nodeIndex));  /* Get the Node */
    while (nodeIndex != bAig_NULL) {
      node = nodeIndex;
      nodeIndex = next(bAig_NonInvertedEdge(nodeIndex));
    }
    next(bAig_NonInvertedEdge(node)) = nodeIndexParent;
    return TRUE;
  }

}



bAigEdge_t
PureSat_CreateAndNode(
   bAig_Manager_t  *manager,
   bAigEdge_t node1,
   bAigEdge_t node2)
{

  bAigEdge_t varIndex;
  char       *name = NIL(char);
  char       *node1Str = util_inttostr(node1);
  char       *node2Str = util_inttostr(node2);
  long class_ = manager->class_;

  name = util_strcat4("Nd", node1Str,"_", node2Str);
  while (st_lookup(manager->SymbolTableArray[class_], name, &varIndex)){
    fprintf(vis_stdout, "Find redundant node at %ld %ld\n", node1, node2);
    name = util_strcat3(name, node1Str, node2Str);
  }
  FREE(node1Str);
  FREE(node2Str);
  varIndex = bAig_CreateNode(manager, node1, node2);
  if (varIndex == bAig_NULL){
    FREE(name);
    return (varIndex);
  }
  /* Insert the varaible in the Symbol Table */
  st_insert(manager->SymbolTableArray[class_], name, (char*) (long) varIndex);
  manager->nameList[bAigNodeID(varIndex)] = name;

  return(varIndex);

}


bAigEdge_t
PureSat_And2(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{
  bAigEdge_t newNodeIndex;

    newNodeIndex = PureSat_CreateAndNode(manager, nodeIndex1, nodeIndex2) ;

    PureSat_HashTableAdd(manager, newNodeIndex, nodeIndex1, nodeIndex2);
    PureSat_connectOutput(manager, nodeIndex1, newNodeIndex, 0);
    PureSat_connectOutput(manager, nodeIndex2, newNodeIndex, 1);

  return newNodeIndex;

}


bAigEdge_t
PureSat_And3(
           bAig_Manager_t *manager,
           bAigEdge_t l,
           bAigEdge_t r)
{
  int caseIndex, caseSig;
  bAigEdge_t rl, rr;

  rl = leftChild(r);
  rr = rightChild(r);

  caseIndex = 0; /* (a)(b c) */
  if(bAigCompareNode(l, rl)) {
    caseIndex = 1; /* (a)(a b) */
  }
  else if(bAigCompareNode(l, rr)) {
    caseIndex = 2; /* (a)(b a) */
  }

  caseSig = 0;
  if(bAig_IsInverted(l))  caseSig += 8;
  if(bAig_IsInverted(rl)) caseSig += 4;
  if(bAig_IsInverted(rr)) caseSig += 2;
  if(bAig_IsInverted(r))  caseSig += 1;
  if(caseIndex == 0) {
    return(PureSat_And2(manager, l, r));
  }
  else if(caseIndex == 1) {
    switch(caseSig) {
        case 2 :
        case 0 :
        case 14 :
        case 12 :
      return(r);
        case 10 :
        case 8 :
        case 6 :
        case 4 :
      return(bAig_Zero);
        case 3 :
        case 1 :
        case 15 :
        case 13 :
      return(PureSat_And(manager, rl, bAig_Not(rr)));
        case 11 :
        case 9 :
        case 7 :
        case 5 :
      return(l);
    }
  }
  else if(caseIndex == 2) {
    switch(caseSig) {
        case 4 :
        case 0 :
        case 14 :
        case 10 :
      return(r);
        case 12 :
        case 8 :
        case 6 :
        case 2 :
      return(bAig_Zero);
        case 5 :
        case 1 :
        case 15 :
        case 11 :
      return(PureSat_And(manager, bAig_Not(rl), rr));
        case 13 :
        case 9 :
        case 7 :
        case 3 :
      return(l);
    }
  }
  return(0);
}


bAigEdge_t
PureSat_And4(
           bAig_Manager_t *manager,
           bAigEdge_t l,
           bAigEdge_t r)
{
  int caseIndex, caseSig;
  bAigEdge_t ll, lr, rl, rr;
  bAigEdge_t t1, t2;

  ll = leftChild(l);
  lr = rightChild(l);
  rl = leftChild(r);
  rr = rightChild(r);

  if(bAigCompareNode(l, rl) ||
     bAigCompareNode(l, rr)) {
    return(PureSat_And3(manager, l, r));
  }
  else if(bAigCompareNode(r, ll) ||
     bAigCompareNode(r, lr)) {
    return(PureSat_And3(manager, r, l));
  }

  if(ll > lr+1) bAigSwap(ll, lr);
  if(rl > rr+1) bAigSwap(rl, rr);

  caseIndex = 0; /* (a b)(c d) */
  if(bAigCompareNode(ll, rl)) {
    if(bAigCompareNode(lr, rr)) {
      caseIndex = 4; /* (a b) (a b) */
    }
    else {
      caseIndex = 1; /* (a b) (a c) */
      if(lr > rr+1) {
        bAigSwap(ll, rl);
        bAigSwap(lr, rr);
        bAigSwap(l, r);
      }
    }
  }
  else if(bAigCompareNode(lr, rl)) {
    caseIndex = 2; /* (b a)(a c) */
  }
  else if(bAigCompareNode(lr, rr)) {
    caseIndex = 3; /* (b a)(c a) */
    if(ll > rl+1) {
      bAigSwap(ll, rl);
      bAigSwap(lr, rr);
      bAigSwap(l, r);
    }
  }
  else if(bAigCompareNode(ll, rr)) {
    /* (a b)(c a)  */
    bAigSwap(ll, rl);
    bAigSwap(lr, rr);
    bAigSwap(l, r);
    caseIndex = 2; /* (c a )(a b) because of c < b */
  }

  caseSig = 0;
  if(bAig_IsInverted(ll)) caseSig += 32;
  if(bAig_IsInverted(lr)) caseSig += 16;
  if(bAig_IsInverted(l))  caseSig += 8;
  if(bAig_IsInverted(rl)) caseSig += 4;
  if(bAig_IsInverted(rr)) caseSig += 2;
  if(bAig_IsInverted(r))  caseSig += 1;

  if(caseIndex == 0) {
    return(PureSat_And2(manager, l, r));
  }
  else if(caseIndex == 1) {
    switch(caseSig) {
        case 19 :
        case 17 :
        case 3 :
        case 1 :
        case 55 :
        case 53 :
        case 39 :
        case 37 :
      t1 = PureSat_And(manager, lr, bAig_Not(rr));
      t2 = PureSat_And(manager, ll, t1);
      return(t2);
        case 18 :
        case 16 :
        case 2 :
        case 0 :
        case 54 :
        case 52 :
        case 38 :
        case 36 :
      t1 = PureSat_And(manager, lr, rr);
      t2 = PureSat_And(manager, ll, t1);
      return(t2);
        case 26 :
        case 24 :
        case 10 :
        case 8 :
        case 62 :
        case 60 :
        case 46 :
        case 44 :
      t1 = PureSat_And(manager, bAig_Not(lr), rr);
      t2 = PureSat_And(manager, ll, t1);
      return(t2);
        case 61 :
        case 27 :
        case 25 :
        case 11 :
        case 63 :
        case 47 :
        case 9 :
        case 45 :
      t1 = PureSat_And(manager, bAig_Not(lr), bAig_Not(rr));
      t2 = PureSat_Or(manager, bAig_Not(ll), t1);
      return(t2);
        case 23 :
        case 21 :
        case 7 :
        case 5 :
        case 51 :
        case 49 :
        case 35 :
        case 33 :
      return(l);
        case 30 :
        case 28 :
        case 14 :
        case 12 :
        case 58 :
        case 56 :
        case 42 :
        case 40 :
      return(r);
        case 22 :
        case 20 :
        case 6 :
        case 4 :
        case 50 :
        case 48 :
        case 34 :
        case 32 :
      return(bAig_Zero);
        case 31 :
        case 29 :
        case 15 :
        case 13 :
        case 59 :
        case 57 :
        case 43 :
        case 41 :
      t1 = PureSat_And2(manager, l, r);
      return(t1);
    }
  }
  else if(caseIndex == 2) {
    switch(caseSig) {
        case 35 :
        case 33 :
        case 3 :
        case 1 :
        case 55 :
        case 53 :
        case 23 :
        case 21 :
      t1 = PureSat_And(manager, lr, bAig_Not(rr));
      t2 = PureSat_And(manager, ll, t1);
      return(t2);
        case 34 :
        case 32 :
        case 2 :
        case 0 :
        case 54 :
        case 52 :
        case 22 :
        case 20 :
      t1 = PureSat_And(manager, lr, rr);
      t2 = PureSat_And(manager, ll, t1);
      return(t2);
        case 42 :
        case 40 :
        case 10 :
        case 8 :
        case 62 :
        case 60 :
        case 30 :
        case 28 :
      t1 = PureSat_And(manager, lr, rr);
      t2 = PureSat_And(manager, bAig_Not(ll), t1);
      return(t2);
        case 43 :
        case 41 :
        case 11 :
        case 9 :
        case 63 :
        case 61 :
        case 31 :
        case 29 :
      t1 = PureSat_And(manager, bAig_Not(ll), bAig_Not(rr));
      t2 = PureSat_Or(manager, bAig_Not(lr), t1);
      return(t2);
        case 39 :
        case 37 :
        case 7 :
        case 5 :
        case 51 :
        case 49 :
        case 19 :
        case 17 :
      return(l);
        case 46 :
        case 44 :
        case 14 :
        case 12 :
        case 58 :
        case 56 :
        case 26 :
        case 24 :
      return(r);
        case 38 :
        case 36 :
        case 6 :
        case 4 :
        case 50 :
        case 48 :
        case 18 :
        case 16 :
      return(bAig_Zero);
        case 45 :
        case 15 :
        case 13 :
        case 59 :
        case 57 :
        case 47 :
        case 27 :
        case 25 :
      t1 = PureSat_And2(manager, l, r);
      return(t1);
    }
  }
  else if(caseIndex == 3) {
    switch(caseSig) {
        case 37 :
        case 33 :
        case 5 :
        case 1 :
        case 55 :
        case 51 :
        case 23 :
        case 19 :
      t1 = PureSat_And(manager, bAig_Not(rl), lr);
      t2 = PureSat_And(manager, ll, t1);
      return(t2);
        case 36 :
        case 32 :
        case 4 :
        case 0 :
        case 54 :
        case 50 :
        case 22 :
        case 18 :
      t1 = PureSat_And(manager, rl, lr);
      t2 = PureSat_And(manager, ll, t1);
      return(t2);
        case 44 :
        case 40 :
        case 12 :
        case 8 :
        case 62 :
        case 58 :
        case 30 :
        case 26 :
      t1 = PureSat_And(manager, rl, lr);
      t2 = PureSat_And(manager, bAig_Not(ll), t1);
      return(t2);
        case 45 :
        case 41 :
        case 13 :
        case 9 :
        case 63 :
        case 59 :
        case 31 :
        case 27 :
      t1 = PureSat_And(manager, bAig_Not(ll), bAig_Not(rl));
      t2 = PureSat_Or(manager, bAig_Not(lr), t1);
      return(t2);
        case 39 :
        case 35 :
        case 7 :
        case 3 :
        case 53 :
        case 49 :
        case 21 :
        case 17 :
      return(l);
        case 46 :
        case 42 :
        case 14 :
        case 10 :
        case 60 :
        case 56 :
        case 28 :
        case 24 :
      return(r);
        case 38 :
        case 34 :
        case 6 :
        case 2 :
        case 52 :
        case 48 :
        case 20 :
        case 16 :
      return(bAig_Zero);
        case 47 :
        case 43 :
        case 15 :
        case 11 :
        case 61 :
        case 57 :
        case 29 :
        case 25 :
      t1 = PureSat_And2(manager, l, r);
      return(t1);
    }
  }
  else if(caseIndex == 4) {
    switch(caseSig) {
        case 22 :
        case 20 :
        case 6 :
        case 4 :
        case 50 :
        case 48 :
        case 34 :
        case 32 :
        case 2 :
        case 16 :
        case 52 :
        case 1 :
        case 8 :
        case 19 :
        case 26 :
        case 37 :
        case 44 :
        case 38 :
        case 55 :
        case 62 :
      return(bAig_Zero);
        case 0 :
        case 18 :
        case 36 :
        case 54 :
        case 9 :
        case 27 :
        case 45 :
        case 63 :
        case 5 :
        case 23 :
        case 33 :
        case 51 :
        case 3 :
        case 17 :
        case 49 :
        case 7 :
        case 35 :
        case 21 :
        case 39 :
        case 53 :
      return(l);
        case 40 :
        case 58 :
        case 12 :
        case 30 :
        case 24 :
        case 10 :
        case 14 :
        case 56 :
        case 28 :
        case 42 :
        case 60 :
        case 46 :
      return(r);
        case 11 :
        case 47 :
        case 25 :
        case 61 :
      return(bAig_Not(ll));
        case 41 :
        case 59 :
        case 13 :
        case 31 :
      return(bAig_Not(lr));
        case 15 :
      t1 = PureSat_And(manager, ll, bAig_Not(lr));
      t2 = PureSat_And(manager, bAig_Not(ll), lr);
      return(bAig_Not(PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
        case 57 :
      t1 = PureSat_And(manager, rl, bAig_Not(rr));
      t2 = PureSat_And(manager, bAig_Not(rl), rr);
      return(bAig_Not(PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
        case 29 :
      t1 = PureSat_And(manager, ll, lr);
      t2 = PureSat_And(manager, bAig_Not(ll), bAig_Not(lr));
      return((PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
        case 43 :
      t1 = PureSat_And(manager, rl, rr);
      t2 = PureSat_And(manager, bAig_Not(rl), bAig_Not(rr));
      return((PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
    }
  }
  return(0);
}



int PureSat_Test2LevelMini(bAig_Manager_t *manager,
                           bAigEdge_t l,
                           bAigEdge_t r)
{
  int class_ = bAig_Class(l);
  bAigEdge_t ll,lr,rl,rr;

  if(!manager->test2LevelMini)
    return 0;

  if(class_!= bAig_Class(r) || class_ != manager->class_)
    return 0;

  ll = leftChild(l);
  if(ll!=bAig_NULL && class_!=bAig_Class(ll))
    return 0;
  lr = rightChild(l);
  if(lr!=bAig_NULL && class_!=bAig_Class(lr))
    return 0;
  rl = leftChild(r);
  if(rl!=bAig_NULL && class_!=bAig_Class(rl))
    return 0;
  rr = rightChild(r);
  if(rr!=bAig_NULL && class_!=bAig_Class(rr))
    return 0;

  return 1;
}

bAigEdge_t
PureSat_And(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{

  bAigEdge_t newNodeIndex;

  nodeIndex1 = bAig_GetCanonical(manager, nodeIndex1);
  nodeIndex2 = bAig_GetCanonical(manager, nodeIndex2);

  newNodeIndex = nodeIndex1;     /* The left node has the smallest index */
  if (bAig_NonInvertedEdge(nodeIndex1) > bAig_NonInvertedEdge(nodeIndex2)){
    nodeIndex1 = nodeIndex2;
    nodeIndex2 = newNodeIndex;
  }

  if ( nodeIndex2 == bAig_Zero ) {
    return bAig_Zero;
  }
  if ( nodeIndex1 == bAig_Zero ) {
    return bAig_Zero;
  }
  if ( nodeIndex2 == bAig_One ) {
    return nodeIndex1;
  }
  if ( nodeIndex1 == bAig_One ) {
    return nodeIndex2;
  }
  if ( nodeIndex1 == nodeIndex2 ) {
    return nodeIndex1;
  }
  if ( nodeIndex1 == bAig_Not(nodeIndex2) ) {
    return bAig_Zero;
  }

  /* Look for the new node in the Hash table */
  newNodeIndex = PureSat_HashTableLookup(manager, nodeIndex1, nodeIndex2);


  if (newNodeIndex == bAig_NULL){
    if(!PureSat_Test2LevelMini(manager,nodeIndex1,nodeIndex2)){
      newNodeIndex = PureSat_And2(manager, nodeIndex1, nodeIndex2);
      return newNodeIndex;
    }

    if(bAigIsVar(manager, nodeIndex1) && bAigIsVar(manager, nodeIndex2))
      newNodeIndex = PureSat_And2(manager, nodeIndex1, nodeIndex2);
    else if(bAigIsVar(manager, nodeIndex1))
      newNodeIndex = PureSat_And3(manager, nodeIndex1, nodeIndex2);
    else if(bAigIsVar(manager, nodeIndex2))
      newNodeIndex = PureSat_And3(manager, nodeIndex2, nodeIndex1);
    else {
      newNodeIndex = PureSat_And4(manager, nodeIndex1, nodeIndex2);
    }
  }

  return newNodeIndex;

}


bAigEdge_t
PureSat_Or(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{
  return ( bAig_Not(PureSat_And(manager,  bAig_Not(nodeIndex1),  bAig_Not(nodeIndex2))));
}


bAigEdge_t
PureSat_Xor(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{
 return PureSat_Or(manager,
            PureSat_And(manager, nodeIndex1, bAig_Not(nodeIndex2)),
            PureSat_And(manager, bAig_Not(nodeIndex1),nodeIndex2)
        );
}


bAigEdge_t
PureSat_Eq(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{
 return bAig_Not(
            PureSat_Xor(manager, nodeIndex1, nodeIndex2)
            );
}


bAigEdge_t
PureSat_Then(
   bAig_Manager_t *manager,
   bAigEdge_t nodeIndex1,
   bAigEdge_t nodeIndex2)
{
 return PureSat_Or(manager,
                bAig_Not(nodeIndex1),
                nodeIndex2);
}



bAigEdge_t
PureSat_CreateVarNode(
   bAig_Manager_t  *manager,
   nameType_t      *name)
{

  bAigEdge_t varIndex;
  int class_ = manager->class_;


  if (!st_lookup(manager->SymbolTableArray[class_], name, &varIndex)){
    varIndex = bAig_CreateNode(manager, bAig_NULL, bAig_NULL);
    if (varIndex == bAig_NULL){
      return (varIndex);
    }
    /* Insert the varaible in the Symbol Table */
    st_insert(manager->SymbolTableArray[class_],
              name, (char*) (long) varIndex);
    manager->nameList[bAigNodeID(varIndex)] = name;
    return(varIndex);
  }
  else {
    return (varIndex);
  }
}