src/aig/cnf/cnf.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "vec.h"
#include "aig.h"
#include "darInt.h"
Include dependency graph for cnf.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures

struct  Cnf_Dat_t_
struct  Cnf_Cut_t_
struct  Cnf_Man_t_

Defines

#define Cnf_CutForEachLeaf(p, pCut, pLeaf, i)   for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )

Typedefs

typedef struct Cnf_Man_t_ Cnf_Man_t
typedef struct Cnf_Dat_t_ Cnf_Dat_t
typedef struct Cnf_Cut_t_ Cnf_Cut_t

Functions

static Dar_Cut_t * Dar_ObjBestCut (Aig_Obj_t *pObj)
static int Cnf_CutSopCost (Cnf_Man_t *p, Dar_Cut_t *pCut)
static int Cnf_CutLeaveNum (Cnf_Cut_t *pCut)
static int * Cnf_CutLeaves (Cnf_Cut_t *pCut)
static unsigned * Cnf_CutTruth (Cnf_Cut_t *pCut)
static Cnf_Cut_t * Cnf_ObjBestCut (Aig_Obj_t *pObj)
static void Cnf_ObjSetBestCut (Aig_Obj_t *pObj, Cnf_Cut_t *pCut)
Cnf_Dat_t * Cnf_Derive (Aig_Man_t *pAig, int nOutputs)
Cnf_Man_t * Cnf_ManRead ()
void Cnf_ClearMemory ()
Cnf_Cut_t * Cnf_CutCreate (Cnf_Man_t *p, Aig_Obj_t *pObj)
void Cnf_CutPrint (Cnf_Cut_t *pCut)
void Cnf_CutFree (Cnf_Cut_t *pCut)
void Cnf_CutUpdateRefs (Cnf_Man_t *p, Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, Cnf_Cut_t *pCutRes)
Cnf_Cut_t * Cnf_CutCompose (Cnf_Man_t *p, Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, int iFan)
void Cnf_ReadMsops (char **ppSopSizes, char ***ppSops)
Cnf_Man_t * Cnf_ManStart ()
void Cnf_ManStop (Cnf_Man_t *p)
Vec_Int_t * Cnf_DataCollectPiSatNums (Cnf_Dat_t *pCnf, Aig_Man_t *p)
void Cnf_DataFree (Cnf_Dat_t *p)
void Cnf_DataWriteIntoFile (Cnf_Dat_t *p, char *pFileName, int fReadable)
void * Cnf_DataWriteIntoSolver (Cnf_Dat_t *p)
void Cnf_DeriveMapping (Cnf_Man_t *p)
int Cnf_ManMapForCnf (Cnf_Man_t *p)
void Cnf_ManTransferCuts (Cnf_Man_t *p)
void Cnf_ManFreeCuts (Cnf_Man_t *p)
void Cnf_ManPostprocess (Cnf_Man_t *p)
Vec_Ptr_t * Aig_ManScanMapping (Cnf_Man_t *p, int fCollect)
Vec_Ptr_t * Cnf_ManScanMapping (Cnf_Man_t *p, int fCollect, int fPreorder)
void Cnf_SopConvertToVector (char *pSop, int nCubes, Vec_Int_t *vCover)
Cnf_Dat_t * Cnf_ManWriteCnf (Cnf_Man_t *p, Vec_Ptr_t *vMapped, int nOutputs)
Cnf_Dat_t * Cnf_DeriveSimple (Aig_Man_t *p, int nOutputs)

Define Documentation

#define Cnf_CutForEachLeaf ( p,
pCut,
pLeaf,
i   )     for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )

MACRO DEFINITIONS /// ITERATORS ///

Definition at line 112 of file cnf.h.

Typedef Documentation

typedef struct Cnf_Cut_t_ Cnf_Cut_t

Definition at line 52 of file cnf.h.

typedef struct Cnf_Dat_t_ Cnf_Dat_t

Definition at line 51 of file cnf.h.

typedef struct Cnf_Man_t_ Cnf_Man_t

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

FileName [cnf.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
cnf.h,v 1.00 2007/04/28 00:00:00 alanmi Exp

] INCLUDES /// PARAMETERS /// BASIC TYPES ///

Definition at line 50 of file cnf.h.

Function Documentation

Vec_Ptr_t* Aig_ManScanMapping ( Cnf_Man_t *  p,
int  fCollect 
)

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

Synopsis [Computes area, references, and nodes used in the mapping.]

Description [Collects the nodes in reverse topological order.]

SideEffects []

SeeAlso []

Definition at line 86 of file cnfUtil.c.

00087 {
00088     Vec_Ptr_t * vMapped = NULL;
00089     Aig_Obj_t * pObj;
00090     int i;
00091     // clean all references
00092     Aig_ManForEachObj( p->pManAig, pObj, i )
00093         pObj->nRefs = 0;
00094     // allocate the array
00095     if ( fCollect )
00096         vMapped = Vec_PtrAlloc( 1000 );
00097     // collect nodes reachable from POs in the DFS order through the best cuts
00098     p->aArea = 0;
00099     Aig_ManForEachPo( p->pManAig, pObj, i )
00100         p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped );
00101 //    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
00102     return vMapped;
00103 }

void Cnf_ClearMemory (  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 113 of file cnfCore.c.

00114 {
00115     if ( s_pManCnf == NULL )
00116         return;
00117     Cnf_ManStop( s_pManCnf );
00118     s_pManCnf = NULL;
00119 }

Cnf_Cut_t* Cnf_CutCompose ( Cnf_Man_t *  p,
Cnf_Cut_t *  pCut,
Cnf_Cut_t *  pCutFan,
int  iFan 
)

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

Synopsis [Merges two cuts.]

Description [Returns NULL of the cuts cannot be merged.]

SideEffects []

SeeAlso []

Definition at line 291 of file cnfCut.c.

00292 {
00293     Cnf_Cut_t * pCutRes;
00294     static int pFanins[32];
00295     unsigned * pTruth, * pTruthFan, * pTruthRes;
00296     unsigned * pTop = p->pTruths[0], * pFan = p->pTruths[2], * pTemp = p->pTruths[3];
00297     unsigned uPhase, uPhaseFan;
00298     int i, iVar, nFanins, RetValue;
00299 
00300     // make sure the second cut is the fanin of the first
00301     for ( iVar = 0; iVar < pCut->nFanins; iVar++ )
00302         if ( pCut->pFanins[iVar] == iFan )
00303             break;
00304     assert( iVar < pCut->nFanins );
00305     // remove this variable
00306     Cnf_CutRemoveIthVar( pCut, iVar, iFan );
00307     // merge leaves of the cuts
00308     nFanins = Cnf_CutMergeLeaves( pCut, pCutFan, pFanins );
00309     if ( nFanins+1 > p->nMergeLimit )
00310     {
00311         Cnf_CutInsertIthVar( pCut, iVar, iFan );
00312         return NULL;
00313     }
00314     // create new cut
00315     pCutRes = Cnf_CutAlloc( p, nFanins );
00316     memcpy( pCutRes->pFanins, pFanins, sizeof(int) * nFanins );
00317     assert( pCutRes->nFanins <= pCut->nFanins + pCutFan->nFanins );
00318 
00319     // derive its truth table
00320     // get the truth tables in the composition space
00321     pTruth    = Cnf_CutTruth(pCut);
00322     pTruthFan = Cnf_CutTruth(pCutFan);
00323     pTruthRes = Cnf_CutTruth(pCutRes);
00324     for ( i = 0; i < 2*pCutRes->nWords; i++ )
00325         pTop[i] = pTruth[i % pCut->nWords];
00326     for ( i = 0; i < pCutRes->nWords; i++ )
00327         pFan[i] = pTruthFan[i % pCutFan->nWords];
00328     // move the variable to the end
00329     uPhase = Kit_BitMask( pCutRes->nFanins+1 ) & ~(1 << iVar);
00330     Kit_TruthShrink( pTemp, pTop, pCutRes->nFanins, pCutRes->nFanins+1, uPhase, 1 );
00331     // compute the phases
00332     uPhase    = Cnf_TruthPhase( pCutRes, pCut    ) | (1 << pCutRes->nFanins);
00333     uPhaseFan = Cnf_TruthPhase( pCutRes, pCutFan );
00334     // permute truth-tables to the common support
00335     Kit_TruthStretch( pTemp, pTop, pCut->nFanins+1,  pCutRes->nFanins+1, uPhase,    1 );
00336     Kit_TruthStretch( pTemp, pFan, pCutFan->nFanins, pCutRes->nFanins,   uPhaseFan, 1 );
00337     // perform Boolean operation
00338     Kit_TruthMux( pTruthRes, pTop, pTop+pCutRes->nWords, pFan, pCutRes->nFanins );
00339     // return the cut to its original condition
00340     Cnf_CutInsertIthVar( pCut, iVar, iFan );
00341     // consider the simple case
00342     if ( pCutRes->nFanins < 5 )
00343     {
00344         pCutRes->Cost = p->pSopSizes[0xFFFF & *pTruthRes] + p->pSopSizes[0xFFFF & ~*pTruthRes];
00345         return pCutRes;
00346     }
00347 
00348     // derive ISOP for positive phase
00349     RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
00350     pCutRes->vIsop[1] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
00351     // derive ISOP for negative phase
00352     Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );
00353     RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
00354     pCutRes->vIsop[0] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
00355     Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );
00356 
00357     // compute the cut cost
00358     if ( pCutRes->vIsop[0] == NULL || pCutRes->vIsop[1] == NULL )
00359         pCutRes->Cost = 127;
00360     else if ( Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]) > 127 )
00361         pCutRes->Cost = 127;
00362     else
00363         pCutRes->Cost = Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]);
00364     return pCutRes;
00365 }

Cnf_Cut_t* Cnf_CutCreate ( Cnf_Man_t *  p,
Aig_Obj_t *  pObj 
)

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

Synopsis [Creates cut for the given node.]

Description []

SideEffects []

SeeAlso []

Definition at line 84 of file cnfCut.c.

00085 {
00086     Dar_Cut_t * pCutBest;
00087     Cnf_Cut_t * pCut;
00088     unsigned * pTruth;
00089     assert( Aig_ObjIsNode(pObj) );
00090     pCutBest = Dar_ObjBestCut( pObj );
00091     assert( pCutBest != NULL );
00092     assert( pCutBest->nLeaves <= 4 );
00093     pCut = Cnf_CutAlloc( p, pCutBest->nLeaves );
00094     memcpy( pCut->pFanins, pCutBest->pLeaves, sizeof(int) * pCutBest->nLeaves );
00095     pTruth = Cnf_CutTruth(pCut);
00096     *pTruth = (pCutBest->uTruth << 16) | pCutBest->uTruth;
00097     pCut->Cost = Cnf_CutSopCost( p, pCutBest );
00098     return pCut;
00099 }

