src/sat/fraig/fraigNode.c File Reference

#include "fraigInt.h"
Include dependency graph for fraigNode.c:

Go to the source code of this file.

Defines

#define Fraig_NodeIsSimComplement(p)   (Fraig_IsComplement(p)? !(Fraig_Regular(p)->fInv) : (p)->fInv)

Functions

Fraig_Node_t * Fraig_NodeCreateConst (Fraig_Man_t *p)
Fraig_Node_t * Fraig_NodeCreatePi (Fraig_Man_t *p)
Fraig_Node_t * Fraig_NodeCreate (Fraig_Man_t *p, Fraig_Node_t *p1, Fraig_Node_t *p2)
void Fraig_NodeSimulate (Fraig_Node_t *pNode, int iWordStart, int iWordStop, int fUseRand)

Define Documentation

#define Fraig_NodeIsSimComplement ( p   )     (Fraig_IsComplement(p)? !(Fraig_Regular(p)->fInv) : (p)->fInv)

CFile****************************************************************

FileName [fraigNode.c]

PackageName [FRAIG: Functionally reduced AND-INV graphs.]

Synopsis [Implementation of the FRAIG node.]

Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - October 1, 2004]

Revision [

Id
fraigNode.c,v 1.3 2005/07/08 01:01:32 alanmi Exp

] DECLARATIONS ///

Definition at line 26 of file fraigNode.c.

Function Documentation

Fraig_Node_t* Fraig_NodeCreate ( Fraig_Man_t *  p,
Fraig_Node_t *  p1,
Fraig_Node_t *  p2 
)

Function*************************************************************

Synopsis [Creates a new node.]

Description [This procedure should be called to create the constant node and the PI nodes first.]

SideEffects []

SeeAlso []

Definition at line 156 of file fraigNode.c.

00157 {
00158     Fraig_Node_t * pNode;
00159     int clk;
00160 
00161     // create the node
00162     pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes );
00163     memset( pNode, 0, sizeof(Fraig_Node_t) );
00164 
00165     // assign the children
00166     pNode->p1  = p1;  Fraig_Ref(p1);  Fraig_Regular(p1)->nRefs++;
00167     pNode->p2  = p2;  Fraig_Ref(p2);  Fraig_Regular(p2)->nRefs++;
00168 
00169     // assign the number and add to the array of nodes
00170     pNode->Num = p->vNodes->nSize;
00171     Fraig_NodeVecPush( p->vNodes,  pNode );
00172 
00173     // assign the PI number
00174     pNode->NumPi = -1;
00175 
00176     // compute the level of this node
00177     pNode->Level = 1 + FRAIG_MAX(Fraig_Regular(p1)->Level, Fraig_Regular(p2)->Level);
00178     pNode->fInv  = Fraig_NodeIsSimComplement(p1) & Fraig_NodeIsSimComplement(p2);
00179     pNode->fFailTfo = Fraig_Regular(p1)->fFailTfo | Fraig_Regular(p2)->fFailTfo;
00180 
00181     // derive the simulation info 
00182 clk = clock();
00183     // allocate memory for the simulation info
00184     pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
00185     pNode->puSimD = pNode->puSimR + p->nWordsRand;
00186     // derive random simulation info
00187     pNode->uHashR = 0;
00188     Fraig_NodeSimulate( pNode, 0, p->nWordsRand, 1 );
00189     // derive dynamic simulation info
00190     pNode->uHashD = 0;
00191     Fraig_NodeSimulate( pNode, 0, p->iWordStart, 0 );
00192     // count the number of ones in the random simulation info
00193     pNode->nOnes = Fraig_BitStringCountOnes( pNode->puSimR, p->nWordsRand );
00194     if ( pNode->fInv )
00195         pNode->nOnes = p->nWordsRand * 32 - pNode->nOnes;
00196     // add to the runtime of simulation
00197 p->timeSims += clock() - clk;
00198 
00199 #ifdef FRAIG_ENABLE_FANOUTS
00200     // create the fanout info
00201     Fraig_NodeAddFaninFanout( Fraig_Regular(p1), pNode );
00202     Fraig_NodeAddFaninFanout( Fraig_Regular(p2), pNode );
00203 #endif
00204     return pNode;
00205 }

Fraig_Node_t* Fraig_NodeCreateConst ( Fraig_Man_t *  p  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Creates the constant 1 node.]

Description []

SideEffects []

SeeAlso []

Definition at line 43 of file fraigNode.c.

00044 {
00045     Fraig_Node_t * pNode;
00046 
00047     // create the node
00048     pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes );
00049     memset( pNode, 0, sizeof(Fraig_Node_t) );
00050 
00051     // assign the number and add to the array of nodes
00052     pNode->Num   = p->vNodes->nSize;
00053     Fraig_NodeVecPush( p->vNodes,  pNode );
00054     pNode->NumPi = -1;  // this is not a PI, so its number is -1
00055     pNode->Level =  0;  // just like a PI, it has 0 level
00056     pNode->nRefs =  1;  // it is a persistent node, which comes referenced
00057     pNode->fInv  =  1;  // the simulation info is complemented
00058 
00059     // create the simulation info
00060     pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
00061     pNode->puSimD = pNode->puSimR + p->nWordsRand;
00062     memset( pNode->puSimR, 0, sizeof(unsigned) * p->nWordsRand );
00063     memset( pNode->puSimD, 0, sizeof(unsigned) * p->nWordsDyna );
00064 
00065     // count the number of ones in the simulation vector
00066     pNode->nOnes = p->nWordsRand * sizeof(unsigned) * 8;
00067 
00068     // insert it into the hash table
00069     Fraig_HashTableLookupF0( p, pNode );
00070     return pNode;
00071 }

Fraig_Node_t* Fraig_NodeCreatePi ( Fraig_Man_t *  p  ) 

Function*************************************************************

Synopsis [Creates a primary input node.]

Description []

SideEffects []

SeeAlso []

Definition at line 84 of file fraigNode.c.

00085 {
00086     Fraig_Node_t * pNode, * pNodeRes;
00087     int i, clk;
00088 
00089     // create the node
00090     pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes );
00091     memset( pNode, 0, sizeof(Fraig_Node_t) );
00092     pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
00093     pNode->puSimD = pNode->puSimR + p->nWordsRand;
00094     memset( pNode->puSimD, 0, sizeof(unsigned) * p->nWordsDyna );
00095 
00096     // assign the number and add to the array of nodes
00097     pNode->Num   = p->vNodes->nSize;
00098     Fraig_NodeVecPush( p->vNodes,  pNode );
00099 
00100     // assign the PI number and add to the array of primary inputs
00101     pNode->NumPi = p->vInputs->nSize;   
00102     Fraig_NodeVecPush( p->vInputs, pNode );
00103 
00104     pNode->Level =  0;  // PI has 0 level
00105     pNode->nRefs =  1;  // it is a persistent node, which comes referenced
00106     pNode->fInv  =  0;  // the simulation info of the PI is not complemented
00107 
00108     // derive the simulation info for the new node
00109 clk = clock();
00110     // set the random simulation info for the primary input
00111     pNode->uHashR = 0;
00112     for ( i = 0; i < p->nWordsRand; i++ )
00113     {
00114         // generate the simulation info
00115         pNode->puSimR[i] = FRAIG_RANDOM_UNSIGNED;
00116         // for reasons that take very long to explain, it makes sense to have (0000000...) 
00117         // pattern in the set (this helps if we need to return the counter-examples)
00118         if ( i == 0 )
00119             pNode->puSimR[i] <<= 1;
00120         // compute the hash key
00121         pNode->uHashR ^= pNode->puSimR[i] * s_FraigPrimes[i];
00122     }
00123     // count the number of ones in the simulation vector
00124     pNode->nOnes = Fraig_BitStringCountOnes( pNode->puSimR, p->nWordsRand );
00125 
00126     // set the systematic simulation info for the primary input
00127     pNode->uHashD = 0;
00128     for ( i = 0; i < p->iWordStart; i++ )
00129     {
00130         // generate the simulation info
00131         pNode->puSimD[i] = FRAIG_RANDOM_UNSIGNED;
00132         // compute the hash key
00133         pNode->uHashD ^= pNode->puSimD[i] * s_FraigPrimes[i];
00134     }
00135 p->timeSims += clock() - clk;
00136 
00137     // insert it into the hash table
00138     pNodeRes = Fraig_HashTableLookupF( p, pNode );
00139     assert( pNodeRes == NULL );
00140     // add to the runtime of simulation
00141     return pNode;
00142 }

void Fraig_NodeSimulate ( Fraig_Node_t *  pNode,
int  iWordStart,
int  iWordStop,
int  fUseRand 
)

Function*************************************************************

Synopsis [Simulates the node.]

Description [Simulates the random or dynamic simulation info through the node. Uses phases of the children to determine their real simulation info. Uses phase of the node to determine the way its simulation info is stored. The resulting info is guaranteed to be 0 for the first pattern.]

SideEffects [This procedure modified the hash value of the simulation info.]

SeeAlso []

Definition at line 222 of file fraigNode.c.

00223 {
00224     unsigned * pSims, * pSims1, * pSims2;
00225     unsigned uHash;
00226     int fCompl, fCompl1, fCompl2, i;
00227 
00228     assert( !Fraig_IsComplement(pNode) );
00229 
00230     // get hold of the simulation information
00231     pSims  = fUseRand? pNode->puSimR                    : pNode->puSimD;
00232     pSims1 = fUseRand? Fraig_Regular(pNode->p1)->puSimR : Fraig_Regular(pNode->p1)->puSimD;
00233     pSims2 = fUseRand? Fraig_Regular(pNode->p2)->puSimR : Fraig_Regular(pNode->p2)->puSimD;
00234 
00235     // get complemented attributes of the children using their random info
00236     fCompl  = pNode->fInv;
00237     fCompl1 = Fraig_NodeIsSimComplement(pNode->p1);
00238     fCompl2 = Fraig_NodeIsSimComplement(pNode->p2);
00239 
00240     // simulate
00241     uHash = 0;
00242     if ( fCompl1 && fCompl2 )
00243     {
00244         if ( fCompl )
00245             for ( i = iWordStart; i < iWordStop; i++ )
00246             {
00247                 pSims[i] = (pSims1[i] | pSims2[i]);
00248                 uHash ^= pSims[i] * s_FraigPrimes[i];
00249             }
00250         else
00251             for ( i = iWordStart; i < iWordStop; i++ )
00252             {
00253                 pSims[i] = ~(pSims1[i] | pSims2[i]);
00254                 uHash ^= pSims[i] * s_FraigPrimes[i];
00255             }
00256     }
00257     else if ( fCompl1 && !fCompl2 )
00258     {
00259         if ( fCompl )
00260             for ( i = iWordStart; i < iWordStop; i++ )
00261             {
00262                 pSims[i] = (pSims1[i] | ~pSims2[i]);
00263                 uHash ^= pSims[i] * s_FraigPrimes[i];
00264             }
00265         else
00266             for ( i = iWordStart; i < iWordStop; i++ )
00267             {
00268                 pSims[i] = (~pSims1[i] & pSims2[i]);
00269                 uHash ^= pSims[i] * s_FraigPrimes[i];
00270             }
00271     }
00272     else if ( !fCompl1 && fCompl2 )
00273     {
00274         if ( fCompl )
00275             for ( i = iWordStart; i < iWordStop; i++ )
00276             {
00277                 pSims[i] = (~pSims1[i] | pSims2[i]);
00278                 uHash ^= pSims[i] * s_FraigPrimes[i];
00279             }
00280         else
00281             for ( i = iWordStart; i < iWordStop; i++ )
00282             {
00283                 pSims[i] = (pSims1[i] & ~pSims2[i]);
00284                 uHash ^= pSims[i] * s_FraigPrimes[i];
00285             }
00286     }
00287     else // if ( !fCompl1 && !fCompl2 )
00288     {
00289         if ( fCompl )
00290             for ( i = iWordStart; i < iWordStop; i++ )
00291             {
00292                 pSims[i] = ~(pSims1[i] & pSims2[i]);
00293                 uHash ^= pSims[i] * s_FraigPrimes[i];
00294             }
00295         else
00296             for ( i = iWordStart; i < iWordStop; i++ )
00297             {
00298                 pSims[i] = (pSims1[i] & pSims2[i]);
00299                 uHash ^= pSims[i] * s_FraigPrimes[i];
00300             }
00301     }
00302 
00303     if ( fUseRand )
00304         pNode->uHashR ^= uHash;
00305     else
00306         pNode->uHashD ^= uHash;
00307 }

Generated on Tue Jan 5 12:19:38 2010 for abc70930 by  doxygen 1.6.1