diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
commit | 4812c90424dfc40d26725244723887a2d16ddfd9 (patch) | |
tree | b32ace96e7e2d84d586e09ba605463b6f49c3271 /src/aig/cnf/cnfCore.c | |
parent | e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (diff) | |
download | abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.gz abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.bz2 abc-4812c90424dfc40d26725244723887a2d16ddfd9.zip |
Version abc71001
Diffstat (limited to 'src/aig/cnf/cnfCore.c')
-rw-r--r-- | src/aig/cnf/cnfCore.c | 185 |
1 files changed, 185 insertions, 0 deletions
diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c new file mode 100644 index 00000000..06731451 --- /dev/null +++ b/src/aig/cnf/cnfCore.c @@ -0,0 +1,185 @@ +/**CFile**************************************************************** + + FileName [cnfCore.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: cnfCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cnf.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Cnf_Man_t * s_pManCnf = NULL; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Converts AIG into the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs ) +{ + Cnf_Man_t * p; + Cnf_Dat_t * pCnf; + Vec_Ptr_t * vMapped; + Aig_MmFixed_t * pMemCuts; + int clk; + // allocate the CNF manager + if ( s_pManCnf == NULL ) + s_pManCnf = Cnf_ManStart(); + // connect the managers + p = s_pManCnf; + p->pManAig = pAig; + + // generate cuts for all nodes, assign cost, and find best cuts +clk = clock(); + pMemCuts = Dar_ManComputeCuts( pAig, 10 ); +p->timeCuts = clock() - clk; + + // find the mapping +clk = clock(); + Cnf_DeriveMapping( p ); +p->timeMap = clock() - clk; +// Aig_ManScanMapping( p, 1 ); + + // convert it into CNF +clk = clock(); + Cnf_ManTransferCuts( p ); + vMapped = Cnf_ManScanMapping( p, 1, 1 ); + pCnf = Cnf_ManWriteCnf( p, vMapped, nOutputs ); + Vec_PtrFree( vMapped ); + Aig_MmFixedStop( pMemCuts, 0 ); +p->timeSave = clock() - clk; + + // reset reference counters + Aig_ManResetRefs( pAig ); +//PRT( "Cuts ", p->timeCuts ); +//PRT( "Map ", p->timeMap ); +//PRT( "Saving ", p->timeSave ); + return pCnf; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cnf_Man_t * Cnf_ManRead() +{ + return s_pManCnf; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cnf_ClearMemory() +{ + if ( s_pManCnf == NULL ) + return; + Cnf_ManStop( s_pManCnf ); + s_pManCnf = NULL; +} + + +#if 0 + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cnf_Dat_t * Cnf_Derive_old( Aig_Man_t * pAig ) +{ +/* + // iteratively improve area flow + for ( i = 0; i < nIters; i++ ) + { +clk = clock(); + Cnf_ManScanMapping( p, 0 ); + Cnf_ManMapForCnf( p ); +PRT( "iter ", clock() - clk ); + } +*/ + // write the file + vMapped = Aig_ManScanMapping( p, 1 ); + Vec_PtrFree( vMapped ); + +clk = clock(); + Cnf_ManTransferCuts( p ); + + Cnf_ManPostprocess( p ); + Cnf_ManScanMapping( p, 0 ); +/* + Cnf_ManPostprocess( p ); + Cnf_ManScanMapping( p, 0 ); + Cnf_ManPostprocess( p ); + Cnf_ManScanMapping( p, 0 ); +*/ +PRT( "Ext ", clock() - clk ); + +/* + vMapped = Cnf_ManScanMapping( p, 1 ); + pCnf = Cnf_ManWriteCnf( p, vMapped ); + Vec_PtrFree( vMapped ); + + // clean up + Cnf_ManFreeCuts( p ); + Dar_ManCutsFree( pAig ); + return pCnf; +*/ + Aig_MmFixedStop( pMemCuts, 0 ); + return NULL; +} + +#endif + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |