diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-14 21:20:37 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-14 21:20:37 -0700 |
commit | 117bc0dbcd4265eb04ed0c47979ec5953a983879 (patch) | |
tree | b71bba56a80267c691cfa62a7a59757441b8006e /src/sat | |
parent | f64bb36fd5081853e0c35ce3d525f2e7041c07ea (diff) | |
download | abc-117bc0dbcd4265eb04ed0c47979ec5953a983879.tar.gz abc-117bc0dbcd4265eb04ed0c47979ec5953a983879.tar.bz2 abc-117bc0dbcd4265eb04ed0c47979ec5953a983879.zip |
Prepared &gla to try abstracting and proving concurrently.
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/cnf/cnf.h | 5 | ||||
-rw-r--r-- | src/sat/cnf/cnfCore.c | 93 |
2 files changed, 47 insertions, 51 deletions
diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h index 1119db3e..f4c96709 100644 --- a/src/sat/cnf/cnf.h +++ b/src/sat/cnf/cnf.h @@ -127,9 +127,12 @@ static inline void Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut /*=== cnfCore.c ========================================================*/ extern Vec_Int_t * Cnf_DeriveMappingArray( Aig_Man_t * pAig ); extern Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs ); +extern Cnf_Dat_t * Cnf_DeriveWithMan( Cnf_Man_t * p, Aig_Man_t * pAig, int nOutputs ); extern Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig, int fSkipTtMin ); +extern Cnf_Dat_t * Cnf_DeriveOtherWithMan( Cnf_Man_t * p, Aig_Man_t * pAig, int fSkipTtMin ); +extern void Cnf_ManPrepare(); extern Cnf_Man_t * Cnf_ManRead(); -extern void Cnf_ClearMemory(); +extern void Cnf_ManFree(); /*=== cnfCut.c ========================================================*/ extern Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Aig_Obj_t * pObj ); extern void Cnf_CutPrint( Cnf_Cut_t * pCut ); diff --git a/src/sat/cnf/cnfCore.c b/src/sat/cnf/cnfCore.c index f08ea6d1..b32d0c7a 100644 --- a/src/sat/cnf/cnfCore.c +++ b/src/sat/cnf/cnfCore.c @@ -32,6 +32,37 @@ static Cnf_Man_t * s_pManCnf = NULL; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cnf_ManPrepare() +{ + if ( s_pManCnf == NULL ) + { + printf( "\n\nCreating CNF manager!!!!!\n\n" ); + s_pManCnf = Cnf_ManStart(); + } +} +Cnf_Man_t * Cnf_ManRead() +{ + return s_pManCnf; +} +void Cnf_ManFree() +{ + if ( s_pManCnf == NULL ) + return; + Cnf_ManStop( s_pManCnf ); + s_pManCnf = NULL; +} + /**Function************************************************************* @@ -52,10 +83,7 @@ Vec_Int_t * Cnf_DeriveMappingArray( Aig_Man_t * pAig ) Aig_MmFixed_t * pMemCuts; clock_t clk; // allocate the CNF manager - if ( s_pManCnf == NULL ) - s_pManCnf = Cnf_ManStart(); - // connect the managers - p = s_pManCnf; + p = Cnf_ManStart(); p->pManAig = pAig; // generate cuts for all nodes, assign cost, and find best cuts @@ -83,6 +111,7 @@ p->timeSave = clock() - clk; //ABC_PRT( "Cuts ", p->timeCuts ); //ABC_PRT( "Map ", p->timeMap ); //ABC_PRT( "Saving ", p->timeSave ); + Cnf_ManStop( p ); return vResult; } @@ -97,18 +126,13 @@ p->timeSave = clock() - clk; SeeAlso [] ***********************************************************************/ -Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs ) +Cnf_Dat_t * Cnf_DeriveWithMan( Cnf_Man_t * p, Aig_Man_t * pAig, int nOutputs ) { - Cnf_Man_t * p; Cnf_Dat_t * pCnf; Vec_Ptr_t * vMapped; Aig_MmFixed_t * pMemCuts; clock_t 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 @@ -138,6 +162,11 @@ p->timeSave = clock() - clk; //ABC_PRT( "Saving ", p->timeSave ); return pCnf; } +Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs ) +{ + Cnf_ManPrepare(); + return Cnf_DeriveWithMan( s_pManCnf, pAig, nOutputs ); +} /**Function************************************************************* @@ -150,18 +179,13 @@ p->timeSave = clock() - clk; SeeAlso [] ***********************************************************************/ -Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig, int fSkipTtMin ) +Cnf_Dat_t * Cnf_DeriveOtherWithMan( Cnf_Man_t * p, Aig_Man_t * pAig, int fSkipTtMin ) { - Cnf_Man_t * p; Cnf_Dat_t * pCnf; Vec_Ptr_t * vMapped; Aig_MmFixed_t * pMemCuts; clock_t 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 @@ -192,43 +216,12 @@ p->timeSave = clock() - clk; //ABC_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() +Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig, int fSkipTtMin ) { - if ( s_pManCnf == NULL ) - return; - Cnf_ManStop( s_pManCnf ); - s_pManCnf = NULL; + Cnf_ManPrepare(); + return Cnf_DeriveOtherWithMan( s_pManCnf, pAig, fSkipTtMin ); } - #if 0 /**Function************************************************************* |