void Cnf_CutFree ( Cnf_Cut_t *  pCut  ) 

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

Synopsis [Deallocates cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 65 of file cnfCut.c.

00066 {
00067     if ( pCut->vIsop[0] )
00068         Vec_IntFree( pCut->vIsop[0] );
00069     if ( pCut->vIsop[1] )
00070         Vec_IntFree( pCut->vIsop[1] );
00071 }

static int Cnf_CutLeaveNum ( Cnf_Cut_t *  pCut  )  [inline, static]

Definition at line 96 of file cnf.h.

00096 { return pCut->nFanins;                               }

static int* Cnf_CutLeaves ( Cnf_Cut_t *  pCut  )  [inline, static]

Definition at line 97 of file cnf.h.

00097 { return pCut->pFanins;                               }

void Cnf_CutPrint ( Cnf_Cut_t *  pCut  ) 

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

Synopsis [Deallocates cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 112 of file cnfCut.c.

00113 {
00114     int i;
00115     printf( "{" );
00116     for ( i = 0; i < pCut->nFanins; i++ )
00117         printf( "%d ", pCut->pFanins[i] );
00118     printf( " } " );
00119 }

static int Cnf_CutSopCost ( Cnf_Man_t *  p,
Dar_Cut_t *  pCut 
) [inline, static]

Definition at line 94 of file cnf.h.

00094 { return p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth]; }

static unsigned* Cnf_CutTruth ( Cnf_Cut_t *  pCut  )  [inline, static]

Definition at line 98 of file cnf.h.

00098 { return (unsigned *)(pCut->pFanins + pCut->nFanins); }

void Cnf_CutUpdateRefs ( Cnf_Man_t *  p,
Cnf_Cut_t *  pCut,
Cnf_Cut_t *  pCutFan,
Cnf_Cut_t *  pCutRes 
)

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

Synopsis [Allocates cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 175 of file cnfCut.c.

00176 {
00177     Cnf_CutDeref( p, pCut );
00178     Cnf_CutDeref( p, pCutFan );
00179     Cnf_CutRef( p, pCutRes );
00180 }

Vec_Int_t* Cnf_DataCollectPiSatNums ( Cnf_Dat_t *  pCnf,
Aig_Man_t *  p 
)

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

Synopsis [Returns the array of CI IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 99 of file cnfMan.c.

00100 {
00101     Vec_Int_t * vCiIds;
00102     Aig_Obj_t * pObj;
00103     int i;
00104     vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) );
00105     Aig_ManForEachPi( p, pObj, i )
00106         Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
00107     return vCiIds;
00108 }

void Cnf_DataFree ( Cnf_Dat_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 121 of file cnfMan.c.

00122 {
00123     if ( p == NULL )
00124         return;
00125     free( p->pClauses[0] );
00126     free( p->pClauses );
00127     free( p->pVarNums );
00128     free( p );
00129 }

void Cnf_DataWriteIntoFile ( Cnf_Dat_t *  p,
char *  pFileName,
int  fReadable 
)

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

Synopsis [Writes CNF into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 142 of file cnfMan.c.

00143 {
00144     FILE * pFile;
00145     int * pLit, * pStop, i;
00146     pFile = fopen( pFileName, "w" );
00147     if ( pFile == NULL )
00148     {
00149         printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" );
00150         return;
00151     }
00152     fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
00153     fprintf( pFile, "p %d %d\n", p->nVars, p->nClauses );
00154     for ( i = 0; i < p->nClauses; i++ )
00155     {
00156         for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
00157             fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
00158         fprintf( pFile, "0\n" );
00159     }
00160     fprintf( pFile, "\n" );
00161     fclose( pFile );
00162 }

void* Cnf_DataWriteIntoSolver ( Cnf_Dat_t *  p  ) 

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

Synopsis [Writes CNF into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 175 of file cnfMan.c.

00176 {
00177     sat_solver * pSat;
00178     int i, status;
00179     pSat = sat_solver_new();
00180     sat_solver_setnvars( pSat, p->nVars );
00181     for ( i = 0; i < p->nClauses; i++ )
00182     {
00183         if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
00184         {
00185             sat_solver_delete( pSat );
00186             return NULL;
00187         }
00188     }
00189     status = sat_solver_simplify(pSat);
00190     if ( status == 0 )
00191     {
00192         sat_solver_delete( pSat );
00193         return NULL;
00194     }
00195     return pSat;
00196 }

Cnf_Dat_t* Cnf_Derive ( Aig_Man_t *  pAig,
int  nOutputs 
)

FUNCTION DECLARATIONS ///

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

Synopsis [Converts AIG into the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 44 of file cnfCore.c.

00045 {
00046     Cnf_Man_t * p;
00047     Cnf_Dat_t * pCnf;
00048     Vec_Ptr_t * vMapped;
00049     Aig_MmFixed_t * pMemCuts;
00050     int clk;
00051     // allocate the CNF manager
00052     if ( s_pManCnf == NULL )
00053         s_pManCnf = Cnf_ManStart();
00054     // connect the managers
00055     p = s_pManCnf;
00056     p->pManAig = pAig;
00057 
00058     // generate cuts for all nodes, assign cost, and find best cuts
00059 clk = clock();
00060     pMemCuts = Dar_ManComputeCuts( pAig, 10 );
00061 p->timeCuts = clock() - clk;
00062 
00063     // find the mapping
00064 clk = clock();
00065     Cnf_DeriveMapping( p );
00066 p->timeMap = clock() - clk;
00067 //    Aig_ManScanMapping( p, 1 );
00068 
00069     // convert it into CNF
00070 clk = clock();
00071     Cnf_ManTransferCuts( p );
00072     vMapped = Cnf_ManScanMapping( p, 1, 1 );
00073     pCnf = Cnf_ManWriteCnf( p, vMapped, nOutputs );
00074     Vec_PtrFree( vMapped );
00075     Aig_MmFixedStop( pMemCuts, 0 );
00076 p->timeSave = clock() - clk;
00077 
00078    // reset reference counters
00079     Aig_ManResetRefs( pAig );
00080 //PRT( "Cuts   ", p->timeCuts );
00081 //PRT( "Map    ", p->timeMap  );
00082 //PRT( "Saving ", p->timeSave );
00083     return pCnf;
00084 }

void Cnf_DeriveMapping ( Cnf_Man_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 96 of file cnfMap.c.

00097 {
00098     Vec_Ptr_t * vSuper;
00099     Aig_Obj_t * pObj;
00100     Dar_Cut_t * pCut, * pCutBest;
00101     int i, k, AreaFlow, * pAreaFlows;
00102     // allocate area flows
00103     pAreaFlows = ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
00104     memset( pAreaFlows, 0, sizeof(int) * Aig_ManObjNumMax(p->pManAig) );
00105     // visit the nodes in the topological order and update their best cuts
00106     vSuper = Vec_PtrAlloc( 100 );
00107     Aig_ManForEachNode( p->pManAig, pObj, i )
00108     {
00109         // go through the cuts
00110         pCutBest = NULL;
00111         Dar_ObjForEachCut( pObj, pCut, k )
00112         {
00113             pCut->fBest = 0;
00114             if ( k == 0 )
00115                 continue;
00116             Cnf_CutAssignAreaFlow( p, pCut, pAreaFlows );
00117             if ( pCutBest == NULL || pCutBest->uSign > pCut->uSign || 
00118                 (pCutBest->uSign == pCut->uSign && pCutBest->Value < pCut->Value) )
00119                  pCutBest = pCut;
00120         }
00121         // check the big cut
00122 //        Aig_ObjCollectSuper( pObj, vSuper );
00123         // get the area flow of this cut
00124 //        AreaFlow = Cnf_CutSuperAreaFlow( vSuper, pAreaFlows );
00125         AreaFlow = AIG_INFINITY;
00126         if ( AreaFlow >= (int)pCutBest->uSign )
00127         {
00128             pAreaFlows[pObj->Id] = pCutBest->uSign;
00129             pCutBest->fBest = 1;
00130         }
00131         else
00132         {
00133             pAreaFlows[pObj->Id] = AreaFlow;
00134             pObj->fMarkB = 1; // mark the special node
00135         }
00136     }
00137     Vec_PtrFree( vSuper );
00138     free( pAreaFlows );
00139 
00140 /*
00141     // compute the area of mapping
00142     AreaFlow = 0;
00143     Aig_ManForEachPo( p->pManAig, pObj, i )
00144         AreaFlow += Dar_ObjBestCut(Aig_ObjFanin0(pObj))->uSign / 100 / Aig_ObjFanin0(pObj)->nRefs;
00145     printf( "Area of the network = %d.\n", AreaFlow );
00146 */
00147 }

Cnf_Dat_t* Cnf_DeriveSimple ( Aig_Man_t *  p,
int  nOutputs 
)

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

Synopsis [Derives a simple CNF for the AIG.]

Description [The last argument shows the number of last outputs of the manager, which will not be converted into clauses but the new variables for which will be introduced.]

SideEffects []

SeeAlso []

Definition at line 335 of file cnfWrite.c.

00336 {
00337     Aig_Obj_t * pObj;
00338     Cnf_Dat_t * pCnf;
00339     int OutVar, PoVar, pVars[32], * pLits, ** pClas;
00340     int i, nLiterals, nClauses, Number;
00341 
00342     // count the number of literals and clauses
00343     nLiterals = 1 + 7 * Aig_ManNodeNum(p) + Aig_ManPoNum( p ) + 3 * nOutputs;
00344     nClauses = 1 + 3 * Aig_ManNodeNum(p) + Aig_ManPoNum( p ) + nOutputs;
00345 
00346     // allocate CNF
00347     pCnf = ALLOC( Cnf_Dat_t, 1 );
00348     memset( pCnf, 0, sizeof(Cnf_Dat_t) );
00349     pCnf->nLiterals = nLiterals;
00350     pCnf->nClauses = nClauses;
00351     pCnf->pClauses = ALLOC( int *, nClauses + 1 );
00352     pCnf->pClauses[0] = ALLOC( int, nLiterals );
00353     pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
00354 
00355     // create room for variable numbers
00356     pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p) );
00357     memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
00358     // assign variables to the last (nOutputs) POs
00359     Number = 1;
00360     if ( nOutputs )
00361     {
00362         assert( nOutputs == Aig_ManRegNum(p) );
00363         Aig_ManForEachLiSeq( p, pObj, i )
00364             pCnf->pVarNums[pObj->Id] = Number++;
00365     }
00366     // assign variables to the internal nodes
00367     Aig_ManForEachNode( p, pObj, i )
00368         pCnf->pVarNums[pObj->Id] = Number++;
00369     // assign variables to the PIs and constant node
00370     Aig_ManForEachPi( p, pObj, i )
00371         pCnf->pVarNums[pObj->Id] = Number++;
00372     pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++;
00373     pCnf->nVars = Number;
00374 /*
00375     // print CNF numbers
00376     printf( "SAT numbers of each node:\n" );
00377     Aig_ManForEachObj( p, pObj, i )
00378         printf( "%d=%d ", pObj->Id, pCnf->pVarNums[pObj->Id] );
00379     printf( "\n" );
00380 */
00381     // assign the clauses
00382     pLits = pCnf->pClauses[0];
00383     pClas = pCnf->pClauses;
00384     Aig_ManForEachNode( p, pObj, i )
00385     {
00386         OutVar   = pCnf->pVarNums[ pObj->Id ];
00387         pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
00388         pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
00389 
00390         // positive phase
00391         *pClas++ = pLits;
00392         *pLits++ = 2 * OutVar; 
00393         *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj); 
00394         *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj); 
00395         // negative phase
00396         *pClas++ = pLits;
00397         *pLits++ = 2 * OutVar + 1; 
00398         *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj); 
00399         *pClas++ = pLits;
00400         *pLits++ = 2 * OutVar + 1; 
00401         *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj); 
00402     }
00403  
00404     // write the constant literal
00405     OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
00406     assert( OutVar <= Aig_ManObjNumMax(p) );
00407     *pClas++ = pLits;
00408     *pLits++ = 2 * OutVar; 
00409 
00410     // write the output literals
00411     Aig_ManForEachPo( p, pObj, i )
00412     {
00413         OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
00414         if ( i < Aig_ManPoNum(p) - nOutputs )
00415         {
00416             *pClas++ = pLits;
00417             *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
00418         }
00419         else
00420         {
00421             PoVar  = pCnf->pVarNums[ pObj->Id ];
00422             // first clause
00423             *pClas++ = pLits;
00424             *pLits++ = 2 * PoVar; 
00425             *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); 
00426             // second clause
00427             *pClas++ = pLits;
00428             *pLits++ = 2 * PoVar + 1; 
00429             *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
00430         }
00431     }
00432 
00433     // verify that the correct number of literals and clauses was written
00434     assert( pLits - pCnf->pClauses[0] == nLiterals );
00435     assert( pClas - pCnf->pClauses == nClauses );
00436     return pCnf;
00437 }

void Cnf_ManFreeCuts ( Cnf_Man_t *  p  ) 

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

Synopsis [Transfers cuts of the mapped nodes into internal representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 139 of file cnfPost.c.

00140 {
00141     Aig_Obj_t * pObj;
00142     int i;
00143     Aig_ManForEachObj( p->pManAig, pObj, i )
00144         if ( pObj->pData )
00145         {
00146             Cnf_CutFree( pObj->pData );
00147             pObj->pData = NULL;
00148         }
00149 }

int Cnf_ManMapForCnf ( Cnf_Man_t *  p  ) 
void Cnf_ManPostprocess ( Cnf_Man_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 162 of file cnfPost.c.

00163 {
00164     Cnf_Cut_t * pCut, * pCutFan, * pCutRes;
00165     Aig_Obj_t * pObj, * pFan;
00166     int Order[16], Costs[16];
00167     int i, k, fChanges;
00168     Aig_ManForEachNode( p->pManAig, pObj, i )
00169     {
00170         if ( pObj->nRefs == 0 )
00171             continue;
00172         pCut = Cnf_ObjBestCut(pObj);
00173 
00174         // sort fanins according to their size
00175         Cnf_CutForEachLeaf( p->pManAig, pCut, pFan, k )
00176         {
00177             Order[k] = k;
00178             Costs[k] = Aig_ObjIsNode(pFan)? Cnf_ObjBestCut(pFan)->Cost : 0;
00179         }
00180         // sort the cuts by Weight
00181         do {
00182             int Temp;
00183             fChanges = 0;
00184             for ( k = 0; k < pCut->nFanins - 1; k++ )
00185             {
00186                 if ( Costs[Order[k]] <= Costs[Order[k+1]] )
00187                     continue;
00188                 Temp = Order[k];
00189                 Order[k] = Order[k+1];
00190                 Order[k+1] = Temp;
00191                 fChanges = 1;
00192             }
00193         } while ( fChanges );
00194 
00195 
00196 //        Cnf_CutForEachLeaf( p->pManAig, pCut, pFan, k )
00197         for ( k = 0; (k < (int)(pCut)->nFanins) && ((pFan) = Aig_ManObj(p->pManAig, (pCut)->pFanins[Order[k]])); k++ )
00198         {
00199             if ( !Aig_ObjIsNode(pFan) )
00200                 continue;
00201             assert( pFan->nRefs != 0 );
00202             if ( pFan->nRefs != 1 )
00203                 continue;
00204             pCutFan = Cnf_ObjBestCut(pFan);
00205             // try composing these two cuts
00206 //            Cnf_CutPrint( pCut );
00207             pCutRes = Cnf_CutCompose( p, pCut, pCutFan, pFan->Id );
00208 //            Cnf_CutPrint( pCut );
00209 //            printf( "\n" );
00210             // check if the cost if reduced
00211             if ( pCutRes == NULL || pCutRes->Cost == 127 || pCutRes->Cost > pCut->Cost + pCutFan->Cost )
00212             {
00213                 if ( pCutRes )
00214                     Cnf_CutFree( pCutRes );
00215                 continue;
00216             }
00217             // update the cut
00218             Cnf_ObjSetBestCut( pObj, pCutRes );
00219             Cnf_ObjSetBestCut( pFan, NULL );
00220             Cnf_CutUpdateRefs( p, pCut, pCutFan, pCutRes );
00221             assert( pFan->nRefs == 0 );
00222             Cnf_CutFree( pCut );
00223             Cnf_CutFree( pCutFan );
00224             break;
00225         }
00226     }
00227 }

Cnf_Man_t* Cnf_ManRead (  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 97 of file cnfCore.c.

00098 {
00099     return s_pManCnf;
00100 }

Vec_Ptr_t* Cnf_ManScanMapping ( Cnf_Man_t *  p,
int  fCollect,
int  fPreorder 
)

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

Synopsis [Computes area, references, and nodes used in the mapping.]

Description [Collects the nodes in reverse topological order.]

SideEffects []

SeeAlso []

Definition at line 165 of file cnfUtil.c.

00166 {
00167     Vec_Ptr_t * vMapped = NULL;
00168     Aig_Obj_t * pObj;
00169     int i;
00170     // clean all references
00171     Aig_ManForEachObj( p->pManAig, pObj, i )
00172         pObj->nRefs = 0;
00173     // allocate the array
00174     if ( fCollect )
00175         vMapped = Vec_PtrAlloc( 1000 );
00176     // collect nodes reachable from POs in the DFS order through the best cuts
00177     p->aArea = 0;
00178     Aig_ManForEachPo( p->pManAig, pObj, i )
00179         p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped, fPreorder );
00180 //    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
00181     return vMapped;
00182 }

Cnf_Man_t* Cnf_ManStart (  ) 

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

Synopsis [Starts the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file cnfMan.c.

00047 {
00048     Cnf_Man_t * p;
00049     int i;
00050     // allocate the manager
00051     p = ALLOC( Cnf_Man_t, 1 );
00052     memset( p, 0, sizeof(Cnf_Man_t) );
00053     // derive internal data structures
00054     Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
00055     // allocate memory manager for cuts
00056     p->pMemCuts = Aig_MmFlexStart();
00057     p->nMergeLimit = 10;
00058     // allocate temporary truth tables
00059     p->pTruths[0] = ALLOC( unsigned, 4 * Aig_TruthWordNum(p->nMergeLimit) );
00060     for ( i = 1; i < 4; i++ )
00061         p->pTruths[i] = p->pTruths[i-1] + Aig_TruthWordNum(p->nMergeLimit);
00062     p->vMemory = Vec_IntAlloc( 1 << 18 );
00063     return p;
00064 }

void Cnf_ManStop ( Cnf_Man_t *  p  ) 

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

Synopsis [Stops the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file cnfMan.c.

00078 {
00079     Vec_IntFree( p->vMemory );
00080     free( p->pTruths[0] );
00081     Aig_MmFlexStop( p->pMemCuts, 0 );
00082     free( p->pSopSizes );
00083     free( p->pSops[1] );
00084     free( p->pSops );
00085     free( p );
00086 }

void Cnf_ManTransferCuts ( Cnf_Man_t *  p  ) 

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

Synopsis [Transfers cuts of the mapped nodes into internal representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 114 of file cnfPost.c.

00115 {
00116     Aig_Obj_t * pObj;
00117     int i;
00118     Aig_MmFlexRestart( p->pMemCuts );
00119     Aig_ManForEachObj( p->pManAig, pObj, i )
00120     {
00121         if ( Aig_ObjIsNode(pObj) && pObj->nRefs > 0 )
00122             pObj->pData = Cnf_CutCreate( p, pObj );
00123         else
00124             pObj->pData = NULL;
00125     }
00126 }

Cnf_Dat_t* Cnf_ManWriteCnf ( Cnf_Man_t *  p,
Vec_Ptr_t *  vMapped,
int  nOutputs 
)

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

Synopsis [Derives CNF for the mapping.]

Description [The last argument shows the number of last outputs of the manager, which will not be converted into clauses but the new variables for which will be introduced.]

SideEffects []

SeeAlso []

Definition at line 159 of file cnfWrite.c.

00160 {
00161     Aig_Obj_t * pObj;
00162     Cnf_Dat_t * pCnf;
00163     Cnf_Cut_t * pCut;
00164     Vec_Int_t * vCover, * vSopTemp;
00165     int OutVar, PoVar, pVars[32], * pLits, ** pClas;
00166     unsigned uTruth;
00167     int i, k, nLiterals, nClauses, Cube, Number;
00168 
00169     // count the number of literals and clauses
00170     nLiterals = 1 + Aig_ManPoNum( p->pManAig ) + 3 * nOutputs;
00171     nClauses = 1 + Aig_ManPoNum( p->pManAig ) + nOutputs;
00172     Vec_PtrForEachEntry( vMapped, pObj, i )
00173     {
00174         assert( Aig_ObjIsNode(pObj) );
00175         pCut = Cnf_ObjBestCut( pObj );
00176 
00177         // positive polarity of the cut
00178         if ( pCut->nFanins < 5 )
00179         {
00180             uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
00181             nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
00182             assert( p->pSopSizes[uTruth] >= 0 );
00183             nClauses += p->pSopSizes[uTruth];
00184         }
00185         else
00186         {
00187             nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]);
00188             nClauses += Vec_IntSize(pCut->vIsop[1]);
00189         }
00190         // negative polarity of the cut
00191         if ( pCut->nFanins < 5 )
00192         {
00193             uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
00194             nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
00195             assert( p->pSopSizes[uTruth] >= 0 );
00196             nClauses += p->pSopSizes[uTruth];
00197         }
00198         else
00199         {
00200             nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
00201             nClauses += Vec_IntSize(pCut->vIsop[0]);
00202         }
00203 //printf( "%d ", nClauses-(1 + Aig_ManPoNum( p->pManAig )) );
00204     }
00205 //printf( "\n" );
00206 
00207     // allocate CNF
00208     pCnf = ALLOC( Cnf_Dat_t, 1 );
00209     memset( pCnf, 0, sizeof(Cnf_Dat_t) );
00210     pCnf->nLiterals = nLiterals;
00211     pCnf->nClauses = nClauses;
00212     pCnf->pClauses = ALLOC( int *, nClauses + 1 );
00213     pCnf->pClauses[0] = ALLOC( int, nLiterals );
00214     pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
00215 
00216     // create room for variable numbers
00217     pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
00218     memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p->pManAig) );
00219     // assign variables to the last (nOutputs) POs
00220     Number = 1;
00221     if ( nOutputs )
00222     {
00223         assert( nOutputs == Aig_ManRegNum(p->pManAig) );
00224         Aig_ManForEachLiSeq( p->pManAig, pObj, i )
00225             pCnf->pVarNums[pObj->Id] = Number++;
00226     }
00227     // assign variables to the internal nodes
00228     Vec_PtrForEachEntry( vMapped, pObj, i )
00229         pCnf->pVarNums[pObj->Id] = Number++;
00230     // assign variables to the PIs and constant node
00231     Aig_ManForEachPi( p->pManAig, pObj, i )
00232         pCnf->pVarNums[pObj->Id] = Number++;
00233     pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number++;
00234     pCnf->nVars = Number;
00235 
00236     // assign the clauses
00237     vSopTemp = Vec_IntAlloc( 1 << 16 );
00238     pLits = pCnf->pClauses[0];
00239     pClas = pCnf->pClauses;
00240     Vec_PtrForEachEntry( vMapped, pObj, i )
00241     {
00242         pCut = Cnf_ObjBestCut( pObj );
00243 
00244         // save variables of this cut
00245         OutVar = pCnf->pVarNums[ pObj->Id ];
00246         for ( k = 0; k < (int)pCut->nFanins; k++ )
00247         {
00248             pVars[k] = pCnf->pVarNums[ pCut->pFanins[k] ];
00249             assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) );
00250         }
00251 
00252         // positive polarity of the cut
00253         if ( pCut->nFanins < 5 )
00254         {
00255             uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
00256             Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
00257             vCover = vSopTemp;
00258         }
00259         else
00260             vCover = pCut->vIsop[1];
00261         Vec_IntForEachEntry( vCover, Cube, k )
00262         {
00263             *pClas++ = pLits;
00264             *pLits++ = 2 * OutVar; 
00265             pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
00266         }
00267 
00268         // negative polarity of the cut
00269         if ( pCut->nFanins < 5 )
00270         {
00271             uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
00272             Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
00273             vCover = vSopTemp;
00274         }
00275         else
00276             vCover = pCut->vIsop[0];
00277         Vec_IntForEachEntry( vCover, Cube, k )
00278         {
00279             *pClas++ = pLits;
00280             *pLits++ = 2 * OutVar + 1; 
00281             pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
00282         }
00283     }
00284     Vec_IntFree( vSopTemp );
00285  
00286     // write the constant literal
00287     OutVar = pCnf->pVarNums[ Aig_ManConst1(p->pManAig)->Id ];
00288     assert( OutVar <= Aig_ManObjNumMax(p->pManAig) );
00289     *pClas++ = pLits;
00290     *pLits++ = 2 * OutVar; 
00291 
00292     // write the output literals
00293     Aig_ManForEachPo( p->pManAig, pObj, i )
00294     {
00295         OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
00296         if ( i < Aig_ManPoNum(p->pManAig) - nOutputs )
00297         {
00298             *pClas++ = pLits;
00299             *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
00300         }
00301         else
00302         {
00303             PoVar = pCnf->pVarNums[ pObj->Id ];
00304             // first clause
00305             *pClas++ = pLits;
00306             *pLits++ = 2 * PoVar; 
00307             *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); 
00308             // second clause
00309             *pClas++ = pLits;
00310             *pLits++ = 2 * PoVar + 1; 
00311             *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
00312         }
00313     }
00314 
00315     // verify that the correct number of literals and clauses was written
00316     assert( pLits - pCnf->pClauses[0] == nLiterals );
00317     assert( pClas - pCnf->pClauses == nClauses );
00318     return pCnf;
00319 }

