diff options
| -rw-r--r-- | abclib.dsp | 12 | ||||
| -rw-r--r-- | src/aig/aig/aigRepar.c | 15 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 3 | ||||
| -rw-r--r-- | src/sat/bsat/module.make | 1 | ||||
| -rw-r--r-- | src/sat/bsat/satMem.c | 2 | ||||
| -rw-r--r-- | src/sat/bsat/satMem.h | 2 | ||||
| -rw-r--r-- | src/sat/bsat/satProof.c | 109 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.h | 1 | ||||
| -rw-r--r-- | src/sat/bsat/satTruth.c | 315 | ||||
| -rw-r--r-- | src/sat/bsat/satTruth.h | 89 | ||||
| -rw-r--r-- | src/sat/bsat/vecRec.h | 306 |
11 files changed, 849 insertions, 6 deletions
@@ -1307,12 +1307,24 @@ SOURCE=.\src\sat\bsat\satTrace.c # End Source File # Begin Source File +SOURCE=.\src\sat\bsat\satTruth.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\bsat\satTruth.h +# End Source File +# Begin Source File + SOURCE=.\src\sat\bsat\satUtil.c # End Source File # Begin Source File SOURCE=.\src\sat\bsat\satVec.h # End Source File +# Begin Source File + +SOURCE=.\src\sat\bsat\vecRec.h +# End Source File # End Group # Begin Group "proof" diff --git a/src/aig/aig/aigRepar.c b/src/aig/aig/aigRepar.c index d10471d7..817cb571 100644 --- a/src/aig/aig/aigRepar.c +++ b/src/aig/aig/aigRepar.c @@ -123,7 +123,8 @@ static inline void Aig_ManInterAddXor( sat_solver2 * pSat, int iVarA, int iVarB, void Aig_ManInterTest( Aig_Man_t * pMan, int fVerbose ) { sat_solver2 * pSat; - Aig_Man_t * pInter; +// Aig_Man_t * pInter; + word * pInter; Vec_Int_t * vVars; Cnf_Dat_t * pCnf; Aig_Obj_t * pObj; @@ -183,12 +184,16 @@ void Aig_ManInterTest( Aig_Man_t * pMan, int fVerbose ) Sat_Solver2PrintStats( stdout, pSat ); // derive interpolant - pInter = Sat_ProofInterpolant( pSat, vVars ); - Aig_ManPrintStats( pInter ); - Aig_ManDumpBlif( pInter, "int.blif", NULL, NULL ); +// pInter = Sat_ProofInterpolant( pSat, vVars ); +// Aig_ManPrintStats( pInter ); +// Aig_ManDumpBlif( pInter, "int.blif", NULL, NULL ); + pInter = Sat_ProofInterpolantTruth( pSat, vVars ); + Extra_PrintHex( stdout, pInter, Vec_IntSize(vVars) ); printf( "\n" ); // clean up - Aig_ManStop( pInter ); +// Aig_ManStop( pInter ); + ABC_FREE( pInter ); + Vec_IntFree( vVars ); Cnf_DataFree( pCnf ); sat_solver2_delete( pSat ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f935506d..1ba1c451 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -8909,7 +8909,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pNtk ) { Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); - Aig_ManInterRepar( pAig, 1 ); +// Aig_ManInterRepar( pAig, 1 ); + Aig_ManInterTest( pAig, 1 ); Aig_ManStop( pAig ); } } diff --git a/src/sat/bsat/module.make b/src/sat/bsat/module.make index d04abc2a..e54dc891 100644 --- a/src/sat/bsat/module.make +++ b/src/sat/bsat/module.make @@ -8,4 +8,5 @@ SRC += src/sat/bsat/satMem.c \ src/sat/bsat/satSolver2.c \ src/sat/bsat/satStore.c \ src/sat/bsat/satTrace.c \ + src/sat/bsat/satTruth.c \ src/sat/bsat/satUtil.c diff --git a/src/sat/bsat/satMem.c b/src/sat/bsat/satMem.c index e947cbf0..187d8d0a 100644 --- a/src/sat/bsat/satMem.c +++ b/src/sat/bsat/satMem.c @@ -2,6 +2,8 @@ FileName [satMem.c] + SystemName [ABC: Logic synthesis and verification system.] + PackageName [SAT solver.] Synopsis [Memory management.] diff --git a/src/sat/bsat/satMem.h b/src/sat/bsat/satMem.h index 128e6c9f..8ea153a6 100644 --- a/src/sat/bsat/satMem.h +++ b/src/sat/bsat/satMem.h @@ -2,6 +2,8 @@ FileName [satMem.h] + SystemName [ABC: Logic synthesis and verification system.] + PackageName [SAT solver.] Synopsis [Memory management.] diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index ded11f1e..c718987e 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -21,6 +21,7 @@ #include "satSolver2.h" #include "vec.h" #include "aig.h" +#include "satTruth.h" ABC_NAMESPACE_IMPL_START @@ -730,6 +731,114 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) return pAig; } + +/**Function************************************************************* + + Synopsis [Computes interpolant of the proof.] + + Description [Aassuming that vars/clause of partA are marked.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ) +{ + Vec_Int_t * vClauses = (Vec_Int_t *)&s->clauses; + Vec_Int_t * vProof = (Vec_Int_t *)&s->proofs; + Vec_Int_t * vGlobVars = (Vec_Int_t *)pGloVars; + int hRoot = veci_begin(&s->claProofs)[satset_read(&s->learnts, s->hLearntLast>>1)->Id]; + + Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap; + satset * pNode, * pFanin; + Tru_Man_t * pTru; + int nVars = Vec_IntSize(vGlobVars); + int nWords = (nVars < 6) ? 1 : (1 << (nVars-6)); + word * pRes = ABC_ALLOC( word, nWords ); + int i, k, iVar, Lit, Entry; + assert( nVars > 0 && nVars <= 16 ); + + Sat_ProofInterpolantCheckVars( s, vGlobVars ); + + // collect visited nodes + vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); + // collect core clauses (cleans vUsed and vCore) + vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 0 ); + + // map variables into their global numbers + vVarMap = Vec_IntStartFull( s->size ); + Vec_IntForEachEntry( vGlobVars, Entry, i ) + Vec_IntWriteEntry( vVarMap, Entry, i ); + + // start the AIG + pTru = Tru_ManAlloc( nVars ); + + // copy the numbers out and derive interpol for clause + vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) ); + Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) + { + if ( pNode->partA ) + { +// pObj = Aig_ManConst0( pAig ); + Tru_ManClear( pRes, nWords ); + satset_foreach_lit( pNode, Lit, k, 0 ) + if ( (iVar = Vec_IntEntry(vVarMap, lit_var(Lit))) >= 0 ) +// pObj = Aig_Or( pAig, pObj, Aig_NotCond(Aig_IthVar(pAig, iVar), lit_sign(Lit)) ); + pRes = Tru_ManOrNotCond( pRes, Tru_ManVar(pTru, iVar), nWords, lit_sign(Lit) ); + } + else +// pObj = Aig_ManConst1( pAig ); + Tru_ManFill( pRes, nWords ); + // remember the interpolant + Vec_IntPush( vCoreNums, pNode->Id ); +// pNode->Id = Aig_ObjToLit(pObj); + pNode->Id = Tru_ManInsert( pTru, pRes ); + } + Vec_IntFree( vVarMap ); + + // copy the numbers out and derive interpol for resolvents + Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) + { +// satset_print( pNode ); + assert( pNode->nEnts > 1 ); + Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k ) + { +// assert( pFanin->Id < 2*Aig_ManObjNumMax(pAig) ); + assert( pFanin->Id <= Tru_ManHandleMax(pTru) ); + if ( k == 0 ) +// pObj = Aig_ObjFromLit( pAig, pFanin->Id ); + pRes = Tru_ManCopyNotCond( pRes, Tru_ManFunc(pTru, pFanin->Id & ~1), nWords, pFanin->Id & 1 ); + else if ( pNode->pEnts[k] & 2 ) // variable of A +// pObj = Aig_Or( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) ); + pRes = Tru_ManOrNotCond( pRes, Tru_ManFunc(pTru, pFanin->Id & ~1), nWords, pFanin->Id & 1 ); + else +// pObj = Aig_And( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) ); + pRes = Tru_ManAndNotCond( pRes, Tru_ManFunc(pTru, pFanin->Id & ~1), nWords, pFanin->Id & 1 ); + } + // remember the interpolant +// pNode->Id = Aig_ObjToLit(pObj); + pNode->Id = Tru_ManInsert( pTru, pRes ); + } + // save the result + assert( Proof_NodeHandle(vProof, pNode) == hRoot ); +// Aig_ObjCreatePo( pAig, pObj ); +// Aig_ManCleanup( pAig ); + + // move the results back + Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) + pNode->Id = Vec_IntEntry( vCoreNums, i ); + Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) + pNode->Id = 0; + // cleanup + Vec_IntFree( vCore ); + Vec_IntFree( vUsed ); + Vec_IntFree( vCoreNums ); + Tru_ManFree( pTru ); +// ABC_FREE( pRes ); + return pRes; +} + /**Function************************************************************* Synopsis [Computes UNSAT core.] diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index e5b85a43..0c08ac1e 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -72,6 +72,7 @@ extern int clause_id(sat_solver2* s, int h); // proof-based APIs extern void * Sat_ProofCore( sat_solver2 * s ); extern void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ); +extern word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ); extern void Sat_ProofReduce( sat_solver2 * s ); extern void Sat_ProofCheck( sat_solver2 * s ); diff --git a/src/sat/bsat/satTruth.c b/src/sat/bsat/satTruth.c new file mode 100644 index 00000000..7d69f558 --- /dev/null +++ b/src/sat/bsat/satTruth.c @@ -0,0 +1,315 @@ +/**CFile**************************************************************** + + FileName [satTruth.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT solver.] + + Synopsis [Truth table computation package.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: satTruth.c,v 1.4 2005/09/16 22:55:03 casem Exp $] + +***********************************************************************/ + +#include "satTruth.h" +#include "vecRec.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +struct Tru_Man_t_ +{ + int nVars; // the number of variables + int nWords; // the number of words in the truth table + int nEntrySize; // the size of one entry in 'int' + int nTableSize; // hash table size + int * pTable; // hash table + Vec_Rec_t * pMem; // memory for truth tables + word * pZero; // temporary truth table + int hIthVars[16]; // variable handles + int nTableLookups; +}; + +typedef struct Tru_One_t_ Tru_One_t; // 16 bytes minimum +struct Tru_One_t_ +{ + int Handle; // support + int Next; // next one in the table + word pTruth[0]; // truth table +}; + +static inline Tru_One_t * Tru_ManReadOne( Tru_Man_t * p, int h ) { return h ? (Tru_One_t *)Vec_RecEntryP(p->pMem, h) : NULL; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns the hash key.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline unsigned Tru_ManHash( word * pTruth, int nWords, int nBins, int * pPrimes ) +{ + int i; + unsigned uHash = 0; + for ( i = 0; i < nWords; i++ ) + uHash ^= pTruth[i] * pPrimes[i & 0x7]; + return uHash % nBins; +} + +/**Function************************************************************* + + Synopsis [Returns the given record.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Tru_ManLookup( Tru_Man_t * p, word * pTruth ) +{ + static int s_Primes[10] = { 1291, 1699, 2357, 4177, 5147, 5647, 6343, 7103, 7873, 8147 }; + Tru_One_t * pEntry; + int * pSpot; + assert( (pTruth[0] & 1) == 0 ); + pSpot = p->pTable + Tru_ManHash( pTruth, p->nWords, p->nTableSize, s_Primes ); + for ( pEntry = Tru_ManReadOne(p, *pSpot); pEntry; pSpot = &pEntry->Next, pEntry = Tru_ManReadOne(p, *pSpot) ) + if ( Tru_ManEqual(pEntry->pTruth, pTruth, p->nWords) ) + return pSpot; + return pSpot; +} + +/**Function************************************************************* + + Synopsis [Returns the given record.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Tru_ManResize( Tru_Man_t * p ) +{ + Tru_One_t * pThis; + int * pTableOld, * pSpot; + int nTableSizeOld, iNext, Counter, i; + assert( p->pTable != NULL ); + // replace the table + pTableOld = p->pTable; + nTableSizeOld = p->nTableSize; + p->nTableSize = 2 * p->nTableSize + 1; + p->pTable = ABC_CALLOC( int, p->nTableSize ); + // rehash the entries from the old table + Counter = 0; + for ( i = 0; i < nTableSizeOld; i++ ) + for ( pThis = Tru_ManReadOne(p, pTableOld[i]), + iNext = (pThis? pThis->Next : 0); + pThis; pThis = Tru_ManReadOne(p, iNext), + iNext = (pThis? pThis->Next : 0) ) + { + assert( pThis->Handle ); + pThis->Next = 0; + pSpot = Tru_ManLookup( p, pThis->pTruth ); + assert( *pSpot == 0 ); // should not be there + *pSpot = pThis->Handle; + Counter++; + } + assert( Counter == Vec_RecEntryNum(p->pMem) ); + ABC_FREE( pTableOld ); +} + +/**Function************************************************************* + + Synopsis [Adds entry to the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Tru_ManInsert( Tru_Man_t * p, word * pTruth ) +{ + int fCompl, * pSpot; + if ( Tru_ManEqual0(pTruth, p->nWords) ) + return 0; + if ( Tru_ManEqual1(pTruth, p->nWords) ) + return 1; + p->nTableLookups++; + if ( Vec_RecEntryNum(p->pMem) > 2 * p->nTableSize ) + Tru_ManResize( p ); + fCompl = pTruth[0] & 1; + if ( fCompl ) + Tru_ManNot( pTruth, p->nWords ); + pSpot = Tru_ManLookup( p, pTruth ); + if ( *pSpot == 0 ) + { + Tru_One_t * pEntry; + *pSpot = Vec_RecAppend( p->pMem, p->nEntrySize ); + assert( (*pSpot & 1) == 0 ); + pEntry = Tru_ManReadOne( p, *pSpot ); + Tru_ManCopy( pEntry->pTruth, pTruth, p->nWords ); + pEntry->Handle = *pSpot; + pEntry->Next = 0; + } + if ( fCompl ) + Tru_ManNot( pTruth, p->nWords ); + return *pSpot ^ fCompl; +} + +/**Function************************************************************* + + Synopsis [Start the truth table logging.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Tru_Man_t * Tru_ManAlloc( int nVars ) +{ + word Masks[6] = + { + 0xAAAAAAAAAAAAAAAA, + 0xCCCCCCCCCCCCCCCC, + 0xF0F0F0F0F0F0F0F0, + 0xFF00FF00FF00FF00, + 0xFFFF0000FFFF0000, + 0xFFFFFFFF00000000 + }; + Tru_Man_t * p; + int i, w; + assert( nVars > 0 && nVars <= 16 ); + p = ABC_CALLOC( Tru_Man_t, 1 ); + p->nVars = nVars; + p->nWords = (nVars < 6) ? 1 : (1 << (nVars-6)); + p->nEntrySize = (sizeof(Tru_One_t) + p->nWords * sizeof(word))/sizeof(int); + p->nTableSize = 8147; + p->pTable = ABC_CALLOC( int, p->nTableSize ); + p->pMem = Vec_RecAlloc(); + // initialize truth tables + p->pZero = ABC_ALLOC( word, p->nWords ); + for ( i = 0; i < nVars; i++ ) + { + for ( w = 0; w < p->nWords; w++ ) + if ( i < 6 ) + p->pZero[w] = Masks[i]; + else if ( w & (1 << (i-6)) ) + p->pZero[w] = ~(word)0; + else + p->pZero[w] = 0; + p->hIthVars[i] = Tru_ManInsert( p, p->pZero ); + assert( !i || p->hIthVars[i] > p->hIthVars[i-1] ); + } + Tru_ManClear( p->pZero, p->nWords ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stop the truth table logging.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Tru_ManFree( Tru_Man_t * p ) +{ + printf( "Lookups = %d. Entries = %d.\n", p->nTableLookups, Vec_RecEntryNum(p->pMem) ); + Vec_RecFree( p->pMem ); + ABC_FREE( p->pZero ); + ABC_FREE( p->pTable ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Returns elementary variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +word * Tru_ManVar( Tru_Man_t * p, int v ) +{ + assert( v >= 0 && v < p->nVars ); + return Tru_ManReadOne( p, p->hIthVars[v] )->pTruth; +} + +/**Function************************************************************* + + Synopsis [Returns stored truth table] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +word * Tru_ManFunc( Tru_Man_t * p, int h ) +{ + assert( (h & 1) == 0 ); + if ( h == 0 ) + return p->pZero; + assert( Vec_RecChunk(h) ); + return Tru_ManReadOne( p, h )->pTruth; +} + +/**Function************************************************************* + + Synopsis [Returns stored truth table] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Tru_ManHandleMax( Tru_Man_t * p ) +{ + return p->pMem->hCurrent; +} +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satTruth.h b/src/sat/bsat/satTruth.h new file mode 100644 index 00000000..e07518b0 --- /dev/null +++ b/src/sat/bsat/satTruth.h @@ -0,0 +1,89 @@ +/**CFile**************************************************************** + + FileName [satTruth.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT solver.] + + Synopsis [Truth table computation package.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - January 1, 2004.] + + Revision [$Id: satTruth.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __SAT_TRUTH_H__ +#define __SAT_TRUTH_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include "abc_global.h" + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// STRUCTURE DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Tru_Man_t_ Tru_Man_t; + +//////////////////////////////////////////////////////////////////////// +/// GLOBAL VARIABLES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Tru_ManEqual( word * pOut, word * pIn, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if(pOut[w]!=pIn[w]) return 0; return 1; } +static inline int Tru_ManEqual0( word * pOut, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if(pOut[w]!=0) return 0; return 1; } +static inline int Tru_ManEqual1( word * pOut, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) if(pOut[w]!=~(word)0)return 0; return 1; } +static inline word * Tru_ManCopy( word * pOut, word * pIn, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) pOut[w] = pIn[w]; return pOut; } +static inline word * Tru_ManClear( word * pOut, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) pOut[w] = 0; return pOut; } +static inline word * Tru_ManFill( word * pOut, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) pOut[w] = ~(word)0; return pOut; } +static inline word * Tru_ManNot( word * pOut, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) pOut[w] = ~pOut[w]; return pOut; } +static inline word * Tru_ManAnd( word * pOut, word * pIn, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) pOut[w] &= pIn[w]; return pOut; } +static inline word * Tru_ManOr( word * pOut, word * pIn, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) pOut[w] |= pIn[w]; return pOut; } +static inline word * Tru_ManCopyNot( word * pOut, word * pIn, int nWords ){ int w; for ( w = 0; w < nWords; w++ ) pOut[w] = ~pIn[w]; return pOut; } +static inline word * Tru_ManAndNot( word * pOut, word * pIn, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) pOut[w] &= ~pIn[w]; return pOut; } +static inline word * Tru_ManOrNot( word * pOut, word * pIn, int nWords ) { int w; for ( w = 0; w < nWords; w++ ) pOut[w] |= ~pIn[w]; return pOut; } +static inline word * Tru_ManCopyNotCond( word * pOut, word * pIn, int nWords, int fCompl ){ return fCompl ? Tru_ManCopyNot(pOut, pIn, nWords) : Tru_ManCopy(pOut, pIn, nWords); } +static inline word * Tru_ManAndNotCond( word * pOut, word * pIn, int nWords, int fCompl ) { return fCompl ? Tru_ManAndNot(pOut, pIn, nWords) : Tru_ManAnd(pOut, pIn, nWords); } +static inline word * Tru_ManOrNotCond( word * pOut, word * pIn, int nWords, int fCompl ) { return fCompl ? Tru_ManOrNot(pOut, pIn, nWords) : Tru_ManOr(pOut, pIn, nWords); } + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern Tru_Man_t * Tru_ManAlloc( int nVars ); +extern void Tru_ManFree( Tru_Man_t * p ); +extern word * Tru_ManVar( Tru_Man_t * p, int v ); +extern word * Tru_ManFunc( Tru_Man_t * p, int h ); +extern int Tru_ManInsert( Tru_Man_t * p, word * pTruth ); +extern int Tru_ManHandleMax( Tru_Man_t * p ); + +ABC_NAMESPACE_HEADER_END + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/sat/bsat/vecRec.h b/src/sat/bsat/vecRec.h new file mode 100644 index 00000000..d81cc631 --- /dev/null +++ b/src/sat/bsat/vecRec.h @@ -0,0 +1,306 @@ +/**CFile**************************************************************** + + FileName [vecRec.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Resizable arrays.] + + Synopsis [Array of records.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: vecRec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __VEC_REC_H__ +#define __VEC_REC_H__ + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include <stdio.h> + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +// data-structure for logging entries +// memory is allocated in 2^(p->LogSize+2) byte chunks +// the first 'int' of each entry cannot be 0 +typedef struct Vec_Rec_t_ Vec_Rec_t; +struct Vec_Rec_t_ +{ + int LogSize; // the log size of one chunk in 'int' + int Mask; // mask for the log size + int hCurrent; // current position + int nEntries; // total number of entries + int nChunks; // total number of chunks + int nChunksAlloc; // the number of allocated chunks + int ** pChunks; // the chunks +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +// p is vector of records +// Size is given by the user +// Handle is returned to the user +// c (chunk) and s (shift) are variables used here +#define Vec_RecForEachEntry( p, Size, Handle, c, s ) \ + for ( c = 1; c <= p->nChunks; c++ ) \ + for ( s = 0; p->pChunks[c][s] && ((Handle) = (((c)<<16)|(s))); s += Size, assert(s < p->Mask) ) + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Rec_t * Vec_RecAlloc() +{ + Vec_Rec_t * p; + p = ABC_CALLOC( Vec_Rec_t, 1 ); + p->LogSize = 15; // chunk size = 2^15 ints = 128 Kb + p->Mask = (1 << p->LogSize) - 1; + p->hCurrent = (1 << 16); + p->nChunks = 1; + p->nChunksAlloc = 16; + p->pChunks = ABC_CALLOC( int *, p->nChunksAlloc ); + p->pChunks[0] = NULL; + p->pChunks[1] = ABC_ALLOC( int, (1 << 16) ); + p->pChunks[1][0] = 0; + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_RecEntryNum( Vec_Rec_t * p ) +{ + return p->nEntries; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_RecChunk( int i ) +{ + return i>>16; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_RecShift( int i ) +{ + return i&0xFFFF; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_RecEntry( Vec_Rec_t * p, int i ) +{ + assert( i <= p->hCurrent ); + return p->pChunks[Vec_RecChunk(i)][Vec_RecShift(i)]; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int * Vec_RecEntryP( Vec_Rec_t * p, int i ) +{ + assert( i <= p->hCurrent ); + return p->pChunks[Vec_RecChunk(i)] + Vec_RecShift(i); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_RecRestart( Vec_Rec_t * p ) +{ + p->hCurrent = (1 << 16); + p->nChunks = 1; + p->nEntries = 0; + p->pChunks[1][0] = 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_RecShrink( Vec_Rec_t * p, int h ) +{ + int i; + assert( Vec_RecEntry(p, h) == 0 ); + for ( i = Vec_RecChunk(h)+1; i < p->nChunksAlloc; i++ ) + ABC_FREE( p->pChunks[i] ); + p->nChunks = Vec_RecChunk(h); + p->hCurrent = h; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_RecFree( Vec_Rec_t * p ) +{ + int i; + for ( i = 0; i < p->nChunksAlloc; i++ ) + ABC_FREE( p->pChunks[i] ); + ABC_FREE( p->pChunks ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_RecAppend( Vec_Rec_t * p, int nSize ) +{ + int RetValue; + assert( nSize <= p->Mask ); + assert( Vec_RecEntry(p, p->hCurrent) == 0 ); + assert( Vec_RecChunk(p->hCurrent) == p->nChunks ); + if ( Vec_RecShift(p->hCurrent) + nSize >= p->Mask ) + { + if ( ++p->nChunks == p->nChunksAlloc ) + { + p->pChunks = ABC_REALLOC( int *, p->pChunks, p->nChunksAlloc * 2 ); + memset( p->pChunks + p->nChunksAlloc, 0, sizeof(int *) * p->nChunksAlloc ); + p->nChunksAlloc *= 2; + } + if ( p->pChunks[p->nChunks] == NULL ) + p->pChunks[p->nChunks] = ABC_ALLOC( int, (1 << p->LogSize) ); + p->pChunks[p->nChunks][0] = 0; + p->hCurrent = p->nChunks << 16; + } + RetValue = p->hCurrent; + p->hCurrent += nSize; + *Vec_RecEntryP(p, p->hCurrent) = 0; + p->nEntries++; + return RetValue; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_RecPush( Vec_Rec_t * p, int * pArray, int nSize ) +{ + int Handle = Vec_RecAppend( p, nSize ); + memmove( Vec_RecEntryP(p, Handle), pArray, sizeof(int) * nSize ); + return Handle; +} + + +ABC_NAMESPACE_HEADER_END + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + |