From c0ef1f469a3204adbd26edec0b9d3af56532d794 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 18 Jan 2006 08:01:00 -0800 Subject: Version abc60118 --- src/sat/aig/aig.h | 64 ++++++- src/sat/aig/aigMan.c | 15 +- src/sat/aig/aigMem.c | 2 +- src/sat/aig/aigNode.c | 7 +- src/sat/aig/aigTable.c | 19 +- src/sat/aig/aigUtil.c | 130 +++++++++++++ src/sat/aig/fraigClass.c | 60 ++++-- src/sat/aig/fraigCnf.c | 476 ++++++++++++++++++++++++++++++++++++++++++++++ src/sat/aig/fraigCore.c | 86 ++++++++- src/sat/aig/fraigEngine.c | 131 +++++++++++++ src/sat/aig/fraigProve.c | 4 +- src/sat/aig/fraigSim.c | 184 +++++++++++++----- src/sat/aig/fraigSolver.c | 47 +++++ src/sat/aig/fraigTrav.c | 47 +++++ src/sat/csat/csat_apis.c | 182 +++++++++--------- src/sat/csat/csat_apis.h | 106 +++++------ src/sat/fraig/fraigMem.c | 2 +- src/sat/msat/msatMem.c | 2 +- 18 files changed, 1333 insertions(+), 231 deletions(-) create mode 100644 src/sat/aig/fraigCnf.c create mode 100644 src/sat/aig/fraigEngine.c create mode 100644 src/sat/aig/fraigSolver.c create mode 100644 src/sat/aig/fraigTrav.c (limited to 'src/sat') diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h index 009a17bb..55a75cf5 100644 --- a/src/sat/aig/aig.h +++ b/src/sat/aig/aig.h @@ -48,6 +48,7 @@ //////////////////////////////////////////////////////////////////////// #include +#include "solver.h" #include "vec.h" //////////////////////////////////////////////////////////////////////// @@ -70,6 +71,7 @@ typedef struct Aig_Edge_t_ Aig_Edge_t; typedef struct Aig_MemFixed_t_ Aig_MemFixed_t; typedef struct Aig_SimInfo_t_ Aig_SimInfo_t; typedef struct Aig_Table_t_ Aig_Table_t; +typedef struct Aig_Pattern_t_ Aig_Pattern_t; // network types typedef enum { @@ -79,12 +81,25 @@ typedef enum { AIG_AND // 3: internal node } Aig_NodeType_t; +// proof outcomes +typedef enum { + AIG_PROOF_NONE = 0, // 0: unknown + AIG_PROOF_SAT, // 1: primary input + AIG_PROOF_UNSAT, // 2: primary output + AIG_PROOF_TIMEOUT, // 3: primary output + AIG_PROOF_FAIL // 4: internal node +} Aig_ProofType_t; + + + // the AIG parameters struct Aig_Param_t_ { int nPatsRand; // the number of random patterns int nBTLimit; // backtrack limit at the intermediate nodes int nSeconds; // the runtime limit at the final miter + int fVerbose; // verbosity + int fSatVerbose; // verbosity of SAT }; // the AIG edge @@ -127,6 +142,13 @@ struct Aig_Man_t_ Vec_Ptr_t * vPos; // all POs Aig_Table_t * pTable; // structural hash table int nLevelMax; // the maximum level + // SAT solver and related structures + solver * pSat; + Vec_Int_t * vVar2Sat; // mapping of nodes into their SAT var numbers (for each node num) + Vec_Int_t * vSat2Var; // mapping of the SAT var numbers into nodes (for each SAT var) + Vec_Int_t * vPiSatNums; // the SAT variable numbers (for each PI) + int * pModel; // the satisfying assignment (for each PI) + int nMuxes; // the number of MUXes // fanout representation Vec_Ptr_t * vFanPivots; // fanout pivots Vec_Ptr_t * vFanFans0; // the next fanout of the first fanin @@ -136,6 +158,7 @@ struct Aig_Man_t_ int nTravIds; // the traversal ID // simulation info Aig_SimInfo_t * pInfo; // random and systematic sim info for PIs + Aig_SimInfo_t * pInfoPi; // temporary sim info for the PI nodes Aig_SimInfo_t * pInfoTemp; // temporary sim info for all nodes // simulation patterns int nPiWords; // the number of words in the PI info @@ -148,6 +171,14 @@ struct Aig_Man_t_ Vec_Ptr_t * vToReplace; // the nodes to replace }; +// the simulation patter +struct Aig_Pattern_t_ +{ + int nBits; + int nWords; + unsigned * pData; +}; + // the AIG simulation info struct Aig_SimInfo_t_ { @@ -166,9 +197,9 @@ struct Aig_SimInfo_t_ for ( i = 0; (i < Aig_ManPiNum(pMan)) && (((pNode) = Aig_ManPi(pMan, i)), 1); i++ ) #define Aig_ManForEachPo( pMan, pNode, i ) \ for ( i = 0; (i < Aig_ManPoNum(pMan)) && (((pNode) = Aig_ManPo(pMan, i)), 1); i++ ) -#define Aig_ManForEachAnd( pNtk, pNode, i ) \ +#define Aig_ManForEachAnd( pMan, pNode, i ) \ for ( i = 0; (i < Aig_ManNodeNum(pMan)) && (((pNode) = Aig_ManNode(pMan, i)), 1); i++ ) \ - if ( Aig_NodeIsAnd(pNode) ) {} else + if ( !Aig_NodeIsAnd(pNode) ) {} else // maximum/minimum operators #define AIG_MIN(a,b) (((a) < (b))? (a) : (b)) @@ -178,8 +209,12 @@ struct Aig_SimInfo_t_ /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -static inline int Aig_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); } +static inline int Aig_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); } +static inline int Aig_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } +static inline void Aig_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } +static inline void Aig_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } +static inline Aig_Node_t * Aig_ManConst1( Aig_Man_t * pMan ) { return pMan->pConst1; } static inline Aig_Node_t * Aig_ManNode( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vNodes, i); } static inline Aig_Node_t * Aig_ManPi( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vPis, i); } static inline Aig_Node_t * Aig_ManPo( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vPos, i); } @@ -216,7 +251,8 @@ static inline Aig_Node_t * Aig_NodeChild0( Aig_Node_t * pNode ) { return Aig_N static inline Aig_Node_t * Aig_NodeChild1( Aig_Node_t * pNode ) { return Aig_NotCond( Aig_NodeFanin1(pNode), Aig_NodeFaninC1(pNode) ); } static inline Aig_Node_t * Aig_NodeNextH( Aig_Node_t * pNode ) { return pNode->NextH? Aig_ManNode(pNode->pMan, pNode->NextH) : NULL; } static inline int Aig_NodeWhatFanin( Aig_Node_t * pNode, Aig_Node_t * pFanin ) { if ( Aig_NodeFaninId0(pNode) == pFanin->Id ) return 0; if ( Aig_NodeFaninId1(pNode) == pFanin->Id ) return 1; assert(0); return -1; } -static inline int Aig_NodeGetLevelNew( Aig_Node_t * pNode ) { return 1 + AIG_MAX(Aig_NodeFanin0(pNode)->Level, Aig_NodeFanin1(pNode)->Level); } +static inline int Aig_NodeGetLevelNew( Aig_Node_t * pNode ) { return 1 + AIG_MAX(Aig_NodeFanin0(pNode)->Level, Aig_NodeFanin1(pNode)->Level); } +static inline int Aig_NodeRequiredLevel( Aig_Node_t * pNode ) { return pNode->pMan->nLevelMax + 1 - pNode->LevelR; } static inline unsigned * Aig_SimInfoForNode( Aig_SimInfo_t * p, Aig_Node_t * pNode ) { assert( p->Type ); return p->pData + p->nWords * pNode->Id; } static inline unsigned * Aig_SimInfoForPi( Aig_SimInfo_t * p, int Num ) { assert( !p->Type ); return p->pData + p->nWords * Num; } @@ -268,6 +304,7 @@ extern void Aig_NodeDisconnectAnd( Aig_Node_t * pNode ); extern void Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot ); extern void Aig_NodePrint( Aig_Node_t * pNode ); extern char * Aig_NodeName( Aig_Node_t * pNode ); +extern void Aig_PrintNode( Aig_Node_t * pNode ); /*=== aigOper.c ==========================================================*/ extern Aig_Node_t * Aig_And( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 ); extern Aig_Node_t * Aig_Or( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 ); @@ -287,18 +324,33 @@ extern void Aig_TableResize( Aig_Man_t * pMan ); extern void Aig_TableRehash( Aig_Man_t * pMan ); /*=== aigUtil.c ==========================================================*/ extern void Aig_ManIncrementTravId( Aig_Man_t * pMan ); -extern void Aig_PrintNode( Aig_Node_t * pNode ); +extern bool Aig_NodeIsMuxType( Aig_Node_t * pNode ); +extern Aig_Node_t * Aig_NodeRecognizeMux( Aig_Node_t * pNode, Aig_Node_t ** ppNodeT, Aig_Node_t ** ppNodeE ); +/*=== fraigCore.c ==========================================================*/ +extern Aig_ProofType_t Aig_FraigProve( Aig_Man_t * pMan ); /*=== fraigClasses.c ==========================================================*/ extern Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfoAll ); +extern void Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses ); +/*=== fraigCnf.c ==========================================================*/ +extern Aig_ProofType_t Aig_ClauseSolverStart( Aig_Man_t * pMan ); +/*=== fraigEngine.c ==========================================================*/ +extern void Aig_EngineSimulateFirst( Aig_Man_t * p ); +extern int Aig_EngineSimulate( Aig_Man_t * p ); +extern void Aig_EngineSimulateRandomFirst( Aig_Man_t * p ); /*=== fraigSim.c ==========================================================*/ extern Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type ); extern void Aig_SimInfoClean( Aig_SimInfo_t * p ); extern void Aig_SimInfoRandom( Aig_SimInfo_t * p ); +extern void Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat ); extern void Aig_SimInfoResize( Aig_SimInfo_t * p ); extern void Aig_SimInfoFree( Aig_SimInfo_t * p ); -extern Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi ); +extern void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t * pInfoAll ); +extern Aig_Pattern_t * Aig_PatternAlloc( int nBits ); +extern void Aig_PatternClean( Aig_Pattern_t * pPat ); +extern void Aig_PatternRandom( Aig_Pattern_t * pPat ); +extern void Aig_PatternFree( Aig_Pattern_t * pPat ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/sat/aig/aigMan.c b/src/sat/aig/aigMan.c index 2058f6b0..3807d28a 100644 --- a/src/sat/aig/aigMan.c +++ b/src/sat/aig/aigMan.c @@ -66,10 +66,11 @@ Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam ) // start the manager p = ALLOC( Aig_Man_t, 1 ); memset( p, 0, sizeof(Aig_Man_t) ); - p->pParam = &p->Param; - p->nTravIds = 1; + p->pParam = &p->Param; + p->nTravIds = 1; + p->nPatsMax = 20; // set the defaults - *p->pParam = *pParam; + *p->pParam = *pParam; // start memory managers p->mmNodes = Aig_MemFixedStart( sizeof(Aig_Node_t) ); // allocate node arrays @@ -121,14 +122,22 @@ int Aig_ManCleanup( Aig_Man_t * pMan ) ***********************************************************************/ void Aig_ManStop( Aig_Man_t * p ) { + // SAT solver + if ( p->pSat ) solver_delete( p->pSat ); + if ( p->vVar2Sat ) Vec_IntFree( p->vVar2Sat ); + if ( p->vSat2Var ) Vec_IntFree( p->vSat2Var ); + if ( p->vPiSatNums ) Vec_IntFree( p->vPiSatNums ); + // fanouts if ( p->vFanPivots ) Vec_PtrFree( p->vFanPivots ); if ( p->vFanFans0 ) Vec_PtrFree( p->vFanFans0 ); if ( p->vFanFans1 ) Vec_PtrFree( p->vFanFans1 ); if ( p->vClasses ) Vec_VecFree( p->vClasses ); + // nodes Aig_MemFixedStop( p->mmNodes, 0 ); Vec_PtrFree( p->vNodes ); Vec_PtrFree( p->vPis ); Vec_PtrFree( p->vPos ); + // temporary Vec_PtrFree( p->vFanouts ); Vec_PtrFree( p->vToReplace ); Aig_TableFree( p->pTable ); diff --git a/src/sat/aig/aigMem.c b/src/sat/aig/aigMem.c index 280cf98b..32709bf6 100644 --- a/src/sat/aig/aigMem.c +++ b/src/sat/aig/aigMem.c @@ -201,7 +201,7 @@ void Aig_MemFixedRestart( Aig_MemFixed_t * p ) int i; char * pTemp; - // delocate all chunks except the first one + // deallocate all chunks except the first one for ( i = 1; i < p->nChunks; i++ ) free( p->pChunks[i] ); p->nChunks = 1; diff --git a/src/sat/aig/aigNode.c b/src/sat/aig/aigNode.c index afccd985..991cc7e5 100644 --- a/src/sat/aig/aigNode.c +++ b/src/sat/aig/aigNode.c @@ -46,6 +46,7 @@ static inline Aig_Node_t * Aig_NodeCreate( Aig_Man_t * p ) pNode = (Aig_Node_t *)Aig_MemFixedEntryFetch( p->mmNodes ); memset( pNode, 0, sizeof(Aig_Node_t) ); // assign the number and add to the array of nodes + pNode->pMan = p; pNode->Id = p->vNodes->nSize; Vec_PtrPush( p->vNodes, pNode ); return pNode; @@ -66,6 +67,7 @@ Aig_Node_t * Aig_NodeCreateConst( Aig_Man_t * p ) { Aig_Node_t * pNode; pNode = Aig_NodeCreate( p ); + pNode->Type = AIG_NONE; pNode->fPhase = 1; // sim value for 000... pattern return pNode; } @@ -86,7 +88,8 @@ Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p ) Aig_Node_t * pNode; pNode = Aig_NodeCreate( p ); Vec_PtrPush( p->vPis, pNode ); - pNode->fPhase = 0; // sim value for 000... pattern + pNode->Type = AIG_PI; + pNode->fPhase = 0; // sim value for 000... pattern return pNode; } @@ -105,6 +108,7 @@ Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin ) { Aig_Node_t * pNode; pNode = Aig_NodeCreate( p ); + pNode->Type = AIG_PO; Vec_PtrPush( p->vPos, pNode ); // connect to the fanin pNode->Fans[0].fComp = Aig_IsComplement(pFanin); @@ -134,6 +138,7 @@ Aig_Node_t * Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t { Aig_Node_t * pNode; pNode = Aig_NodeCreate( p ); + pNode->Type = AIG_AND; Aig_NodeConnectAnd( pFanin0, pFanin1, pNode ); return pNode; } diff --git a/src/sat/aig/aigTable.c b/src/sat/aig/aigTable.c index cfc94f6b..e6fe87d6 100644 --- a/src/sat/aig/aigTable.c +++ b/src/sat/aig/aigTable.c @@ -36,7 +36,7 @@ struct Aig_Table_t_ #define Aig_TableBinForEachEntry( pBin, pEnt ) \ for ( pEnt = pBin; \ pEnt; \ - pEnt = pEnt->NextH? Aig_ManNode(pEnt->pMan, pEnt->NextH) : NULL ) + pEnt = Aig_NodeNextH(pEnt) ) #define Aig_TableBinForEachEntrySafe( pBin, pEnt, pEnt2 ) \ for ( pEnt = pBin, \ pEnt2 = pEnt? Aig_NodeNextH(pEnt) : NULL; \ @@ -127,9 +127,8 @@ Aig_Node_t * Aig_TableLookupNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t Aig_Node_t * pAnd; unsigned Key; assert( Aig_Regular(p0)->Id < Aig_Regular(p1)->Id ); - assert( p0->pMan == p1->pMan ); // get the hash key for these two nodes - Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins ); + Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins ); // find the matching node in the table Aig_TableBinForEachEntry( pMan->pTable->pBins[Key], pAnd ) if ( p0 == Aig_NodeChild0(pAnd) && p1 == Aig_NodeChild1(pAnd) ) @@ -157,8 +156,8 @@ Aig_Node_t * Aig_TableInsertNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t Aig_TableResize( pMan ); // add the node to the corresponding linked list in the table Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins ); - pAnd->NextH = pMan->pTable->pBins[Key]->Id; - pMan->pTable->pBins[Key]->NextH = pAnd->Id; + pAnd->NextH = pMan->pTable->pBins[Key]? pMan->pTable->pBins[Key]->Id : 0; + pMan->pTable->pBins[Key] = pAnd; pMan->pTable->nEntries++; return pAnd; } @@ -195,7 +194,7 @@ void Aig_TableDeleteNode( Aig_Man_t * pMan, Aig_Node_t * pThis ) if ( pPlace == NULL ) pMan->pTable->pBins[Key] = Aig_NodeNextH(pThis); else - pPlace->NextH = pThis->Id; + pPlace->NextH = pThis->NextH; break; } assert( pThis == pAnd ); @@ -232,8 +231,8 @@ clk = clock(); Aig_TableBinForEachEntrySafe( pMan->pTable->pBins[i], pEnt, pEnt2 ) { Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), nBinsNew ); - pEnt->NextH = pBinsNew[Key]->Id; - pBinsNew[Key]->NextH = pEnt->Id; + pEnt->NextH = pBinsNew[Key]? pBinsNew[Key]->Id : 0; + pBinsNew[Key] = pEnt; Counter++; } assert( Counter == pMan->pTable->nEntries ); @@ -282,8 +281,8 @@ void Aig_TableRehash( Aig_Man_t * pMan ) } // rehash the node Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), pMan->pTable->nBins ); - pEnt->NextH = pBinsNew[Key]->Id; - pBinsNew[Key]->NextH = pEnt->Id; + pEnt->NextH = pBinsNew[Key]? pBinsNew[Key]->Id : 0; + pBinsNew[Key] = pEnt; Counter++; } assert( Counter == pMan->pTable->nEntries ); diff --git a/src/sat/aig/aigUtil.c b/src/sat/aig/aigUtil.c index a1c9ca44..40f7aba1 100644 --- a/src/sat/aig/aigUtil.c +++ b/src/sat/aig/aigUtil.c @@ -53,6 +53,136 @@ void Aig_ManIncrementTravId( Aig_Man_t * pMan ) } +/**Function************************************************************* + + Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Aig_NodeIsMuxType( Aig_Node_t * pNode ) +{ + Aig_Node_t * pNode0, * pNode1; + // check that the node is regular + assert( !Aig_IsComplement(pNode) ); + // if the node is not AND, this is not MUX + if ( !Aig_NodeIsAnd(pNode) ) + return 0; + // if the children are not complemented, this is not MUX + if ( !Aig_NodeFaninC0(pNode) || !Aig_NodeFaninC1(pNode) ) + return 0; + // get children + pNode0 = Aig_NodeFanin0(pNode); + pNode1 = Aig_NodeFanin1(pNode); + // if the children are not ANDs, this is not MUX + if ( !Aig_NodeIsAnd(pNode0) || !Aig_NodeIsAnd(pNode1) ) + return 0; + // otherwise the node is MUX iff it has a pair of equal grandchildren + return (Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC0(pNode1))) || + (Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC1(pNode1))) || + (Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC0(pNode1))) || + (Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC1(pNode1))); +} + +/**Function************************************************************* + + Synopsis [Recognizes what nodes are control and data inputs of a MUX.] + + Description [If the node is a MUX, returns the control variable C. + Assigns nodes T and E to be the then and else variables of the MUX. + Node C is never complemented. Nodes T and E can be complemented. + This function also recognizes EXOR/NEXOR gates as MUXes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Aig_NodeRecognizeMux( Aig_Node_t * pNode, Aig_Node_t ** ppNodeT, Aig_Node_t ** ppNodeE ) +{ + Aig_Node_t * pNode0, * pNode1; + assert( !Aig_IsComplement(pNode) ); + assert( Aig_NodeIsMuxType(pNode) ); + // get children + pNode0 = Aig_NodeFanin0(pNode); + pNode1 = Aig_NodeFanin1(pNode); + // find the control variable +// if ( pNode1->p1 == Fraig_Not(pNode2->p1) ) + if ( Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC0(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p1) ) + if ( Aig_NodeFaninC0(pNode0) ) + { // pNode2->p1 is positive phase of C + *ppNodeT = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2); + *ppNodeE = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2); + return Aig_NodeChild0(pNode1);//pNode2->p1; + } + else + { // pNode1->p1 is positive phase of C + *ppNodeT = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2); + *ppNodeE = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2); + return Aig_NodeChild0(pNode0);//pNode1->p1; + } + } +// else if ( pNode1->p1 == Fraig_Not(pNode2->p2) ) + else if ( Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC1(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p1) ) + if ( Aig_NodeFaninC0(pNode0) ) + { // pNode2->p2 is positive phase of C + *ppNodeT = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1); + *ppNodeE = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2); + return Aig_NodeChild1(pNode1);//pNode2->p2; + } + else + { // pNode1->p1 is positive phase of C + *ppNodeT = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2); + *ppNodeE = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1); + return Aig_NodeChild0(pNode0);//pNode1->p1; + } + } +// else if ( pNode1->p2 == Fraig_Not(pNode2->p1) ) + else if ( Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC0(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p2) ) + if ( Aig_NodeFaninC1(pNode0) ) + { // pNode2->p1 is positive phase of C + *ppNodeT = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2); + *ppNodeE = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1); + return Aig_NodeChild0(pNode1);//pNode2->p1; + } + else + { // pNode1->p2 is positive phase of C + *ppNodeT = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1); + *ppNodeE = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2); + return Aig_NodeChild1(pNode0);//pNode1->p2; + } + } +// else if ( pNode1->p2 == Fraig_Not(pNode2->p2) ) + else if ( Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC1(pNode1)) ) + { +// if ( Fraig_IsComplement(pNode1->p2) ) + if ( Aig_NodeFaninC1(pNode0) ) + { // pNode2->p2 is positive phase of C + *ppNodeT = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1); + *ppNodeE = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1); + return Aig_NodeChild1(pNode1);//pNode2->p2; + } + else + { // pNode1->p2 is positive phase of C + *ppNodeT = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1); + *ppNodeE = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1); + return Aig_NodeChild1(pNode0);//pNode1->p2; + } + } + assert( 0 ); // this is not MUX + return NULL; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/aig/fraigClass.c b/src/sat/aig/fraigClass.c index b3040e2a..2f2d3e0c 100644 --- a/src/sat/aig/fraigClass.c +++ b/src/sat/aig/fraigClass.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [aigFraig.c] + FileName [fraigClass.c] SystemName [ABC: Logic synthesis and verification system.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: fraigClass.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -25,7 +25,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static unsigned Aig_ManHashKey( unsigned * pData, int nWords ); +static unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -44,20 +44,24 @@ static unsigned Aig_ManHashKey( unsigned * pData, int nWords ); ***********************************************************************/ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo ) { - Vec_Vec_t * vClasses; // equivalence classes + Vec_Vec_t * vClasses; // equivalence classes stmm_table * tSim2Node; // temporary hash table hashing key into the class number Aig_Node_t * pNode; unsigned uKey; - int i, * pSpot, ClassNum; + int i, * pSpot, Entry, ClassNum; assert( pInfo->Type == 1 ); // fill in the hash table tSim2Node = stmm_init_table( stmm_numcmp, stmm_numhash ); vClasses = Vec_VecAlloc( 100 ); - Aig_ManForEachNode( p, pNode, i ) + // enumerate the nodes considered in the equivalence classes +// Aig_ManForEachNode( p, pNode, i ) + Vec_IntForEachEntry( p->vSat2Var, Entry, i ) { + pNode = Aig_ManNode( p, Entry ); + if ( Aig_NodeIsPo(pNode) ) continue; - uKey = Aig_ManHashKey( Aig_SimInfoForNode(pInfo, pNode), pInfo->nWords ); + uKey = Aig_ManHashKey( Aig_SimInfoForNode(pInfo, pNode), pInfo->nWords, pNode->fPhase ); if ( !stmm_find_or_add( tSim2Node, (char *)uKey, (char ***)&pSpot ) ) // does not exist *pSpot = (pNode->Id << 1) | 1; // save the node, and do nothing else if ( (*pSpot) & 1 ) // this is a node @@ -71,11 +75,24 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo ) } else // this is a class { - ClassNum = (*pSpot) >> 1; + ClassNum = ((*pSpot) >> 1); Vec_VecPush( vClasses, ClassNum, (void *)pNode->Id ); } } stmm_free_table( tSim2Node ); + + // print the classes + { + Vec_Ptr_t * vVec; + printf( "PI/PO = %4d/%4d. Nodes = %7d. SatVars = %7d. Non-trivial classes = %5d: \n", + Aig_ManPiNum(p), Aig_ManPoNum(p), + Aig_ManNodeNum(p) - Aig_ManPoNum(p), + Vec_IntSize(p->vSat2Var), Vec_VecSize(vClasses) ); + + Vec_VecForEachLevel( vClasses, vVec, i ) + printf( "%d ", Vec_PtrSize(vVec) ); + printf( "\n" ); + } return vClasses; } @@ -90,17 +107,38 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo ) SeeAlso [] ***********************************************************************/ -unsigned Aig_ManHashKey( unsigned * pData, int nWords ) +unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase ) { static int Primes[10] = { 1009, 2207, 3779, 4001, 4877, 5381, 6427, 6829, 7213, 7919 }; unsigned uKey; int i; uKey = 0; - for ( i = 0; i < nWords; i++ ) - uKey ^= pData[i] * Primes[i%10]; + if ( fPhase ) + for ( i = 0; i < nWords; i++ ) + uKey ^= Primes[i%10] * pData[i]; + else + for ( i = 0; i < nWords; i++ ) + uKey ^= Primes[i%10] * ~pData[i]; return uKey; } + +/**Function************************************************************* + + Synopsis [Updates the equivalence classes using the simulation info.] + + Description [Records successful simulation patterns into the pattern + storage.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses ) +{ +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/aig/fraigCnf.c b/src/sat/aig/fraigCnf.c new file mode 100644 index 00000000..913165b2 --- /dev/null +++ b/src/sat/aig/fraigCnf.c @@ -0,0 +1,476 @@ +/**CFile**************************************************************** + + FileName [fraigCnf.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: fraigCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Adds trivial clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ClauseTriv( solver * pSat, Aig_Node_t * pNode, Vec_Int_t * vVars ) +{ +//printf( "Adding triv %d. %d\n", Aig_Regular(pNode)->Id, (int)pSat->solver_stats.clauses ); + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond( Aig_Regular(pNode)->Data, Aig_IsComplement(pNode) ) ); +// Vec_IntPush( vVars, toLitCond( (int)Aig_Regular(pNode)->Id, Aig_IsComplement(pNode) ) ); + return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); +} + +/**Function************************************************************* + + Synopsis [Adds trivial clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ClauseAnd( solver * pSat, Aig_Node_t * pNode, Vec_Ptr_t * vSuper, Vec_Int_t * vVars ) +{ + int fComp1, Var, Var1, i; +//printf( "Adding AND %d. (%d) %d\n", pNode->Id, vSuper->nSize+1, (int)pSat->solver_stats.clauses ); + + assert( !Aig_IsComplement( pNode ) ); + assert( Aig_NodeIsAnd( pNode ) ); + +// nVars = solver_nvars(pSat); + Var = pNode->Data; +// Var = pNode->Id; + +// assert( Var < nVars ); + for ( i = 0; i < vSuper->nSize; i++ ) + { + // get the predecessor nodes + // get the complemented attributes of the nodes + fComp1 = Aig_IsComplement(vSuper->pArray[i]); + // determine the variable numbers + Var1 = Aig_Regular(vSuper->pArray[i])->Data; +// Var1 = (int)Aig_Regular(vSuper->pArray[i])->Id; + + // check that the variables are in the SAT manager +// assert( Var1 < nVars ); + + // suppose the AND-gate is A * B = C + // add !A => !C or A + !C + // fprintf( pFile, "%d %d 0%c", Var1, -Var, 10 ); + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(Var1, fComp1) ); + Vec_IntPush( vVars, toLitCond(Var, 1 ) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + } + + // add A & B => C or !A + !B + C +// fprintf( pFile, "%d %d %d 0%c", -Var1, -Var2, Var, 10 ); + vVars->nSize = 0; + for ( i = 0; i < vSuper->nSize; i++ ) + { + // get the predecessor nodes + // get the complemented attributes of the nodes + fComp1 = Aig_IsComplement(vSuper->pArray[i]); + // determine the variable numbers + Var1 = Aig_Regular(vSuper->pArray[i])->Data; +// Var1 = (int)Aig_Regular(vSuper->pArray[i])->Id; + // add this variable to the array + Vec_IntPush( vVars, toLitCond(Var1, !fComp1) ); + } + Vec_IntPush( vVars, toLitCond(Var, 0) ); + return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); +} + +/**Function************************************************************* + + Synopsis [Adds trivial clause.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ClauseMux( solver * pSat, Aig_Node_t * pNode, Aig_Node_t * pNodeC, Aig_Node_t * pNodeT, Aig_Node_t * pNodeE, Vec_Int_t * vVars ) +{ + int VarF, VarI, VarT, VarE, fCompT, fCompE; +//printf( "Adding mux %d. %d\n", pNode->Id, (int)pSat->solver_stats.clauses ); + + assert( !Aig_IsComplement( pNode ) ); + assert( Aig_NodeIsMuxType( pNode ) ); + // get the variable numbers + VarF = pNode->Data; + VarI = pNodeC->Data; + VarT = Aig_Regular(pNodeT)->Data; + VarE = Aig_Regular(pNodeE)->Data; +// VarF = (int)pNode->Id; +// VarI = (int)pNodeC->Id; +// VarT = (int)Aig_Regular(pNodeT)->Id; +// VarE = (int)Aig_Regular(pNodeE)->Id; + + // get the complementation flags + fCompT = Aig_IsComplement(pNodeT); + fCompE = Aig_IsComplement(pNodeE); + + // f = ITE(i, t, e) + // i' + t' + f + // i' + t + f' + // i + e' + f + // i + e + f' + // create four clauses + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarI, 1) ); + Vec_IntPush( vVars, toLitCond(VarT, 1^fCompT) ); + Vec_IntPush( vVars, toLitCond(VarF, 0) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarI, 1) ); + Vec_IntPush( vVars, toLitCond(VarT, 0^fCompT) ); + Vec_IntPush( vVars, toLitCond(VarF, 1) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarI, 0) ); + Vec_IntPush( vVars, toLitCond(VarE, 1^fCompE) ); + Vec_IntPush( vVars, toLitCond(VarF, 0) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarI, 0) ); + Vec_IntPush( vVars, toLitCond(VarE, 0^fCompE) ); + Vec_IntPush( vVars, toLitCond(VarF, 1) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + + if ( VarT == VarE ) + { +// assert( fCompT == !fCompE ); + return 1; + } + + // two additional clauses + // t' & e' -> f' t + e + f' + // t & e -> f t' + e' + f + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarT, 0^fCompT) ); + Vec_IntPush( vVars, toLitCond(VarE, 0^fCompE) ); + Vec_IntPush( vVars, toLitCond(VarF, 1) ); + if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) + return 0; + vVars->nSize = 0; + Vec_IntPush( vVars, toLitCond(VarT, 1^fCompT) ); + Vec_IntPush( vVars, toLitCond(VarE, 1^fCompE) ); + Vec_IntPush( vVars, toLitCond(VarF, 0) ); + return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); +} + +/**Function************************************************************* + + Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ClauseCollectSupergate_rec( Aig_Node_t * pNode, Vec_Ptr_t * vSuper, int fFirst, int fStopAtMux ) +{ + int RetValue1, RetValue2, i; + // check if the node is visited + if ( Aig_Regular(pNode)->fMarkB ) + { + // check if the node occurs in the same polarity + for ( i = 0; i < vSuper->nSize; i++ ) + if ( vSuper->pArray[i] == pNode ) + return 1; + // check if the node is present in the opposite polarity + for ( i = 0; i < vSuper->nSize; i++ ) + if ( vSuper->pArray[i] == Aig_Not(pNode) ) + return -1; + assert( 0 ); + return 0; + } + // if the new node is complemented or a PI, another gate begins + if ( !fFirst ) + if ( Aig_IsComplement(pNode) || !Aig_NodeIsAnd(pNode) || Aig_NodeRefs(pNode) > 1 || fStopAtMux && Aig_NodeIsMuxType(pNode) ) + { + Vec_PtrPush( vSuper, pNode ); + Aig_Regular(pNode)->fMarkB = 1; + return 0; + } + assert( !Aig_IsComplement(pNode) ); + assert( Aig_NodeIsAnd(pNode) ); + // go through the branches + RetValue1 = Aig_ClauseCollectSupergate_rec( Aig_NodeChild0(pNode), vSuper, 0, fStopAtMux ); + RetValue2 = Aig_ClauseCollectSupergate_rec( Aig_NodeChild1(pNode), vSuper, 0, fStopAtMux ); + if ( RetValue1 == -1 || RetValue2 == -1 ) + return -1; + // return 1 if at least one branch has a duplicate + return RetValue1 || RetValue2; +} + +/**Function************************************************************* + + Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ClauseCollectSupergate( Aig_Node_t * pNode, int fStopAtMux, Vec_Ptr_t * vNodes ) +{ + int RetValue, i; + assert( !Aig_IsComplement(pNode) ); + // collect the nodes in the implication supergate + Vec_PtrClear( vNodes ); + RetValue = Aig_ClauseCollectSupergate_rec( pNode, vNodes, 1, fStopAtMux ); + assert( vNodes->nSize > 1 ); + // unmark the visited nodes + for ( i = 0; i < vNodes->nSize; i++ ) + Aig_Regular((Aig_Node_t *)vNodes->pArray[i])->fMarkB = 0; + // if we found the node and its complement in the same implication supergate, + // return empty set of nodes (meaning that we should use constant-0 node) + if ( RetValue == -1 ) + vNodes->nSize = 0; +} + + +/**Function************************************************************* + + Synopsis [Sets up the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ClauseCreateCnfInt( solver * pSat, Aig_Man_t * pNtk ) +{ + Aig_Node_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE; + Vec_Ptr_t * vNodes, * vSuper; + Vec_Int_t * vVars; + int i, k, fUseMuxes = 1; + + // start the data structures + vNodes = Vec_PtrAlloc( 1000 ); // the nodes corresponding to vars in the solver + vSuper = Vec_PtrAlloc( 100 ); // the nodes belonging to the given implication supergate + vVars = Vec_IntAlloc( 100 ); // the temporary array for variables in the clause + + // add the clause for the constant node + pNode = Aig_ManConst1(pNtk); + pNode->fMarkA = 1; + pNode->Data = vNodes->nSize; + Vec_PtrPush( vNodes, pNode ); + Aig_ClauseTriv( pSat, pNode, vVars ); + + // collect the nodes that need clauses and top-level assignments + Aig_ManForEachPo( pNtk, pNode, i ) + { + // get the fanin + pFanin = Aig_NodeFanin0(pNode); + // create the node's variable + if ( pFanin->fMarkA == 0 ) + { + pFanin->fMarkA = 1; + pFanin->Data = vNodes->nSize; + Vec_PtrPush( vNodes, pFanin ); + } + // add the trivial clause + if ( !Aig_ClauseTriv( pSat, Aig_NodeChild0(pNode), vVars ) ) + return 0; + } + + // add the clauses + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + assert( !Aig_IsComplement(pNode) ); + if ( !Aig_NodeIsAnd(pNode) ) + continue; +//printf( "%d ", pNode->Id ); + + // add the clauses + if ( fUseMuxes && Aig_NodeIsMuxType(pNode) ) + { + pNode->pMan->nMuxes++; + pNodeC = Aig_NodeRecognizeMux( pNode, &pNodeT, &pNodeE ); + Vec_PtrClear( vSuper ); + Vec_PtrPush( vSuper, pNodeC ); + Vec_PtrPush( vSuper, pNodeT ); + Vec_PtrPush( vSuper, pNodeE ); + // add the fanin nodes to explore + Vec_PtrForEachEntry( vSuper, pFanin, k ) + { + pFanin = Aig_Regular(pFanin); + if ( pFanin->fMarkA == 0 ) + { + pFanin->fMarkA = 1; + pFanin->Data = vNodes->nSize; + Vec_PtrPush( vNodes, pFanin ); + } + } + // add the clauses + if ( !Aig_ClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) ) + return 0; + } + else + { + // get the supergate + Aig_ClauseCollectSupergate( pNode, fUseMuxes, vSuper ); + // add the fanin nodes to explore + Vec_PtrForEachEntry( vSuper, pFanin, k ) + { + pFanin = Aig_Regular(pFanin); + if ( pFanin->fMarkA == 0 ) + { + pFanin->fMarkA = 1; + pFanin->Data = vNodes->nSize; + Vec_PtrPush( vNodes, pFanin ); + } + } + // add the clauses + if ( vSuper->nSize == 0 ) + { + if ( !Aig_ClauseTriv( pSat, Aig_Not(pNode), vVars ) ) + return 0; + } + else + { + if ( !Aig_ClauseAnd( pSat, pNode, vSuper, vVars ) ) + return 0; + } + } + } + + // delete + Vec_IntFree( vVars ); + Vec_PtrFree( vNodes ); + Vec_PtrFree( vSuper ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Sets up the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +solver * Aig_ClauseCreateCnf( Aig_Man_t * pMan ) +{ + solver * pSat; + Aig_Node_t * pNode; + int RetValue, i, clk = clock(); + // clean the marks + Aig_ManForEachNode( pMan, pNode, i ) + pNode->fMarkA = 0, pNode->Data = -1; + // create the solver + pMan->nMuxes = 0; + pSat = solver_new(); + RetValue = Aig_ClauseCreateCnfInt( pSat, pMan ); +// Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 ); + if ( RetValue == 0 ) + { + solver_delete(pSat); + Aig_ManForEachNode( pMan, pNode, i ) + pNode->fMarkA = 0; + return NULL; + } + printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", + pNode->pMan->nMuxes, 300.0*pNode->pMan->nMuxes/Aig_ManNodeNum(pMan) ); + PRT( "Creating solver", clock() - clk ); + return pSat; +} + +/**Function************************************************************* + + Synopsis [Starts the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_ProofType_t Aig_ClauseSolverStart( Aig_Man_t * pMan ) +{ + Aig_Node_t * pNode; + int i; + + // make sure it has one PO + if ( Aig_ManPoNum(pMan) != 1 ) + { + printf( "The miter has other than 1 output.\n" ); + return AIG_PROOF_FAIL; + } + + // get the solver + assert( pMan->pSat == NULL ); + pMan->pSat = Aig_ClauseCreateCnf( pMan ); + if ( pMan->pSat == NULL ) + return AIG_PROOF_UNSAT; + + // get the variable mappings + pMan->vVar2Sat = Vec_IntStart( Aig_ManNodeNum(pMan) ); + pMan->vSat2Var = Vec_IntStart( solver_nvars(pMan->pSat) ); + Aig_ManForEachNode( pMan, pNode, i ) + { + Vec_IntWriteEntry( pMan->vVar2Sat, i, pNode->Data ); + if ( pNode->Data >= 0 ) Vec_IntWriteEntry( pMan->vSat2Var, pNode->Data, i ); + } + // get the SAT var numbers of the primary inputs + pMan->vPiSatNums = Vec_IntAlloc( Aig_ManPiNum(pMan) ); + Aig_ManForEachPi( pMan, pNode, i ) + Vec_IntPush( pMan->vPiSatNums, (pNode->Data >= 0)? pNode->Data : 0 ); + return AIG_PROOF_NONE; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/fraigCore.c b/src/sat/aig/fraigCore.c index 6187538b..e7df1335 100644 --- a/src/sat/aig/fraigCore.c +++ b/src/sat/aig/fraigCore.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [aigFraig.c] + FileName [fraigCore.c] SystemName [ABC: Logic synthesis and verification system.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: fraigCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -24,13 +24,56 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [] + Synopsis [Top-level equivalence checking procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_ProofType_t Aig_FraigProve( Aig_Man_t * pMan ) +{ + Aig_ProofType_t RetValue; + int clk, status; + + // create the solver + RetValue = Aig_ClauseSolverStart( pMan ); + if ( RetValue != AIG_PROOF_NONE ) + return RetValue; + // perform solving + + // simplify the problem + clk = clock(); + status = solver_simplify(pMan->pSat); + if ( status == 0 ) + { +// printf( "The problem is UNSATISFIABLE after simplification.\n" ); + return AIG_PROOF_UNSAT; + } + + // try to prove the output + RetValue = Aig_FraigProveOutput( pMan ); + if ( RetValue != AIG_PROOF_TIMEOUT ) + return RetValue; + + // create equivalence classes + Aig_EngineSimulateRandomFirst( pMan ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Top-level equivalence checking procedure.] Description [] @@ -39,6 +82,43 @@ SeeAlso [] ***********************************************************************/ +Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan ) +{ + Aig_ProofType_t RetValue; + int clk, status; + + // solve the miter + clk = clock(); + pMan->pSat->verbosity = pMan->pParam->fSatVerbose; + status = solver_solve( pMan->pSat, NULL, NULL, pMan->pParam->nSeconds ); + if ( status == l_Undef ) + { +// printf( "The problem timed out.\n" ); + RetValue = AIG_PROOF_TIMEOUT; + } + else if ( status == l_True ) + { +// printf( "The problem is SATISFIABLE.\n" ); + RetValue = AIG_PROOF_SAT; + } + else if ( status == l_False ) + { +// printf( "The problem is UNSATISFIABLE.\n" ); + RetValue = AIG_PROOF_UNSAT; + } + else + assert( 0 ); +// PRT( "SAT solver time", clock() - clk ); + + // if the problem is SAT, get the counterexample + if ( status == l_True ) + { + if ( pMan->pModel ) free( pMan->pModel ); + pMan->pModel = solver_get_model( pMan->pSat, pMan->vPiSatNums->pArray, pMan->vPiSatNums->nSize ); + printf( "%d %d %d %d\n", pMan->pModel[0], pMan->pModel[1], pMan->pModel[2], pMan->pModel[3] ); + } + return RetValue; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/sat/aig/fraigEngine.c b/src/sat/aig/fraigEngine.c new file mode 100644 index 00000000..6214bf3b --- /dev/null +++ b/src/sat/aig/fraigEngine.c @@ -0,0 +1,131 @@ +/**CFile**************************************************************** + + FileName [fraigEngine.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: fraigEngine.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the simulation engine for the first time.] + + Description [Tries several random patterns and their distance-1 + minterms hoping to get simulation started.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_EngineSimulateFirst( Aig_Man_t * p ) +{ + Aig_Pattern_t * pPat; + int i; + assert( Vec_PtrSize(p->vPats) == 0 ); + for ( i = 0; i < p->nPatsMax; i++ ) + { + pPat = Aig_PatternAlloc( Aig_ManPiNum(p) ); + Aig_PatternRandom( pPat ); + Vec_PtrPush( p->vPats, pPat ); + if ( !Aig_EngineSimulate( p ) ) + return; + } +} + +/**Function************************************************************* + + Synopsis [Implements intelligent simulation engine.] + + Description [Assumes that the good simulation patterns have been + assigned (p->vPats). Simulates until all of them are gone. Returns 1 + if some classes are left. Returns 0 if there is no more classes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_EngineSimulate( Aig_Man_t * p ) +{ + Aig_Pattern_t * pPat; + if ( Vec_VecSize(p->vClasses) == 0 ) + return 0; + assert( Vec_PtrSize(p->vPats) > 0 ); + // process patterns + while ( Vec_PtrSize(p->vPats) > 0 && Vec_VecSize(p->vClasses) > 0 ) + { + // get the pattern and create new siminfo + pPat = Vec_PtrPop(p->vPats); + // create the new siminfo + Aig_SimInfoFromPattern( p->pInfoPi, pPat ); + // free the patter + Aig_PatternFree( pPat ); + + // simulate this info + Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp ); + // split the classes and collect the new patterns + Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses ); + } + return Vec_VecSize(p->vClasses) > 0; +} + +/**Function************************************************************* + + Synopsis [Simulates all nodes using random simulation for the first time.] + + Description [Assigns the original simulation info and the storage for the + future simulation info.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_EngineSimulateRandomFirst( Aig_Man_t * p ) +{ + Aig_SimInfo_t * pInfoPi, * pInfoAll; + assert( !p->pInfo && !p->pInfoTemp ); + // create random PI info + pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 ); + Aig_SimInfoRandom( pInfoPi ); + // allocate sim info for all nodes + pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 ); + // simulate though the circuit + Aig_ManSimulateInfo( p, pInfoPi, pInfoAll ); + // detect classes + p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll ); + Aig_SimInfoFree( pInfoAll ); + // save simulation info + p->pInfo = pInfoPi; + p->pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->vPis->nSize), 0 ); + p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize), 1 ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/fraigProve.c b/src/sat/aig/fraigProve.c index b5cce582..901f2fe2 100644 --- a/src/sat/aig/fraigProve.c +++ b/src/sat/aig/fraigProve.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [aigProve.c] + FileName [fraigProve.c] SystemName [ABC: Logic synthesis and verification system.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: aigProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: fraigProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ diff --git a/src/sat/aig/fraigSim.c b/src/sat/aig/fraigSim.c index 1d547621..415b6918 100644 --- a/src/sat/aig/fraigSim.c +++ b/src/sat/aig/fraigSim.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [aigSim.c] + FileName [fraigSim.c] SystemName [ABC: Logic synthesis and verification system.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - June 20, 2005.] - Revision [$Id: aigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + Revision [$Id: fraigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -28,61 +28,30 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -/**Function************************************************************* - - Synopsis [Simulates all nodes using random simulation.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Aig_ManSimulateRandomFirst( Aig_Man_t * p ) -{ - Aig_SimInfo_t * pInfoPi, * pInfoAll; - assert( p->pInfo && p->pInfoTemp ); - // create random PI info - pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 ); - Aig_SimInfoRandom( pInfoPi ); - // simulate it though the circuit - pInfoAll = Aig_ManSimulateInfo( p, pInfoPi ); - // detect classes - p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll ); - Aig_SimInfoFree( pInfoAll ); - // save simulation info - p->pInfo = pInfoPi; - p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize), 1 ); -} - /**Function************************************************************* Synopsis [Simulates all nodes using the given simulation info.] - Description [] + Description [Returns the simulation info for all nodes.] SideEffects [] SeeAlso [] ***********************************************************************/ -Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi ) +void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t * pInfoAll ) { - Aig_SimInfo_t * pInfoAll; Aig_Node_t * pNode; - unsigned * pDataPi, * pData0, * pData1, * pDataAnd; + unsigned * pDataPi, * pDataPo, * pData0, * pData1, * pDataAnd; int i, k, fComp0, fComp1; assert( !pInfoPi->Type ); // PI siminfo - // allocate sim info for all nodes - pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 ); // set the constant sim info pData1 = Aig_SimInfoForNode( pInfoAll, p->pConst1 ); for ( k = 0; k < pInfoPi->nWords; k++ ) pData1[k] = ~((unsigned)0); - // copy the PI siminfo - Vec_PtrForEachEntry( p->vPis, pNode, i ) + // set the PI siminfo + Aig_ManForEachPi( p, pNode, i ) { pDataPi = Aig_SimInfoForPi( pInfoPi, i ); pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode ); @@ -90,10 +59,8 @@ Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi ) pDataAnd[k] = pDataPi[k]; } // simulate the nodes - Vec_PtrForEachEntry( p->vNodes, pNode, i ) + Aig_ManForEachAnd( p, pNode, i ) { - if ( !Aig_NodeIsAnd(pNode) ) - continue; pData0 = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) ); pData1 = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin1(pNode) ); pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode ); @@ -112,13 +79,25 @@ Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi ) for ( k = 0; k < pInfoPi->nWords; k++ ) pDataAnd[k] = pData0[k] & pData1[k]; } - return pInfoAll; + // derive the PO siminfo + Aig_ManForEachPi( p, pNode, i ) + { + pDataPo = Aig_SimInfoForNode( pInfoAll, pNode ); + pDataAnd = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) ); + if ( Aig_NodeFaninC0(pNode) ) + for ( k = 0; k < pInfoPi->nWords; k++ ) + pDataPo[k] = ~pDataAnd[k]; + else + for ( k = 0; k < pInfoPi->nWords; k++ ) + pDataPo[k] = pDataAnd[k]; + } } + /**Function************************************************************* - Synopsis [] + Synopsis [Allocates the simulation info.] Description [] @@ -142,7 +121,7 @@ Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type ) /**Function************************************************************* - Synopsis [] + Synopsis [Sets the simulation info to zero.] Description [] @@ -161,7 +140,7 @@ void Aig_SimInfoClean( Aig_SimInfo_t * p ) /**Function************************************************************* - Synopsis [] + Synopsis [Sets the random simulation info.] Description [] @@ -187,7 +166,40 @@ void Aig_SimInfoRandom( Aig_SimInfo_t * p ) /**Function************************************************************* - Synopsis [] + Synopsis [Sets the random simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat ) +{ + unsigned * pData; + int i, k; + assert( p->Type == 0 ); + assert( p->nNodes == pPat->nBits ); + for ( i = 0; i < p->nNodes; i++ ) + { + // get the pointer to the bitdata for node i + pData = p->pData + p->nWords * i; + // fill in the bit data according to the pattern + if ( Aig_InfoHasBit(pPat->pData, i) ) // PI has bit set to 1 + for ( k = 0; k < p->nWords; k++ ) + pData[k] = ~((unsigned)0); + else + for ( k = 0; k < p->nWords; k++ ) + pData[k] = 0; + // flip one bit + Aig_InfoXorBit( pData, i ); + } +} + +/**Function************************************************************* + + Synopsis [Resizes the simulation info.] Description [] @@ -209,13 +221,15 @@ void Aig_SimInfoResize( Aig_SimInfo_t * p ) for ( k = 0; k < p->nWords; k++ ) pData[2 * p->nWords * i + k + p->nWords] = 0; } - p->nPatsMax *= 2; p->nWords *= 2; + p->nPatsMax *= 2; + free( p->pData ); + p->pData = pData; } /**Function************************************************************* - Synopsis [] + Synopsis [Deallocates the simulation info.] Description [] @@ -231,6 +245,80 @@ void Aig_SimInfoFree( Aig_SimInfo_t * p ) } +/**Function************************************************************* + + Synopsis [Allocates the simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Pattern_t * Aig_PatternAlloc( int nBits ) +{ + Aig_Pattern_t * pPat; + pPat = ALLOC( Aig_Pattern_t, 1 ); + memset( pPat, 0, sizeof(Aig_Pattern_t) ); + pPat->nBits = nBits; + pPat->nWords = Aig_BitWordNum(nBits); + pPat->pData = ALLOC( unsigned, pPat->nWords ); + return pPat; +} + +/**Function************************************************************* + + Synopsis [Cleans the pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_PatternClean( Aig_Pattern_t * pPat ) +{ + memset( pPat->pData, 0, sizeof(unsigned) * pPat->nWords ); +} + +/**Function************************************************************* + + Synopsis [Sets the random pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_PatternRandom( Aig_Pattern_t * pPat ) +{ + int i; + for ( i = 0; i < pPat->nWords; i++ ) + pPat->pData[i] = ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand())); +} + +/**Function************************************************************* + + Synopsis [Deallocates the pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_PatternFree( Aig_Pattern_t * pPat ) +{ + free( pPat->pData ); + free( pPat ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/aig/fraigSolver.c b/src/sat/aig/fraigSolver.c new file mode 100644 index 00000000..12502951 --- /dev/null +++ b/src/sat/aig/fraigSolver.c @@ -0,0 +1,47 @@ +/**CFile**************************************************************** + + FileName [fraigSolver.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: fraigSolver.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/fraigTrav.c b/src/sat/aig/fraigTrav.c new file mode 100644 index 00000000..d5a09259 --- /dev/null +++ b/src/sat/aig/fraigTrav.c @@ -0,0 +1,47 @@ +/**CFile**************************************************************** + + FileName [fraigTrav.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: fraigTrav.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index eb1c5374..3fadd457 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -26,7 +26,7 @@ #define ABC_DEFAULT_TIMEOUT 60 // 60 seconds -struct CSAT_ManagerStruct_t +struct ABC_ManagerStruct_t { // information about the problem stmm_table * tName2Node; // the hash table mapping names to nodes @@ -43,11 +43,11 @@ struct CSAT_ManagerStruct_t Vec_Ptr_t * vNodes; // the gates in the target Vec_Int_t * vValues; // the values of gate's outputs in the target // solution - CSAT_Target_ResultT * pResult; // the result of solving the target + ABC_Target_ResultT * pResult; // the result of solving the target }; -static CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars ); -static char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode ); +static ABC_Target_ResultT * ABC_TargetResAlloc( int nVars ); +static char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode ); // some external procedures extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName ); @@ -67,11 +67,11 @@ extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName ); SeeAlso [] ***********************************************************************/ -CSAT_Manager CSAT_InitManager() +ABC_Manager ABC_InitManager() { - CSAT_Manager_t * mng; - mng = ALLOC( CSAT_Manager_t, 1 ); - memset( mng, 0, sizeof(CSAT_Manager_t) ); + ABC_Manager_t * mng; + 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->tName2Node = stmm_init_table(strcmp, stmm_strhash); @@ -93,7 +93,7 @@ CSAT_Manager CSAT_InitManager() SeeAlso [] ***********************************************************************/ -void CSAT_QuitManager( CSAT_Manager mng ) +void ABC_QuitManager( ABC_Manager mng ) { if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name ); if ( mng->tName2Node ) stmm_free_table( mng->tName2Node ); @@ -116,15 +116,15 @@ void CSAT_QuitManager( CSAT_Manager mng ) SeeAlso [] ***********************************************************************/ -void CSAT_SetSolveOption( CSAT_Manager mng, enum CSAT_OptionT option ) +void ABC_SetSolveOption( ABC_Manager mng, enum ABC_OptionT option ) { mng->mode = option; if ( option == 0 ) - printf( "CSAT_SetSolveOption: Setting brute-force SAT mode.\n" ); + printf( "ABC_SetSolveOption: Setting brute-force SAT mode.\n" ); else if ( option == 1 ) - printf( "CSAT_SetSolveOption: Setting resource-aware FRAIG mode.\n" ); + printf( "ABC_SetSolveOption: Setting resource-aware FRAIG mode.\n" ); else - printf( "CSAT_SetSolveOption: Unknown solving mode.\n" ); + printf( "ABC_SetSolveOption: Unknown solving mode.\n" ); } @@ -143,7 +143,7 @@ void CSAT_SetSolveOption( CSAT_Manager mng, enum CSAT_OptionT option ) SeeAlso [] ***********************************************************************/ -int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, char ** fanins, int dc_attr ) +int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, char ** fanins, int dc_attr ) { Abc_Obj_t * pObj, * pFanin; char * pSop; @@ -151,82 +151,82 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c switch( type ) { - case CSAT_BPI: - case CSAT_BPPI: + case ABC_BPI: + case ABC_BPPI: if ( nofi != 0 ) - { printf( "CSAT_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 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 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: + 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: // create the node pObj = Abc_NtkCreateNode( mng->pNtk ); // create the fanins for ( i = 0; i < nofi; i++ ) { if ( !stmm_lookup( mng->tName2Node, fanins[i], (char **)&pFanin ) ) - { printf( "CSAT_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[i] ); return 0; } + { printf( "ABC_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[i] ); return 0; } Abc_ObjAddFanin( pObj, pFanin ); } // create the node function switch( type ) { - case CSAT_CONST: + case ABC_CONST: if ( nofi != 0 ) - { printf( "CSAT_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; } pSop = Abc_SopCreateConst1( mng->pNtk->pManFunc ); break; - case CSAT_BAND: + case ABC_BAND: if ( nofi < 1 ) - { printf( "CSAT_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; } pSop = Abc_SopCreateAnd( mng->pNtk->pManFunc, nofi, NULL ); break; - case CSAT_BNAND: + case ABC_BNAND: if ( nofi < 1 ) - { printf( "CSAT_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; } pSop = Abc_SopCreateNand( mng->pNtk->pManFunc, nofi ); break; - case CSAT_BOR: + case ABC_BOR: if ( nofi < 1 ) - { printf( "CSAT_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; } pSop = Abc_SopCreateOr( mng->pNtk->pManFunc, nofi, NULL ); break; - case CSAT_BNOR: + case ABC_BNOR: if ( nofi < 1 ) - { printf( "CSAT_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; } pSop = Abc_SopCreateNor( mng->pNtk->pManFunc, nofi ); break; - case CSAT_BXOR: + case ABC_BXOR: if ( nofi < 1 ) - { printf( "CSAT_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; } if ( nofi > 2 ) - { printf( "CSAT_AddGate: The XOR gate \"%s\" has more than two fanins.\n", name ); return 0; } + { 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 CSAT_BXNOR: + case ABC_BXNOR: if ( nofi < 1 ) - { printf( "CSAT_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; } + { printf( "ABC_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; } if ( nofi > 2 ) - { printf( "CSAT_AddGate: The XNOR gate \"%s\" has more than two fanins.\n", name ); return 0; } + { 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 CSAT_BINV: + case ABC_BINV: if ( nofi != 1 ) - { printf( "CSAT_AddGate: The inverter gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } + { 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 CSAT_BBUF: + case ABC_BBUF: if ( nofi != 1 ) - { printf( "CSAT_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } + { printf( "ABC_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } pSop = Abc_SopCreateBuf( mng->pNtk->pManFunc ); break; default : @@ -234,24 +234,24 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c } Abc_ObjSetData( pObj, pSop ); break; - case CSAT_BPPO: - case CSAT_BPO: + case ABC_BPPO: + case ABC_BPO: if ( nofi != 1 ) - { printf( "CSAT_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } + { printf( "ABC_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; } // create the PO pObj = Abc_NtkCreatePo( mng->pNtk ); stmm_insert( mng->tNode2Name, (char *)pObj, name ); // connect to the PO fanin if ( !stmm_lookup( mng->tName2Node, fanins[0], (char **)&pFanin ) ) - { printf( "CSAT_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; } + { printf( "ABC_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; } Abc_ObjAddFanin( pObj, pFanin ); break; default: - printf( "CSAT_AddGate: Unknown gate type.\n" ); + printf( "ABC_AddGate: Unknown gate type.\n" ); break; } if ( stmm_insert( mng->tName2Node, name, (char *)pObj ) ) - { printf( "CSAT_AddGate: The same gate \"%s\" is added twice.\n", name ); return 0; } + { printf( "ABC_AddGate: The same gate \"%s\" is added twice.\n", name ); return 0; } return 1; } @@ -267,7 +267,7 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c SeeAlso [] ***********************************************************************/ -int CSAT_Check_Integrity( CSAT_Manager mng ) +int ABC_Check_Integrity( ABC_Manager mng ) { Abc_Ntk_t * pNtk = mng->pNtk; Abc_Obj_t * pObj; @@ -276,15 +276,15 @@ int CSAT_Check_Integrity( CSAT_Manager mng ) // this procedure also finalizes construction of the ABC network Abc_NtkFixNonDrivenNets( pNtk ); Abc_NtkForEachPi( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj, CSAT_GetNodeName(mng, pObj) ); + Abc_NtkLogicStoreName( pObj, ABC_GetNodeName(mng, pObj) ); Abc_NtkForEachPo( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj, CSAT_GetNodeName(mng, pObj) ); + 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( "CSAT_Check_Integrity: The internal network check has failed.\n" ); + printf( "ABC_Check_Integrity: The internal network check has failed.\n" ); return 0; } @@ -295,7 +295,7 @@ int CSAT_Check_Integrity( CSAT_Manager mng ) continue; if ( Abc_ObjFanoutNum(pObj) == 0 ) { - printf( "CSAT_Check_Integrity: The network has dangling nodes.\n" ); + printf( "ABC_Check_Integrity: The network has dangling nodes.\n" ); return 0; } } @@ -313,7 +313,7 @@ int CSAT_Check_Integrity( CSAT_Manager mng ) SeeAlso [] ***********************************************************************/ -void CSAT_SetTimeLimit( CSAT_Manager mng, int runtime ) +void ABC_SetTimeLimit( ABC_Manager mng, int runtime ) { mng->nSeconds = runtime; } @@ -329,9 +329,9 @@ void CSAT_SetTimeLimit( CSAT_Manager mng, int runtime ) SeeAlso [] ***********************************************************************/ -void CSAT_SetLearnLimit( CSAT_Manager mng, int num ) +void ABC_SetLearnLimit( ABC_Manager mng, int num ) { - printf( "CSAT_SetLearnLimit: The resource limit is not implemented (warning).\n" ); + printf( "ABC_SetLearnLimit: The resource limit is not implemented (warning).\n" ); } /**Function************************************************************* @@ -345,9 +345,9 @@ void CSAT_SetLearnLimit( CSAT_Manager mng, int num ) SeeAlso [] ***********************************************************************/ -void CSAT_SetSolveBacktrackLimit( CSAT_Manager mng, int num ) +void ABC_SetSolveBacktrackLimit( ABC_Manager mng, int num ) { - printf( "CSAT_SetSolveBacktrackLimit: The resource limit is not implemented (warning).\n" ); + printf( "ABC_SetSolveBacktrackLimit: The resource limit is not implemented (warning).\n" ); } /**Function************************************************************* @@ -361,9 +361,9 @@ void CSAT_SetSolveBacktrackLimit( CSAT_Manager mng, int num ) SeeAlso [] ***********************************************************************/ -void CSAT_SetLearnBacktrackLimit( CSAT_Manager mng, int num ) +void ABC_SetLearnBacktrackLimit( ABC_Manager mng, int num ) { - printf( "CSAT_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" ); + printf( "ABC_SetLearnBacktrackLimit: The resource limit is not implemented (warning).\n" ); } /**Function************************************************************* @@ -377,7 +377,7 @@ void CSAT_SetLearnBacktrackLimit( CSAT_Manager mng, int num ) SeeAlso [] ***********************************************************************/ -void CSAT_EnableDump( CSAT_Manager mng, char * dump_file ) +void ABC_EnableDump( ABC_Manager mng, char * dump_file ) { FREE( mng->pDumpFileName ); mng->pDumpFileName = util_strsav( dump_file ); @@ -398,12 +398,12 @@ void CSAT_EnableDump( CSAT_Manager mng, char * dump_file ) SeeAlso [] ***********************************************************************/ -int CSAT_AddTarget( CSAT_Manager mng, int nog, char ** names, int * values ) +int ABC_AddTarget( ABC_Manager mng, int nog, char ** names, int * values ) { Abc_Obj_t * pObj; int i; if ( nog < 1 ) - { printf( "CSAT_AddTarget: The target has no gates.\n" ); return 0; } + { printf( "ABC_AddTarget: The target has no gates.\n" ); return 0; } // clear storage for the target mng->nog = 0; Vec_PtrClear( mng->vNodes ); @@ -412,10 +412,10 @@ int CSAT_AddTarget( CSAT_Manager mng, int nog, char ** names, int * values ) for ( i = 0; i < nog; i++ ) { if ( !stmm_lookup( mng->tName2Node, names[i], (char **)&pObj ) ) - { printf( "CSAT_AddTarget: The target gate \"%s\" is not in the network.\n", names[i] ); return 0; } + { printf( "ABC_AddTarget: The target gate \"%s\" is not in the network.\n", names[i] ); return 0; } Vec_PtrPush( mng->vNodes, pObj ); if ( values[i] < 0 || values[i] > 1 ) - { printf( "CSAT_AddTarget: The value of gate \"%s\" is not 0 or 1.\n", names[i] ); return 0; } + { printf( "ABC_AddTarget: The value of gate \"%s\" is not 0 or 1.\n", names[i] ); return 0; } Vec_IntPush( mng->vValues, values[i] ); } mng->nog = nog; @@ -427,14 +427,14 @@ int CSAT_AddTarget( CSAT_Manager mng, int nog, char ** names, int * values ) Synopsis [Initialize the solver internal data structure.] Description [Prepares the solver to work on one specific target - set by calling CSAT_AddTarget before.] + set by calling ABC_AddTarget before.] SideEffects [] SeeAlso [] ***********************************************************************/ -void CSAT_SolveInit( CSAT_Manager mng ) +void ABC_SolveInit( ABC_Manager mng ) { Fraig_Params_t * pParams = &mng->Params; int nWords1, nWords2, nWordsMin; @@ -442,7 +442,7 @@ void CSAT_SolveInit( CSAT_Manager mng ) // check if the target is available assert( mng->nog == Vec_PtrSize(mng->vNodes) ); if ( mng->nog == 0 ) - { printf( "CSAT_SolveInit: Target is not specified by CSAT_AddTarget().\n" ); return; } + { printf( "ABC_SolveInit: Target is not specified by ABC_AddTarget().\n" ); return; } // free the previous target network if present if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget ); @@ -485,13 +485,13 @@ void CSAT_SolveInit( CSAT_Manager mng ) SeeAlso [] ***********************************************************************/ -void CSAT_AnalyzeTargets( CSAT_Manager mng ) +void ABC_AnalyzeTargets( ABC_Manager mng ) { } /**Function************************************************************* - Synopsis [Solves the targets added by CSAT_AddTarget().] + Synopsis [Solves the targets added by ABC_AddTarget().] Description [] @@ -500,7 +500,7 @@ void CSAT_AnalyzeTargets( CSAT_Manager mng ) SeeAlso [] ***********************************************************************/ -enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) +enum ABC_StatusT ABC_Solve( ABC_Manager mng ) { Fraig_Man_t * pMan; Abc_Ntk_t * pCnf; @@ -509,7 +509,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) // check if the target network is available if ( mng->pTarget == NULL ) - { printf( "CSAT_Solve: Target network is not derived by CSAT_SolveInit().\n" ); return UNDETERMINED; } + { 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 @@ -522,7 +522,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) RetValue = Abc_NtkMiterSat( pCnf, mng->nSeconds, 0 ); // analyze the result - mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); + mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); if ( RetValue == -1 ) mng->pResult->status = UNDETERMINED; else if ( RetValue == 1 ) @@ -533,7 +533,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) // create the array of PI names and values for ( i = 0; i < mng->pResult->no_sig; i++ ) { - mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given + 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 ); @@ -549,7 +549,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) RetValue = Fraig_ManCheckMiter( pMan ); // analyze the result - mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); + mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); if ( RetValue == -1 ) mng->pResult->status = UNDETERMINED; else if ( RetValue == 1 ) @@ -562,7 +562,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) // create the array of PI names and values for ( i = 0; i < mng->pResult->no_sig; i++ ) { - mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given + 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]; } } @@ -584,14 +584,14 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) Synopsis [Gets the solve status of a target.] - Description [TargetID: the target id returned by CSAT_AddTarget().] + Description [TargetID: the target id returned by ABC_AddTarget().] SideEffects [] SeeAlso [] ***********************************************************************/ -CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID ) +ABC_Target_ResultT * ABC_Get_Target_Result( ABC_Manager mng, int TargetID ) { return mng->pResult; } @@ -607,7 +607,7 @@ CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID ) SeeAlso [] ***********************************************************************/ -void CSAT_Dump_Bench_File( CSAT_Manager mng ) +void ABC_Dump_Bench_File( ABC_Manager mng ) { Abc_Ntk_t * pNtkTemp, * pNtkAig; char * pFileName; @@ -617,7 +617,7 @@ void CSAT_Dump_Bench_File( CSAT_Manager mng ) pNtkTemp = Abc_NtkLogicToNetlistBench( pNtkAig ); Abc_NtkDelete( pNtkAig ); if ( pNtkTemp == NULL ) - { printf( "CSAT_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; } + { printf( "ABC_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; } pFileName = mng->pDumpFileName? mng->pDumpFileName: "abc_test.bench"; Io_WriteBench( pNtkTemp, pFileName ); Abc_NtkDelete( pNtkTemp ); @@ -636,11 +636,11 @@ void CSAT_Dump_Bench_File( CSAT_Manager mng ) SeeAlso [] ***********************************************************************/ -CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars ) +ABC_Target_ResultT * ABC_TargetResAlloc( int nVars ) { - CSAT_Target_ResultT * p; - p = ALLOC( CSAT_Target_ResultT, 1 ); - memset( p, 0, sizeof(CSAT_Target_ResultT) ); + ABC_Target_ResultT * p; + p = ALLOC( ABC_Target_ResultT, 1 ); + memset( p, 0, sizeof(ABC_Target_ResultT) ); p->no_sig = nVars; p->names = ALLOC( char *, nVars ); p->values = ALLOC( int, nVars ); @@ -660,7 +660,7 @@ CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars ) SeeAlso [] ***********************************************************************/ -void CSAT_TargetResFree( CSAT_Target_ResultT * p ) +void ABC_TargetResFree( ABC_Target_ResultT * p ) { if ( p == NULL ) return; @@ -680,7 +680,7 @@ void CSAT_TargetResFree( CSAT_Target_ResultT * p ) SeeAlso [] ***********************************************************************/ -char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode ) +char * ABC_GetNodeName( ABC_Manager mng, Abc_Obj_t * pNode ) { char * pName = NULL; if ( !stmm_lookup( mng->tNode2Name, (char *)pNode, (char **)&pName ) ) diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h index e567241f..3e04c7df 100644 --- a/src/sat/csat/csat_apis.h +++ b/src/sat/csat/csat_apis.h @@ -16,8 +16,8 @@ ***********************************************************************/ -#ifndef __CSAT_APIS_H__ -#define __CSAT_APIS_H__ +#ifndef __ABC_APIS_H__ +#define __ABC_APIS_H__ //////////////////////////////////////////////////////////////////////// /// INCLUDES /// @@ -32,37 +32,37 @@ //////////////////////////////////////////////////////////////////////// -typedef struct CSAT_ManagerStruct_t CSAT_Manager_t; -typedef struct CSAT_ManagerStruct_t * CSAT_Manager; +typedef struct ABC_ManagerStruct_t ABC_Manager_t; +typedef struct ABC_ManagerStruct_t * ABC_Manager; // GateType defines the gate type that can be added to circuit by -// CSAT_AddGate(); -#ifndef _CSAT_GATE_TYPE_ -#define _CSAT_GATE_TYPE_ +// ABC_AddGate(); +#ifndef _ABC_GATE_TYPE_ +#define _ABC_GATE_TYPE_ enum GateType { - 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_BPPO, // bit level PSEUDO PRIMARY OUTPUT - CSAT_BPO // boolean PO + 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 }; #endif -//CSAT_StatusT defines the return value by CSAT_Solve(); -#ifndef _CSAT_STATUS_ -#define _CSAT_STATUS_ -enum CSAT_StatusT +//ABC_StatusT defines the return value by ABC_Solve(); +#ifndef _ABC_STATUS_ +#define _ABC_STATUS_ +enum ABC_StatusT { UNDETERMINED = 0, UNSATISFIABLE, @@ -76,11 +76,11 @@ enum CSAT_StatusT #endif -// CSAT_OptionT defines the solver option about learning -// which is used by CSAT_SetSolveOption(); -#ifndef _CSAT_OPTION_ -#define _CSAT_OPTION_ -enum CSAT_OptionT +// ABC_OptionT defines the solver option about learning +// which is used by ABC_SetSolveOption(); +#ifndef _ABC_OPTION_ +#define _ABC_OPTION_ +enum ABC_OptionT { BASE_LINE = 0, IMPLICT_LEARNING, //default @@ -89,12 +89,12 @@ enum CSAT_OptionT #endif -#ifndef _CSAT_Target_Result -#define _CSAT_Target_Result -typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT; -struct _CSAT_Target_ResultT +#ifndef _ABC_Target_Result +#define _ABC_Target_Result +typedef struct _ABC_Target_ResultT ABC_Target_ResultT; +struct _ABC_Target_ResultT { - enum CSAT_StatusT status; // solve status of the target + enum ABC_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 +118,10 @@ struct _CSAT_Target_ResultT //////////////////////////////////////////////////////////////////////// // create a new manager -extern CSAT_Manager CSAT_InitManager(void); +extern ABC_Manager ABC_InitManager(void); // set solver options for learning -extern void CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_OptionT option); +extern void ABC_SetSolveOption(ABC_Manager mng, enum ABC_OptionT option); // add a gate to the circuit // the meaning of the parameters are: @@ -129,7 +129,7 @@ extern void CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_Opt // name: the name of the gate to be added, name should be unique in a circuit. // nofi: number of fanins of the gate to be added; // fanins: the name array of fanins of the gate to be added -extern int CSAT_AddGate(CSAT_Manager mng, +extern int ABC_AddGate(ABC_Manager mng, enum GateType type, char* name, int nofi, @@ -138,38 +138,38 @@ extern int CSAT_AddGate(CSAT_Manager mng, // 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 CSAT_Check_Integrity(CSAT_Manager mng); +extern int ABC_Check_Integrity(ABC_Manager mng); // set time limit for solving a target. // runtime: time limit (in second). -extern void CSAT_SetTimeLimit(CSAT_Manager mng, int runtime); -extern void CSAT_SetLearnLimit(CSAT_Manager mng, int num); -extern void CSAT_SetSolveBacktrackLimit(CSAT_Manager mng, int num); -extern void CSAT_SetLearnBacktrackLimit(CSAT_Manager mng, int num); -extern void CSAT_EnableDump(CSAT_Manager mng, char* dump_file); +extern void ABC_SetTimeLimit(ABC_Manager mng, int runtime); +extern void ABC_SetLearnLimit(ABC_Manager mng, int num); +extern void ABC_SetSolveBacktrackLimit(ABC_Manager mng, int num); +extern void ABC_SetLearnBacktrackLimit(ABC_Manager mng, int num); +extern void ABC_EnableDump(ABC_Manager mng, char* dump_file); // the meaning of the parameters are: // nog: number of gates that are in the targets // names: name array of gates // values: value array of the corresponding gates given in "names" to be // solved. the relation of them is AND. -extern int CSAT_AddTarget(CSAT_Manager mng, int nog, char**names, int* values); +extern int ABC_AddTarget(ABC_Manager mng, int nog, char**names, int* values); // initialize the solver internal data structure. -extern void CSAT_SolveInit(CSAT_Manager mng); -extern void CSAT_AnalyzeTargets(CSAT_Manager mng); +extern void ABC_SolveInit(ABC_Manager mng); +extern void ABC_AnalyzeTargets(ABC_Manager mng); -// solve the targets added by CSAT_AddTarget() -extern enum CSAT_StatusT CSAT_Solve(CSAT_Manager mng); +// solve the targets added by ABC_AddTarget() +extern enum ABC_StatusT ABC_Solve(ABC_Manager mng); // get the solve status of a target -// TargetID: the target id returned by CSAT_AddTarget(). -extern CSAT_Target_ResultT * CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID); -extern void CSAT_Dump_Bench_File(CSAT_Manager mng); +// TargetID: the target id returned by ABC_AddTarget(). +extern ABC_Target_ResultT * ABC_Get_Target_Result(ABC_Manager mng, int TargetID); +extern void ABC_Dump_Bench_File(ABC_Manager mng); // ADDED PROCEDURES: -extern void CSAT_QuitManager( CSAT_Manager mng ); -extern void CSAT_TargetResFree( CSAT_Target_ResultT * p ); +extern void ABC_QuitManager( ABC_Manager mng ); +extern void ABC_TargetResFree( ABC_Target_ResultT * p ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/sat/fraig/fraigMem.c b/src/sat/fraig/fraigMem.c index 7dc46430..500431c6 100644 --- a/src/sat/fraig/fraigMem.c +++ b/src/sat/fraig/fraigMem.c @@ -201,7 +201,7 @@ void Fraig_MemFixedRestart( Fraig_MemFixed_t * p ) int i; char * pTemp; - // delocate all chunks except the first one + // deallocate all chunks except the first one for ( i = 1; i < p->nChunks; i++ ) free( p->pChunks[i] ); p->nChunks = 1; diff --git a/src/sat/msat/msatMem.c b/src/sat/msat/msatMem.c index 40aa223b..30bf4a96 100644 --- a/src/sat/msat/msatMem.c +++ b/src/sat/msat/msatMem.c @@ -231,7 +231,7 @@ void Msat_MmFixedRestart( Msat_MmFixed_t * p ) int i; char * pTemp; - // delocate all chunks except the first one + // deallocate all chunks except the first one for ( i = 1; i < p->nChunks; i++ ) free( p->pChunks[i] ); p->nChunks = 1; -- cgit v1.2.3