Computing interpolants as truth tables.

10 files changed, 837 insertions, 6 deletions

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                                ///
+////////////////////////////////////////////////////////////////////////
+