static Cnf_Cut_t* Cnf_ObjBestCut ( Aig_Obj_t *  pObj  )  [inline, static]

Definition at line 100 of file cnf.h.

00100 { return pObj->pData;  }

static void Cnf_ObjSetBestCut ( Aig_Obj_t *  pObj,
Cnf_Cut_t *  pCut 
) [inline, static]

Definition at line 101 of file cnf.h.

00101 { pObj->pData = pCut;  }

void Cnf_ReadMsops ( char **  ppSopSizes,
char ***  ppSops 
)

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

Synopsis [Prepares the data for MSOPs of 4-variable functions.]

Description []

SideEffects []

SeeAlso []

Definition at line 4534 of file cnfData.c.

04535 {
04536     unsigned uMasks[4][2] = {
04537         { 0x5555, 0xAAAA },
04538         { 0x3333, 0xCCCC },
04539         { 0x0F0F, 0xF0F0 },
04540         { 0x00FF, 0xFF00 }
04541     };
04542     char Map[256], * pPrev, * pMemory;
04543     char * pSopSizes, ** pSops;
04544     int i, k, b, Size;
04545 
04546     // map chars into their numbers
04547     for ( i = 0; i < 256; i++ )
04548         Map[i] = -1;
04549     for ( i = 0; i < 81; i++ )
04550         Map[s_Data3[i]] = i;
04551 
04552     // count the number of strings
04553     for ( Size = 0; s_Data4[Size] && Size < 100000; Size++ );
04554     assert( Size < 100000 );
04555 
04556     // allocate memory
04557     pMemory = ALLOC( char, Size * 75 );
04558     // copy the array into memory
04559     for ( i = 0; i < Size; i++ )
04560         for ( k = 0; k < 75; k++ )
04561             if ( s_Data4[i][k] == ' ' )
04562                 pMemory[i*75+k] = -1;
04563             else
04564                 pMemory[i*75+k] = Map[s_Data4[i][k]];
04565 
04566     // set pointers and compute SOP sizes
04567     pSopSizes = ALLOC( char, 65536 );
04568     pSops = ALLOC( char *, 65536 );
04569     pSopSizes[0] = 0;
04570     pSops[0] = NULL;
04571     pPrev = pMemory;
04572     for ( k = 0, i = 1; i < 65536; k++ )
04573         if ( pMemory[k] == -1 )
04574         {
04575             pSopSizes[i] = pMemory + k - pPrev; 
04576             pSops[i++] = pPrev;
04577             pPrev = pMemory + k + 1;
04578         }
04579     *ppSopSizes = pSopSizes;
04580     *ppSops = pSops;
04581 
04582     // verify the results - derive truth table from SOP
04583     for ( i = 1; i < 65536; i++ )
04584     {
04585         int uTruth = 0, uCube, Lit;
04586         for ( k = 0; k < pSopSizes[i]; k++ )
04587         {
04588             uCube = 0xFFFF;
04589             Lit = pSops[i][k];
04590             for ( b = 3; b >= 0; b-- )
04591             {
04592                 if ( Lit % 3 == 0 )
04593                     uCube &= uMasks[b][0];
04594                 else if ( Lit % 3 == 1 )
04595                     uCube &= uMasks[b][1];
04596                 Lit = Lit / 3;
04597             }
04598             uTruth |= uCube;
04599         }
04600         assert( uTruth == i );
04601     }
04602 }

