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/aig/aig.h | 3 +- src/sat/aig/aigNode.c | 23 +- src/sat/aig/fraigCore.c | 2 +- src/sat/aig/rwrMffc.c | 303 ++++++++++++++++++++++++++ src/sat/aig/rwrTruth.c | 2 + src/sat/aig/rwr_.c | 48 +++++ src/sat/asat/asatmem.c | 527 +++++++++++++++++++++++++++++++++++++++++++++ src/sat/asat/asatmem.h | 76 +++++++ src/sat/asat/module.make | 1 + src/sat/asat/solver.c | 65 +++++- src/sat/asat/solver.h | 9 +- src/sat/csat/csat_apis.c | 356 ++++++++++-------------------- src/sat/csat/csat_apis.h | 99 ++++++--- src/sat/fraig/fraig.h | 2 + src/sat/fraig/fraigCanon.c | 2 +- 15 files changed, 1232 insertions(+), 286 deletions(-) create mode 100644 src/sat/aig/rwrMffc.c create mode 100644 src/sat/aig/rwr_.c create mode 100644 src/sat/asat/asatmem.c create mode 100644 src/sat/asat/asatmem.h (limited to 'src/sat') diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h index ee029789..c83af527 100644 --- a/src/sat/aig/aig.h +++ b/src/sat/aig/aig.h @@ -300,8 +300,9 @@ extern void Aig_ManStop( Aig_Man_t * p ); /*=== aigNode.c =============================================================*/ extern Aig_Node_t * Aig_NodeCreateConst( Aig_Man_t * p ); extern Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p ); -extern Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin ); +extern Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p ); extern Aig_Node_t * Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t * pFanin1 ); +extern Aig_Node_t * Aig_NodeConnectPo( Aig_Man_t * p, Aig_Node_t * pNode, Aig_Node_t * pFanin ); extern void Aig_NodeConnectAnd( Aig_Node_t * pFanin0, Aig_Node_t * pFanin1, Aig_Node_t * pNode ); extern void Aig_NodeDisconnectAnd( Aig_Node_t * pNode ); extern void Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot ); diff --git a/src/sat/aig/aigNode.c b/src/sat/aig/aigNode.c index 991cc7e5..ce458353 100644 --- a/src/sat/aig/aigNode.c +++ b/src/sat/aig/aigNode.c @@ -104,12 +104,30 @@ Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin ) +Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p ) { Aig_Node_t * pNode; pNode = Aig_NodeCreate( p ); pNode->Type = AIG_PO; Vec_PtrPush( p->vPos, pNode ); + return pNode; +} + +/**Function************************************************************* + + Synopsis [Creates a primary output node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Node_t * Aig_NodeConnectPo( Aig_Man_t * p, Aig_Node_t * pNode, Aig_Node_t * pFanin ) +{ + assert( Aig_NodeIsPo(pNode) ); + assert( !Aig_IsComplement(pNode) ); // connect to the fanin pNode->Fans[0].fComp = Aig_IsComplement(pFanin); pNode->Fans[0].iNode = Aig_Regular(pFanin)->Id; @@ -224,13 +242,14 @@ void Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot ) assert( !Aig_IsComplement(pRoot) ); assert( pRoot->nRefs == 0 ); assert( Aig_NodeIsAnd(pRoot) ); - // save the children + // remember the children pNode0 = Aig_NodeFanin0(pRoot); pNode1 = Aig_NodeFanin1(pRoot); // disconnect the node Aig_NodeDisconnectAnd( pRoot ); // recycle the node Vec_PtrWriteEntry( pMan->vNodes, pRoot->Id, NULL ); + memset( pRoot, 0, sizeof(Aig_Node_t) ); // this is a temporary hack to skip dead children below!!! Aig_MemFixedEntryRecycle( pMan->mmNodes, (char *)pRoot ); // call recursively if ( Aig_NodeIsAnd(pNode0) && pNode0->nRefs == 0 ) diff --git a/src/sat/aig/fraigCore.c b/src/sat/aig/fraigCore.c index decf05ee..525d4a14 100644 --- a/src/sat/aig/fraigCore.c +++ b/src/sat/aig/fraigCore.c @@ -92,7 +92,7 @@ Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan ) // solve the miter clk = clock(); pMan->pSat->verbosity = pMan->pParam->fSatVerbose; - status = solver_solve( pMan->pSat, NULL, NULL, pMan->pParam->nSeconds ); + status = solver_solve( pMan->pSat, NULL, NULL, 0, 0 );//pMan->pParam->nConfLimit, pMan->pParam->nImpLimit ); if ( status == l_Undef ) { // printf( "The problem timed out.\n" ); diff --git a/src/sat/aig/rwrMffc.c b/src/sat/aig/rwrMffc.c new file mode 100644 index 00000000..663534b3 --- /dev/null +++ b/src/sat/aig/rwrMffc.c @@ -0,0 +1,303 @@ +/**CFile**************************************************************** + + FileName [rwrMffc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [Procedures working with Maximum Fanout-Free Cones.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: rwrMffc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern int Aig_NodeDeref_rec( Aig_Node_t * pNode ); +extern int Aig_NodeRef_rec( Aig_Node_t * pNode ); +extern void Aig_NodeMffsConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ); +extern void Aig_NodeFactorConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ); + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_MffcTest( Aig_Man_t * pMan ) +{ + Aig_Node_t * pNode, * pNodeA, * pNodeB, * pNodeC, * pLeaf; + Vec_Ptr_t * vCone, * vSupp; + int i, k;//, nNodes1, nNodes2; + int nSizes = 0; + int nCones = 0; + int nMuxes = 0; + int nExors = 0; + + vCone = Vec_PtrAlloc( 100 ); + vSupp = Vec_PtrAlloc( 100 ); + + // mark the multiple-fanout nodes + Aig_ManForEachAnd( pMan, pNode, i ) + if ( pNode->nRefs > 1 ) + pNode->fMarkA = 1; + // unmark the control inputs of MUXes and inputs of EXOR gates + Aig_ManForEachAnd( pMan, pNode, i ) + { + if ( !Aig_NodeIsMuxType(pNode) ) + continue; + + pNodeC = Aig_NodeRecognizeMux( pNode, &pNodeA, &pNodeB ); + // if real children are used, skip + if ( Aig_NodeFanin0(pNode)->nRefs > 1 || Aig_NodeFanin1(pNode)->nRefs > 1 ) + continue; +/* + + if ( pNodeC->nRefs == 2 ) + pNodeC->fMarkA = 0; + if ( Aig_Regular(pNodeA) == Aig_Regular(pNodeB) && Aig_Regular(pNodeA)->nRefs == 2 ) + Aig_Regular(pNodeA)->fMarkA = 0; +*/ + + if ( Aig_Regular(pNodeA) == Aig_Regular(pNodeB) ) + nExors++; + else + nMuxes++; + } + // mark the PO drivers + Aig_ManForEachPo( pMan, pNode, i ) + { + Aig_NodeFanin0(pNode)->fMarkA = 1; + Aig_NodeFanin0(pNode)->fMarkB = 1; + } + + + // print sizes of MFFCs + Aig_ManForEachAnd( pMan, pNode, i ) + { + if ( !pNode->fMarkA ) + continue; + +// nNodes1 = Aig_NodeDeref_rec( pNode ); +// Aig_NodeMffsConeSupp( pNode, vCone, vSupp ); +// nNodes2 = Aig_NodeRef_rec( pNode ); +// assert( nNodes1 == nNodes2 ); + + Aig_NodeFactorConeSupp( pNode, vCone, vSupp ); + + printf( "%6d : Fan = %4d. Co = %5d. Su = %5d. %s ", + pNode->Id, pNode->nRefs, Vec_PtrSize(vCone), Vec_PtrSize(vSupp), pNode->fMarkB? "po" : " " ); + + Vec_PtrForEachEntry( vSupp, pLeaf, k ) + printf( " %d", pLeaf->Id ); + + printf( "\n" ); + + nSizes += Vec_PtrSize(vCone); + nCones++; + } + printf( "Nodes = %6d. MFFC sizes = %6d. Cones = %6d. nExors = %6d. Muxes = %6d.\n", + Aig_ManAndNum(pMan), nSizes, nCones, nExors, nMuxes ); + + // unmark the nodes + Aig_ManForEachNode( pMan, pNode, i ) + { + pNode->fMarkA = 0; + pNode->fMarkB = 0; + pNode->fMarkC = 0; + } + + Vec_PtrFree( vCone ); + Vec_PtrFree( vSupp ); +} + +/**Function************************************************************* + + Synopsis [Dereferences the node's MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_NodeDeref_rec( Aig_Node_t * pNode ) +{ + Aig_Node_t * pNode0, * pNode1; + int Counter = 1; + if ( Aig_NodeIsPi(pNode) ) + return 0; + pNode0 = Aig_NodeFanin0(pNode); + pNode1 = Aig_NodeFanin1(pNode); + assert( pNode0->nRefs > 0 ); + assert( pNode1->nRefs > 0 ); + if ( --pNode0->nRefs == 0 ) + Counter += Aig_NodeDeref_rec( pNode0 ); + if ( --pNode1->nRefs == 0 ) + Counter += Aig_NodeDeref_rec( pNode1 ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [References the node's MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_NodeRef_rec( Aig_Node_t * pNode ) +{ + Aig_Node_t * pNode0, * pNode1; + int Counter = 1; + if ( Aig_NodeIsPi(pNode) ) + return 0; + pNode0 = Aig_NodeFanin0(pNode); + pNode1 = Aig_NodeFanin1(pNode); + if ( pNode0->nRefs++ == 0 ) + Counter += Aig_NodeRef_rec( pNode0 ); + if ( pNode1->nRefs++ == 0 ) + Counter += Aig_NodeRef_rec( pNode1 ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Collects the internal and leaf nodes in the derefed MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_NodeMffsConeSupp_rec( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost ) +{ + // skip visited nodes + if ( Aig_NodeIsTravIdCurrent(pNode) ) + return; + Aig_NodeSetTravIdCurrent(pNode); + // add to the new support nodes + if ( !fTopmost && (Aig_NodeIsPi(pNode) || pNode->nRefs > 0) ) + { + Vec_PtrPush( vSupp, pNode ); + return; + } + // recur on the children + Aig_NodeMffsConeSupp_rec( Aig_NodeFanin0(pNode), vCone, vSupp, 0 ); + Aig_NodeMffsConeSupp_rec( Aig_NodeFanin1(pNode), vCone, vSupp, 0 ); + // collect the internal node + Vec_PtrPush( vCone, pNode ); +} + +/**Function************************************************************* + + Synopsis [Collects the support of the derefed MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_NodeMffsConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ) +{ + assert( Aig_NodeIsAnd(pNode) ); + assert( !Aig_IsComplement(pNode) ); + Vec_PtrClear( vCone ); + Vec_PtrClear( vSupp ); + Aig_ManIncrementTravId( pNode->pMan ); + Aig_NodeMffsConeSupp_rec( pNode, vCone, vSupp, 1 ); +} + + + + + +/**Function************************************************************* + + Synopsis [Collects the internal and leaf nodes of the factor-cut of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_NodeFactorConeSupp_rec( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost ) +{ + // skip visited nodes + if ( Aig_NodeIsTravIdCurrent(pNode) ) + return; + Aig_NodeSetTravIdCurrent(pNode); + // add to the new support nodes + if ( !fTopmost && (Aig_NodeIsPi(pNode) || pNode->fMarkA) ) + { + Vec_PtrPush( vSupp, pNode ); + return; + } + // recur on the children + Aig_NodeFactorConeSupp_rec( Aig_NodeFanin0(pNode), vCone, vSupp, 0 ); + Aig_NodeFactorConeSupp_rec( Aig_NodeFanin1(pNode), vCone, vSupp, 0 ); + // collect the internal node + assert( fTopmost || !pNode->fMarkA ); + Vec_PtrPush( vCone, pNode ); + + assert( pNode->fMarkC == 0 ); + pNode->fMarkC = 1; +} + +/**Function************************************************************* + + Synopsis [Collects the support of the derefed MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_NodeFactorConeSupp( Aig_Node_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ) +{ + assert( Aig_NodeIsAnd(pNode) ); + assert( !Aig_IsComplement(pNode) ); + Vec_PtrClear( vCone ); + Vec_PtrClear( vSupp ); + Aig_ManIncrementTravId( pNode->pMan ); + Aig_NodeFactorConeSupp_rec( pNode, vCone, vSupp, 1 ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/sat/aig/rwrTruth.c b/src/sat/aig/rwrTruth.c index 2c402184..63a437ce 100644 --- a/src/sat/aig/rwrTruth.c +++ b/src/sat/aig/rwrTruth.c @@ -444,6 +444,8 @@ Aig_Node_t * Aig_TruthDecompose( Aig_Truth_t * p ) assert( 0 ); } + + return NULL; } diff --git a/src/sat/aig/rwr_.c b/src/sat/aig/rwr_.c new file mode 100644 index 00000000..45e76f75 --- /dev/null +++ b/src/sat/aig/rwr_.c @@ -0,0 +1,48 @@ +/**CFile**************************************************************** + + FileName [rwr_.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: rwr_.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/asat/asatmem.c b/src/sat/asat/asatmem.c new file mode 100644 index 00000000..24c1b1a8 --- /dev/null +++ b/src/sat/asat/asatmem.c @@ -0,0 +1,527 @@ +/**CFile**************************************************************** + + FileName [asatmem.c] + + PackageName [SAT solver.] + + Synopsis [Memory management.] + + Author [Alan Mishchenko ] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - January 1, 2004.] + + Revision [$Id: asatmem.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "asatmem.h" +#include "extra.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +struct Asat_MmFixed_t_ +{ + // information about individual entries + int nEntrySize; // the size of one entry + int nEntriesAlloc; // the total number of entries allocated + int nEntriesUsed; // the number of entries in use + int nEntriesMax; // the max number of entries in use + char * pEntriesFree; // the linked list of free entries + + // this is where the memory is stored + int nChunkSize; // the size of one chunk + int nChunksAlloc; // the maximum number of memory chunks + int nChunks; // the current number of memory chunks + char ** pChunks; // the allocated memory + + // statistics + int nMemoryUsed; // memory used in the allocated entries + int nMemoryAlloc; // memory allocated +}; + +struct Asat_MmFlex_t_ +{ + // information about individual entries + int nEntriesUsed; // the number of entries allocated + char * pCurrent; // the current pointer to free memory + char * pEnd; // the first entry outside the free memory + + // this is where the memory is stored + int nChunkSize; // the size of one chunk + int nChunksAlloc; // the maximum number of memory chunks + int nChunks; // the current number of memory chunks + char ** pChunks; // the allocated memory + + // statistics + int nMemoryUsed; // memory used in the allocated entries + int nMemoryAlloc; // memory allocated +}; + +struct Asat_MmStep_t_ +{ + int nMems; // the number of fixed memory managers employed + Asat_MmFixed_t ** pMems; // memory managers: 2^1 words, 2^2 words, etc + int nMapSize; // the size of the memory array + Asat_MmFixed_t ** pMap; // maps the number of bytes into its memory manager +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates memory pieces of fixed size.] + + Description [The size of the chunk is computed as the minimum of + 1024 entries and 64K. Can only work with entry size at least 4 byte long.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Asat_MmFixed_t * Asat_MmFixedStart( int nEntrySize ) +{ + Asat_MmFixed_t * p; + + p = ALLOC( Asat_MmFixed_t, 1 ); + memset( p, 0, sizeof(Asat_MmFixed_t) ); + + p->nEntrySize = nEntrySize; + p->nEntriesAlloc = 0; + p->nEntriesUsed = 0; + p->pEntriesFree = NULL; + + if ( nEntrySize * (1 << 10) < (1<<16) ) + p->nChunkSize = (1 << 10); + else + p->nChunkSize = (1<<16) / nEntrySize; + if ( p->nChunkSize < 8 ) + p->nChunkSize = 8; + + p->nChunksAlloc = 64; + p->nChunks = 0; + p->pChunks = ALLOC( char *, p->nChunksAlloc ); + + p->nMemoryUsed = 0; + p->nMemoryAlloc = 0; + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Asat_MmFixedStop( Asat_MmFixed_t * p, int fVerbose ) +{ + int i; + if ( p == NULL ) + return; + if ( fVerbose ) + { + printf( "Fixed memory manager: Entry = %5d. Chunk = %5d. Chunks used = %5d.\n", + p->nEntrySize, p->nChunkSize, p->nChunks ); + printf( " Entries used = %8d. Entries peak = %8d. Memory used = %8d. Memory alloc = %8d.\n", + p->nEntriesUsed, p->nEntriesMax, p->nEntrySize * p->nEntriesUsed, p->nMemoryAlloc ); + } + for ( i = 0; i < p->nChunks; i++ ) + free( p->pChunks[i] ); + free( p->pChunks ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Asat_MmFixedEntryFetch( Asat_MmFixed_t * p ) +{ + char * pTemp; + int i; + + // check if there are still free entries + if ( p->nEntriesUsed == p->nEntriesAlloc ) + { // need to allocate more entries + assert( p->pEntriesFree == NULL ); + if ( p->nChunks == p->nChunksAlloc ) + { + p->nChunksAlloc *= 2; + p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); + } + p->pEntriesFree = ALLOC( char, p->nEntrySize * p->nChunkSize ); + p->nMemoryAlloc += p->nEntrySize * p->nChunkSize; + // transform these entries into a linked list + pTemp = p->pEntriesFree; + for ( i = 1; i < p->nChunkSize; i++ ) + { + *((char **)pTemp) = pTemp + p->nEntrySize; + pTemp += p->nEntrySize; + } + // set the last link + *((char **)pTemp) = NULL; + // add the chunk to the chunk storage + p->pChunks[ p->nChunks++ ] = p->pEntriesFree; + // add to the number of entries allocated + p->nEntriesAlloc += p->nChunkSize; + } + // incrememt the counter of used entries + p->nEntriesUsed++; + if ( p->nEntriesMax < p->nEntriesUsed ) + p->nEntriesMax = p->nEntriesUsed; + // return the first entry in the free entry list + pTemp = p->pEntriesFree; + p->pEntriesFree = *((char **)pTemp); + return pTemp; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Asat_MmFixedEntryRecycle( Asat_MmFixed_t * p, char * pEntry ) +{ + // decrement the counter of used entries + p->nEntriesUsed--; + // add the entry to the linked list of free entries + *((char **)pEntry) = p->pEntriesFree; + p->pEntriesFree = pEntry; +} + +/**Function************************************************************* + + Synopsis [] + + Description [Relocates all the memory except the first chunk.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Asat_MmFixedRestart( Asat_MmFixed_t * p ) +{ + int i; + char * pTemp; + + // deallocate all chunks except the first one + for ( i = 1; i < p->nChunks; i++ ) + free( p->pChunks[i] ); + p->nChunks = 1; + // transform these entries into a linked list + pTemp = p->pChunks[0]; + for ( i = 1; i < p->nChunkSize; i++ ) + { + *((char **)pTemp) = pTemp + p->nEntrySize; + pTemp += p->nEntrySize; + } + // set the last link + *((char **)pTemp) = NULL; + // set the free entry list + p->pEntriesFree = p->pChunks[0]; + // set the correct statistics + p->nMemoryAlloc = p->nEntrySize * p->nChunkSize; + p->nMemoryUsed = 0; + p->nEntriesAlloc = p->nChunkSize; + p->nEntriesUsed = 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Asat_MmFixedReadMemUsage( Asat_MmFixed_t * p ) +{ + return p->nMemoryAlloc; +} + + + +/**Function************************************************************* + + Synopsis [Allocates entries of flexible size.] + + Description [Can only work with entry size at least 4 byte long.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Asat_MmFlex_t * Asat_MmFlexStart() +{ + Asat_MmFlex_t * p; + + p = ALLOC( Asat_MmFlex_t, 1 ); + memset( p, 0, sizeof(Asat_MmFlex_t) ); + + p->nEntriesUsed = 0; + p->pCurrent = NULL; + p->pEnd = NULL; + + p->nChunkSize = (1 << 12); + p->nChunksAlloc = 64; + p->nChunks = 0; + p->pChunks = ALLOC( char *, p->nChunksAlloc ); + + p->nMemoryUsed = 0; + p->nMemoryAlloc = 0; + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Asat_MmFlexStop( Asat_MmFlex_t * p, int fVerbose ) +{ + int i; + if ( p == NULL ) + return; + if ( fVerbose ) + { + printf( "Flexible memory manager: Chunk size = %d. Chunks used = %d.\n", + p->nChunkSize, p->nChunks ); + printf( " Entries used = %d. Memory used = %d. Memory alloc = %d.\n", + p->nEntriesUsed, p->nMemoryUsed, p->nMemoryAlloc ); + } + for ( i = 0; i < p->nChunks; i++ ) + free( p->pChunks[i] ); + free( p->pChunks ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Asat_MmFlexEntryFetch( Asat_MmFlex_t * p, int nBytes ) +{ + char * pTemp; + // check if there are still free entries + if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd ) + { // need to allocate more entries + if ( p->nChunks == p->nChunksAlloc ) + { + p->nChunksAlloc *= 2; + p->pChunks = REALLOC( char *, p->pChunks, p->nChunksAlloc ); + } + if ( nBytes > p->nChunkSize ) + { + // resize the chunk size if more memory is requested than it can give + // (ideally, this should never happen) + p->nChunkSize = 2 * nBytes; + } + p->pCurrent = ALLOC( char, p->nChunkSize ); + p->pEnd = p->pCurrent + p->nChunkSize; + p->nMemoryAlloc += p->nChunkSize; + // add the chunk to the chunk storage + p->pChunks[ p->nChunks++ ] = p->pCurrent; + } + assert( p->pCurrent + nBytes <= p->pEnd ); + // increment the counter of used entries + p->nEntriesUsed++; + // keep track of the memory used + p->nMemoryUsed += nBytes; + // return the next entry + pTemp = p->pCurrent; + p->pCurrent += nBytes; + return pTemp; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Asat_MmFlexReadMemUsage( Asat_MmFlex_t * p ) +{ + return p->nMemoryAlloc; +} + + + + + +/**Function************************************************************* + + Synopsis [Starts the hierarchical memory manager.] + + Description [This manager can allocate entries of any size. + Iternally they are mapped into the entries with the number of bytes + equal to the power of 2. The smallest entry size is 8 bytes. The + next one is 16 bytes etc. So, if the user requests 6 bytes, he gets + 8 byte entry. If we asks for 25 bytes, he gets 32 byte entry etc. + The input parameters "nSteps" says how many fixed memory managers + are employed internally. Calling this procedure with nSteps equal + to 10 results in 10 hierarchically arranged internal memory managers, + which can allocate up to 4096 (1Kb) entries. Requests for larger + entries are handed over to malloc() and then free()ed.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Asat_MmStep_t * Asat_MmStepStart( int nSteps ) +{ + Asat_MmStep_t * p; + int i, k; + p = ALLOC( Asat_MmStep_t, 1 ); + p->nMems = nSteps; + // start the fixed memory managers + p->pMems = ALLOC( Asat_MmFixed_t *, p->nMems ); + for ( i = 0; i < p->nMems; i++ ) + p->pMems[i] = Asat_MmFixedStart( (8<nMapSize = (4<nMems); + p->pMap = ALLOC( Asat_MmFixed_t *, p->nMapSize+1 ); + p->pMap[0] = NULL; + for ( k = 1; k <= 4; k++ ) + p->pMap[k] = p->pMems[0]; + for ( i = 0; i < p->nMems; i++ ) + for ( k = (4<pMap[k] = p->pMems[i]; +//for ( i = 1; i < 100; i ++ ) +//printf( "%10d: size = %10d\n", i, p->pMap[i]->nEntrySize ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the memory manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Asat_MmStepStop( Asat_MmStep_t * p, int fVerbose ) +{ + int i; + for ( i = 0; i < p->nMems; i++ ) + Asat_MmFixedStop( p->pMems[i], fVerbose ); + free( p->pMems ); + free( p->pMap ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Creates the entry.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Asat_MmStepEntryFetch( Asat_MmStep_t * p, int nBytes ) +{ + if ( nBytes == 0 ) + return NULL; + if ( nBytes > p->nMapSize ) + { +// printf( "Allocating %d bytes.\n", nBytes ); + return ALLOC( char, nBytes ); + } + return Asat_MmFixedEntryFetch( p->pMap[nBytes] ); +} + + +/**Function************************************************************* + + Synopsis [Recycles the entry.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Asat_MmStepEntryRecycle( Asat_MmStep_t * p, char * pEntry, int nBytes ) +{ + if ( nBytes == 0 ) + return; + if ( nBytes > p->nMapSize ) + { + free( pEntry ); + return; + } + Asat_MmFixedEntryRecycle( p->pMap[nBytes], pEntry ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Asat_MmStepReadMemUsage( Asat_MmStep_t * p ) +{ + int i, nMemTotal = 0; + for ( i = 0; i < p->nMems; i++ ) + nMemTotal += p->pMems[i]->nMemoryAlloc; + return nMemTotal; +} diff --git a/src/sat/asat/asatmem.h b/src/sat/asat/asatmem.h new file mode 100644 index 00000000..56115e7d --- /dev/null +++ b/src/sat/asat/asatmem.h @@ -0,0 +1,76 @@ +/**CFile**************************************************************** + + FileName [asatmem.h] + + PackageName [SAT solver.] + + Synopsis [Memory management.] + + Author [Alan Mishchenko ] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - January 1, 2004.] + + Revision [$Id: asatmem.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __ASAT_MEM_H__ +#define __ASAT_MEM_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//#include "leaks.h" +#include +#include + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Asat_MmFixed_t_ Asat_MmFixed_t; +typedef struct Asat_MmFlex_t_ Asat_MmFlex_t; +typedef struct Asat_MmStep_t_ Asat_MmStep_t; + +//////////////////////////////////////////////////////////////////////// +/// GLOBAL VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// fixed-size-block memory manager +extern Asat_MmFixed_t * Asat_MmFixedStart( int nEntrySize ); +extern void Asat_MmFixedStop( Asat_MmFixed_t * p, int fVerbose ); +extern char * Asat_MmFixedEntryFetch( Asat_MmFixed_t * p ); +extern void Asat_MmFixedEntryRecycle( Asat_MmFixed_t * p, char * pEntry ); +extern void Asat_MmFixedRestart( Asat_MmFixed_t * p ); +extern int Asat_MmFixedReadMemUsage( Asat_MmFixed_t * p ); +// flexible-size-block memory manager +extern Asat_MmFlex_t * Asat_MmFlexStart(); +extern void Asat_MmFlexStop( Asat_MmFlex_t * p, int fVerbose ); +extern char * Asat_MmFlexEntryFetch( Asat_MmFlex_t * p, int nBytes ); +extern int Asat_MmFlexReadMemUsage( Asat_MmFlex_t * p ); +// hierarchical memory manager +extern Asat_MmStep_t * Asat_MmStepStart( int nSteps ); +extern void Asat_MmStepStop( Asat_MmStep_t * p, int fVerbose ); +extern char * Asat_MmStepEntryFetch( Asat_MmStep_t * p, int nBytes ); +extern void Asat_MmStepEntryRecycle( Asat_MmStep_t * p, char * pEntry, int nBytes ); +extern int Asat_MmStepReadMemUsage( Asat_MmStep_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// +#endif diff --git a/src/sat/asat/module.make b/src/sat/asat/module.make index 882176fa..d5cf69bf 100644 --- a/src/sat/asat/module.make +++ b/src/sat/asat/module.make @@ -1,2 +1,3 @@ SRC += src/sat/asat/added.c \ + src/sat/asat/asatmem.c \ src/sat/asat/solver.c diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c index 3927fac3..1130d437 100644 --- a/src/sat/asat/solver.c +++ b/src/sat/asat/solver.c @@ -26,6 +26,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "solver.h" +//#define ASAT_USE_SYSTEM_MEMORY_MANAGEMENT + //================================================================================================= // Simple (var/literal) helpers: @@ -275,7 +277,14 @@ static clause* clause_new(solver* s, lit* begin, lit* end, int learnt) assert(end - begin > 1); assert(learnt >= 0 && learnt < 2); size = end - begin; - c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); + +// c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); +#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT + c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); +#else + c = (clause*)Asat_MmStepEntryFetch( s->pMem, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float) ); +#endif + c->size_learnt = (size << 1) | learnt; assert(((unsigned int)c & 1) == 0); @@ -324,7 +333,12 @@ static void clause_remove(solver* s, clause* c) s->solver_stats.clauses_literals -= clause_size(c); } +#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT free(c); +#else + Asat_MmStepEntryRecycle( s->pMem, (char *)c, sizeof(clause) + sizeof(lit) * clause_size(c) + clause_learnt(c) * sizeof(float) ); +#endif + } @@ -829,12 +843,24 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts) // NO CONFLICT int next; - if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ + if (nof_conflicts >= 0 && conflictC >= nof_conflicts) + { // Reached bound on number of conflicts: s->progress_estimate = solver_progress(s); solver_canceluntil(s,s->root_level); vec_delete(&learnt_clause); - return l_Undef; } + return l_Undef; + } + + if ( s->nConfLimit && s->solver_stats.conflicts > s->nConfLimit || + s->nImpLimit && s->solver_stats.propagations > s->nImpLimit ) + { + // Reached bound on number of conflicts: + s->progress_estimate = solver_progress(s); + solver_canceluntil(s,s->root_level); + vec_delete(&learnt_clause); + return l_Undef; + } if (solver_dlevel(s) == 0) // Simplify the set of problem clauses: @@ -922,18 +948,28 @@ solver* solver_new(void) s->solver_stats.max_literals = 0; s->solver_stats.tot_literals = 0; +#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT + s->pMem = NULL; +#else + s->pMem = Asat_MmStepStart( 10 ); +#endif + return s; } void solver_delete(solver* s) { + +#ifdef ASAT_USE_SYSTEM_MEMORY_MANAGEMENT int i; for (i = 0; i < vec_size(&s->clauses); i++) free(vec_begin(&s->clauses)[i]); - for (i = 0; i < vec_size(&s->learnts); i++) free(vec_begin(&s->learnts)[i]); +#else + Asat_MmStepStop( s->pMem, 0 ); +#endif // delete vectors vec_delete(&s->clauses); @@ -1056,14 +1092,18 @@ bool solver_simplify(solver* s) } -bool solver_solve(solver* s, lit* begin, lit* end, int nSeconds) +bool solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit ) { double nof_conflicts = 100; double nof_learnts = solver_nclauses(s) / 3; lbool status = l_Undef; lbool* values = s->assigns; lit* i; - int timeStart = clock(); + + // set the external limits + s->nConfLimit = nConfLimit; // external limit on the number of conflicts + s->nImpLimit = nImpLimit; // external limit on the number of implications + for (i = begin; i < end; i++) if ((lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]) == l_False || (assume(s,*i), solver_propagate(s) != 0)){ @@ -1098,9 +1138,18 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nSeconds) status = solver_search(s,(int)nof_conflicts, (int)nof_learnts); nof_conflicts *= 1.5; nof_learnts *= 1.1; - // if the runtime limit is exceeded, quit the restart loop - if ( (nSeconds >= 0) && (clock() - timeStart >= nSeconds * CLOCKS_PER_SEC) ) + + // quit the loop if reached an external limit + if ( s->nConfLimit && s->solver_stats.conflicts > s->nConfLimit ) + { +// printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit ); break; + } + if ( s->nImpLimit && s->solver_stats.propagations > s->nImpLimit ) + { +// printf( "Reached the limit on the number of implications (%d).\n", s->nImpLimit ); + break; + } } if (s->verbosity >= 1) printf("==============================================================================\n"); diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h index 9618603c..d798a7a9 100644 --- a/src/sat/asat/solver.h +++ b/src/sat/asat/solver.h @@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #endif #include "solver_vec.h" +#include "asatmem.h" //================================================================================================= // Simple types: @@ -67,7 +68,7 @@ extern void solver_delete(solver* s); extern bool solver_addclause(solver* s, lit* begin, lit* end); extern bool solver_simplify(solver* s); -extern int solver_solve(solver* s, lit* begin, lit* end, int nSeconds); +extern int solver_solve(solver* s, lit* begin, lit* end, int nConfLimit, int nImpLimit ); extern int * solver_get_model( solver * p, int * pVars, int nVars ); extern int solver_nvars(solver* s); @@ -132,6 +133,12 @@ struct solver_t double progress_estimate; int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything + int nConfLimit; // external limit on the number of conflicts + int nImpLimit; // external limit on the number of implications + + // the memory manager + Asat_MmStep_t * pMem; + stats solver_stats; }; 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 diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h index 237030af..4637c030 100644 --- a/src/sat/fraig/fraig.h +++ b/src/sat/fraig/fraig.h @@ -44,6 +44,8 @@ struct Fraig_ParamsStruct_t_ int nPatsDyna; // the number of words of dynamic simulation info int nBTLimit; // the max number of backtracks to perform int nSeconds; // the timeout for the final proof + int nConfLimit; + int nImpLimit; int fFuncRed; // performs only one level hashing int fFeedBack; // enables solver feedback int fDist1Pats; // enables distance-1 patterns diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c index fab01368..4ebb9a9f 100644 --- a/src/sat/fraig/fraigCanon.c +++ b/src/sat/fraig/fraigCanon.c @@ -49,7 +49,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2 ) { Fraig_Node_t * pNodeNew, * pNodeOld, * pNodeRepr; - int RetValue; +// int RetValue; // check for trivial cases if ( p1 == p2 ) -- cgit v1.2.3