From 8eef7f8326e715ea4e9e84f46487cf4657601c25 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 20 Feb 2006 08:01:00 -0800 Subject: Version abc60220 --- src/sat/csat/csat_apis.c | 356 ++++++++++++++++------------------------------- src/sat/csat/csat_apis.h | 99 ++++++++----- 2 files changed, 183 insertions(+), 272 deletions(-) (limited to 'src/sat/csat') diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index d25e42db..d286ea9c 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -17,14 +17,15 @@ ***********************************************************************/ #include "abc.h" -#include "fraig.h" #include "csat_apis.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -#define ABC_DEFAULT_TIMEOUT 60 // 60 seconds +#define ABC_DEFAULT_CONF_LIMIT 0 // limit on conflicts +#define ABC_DEFAULT_IMP_LIMIT 0 // limit on implications + struct ABC_ManagerStruct_t { @@ -37,19 +38,24 @@ struct ABC_ManagerStruct_t Extra_MmFlex_t * pMmNames; // memory manager for signal names // solving parameters int mode; // 0 = brute-force SAT; 1 = resource-aware FRAIG - int nSeconds; // time limit for pure SAT solving - Fraig_Params_t Params; // the set of parameters to call FRAIG package + int nConfLimit; // time limit for pure SAT solving + int nImpLimit; // time limit for pure SAT solving +// Fraig_Params_t Params; // the set of parameters to call FRAIG package // information about the target int nog; // the numbers of gates in the target Vec_Ptr_t * vNodes; // the gates in the target Vec_Int_t * vValues; // the values of gate's outputs in the target // solution - ABC_Target_ResultT * pResult; // the result of solving the target + CSAT_Target_ResultT * pResult; // the result of solving the target }; -static ABC_Target_ResultT * ABC_TargetResAlloc( int nVars ); +static CSAT_Target_ResultT * ABC_TargetResAlloc( int nVars ); static char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode ); +// procedures to start and stop the ABC framework +extern void Abc_Start(); +extern void Abc_Stop(); + // some external procedures extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName ); @@ -71,16 +77,18 @@ extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName ); ABC_Manager ABC_InitManager() { ABC_Manager_t * mng; + Abc_Start(); mng = ALLOC( ABC_Manager_t, 1 ); memset( mng, 0, sizeof(ABC_Manager_t) ); mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP ); - mng->pNtk->pName = util_strsav("csat_network"); + mng->pNtk->pName = Extra_UtilStrsav("csat_network"); mng->tName2Node = stmm_init_table(strcmp, stmm_strhash); mng->tNode2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash); mng->pMmNames = Extra_MmFlexStart(); mng->vNodes = Vec_PtrAlloc( 100 ); mng->vValues = Vec_IntAlloc( 100 ); - mng->nSeconds = ABC_DEFAULT_TIMEOUT; + mng->nConfLimit = ABC_DEFAULT_CONF_LIMIT; + mng->nImpLimit = ABC_DEFAULT_IMP_LIMIT; return mng; } @@ -95,7 +103,7 @@ ABC_Manager ABC_InitManager() SeeAlso [] ***********************************************************************/ -void ABC_QuitManager( ABC_Manager mng ) +void ABC_ReleaseManager( ABC_Manager mng ) { if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name ); if ( mng->tName2Node ) stmm_free_table( mng->tName2Node ); @@ -106,6 +114,7 @@ void ABC_QuitManager( ABC_Manager mng ) if ( mng->vValues ) Vec_IntFree( mng->vValues ); FREE( mng->pDumpFileName ); free( mng ); + Abc_Stop(); } /**Function************************************************************* @@ -119,7 +128,7 @@ void ABC_QuitManager( ABC_Manager mng ) SeeAlso [] ***********************************************************************/ -void ABC_SetSolveOption( ABC_Manager mng, enum ABC_OptionT option ) +void ABC_SetSolveOption( ABC_Manager mng, enum CSAT_OptionT option ) { mng->mode = option; if ( option == 0 ) @@ -160,23 +169,23 @@ int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, cha // consider different cases, create the node, and map the node into the name switch( type ) { - case ABC_BPI: - case ABC_BPPI: + case CSAT_BPI: + case CSAT_BPPI: if ( nofi != 0 ) { printf( "ABC_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 0; } // create the PI pObj = Abc_NtkCreatePi( mng->pNtk ); stmm_insert( mng->tNode2Name, (char *)pObj, name ); break; - case ABC_CONST: - case ABC_BAND: - case ABC_BNAND: - case ABC_BOR: - case ABC_BNOR: - case ABC_BXOR: - case ABC_BXNOR: - case ABC_BINV: - case ABC_BBUF: + case CSAT_CONST: + case CSAT_BAND: + case CSAT_BNAND: + case CSAT_BOR: + case CSAT_BNOR: + case CSAT_BXOR: + case CSAT_BXNOR: + case CSAT_BINV: + case CSAT_BBUF: // create the node pObj = Abc_NtkCreateNode( mng->pNtk ); // create the fanins @@ -189,51 +198,51 @@ int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, cha // create the node function switch( type ) { - case ABC_CONST: + case CSAT_CONST: if ( nofi != 0 ) { printf( "ABC_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; } pSop = Abc_SopCreateConst1( mng->pNtk->pManFunc ); break; - case ABC_BAND: + case CSAT_BAND: if ( nofi < 1 ) { printf( "ABC_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; } pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi, NULL ); break; - case ABC_BNAND: + case CSAT_BNAND: if ( nofi < 1 ) { printf( "ABC_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; } pSop = Abc_SopCreateNand( mng->pNtk->pManFunc, nofi ); break; - case ABC_BOR: + case CSAT_BOR: if ( nofi < 1 ) { printf( "ABC_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; } pSop = Abc_SopCreateOr( mng->pNtk->pManFunc, nofi, NULL ); break; - case ABC_BNOR: + case CSAT_BNOR: if ( nofi < 1 ) { printf( "ABC_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; } pSop = Abc_SopCreateNor( mng->pNtk->pManFunc, nofi ); break; - case ABC_BXOR: + case CSAT_BXOR: if ( nofi < 1 ) { printf( "ABC_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; } if ( nofi > 2 ) { printf( "ABC_AddGate: The XOR gate \"%s\" has more than two fanins.\n", name ); return 0; } pSop = Abc_SopCreateXor( mng->pNtk->pManFunc, nofi ); break; - case ABC_BXNOR: + case CSAT_BXNOR: if ( nofi < 1 ) { printf( "ABC_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; } if ( nofi > 2 ) { printf( "ABC_AddGate: The XNOR gate \"%s\" has more than two fanins.\n", name ); return 0; } pSop = Abc_SopCreateNxor( mng->pNtk->pManFunc, nofi ); break; - case ABC_BINV: + case CSAT_BINV: if ( nofi != 1 ) { printf( "ABC_AddGate: The inverter gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } pSop = Abc_SopCreateInv( mng->pNtk->pManFunc ); break; - case ABC_BBUF: + case CSAT_BBUF: if ( nofi != 1 ) { printf( "ABC_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } pSop = Abc_SopCreateBuf( mng->pNtk->pManFunc ); @@ -243,8 +252,8 @@ int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, cha } Abc_ObjSetData( pObj, pSop ); break; - case ABC_BPPO: - case ABC_BPO: + case CSAT_BPPO: + case CSAT_BPO: if ( nofi != 1 ) { printf( "ABC_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } // create the PO @@ -268,38 +277,46 @@ int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, cha /**Function************************************************************* - Synopsis [Checks integraty of the manager.] + Synopsis [This procedure also finalizes construction of the ABC network.] - Description [Checks if there are gates that are not used by any primary output. - If no such gates exist, return 1 else return 0.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -int ABC_Check_Integrity( ABC_Manager mng ) +void ABC_Network_Finalize( ABC_Manager mng ) { Abc_Ntk_t * pNtk = mng->pNtk; Abc_Obj_t * pObj; int i; - - // this procedure also finalizes construction of the ABC network - Abc_NtkFixNonDrivenNets( pNtk ); Abc_NtkForEachPi( pNtk, pObj, i ) Abc_NtkLogicStoreName( pObj, ABC_GetNodeName(mng, pObj) ); Abc_NtkForEachPo( pNtk, pObj, i ) Abc_NtkLogicStoreName( pObj, ABC_GetNodeName(mng, pObj) ); assert( Abc_NtkLatchNum(pNtk) == 0 ); +} - // make sure everything is okay with the network structure - if ( !Abc_NtkDoCheck( pNtk ) ) - { - printf( "ABC_Check_Integrity: The internal network check has failed.\n" ); - return 0; - } +/**Function************************************************************* + + Synopsis [Checks integraty of the manager.] + + Description [Checks if there are gates that are not used by any primary output. + If no such gates exist, return 1 else return 0.] + + SideEffects [] + + SeeAlso [] - // check that there is no dangling nodes +***********************************************************************/ +int ABC_Check_Integrity( ABC_Manager mng ) +{ + Abc_Ntk_t * pNtk = mng->pNtk; + Abc_Obj_t * pObj; + int i; + + // check that there are no dangling nodes Abc_NtkForEachNode( pNtk, pObj, i ) { if ( i == 0 ) @@ -310,6 +327,13 @@ int ABC_Check_Integrity( ABC_Manager mng ) return 0; } } + + // make sure everything is okay with the network structure + if ( !Abc_NtkDoCheck( pNtk ) ) + { + printf( "ABC_Check_Integrity: The internal network check has failed.\n" ); + return 0; + } return 1; } @@ -326,7 +350,7 @@ int ABC_Check_Integrity( ABC_Manager mng ) ***********************************************************************/ void ABC_SetTimeLimit( ABC_Manager mng, int runtime ) { - mng->nSeconds = runtime; + printf( "ABC_SetTimeLimit: The resource limit is not implemented (warning).\n" ); } /**Function************************************************************* @@ -345,6 +369,22 @@ void ABC_SetLearnLimit( ABC_Manager mng, int num ) printf( "ABC_SetLearnLimit: The resource limit is not implemented (warning).\n" ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void ABC_SetLearnBacktrackLimit( ABC_Manager mng, int num ) +{ + printf( "ABC_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" ); +} + /**Function************************************************************* Synopsis [] @@ -358,7 +398,7 @@ void ABC_SetLearnLimit( ABC_Manager mng, int num ) ***********************************************************************/ void ABC_SetSolveBacktrackLimit( ABC_Manager mng, int num ) { - printf( "ABC_SetSolveBacktrackLimit: The resource limit is not implemented (warning).\n" ); + mng->nConfLimit = num; } /**Function************************************************************* @@ -372,9 +412,9 @@ void ABC_SetSolveBacktrackLimit( ABC_Manager mng, int num ) SeeAlso [] ***********************************************************************/ -void ABC_SetLearnBacktrackLimit( ABC_Manager mng, int num ) +void ABC_SetSolveImplicationLimit( ABC_Manager mng, int num ) { - printf( "ABC_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" ); + mng->nImpLimit = num; } /**Function************************************************************* @@ -391,7 +431,7 @@ void ABC_SetLearnBacktrackLimit( ABC_Manager mng, int num ) void ABC_EnableDump( ABC_Manager mng, char * dump_file ) { FREE( mng->pDumpFileName ); - mng->pDumpFileName = util_strsav( dump_file ); + mng->pDumpFileName = Extra_UtilStrsav( dump_file ); } /**Function************************************************************* @@ -447,9 +487,6 @@ int ABC_AddTarget( ABC_Manager mng, int nog, char ** names, int * values ) ***********************************************************************/ void ABC_SolveInit( ABC_Manager mng ) { - Fraig_Params_t * pParams = &mng->Params; - int nWords1, nWords2, nWordsMin; - // check if the target is available assert( mng->nog == Vec_PtrSize(mng->vNodes) ); if ( mng->nog == 0 ) @@ -459,30 +496,8 @@ void ABC_SolveInit( ABC_Manager mng ) if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget ); // set the new target network - mng->pTarget = Abc_NtkCreateCone( mng->pNtk, mng->vNodes, mng->vValues ); - - // to determine the number of simulation patterns - // use the following strategy - // at least 64 words (32 words random and 32 words dynamic) - // no more than 256M for one circuit (128M + 128M) - nWords1 = 32; - nWords2 = (1<<27) / (Abc_NtkNodeNum(mng->pTarget) + Abc_NtkCiNum(mng->pTarget)); - nWordsMin = ABC_MIN( nWords1, nWords2 ); - - // set parameters for fraiging - memset( pParams, 0, sizeof(Fraig_Params_t) ); - pParams->nPatsRand = nWordsMin * 32; // the number of words of random simulation info - pParams->nPatsDyna = nWordsMin * 32; // the number of words of dynamic simulation info - pParams->nBTLimit = 10; // the max number of backtracks to perform at a node - pParams->nSeconds = mng->nSeconds; // the time out for the final proof - pParams->fFuncRed = mng->mode; // performs only one level hashing - pParams->fFeedBack = 1; // enables solver feedback - pParams->fDist1Pats = 1; // enables distance-1 patterns - pParams->fDoSparse = 0; // performs equiv tests for sparse functions - pParams->fChoicing = 0; // enables recording structural choices - pParams->fTryProve = 1; // tries to solve the final miter - pParams->fVerbose = 0; // the verbosiness flag - pParams->fVerboseP = 0; // the verbosiness flag for proof reporting + mng->pTarget = Abc_NtkCreateTarget( mng->pNtk, mng->vNodes, mng->vValues ); + } /**Function************************************************************* @@ -511,78 +526,35 @@ void ABC_AnalyzeTargets( ABC_Manager mng ) SeeAlso [] ***********************************************************************/ -enum ABC_StatusT ABC_Solve( ABC_Manager mng ) +enum CSAT_StatusT ABC_Solve( ABC_Manager mng ) { - Fraig_Man_t * pMan; - Abc_Ntk_t * pCnf; - int * pModel; int RetValue, i; // check if the target network is available if ( mng->pTarget == NULL ) { printf( "ABC_Solve: Target network is not derived by ABC_SolveInit().\n" ); return UNDETERMINED; } - // optimizations of the target go here - // for example, to enable one pass of rewriting, uncomment this line -// Abc_NtkRewrite( mng->pTarget, 0, 1, 0 ); + // try to prove the miter using a number of techniques + RetValue = Abc_NtkMiterProve( &mng->pTarget, mng->nConfLimit, mng->nImpLimit, 1, 1, 0 ); - if ( mng->mode == 0 ) // brute-force SAT - { - // transform the AIG into a logic network for efficient CNF construction - pCnf = Abc_NtkRenode( mng->pTarget, 0, 100, 1, 0, 0 ); - RetValue = Abc_NtkMiterSat( pCnf, mng->nSeconds, 0 ); - - // analyze the result - mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); - if ( RetValue == -1 ) - mng->pResult->status = UNDETERMINED; - else if ( RetValue == 1 ) - mng->pResult->status = UNSATISFIABLE; - else if ( RetValue == 0 ) - { - mng->pResult->status = SATISFIABLE; - // create the array of PI names and values - for ( i = 0; i < mng->pResult->no_sig; i++ ) - { - mng->pResult->names[i] = ABC_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given - mng->pResult->values[i] = pCnf->pModel[i]; - } - FREE( mng->pTarget->pModel ); - } - else assert( 0 ); - Abc_NtkDelete( pCnf ); - } - else if ( mng->mode == 1 ) // resource-aware fraiging + // analyze the result + mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); + if ( RetValue == -1 ) + mng->pResult->status = UNDETERMINED; + else if ( RetValue == 1 ) + mng->pResult->status = UNSATISFIABLE; + else if ( RetValue == 0 ) { - // transform the target into a fraig - pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0, 0 ); - Fraig_ManProveMiter( pMan ); - RetValue = Fraig_ManCheckMiter( pMan ); - - // analyze the result - mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); - if ( RetValue == -1 ) - mng->pResult->status = UNDETERMINED; - else if ( RetValue == 1 ) - mng->pResult->status = UNSATISFIABLE; - else if ( RetValue == 0 ) + mng->pResult->status = SATISFIABLE; + // create the array of PI names and values + for ( i = 0; i < mng->pResult->no_sig; i++ ) { - mng->pResult->status = SATISFIABLE; - pModel = Fraig_ManReadModel( pMan ); - assert( pModel != NULL ); - // create the array of PI names and values - for ( i = 0; i < mng->pResult->no_sig; i++ ) - { - mng->pResult->names[i] = ABC_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given - mng->pResult->values[i] = pModel[i]; - } + mng->pResult->names[i] = Extra_UtilStrsav( ABC_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)) ); + mng->pResult->values[i] = mng->pTarget->pModel[i]; } - else assert( 0 ); - // delete the fraig manager - Fraig_ManFree( pMan ); + FREE( mng->pTarget->pModel ); } - else - assert( 0 ); + else assert( 0 ); // delete the target Abc_NtkDelete( mng->pTarget ); @@ -602,7 +574,7 @@ enum ABC_StatusT ABC_Solve( ABC_Manager mng ) SeeAlso [] ***********************************************************************/ -ABC_Target_ResultT * ABC_Get_Target_Result( ABC_Manager mng, int TargetID ) +CSAT_Target_ResultT * ABC_Get_Target_Result( ABC_Manager mng, int TargetID ) { return mng->pResult; } @@ -615,7 +587,7 @@ ABC_Target_ResultT * ABC_Get_Target_Result( ABC_Manager mng, int TargetID ) SideEffects [] - SeeAlso [] + SeeAlso [] ***********************************************************************/ void ABC_Dump_Bench_File( ABC_Manager mng ) @@ -647,11 +619,11 @@ void ABC_Dump_Bench_File( ABC_Manager mng ) SeeAlso [] ***********************************************************************/ -ABC_Target_ResultT * ABC_TargetResAlloc( int nVars ) +CSAT_Target_ResultT * ABC_TargetResAlloc( int nVars ) { - ABC_Target_ResultT * p; - p = ALLOC( ABC_Target_ResultT, 1 ); - memset( p, 0, sizeof(ABC_Target_ResultT) ); + CSAT_Target_ResultT * p; + p = ALLOC( CSAT_Target_ResultT, 1 ); + memset( p, 0, sizeof(CSAT_Target_ResultT) ); p->no_sig = nVars; p->names = ALLOC( char *, nVars ); p->values = ALLOC( int, nVars ); @@ -671,7 +643,7 @@ ABC_Target_ResultT * ABC_TargetResAlloc( int nVars ) SeeAlso [] ***********************************************************************/ -void ABC_TargetResFree( ABC_Target_ResultT * p ) +void ABC_TargetResFree( CSAT_Target_ResultT * p ) { if ( p == NULL ) return; @@ -702,100 +674,6 @@ char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode ) } - -/**Function************************************************************* - - Synopsis [This procedure applies a rewriting script to the network.] - - Description [Rewriting is performed without regard for the number of - logic levels. This corresponds to "circuit compression for formal - verification" (Per Bjesse et al, ICCAD 2004) but implemented in a more - exhaustive way than in the above paper.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void ABC_PerformRewriting( ABC_Manager mng ) -{ - void * pAbc; - char Command[1000]; - int clkBalan, clkResyn, clk; - int fPrintStats = 1; - int fUseResyn = 1; - - // procedures to get the ABC framework and execute commands in it - extern void * Abc_FrameGetGlobalFrame(); - extern void Abc_FrameReplaceCurrentNetwork( void * p, Abc_Ntk_t * pNtk ); - extern int Cmd_CommandExecute( void * p, char * sCommand ); - extern Abc_Ntk_t * Abc_FrameReadNtk( void * p ); - - - // get the pointer to the ABC framework - pAbc = Abc_FrameGetGlobalFrame(); - assert( pAbc != NULL ); - - // replace the current network by the target network - Abc_FrameReplaceCurrentNetwork( pAbc, mng->pTarget ); - -clk = clock(); - ////////////////////////////////////////////////////////////////////////// - // balance - sprintf( Command, "balance" ); - if ( Cmd_CommandExecute( pAbc, Command ) ) - { - fprintf( stdout, "Cannot execute command \"%s\".\n", Command ); - return; - } -clkBalan = clock() - clk; - - ////////////////////////////////////////////////////////////////////////// - // print stats - if ( fPrintStats ) - { - sprintf( Command, "print_stats" ); - if ( Cmd_CommandExecute( pAbc, Command ) ) - { - fprintf( stdout, "Cannot execute command \"%s\".\n", Command ); - return; - } - } - -clk = clock(); - ////////////////////////////////////////////////////////////////////////// - // synthesize - if ( fUseResyn ) - { - sprintf( Command, "balance; rewrite -l; rewrite -lz; balance; rewrite -lz; balance" ); - if ( Cmd_CommandExecute( pAbc, Command ) ) - { - fprintf( stdout, "Cannot execute command \"%s\".\n", Command ); - return; - } - } -clkResyn = clock() - clk; - - ////////////////////////////////////////////////////////////////////////// - // print stats - if ( fPrintStats ) - { - sprintf( Command, "print_stats" ); - if ( Cmd_CommandExecute( pAbc, Command ) ) - { - fprintf( stdout, "Cannot execute command \"%s\".\n", Command ); - return; - } - } - printf( "Balancing = %6.2f sec ", (float)(clkBalan)/(float)(CLOCKS_PER_SEC) ); - printf( "Rewriting = %6.2f sec ", (float)(clkResyn)/(float)(CLOCKS_PER_SEC) ); - printf( "\n" ); - - // read the target network from the current network - mng->pTarget = Abc_NtkDup( Abc_FrameReadNtk(pAbc) ); -} - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h index a6179710..faba9ee4 100644 --- a/src/sat/csat/csat_apis.h +++ b/src/sat/csat/csat_apis.h @@ -12,13 +12,17 @@ Date [Ver. 1.0. Started - August 28, 2005] - Revision [$Id: csat_apis.h,v 1.00 2005/08/28 00:00:00 alanmi Exp $] + Revision [$Id: csat_apis.h,v 1.5 2005/12/30 10:54:40 rmukherj Exp $] ***********************************************************************/ #ifndef __ABC_APIS_H__ #define __ABC_APIS_H__ +#ifdef __cplusplus +extern "C" { +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// @@ -42,27 +46,35 @@ typedef struct ABC_ManagerStruct_t * ABC_Manager; #define _ABC_GATE_TYPE_ enum GateType { - ABC_CONST = 0, // constant gate - ABC_BPI, // boolean PI - ABC_BPPI, // bit level PSEUDO PRIMARY INPUT - ABC_BAND, // bit level AND - ABC_BNAND, // bit level NAND - ABC_BOR, // bit level OR - ABC_BNOR, // bit level NOR - ABC_BXOR, // bit level XOR - ABC_BXNOR, // bit level XNOR - ABC_BINV, // bit level INVERTER - ABC_BBUF, // bit level BUFFER - ABC_BPPO, // bit level PSEUDO PRIMARY OUTPUT - ABC_BPO // boolean PO + CSAT_CONST = 0, // constant gate + CSAT_BPI, // boolean PI + CSAT_BPPI, // bit level PSEUDO PRIMARY INPUT + CSAT_BAND, // bit level AND + CSAT_BNAND, // bit level NAND + CSAT_BOR, // bit level OR + CSAT_BNOR, // bit level NOR + CSAT_BXOR, // bit level XOR + CSAT_BXNOR, // bit level XNOR + CSAT_BINV, // bit level INVERTER + CSAT_BBUF, // bit level BUFFER + CSAT_BMUX, // bit level MUX --not supported + CSAT_BDFF, // bit level D-type FF + CSAT_BSDFF, // bit level scan FF --not supported + CSAT_BTRIH, // bit level TRISTATE gate with active high control --not supported + CSAT_BTRIL, // bit level TRISTATE gate with active low control --not supported + CSAT_BBUS, // bit level BUS --not supported + CSAT_BPPO, // bit level PSEUDO PRIMARY OUTPUT + CSAT_BPO, // boolean PO + CSAT_BCNF, // boolean constraint + CSAT_BDC, // boolean don't care gate (2 input) }; #endif -//ABC_StatusT defines the return value by ABC_Solve(); +//CSAT_StatusT defines the return value by ABC_Solve(); #ifndef _ABC_STATUS_ #define _ABC_STATUS_ -enum ABC_StatusT +enum CSAT_StatusT { UNDETERMINED = 0, UNSATISFIABLE, @@ -76,11 +88,23 @@ enum ABC_StatusT #endif -// ABC_OptionT defines the solver option about learning +// to identify who called the CSAT solver +#ifndef _ABC_CALLER_ +#define _ABC_CALLER_ +enum CSAT_CallerT +{ + BLS = 0, + SATORI, + NONE +}; +#endif + + +// CSAT_OptionT defines the solver option about learning // which is used by ABC_SetSolveOption(); #ifndef _ABC_OPTION_ #define _ABC_OPTION_ -enum ABC_OptionT +enum CSAT_OptionT { BASE_LINE = 0, IMPLICT_LEARNING, //default @@ -91,10 +115,10 @@ enum ABC_OptionT #ifndef _ABC_Target_Result #define _ABC_Target_Result -typedef struct _ABC_Target_ResultT ABC_Target_ResultT; -struct _ABC_Target_ResultT +typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT; +struct _CSAT_Target_ResultT { - enum ABC_StatusT status; // solve status of the target + enum CSAT_StatusT status; // solve status of the target int num_dec; // num of decisions to solve the target int num_imp; // num of implications to solve the target int num_cftg; // num of conflict gates learned @@ -118,10 +142,13 @@ struct _ABC_Target_ResultT //////////////////////////////////////////////////////////////////////// // create a new manager -extern ABC_Manager ABC_InitManager(void); +extern ABC_Manager ABC_InitManager(void); + +// release a manager +extern void ABC_ReleaseManager(ABC_Manager mng); // set solver options for learning -extern void ABC_SetSolveOption(ABC_Manager mng, enum ABC_OptionT option); +extern void ABC_SetSolveOption(ABC_Manager mng, enum CSAT_OptionT option); // add a gate to the circuit // the meaning of the parameters are: @@ -130,16 +157,19 @@ extern void ABC_SetSolveOption(ABC_Manager mng, enum ABC_Option // nofi: number of fanins of the gate to be added; // fanins: the name array of fanins of the gate to be added extern int ABC_AddGate(ABC_Manager mng, - enum GateType type, - char* name, - int nofi, - char** fanins, - int dc_attr); + enum GateType type, + char* name, + int nofi, + char** fanins, + int dc_attr); // check if there are gates that are not used by any primary ouput. // if no such gates exist, return 1 else return 0; extern int ABC_Check_Integrity(ABC_Manager mng); +// THIS PROCEDURE SHOULD BE CALLED AFTER THE NETWORK IS CONSTRUCTED!!! +extern void ABC_Network_Finalize( ABC_Manager mng ); + // set time limit for solving a target. // runtime: time limit (in second). extern void ABC_SetTimeLimit(ABC_Manager mng, int runtime); @@ -160,21 +190,24 @@ extern void ABC_SolveInit(ABC_Manager mng); extern void ABC_AnalyzeTargets(ABC_Manager mng); // solve the targets added by ABC_AddTarget() -extern enum ABC_StatusT ABC_Solve(ABC_Manager mng); +extern enum CSAT_StatusT ABC_Solve(ABC_Manager mng); // get the solve status of a target // TargetID: the target id returned by ABC_AddTarget(). -extern ABC_Target_ResultT * ABC_Get_Target_Result(ABC_Manager mng, int TargetID); +extern CSAT_Target_ResultT * ABC_Get_Target_Result(ABC_Manager mng, int TargetID); extern void ABC_Dump_Bench_File(ABC_Manager mng); // ADDED PROCEDURES: -extern void ABC_QuitManager( ABC_Manager mng ); -extern void ABC_TargetResFree( ABC_Target_ResultT * p ); +extern void ABC_TargetResFree( CSAT_Target_ResultT * p ); -extern void ABC_PerformRewriting( ABC_Manager mng ); +extern void CSAT_SetCaller(ABC_Manager mng, enum CSAT_CallerT caller); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// +#ifdef __cplusplus +} +#endif + #endif -- cgit v1.2.3