Skip to content

A
abc
Commit d0da3a82 by Alan Mishchenko
Options

Computing interpolants as truth tables.

parent 82a2495c
Showing with 849 additions and 6 deletions
abclib.dsp
...@@ -1307,12 +1307,24 @@ SOURCE=.\src\sat\bsat\satTrace.c ...@@ -1307,12 +1307,24 @@ SOURCE=.\src\sat\bsat\satTrace.c
# End Source File # End Source File
# Begin 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 SOURCE=.\src\sat\bsat\satUtil.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\sat\bsat\satVec.h SOURCE=.\src\sat\bsat\satVec.h
# End Source File # End Source File
# Begin Source File
SOURCE=.\src\sat\bsat\vecRec.h
# End Source File
# End Group # End Group
# Begin Group "proof" # Begin Group "proof"
......
src/aig/aig/aigRepar.c
...@@ -123,7 +123,8 @@ static inline void Aig_ManInterAddXor( sat_solver2 * pSat, int iVarA, int iVarB, ...@@ -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 ) void Aig_ManInterTest( Aig_Man_t * pMan, int fVerbose )
{ {
sat_solver2 * pSat; sat_solver2 * pSat;
Aig_Man_t * pInter; // Aig_Man_t * pInter;
word * pInter;
Vec_Int_t * vVars; Vec_Int_t * vVars;
Cnf_Dat_t * pCnf; Cnf_Dat_t * pCnf;
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
...@@ -183,12 +184,16 @@ void Aig_ManInterTest( Aig_Man_t * pMan, int fVerbose ) ...@@ -183,12 +184,16 @@ void Aig_ManInterTest( Aig_Man_t * pMan, int fVerbose )
Sat_Solver2PrintStats( stdout, pSat ); Sat_Solver2PrintStats( stdout, pSat );
// derive interpolant // derive interpolant
pInter = Sat_ProofInterpolant( pSat, vVars ); // pInter = Sat_ProofInterpolant( pSat, vVars );
Aig_ManPrintStats( pInter ); // Aig_ManPrintStats( pInter );
Aig_ManDumpBlif( pInter, "int.blif", NULL, NULL ); // Aig_ManDumpBlif( pInter, "int.blif", NULL, NULL );
pInter = Sat_ProofInterpolantTruth( pSat, vVars );
Extra_PrintHex( stdout, pInter, Vec_IntSize(vVars) ); printf( "\n" );
// clean up // clean up
Aig_ManStop( pInter ); // Aig_ManStop( pInter );
ABC_FREE( pInter );
Vec_IntFree( vVars ); Vec_IntFree( vVars );
Cnf_DataFree( pCnf ); Cnf_DataFree( pCnf );
sat_solver2_delete( pSat ); sat_solver2_delete( pSat );
......
src/base/abci/abc.c
...@@ -8909,7 +8909,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -8909,7 +8909,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pNtk ) if ( pNtk )
{ {
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
Aig_ManInterRepar( pAig, 1 ); // Aig_ManInterRepar( pAig, 1 );
Aig_ManInterTest( pAig, 1 );
Aig_ManStop( pAig ); Aig_ManStop( pAig );
} }
} }
......
src/sat/bsat/module.make
...@@ -8,4 +8,5 @@ SRC += src/sat/bsat/satMem.c \ ...@@ -8,4 +8,5 @@ SRC += src/sat/bsat/satMem.c \
src/sat/bsat/satSolver2.c \ src/sat/bsat/satSolver2.c \
src/sat/bsat/satStore.c \ src/sat/bsat/satStore.c \
src/sat/bsat/satTrace.c \ src/sat/bsat/satTrace.c \
src/sat/bsat/satTruth.c \
src/sat/bsat/satUtil.c src/sat/bsat/satUtil.c
src/sat/bsat/satMem.c
...@@ -2,6 +2,8 @@ ...@@ -2,6 +2,8 @@
FileName [satMem.c] FileName [satMem.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT solver.] PackageName [SAT solver.]
Synopsis [Memory management.] Synopsis [Memory management.]
......
src/sat/bsat/satMem.h
...@@ -2,6 +2,8 @@ ...@@ -2,6 +2,8 @@
FileName [satMem.h] FileName [satMem.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT solver.] PackageName [SAT solver.]
Synopsis [Memory management.] Synopsis [Memory management.]
......
src/sat/bsat/satProof.c
...@@ -21,6 +21,7 @@ ...@@ -21,6 +21,7 @@
#include "satSolver2.h" #include "satSolver2.h"
#include "vec.h" #include "vec.h"
#include "aig.h" #include "aig.h"
#include "satTruth.h"
ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_START
...@@ -730,6 +731,114 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) ...@@ -730,6 +731,114 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
return pAig; 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************************************************************* /**Function*************************************************************
Synopsis [Computes UNSAT core.] Synopsis [Computes UNSAT core.]
......
src/sat/bsat/satSolver2.h
...@@ -72,6 +72,7 @@ extern int clause_id(sat_solver2* s, int h); ...@@ -72,6 +72,7 @@ extern int clause_id(sat_solver2* s, int h);
// proof-based APIs // proof-based APIs
extern void * Sat_ProofCore( sat_solver2 * s ); extern void * Sat_ProofCore( sat_solver2 * s );
extern void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ); 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_ProofReduce( sat_solver2 * s );
extern void Sat_ProofCheck( sat_solver2 * s ); extern void Sat_ProofCheck( sat_solver2 * s );
......
src/sat/bsat/satTruth.c 0 → 100644
/**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
src/sat/bsat/satTruth.h 0 → 100644
/**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 ///
////////////////////////////////////////////////////////////////////////
src/sat/bsat/vecRec.h 0 → 100644
/**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 ///
////////////////////////////////////////////////////////////////////////
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment