summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--abclib.dsp12
-rw-r--r--src/aig/aig/aigRepar.c15
-rw-r--r--src/base/abci/abc.c3
-rw-r--r--src/sat/bsat/module.make1
-rw-r--r--src/sat/bsat/satMem.c2
-rw-r--r--src/sat/bsat/satMem.h2
-rw-r--r--src/sat/bsat/satProof.c109
-rw-r--r--src/sat/bsat/satSolver2.h1
-rw-r--r--src/sat/bsat/satTruth.c315
-rw-r--r--src/sat/bsat/satTruth.h89
-rw-r--r--src/sat/bsat/vecRec.h306
11 files changed, 849 insertions, 6 deletions
diff --git a/abclib.dsp b/abclib.dsp
index c648f33b..1257e434 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -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 ///
+////////////////////////////////////////////////////////////////////////
+