void Cnf_SopConvertToVector ( char *  pSop,
int  nCubes,
Vec_Int_t *  vCover 
)

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

FileName [cnfWrite.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG-to-CNF conversion.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
cnfWrite.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Writes the cover into the array.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file cnfWrite.c.

00043 {
00044     int Lits[4], Cube, iCube, i, b;
00045     Vec_IntClear( vCover );
00046     for ( i = 0; i < nCubes; i++ )
00047     {
00048         Cube = pSop[i];
00049         for ( b = 0; b < 4; b++ )
00050         {
00051             if ( Cube % 3 == 0 )
00052                 Lits[b] = 1;
00053             else if ( Cube % 3 == 1 )
00054                 Lits[b] = 2;
00055             else
00056                 Lits[b] = 0;
00057             Cube = Cube / 3;
00058         }
00059         iCube = 0;
00060         for ( b = 0; b < 4; b++ )
00061             iCube = (iCube << 2) | Lits[b];
00062         Vec_IntPush( vCover, iCube );
00063     }
00064 }

static Dar_Cut_t* Dar_ObjBestCut ( Aig_Obj_t *  pObj  )  [inline, static]

Definition at line 92 of file cnf.h.

00092 { Dar_Cut_t * pCut; int i; Dar_ObjForEachCut( pObj, pCut, i ) if ( pCut->fBest ) return pCut; return NULL; }

Generated on Tue Jan 5 12:18:14 2010 for abc70930 by  doxygen 1.6.1