diff options
Diffstat (limited to 'src/aig/cnf/cnfCore.c')
-rw-r--r-- | src/aig/cnf/cnfCore.c | 97 |
1 files changed, 89 insertions, 8 deletions
diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c index a3a7efaa..7480d45d 100644 --- a/src/aig/cnf/cnfCore.c +++ b/src/aig/cnf/cnfCore.c @@ -24,13 +24,15 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static Cnf_Man_t * s_pManCnf = NULL; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [] + Synopsis [Converts AIG into the SAT solver.] Description [] @@ -39,21 +41,97 @@ SeeAlso [] ***********************************************************************/ -Cnf_Dat_t * Cnf_Derive( Cnf_Man_t * p, Aig_Man_t * pAig ) +Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig ) { - Aig_MmFixed_t * pMemCuts; - Cnf_Dat_t * pCnf = NULL; + Cnf_Man_t * p; + Cnf_Dat_t * pCnf; Vec_Ptr_t * vMapped; - int nIters = 2; + 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 ); -PRT( "Cuts", clock() - clk ); + 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 ); + Vec_PtrFree( vMapped ); + Aig_MmFixedStop( pMemCuts, 0 ); +p->timeSave = clock() - clk; + +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++ ) @@ -95,6 +173,9 @@ PRT( "Ext ", clock() - clk ); return NULL; } +#endif + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |