src/aig/cnf/cnfWrite.c File Reference

#include "cnf.h"
Include dependency graph for cnfWrite.c:

Go to the source code of this file.

Functions

void Cnf_SopConvertToVector (char *pSop, int nCubes, Vec_Int_t *vCover)
int Cnf_SopCountLiterals (char *pSop, int nCubes)
int Cnf_IsopCountLiterals (Vec_Int_t *vIsop, int nVars)
int Cnf_IsopWriteCube (int Cube, int nVars, int *pVars, int *pLiterals)
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)

Function Documentation

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 }

int Cnf_IsopCountLiterals ( Vec_Int_t *  vIsop,
int  nVars 
)

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

Synopsis [Returns the number of literals in the SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file cnfWrite.c.

00105 {
00106     int nLits = 0, Cube, i, b;
00107     Vec_IntForEachEntry( vIsop, Cube, i )
00108     {
00109         for ( b = 0; b < nVars; b++ )
00110         {
00111             if ( (Cube & 3) == 1 || (Cube & 3) == 2 )
00112                 nLits++;
00113             Cube >>= 2;
00114         }
00115     }
00116     return nLits;
00117 }

int Cnf_IsopWriteCube ( int  Cube,
int  nVars,
int *  pVars,
int *  pLiterals 
)

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

Synopsis [Writes the cube and returns the number of literals in it.]

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file cnfWrite.c.

00131 {
00132     int nLits = nVars, b;
00133     for ( b = 0; b < nVars; b++ )
00134     {
00135         if ( (Cube & 3) == 1 ) // value 0 --> write positive literal
00136             *pLiterals++ = 2 * pVars[b];
00137         else if ( (Cube & 3) == 2 ) // value 1 --> write negative literal
00138             *pLiterals++ = 2 * pVars[b] + 1;
00139         else
00140             nLits--;
00141         Cube >>= 2;
00142     }
00143     return nLits;
00144 }

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 }

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 }

int Cnf_SopCountLiterals ( char *  pSop,
int  nCubes 
)

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

Synopsis [Returns the number of literals in the SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file cnfWrite.c.

00078 {
00079     int nLits = 0, Cube, i, b;
00080     for ( i = 0; i < nCubes; i++ )
00081     {
00082         Cube = pSop[i];
00083         for ( b = 0; b < 4; b++ )
00084         {
00085             if ( Cube % 3 != 2 )
00086                 nLits++;
00087             Cube = Cube / 3;
00088         }
00089     }
00090     return nLits;
00091 }

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