Version abc80307

18 files changed, 1191 insertions, 59 deletions

diff --git a/Makefile b/Makefile
index 4a91e6a9..cce30dee 100644
--- a/Makefile
+++ b/Makefile
@@ -24,7 +24,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
 default: $(PROG)
 
 #OPTFLAGS  := -DNDEBUG -O3
-OPTFLAGS  := -g -O
+OPTFLAGS  := -g -O -DLIN64
 
 CFLAGS   += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES)) 
 CXXFLAGS += $(CFLAGS) 
diff --git a/abc.dsp b/abc.dsp
index a8d6a3c6..9c043b24 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -1178,6 +1178,10 @@ SOURCE=.\src\sat\bsat\satInterA.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\bsat\satInterP.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\bsat\satMem.c
 # End Source File
 # Begin Source File
diff --git a/readme b/readme
index 5c06d4b5..b1588510 100644
--- a/readme
+++ b/readme
@@ -21,6 +21,13 @@ Several things to try if it does not compile on your platform:
   compiling ABC with gcc. Please try installing this library from
   http://tiswww.case.edu/php/chet/readline/rltop.html
 
+To compile the latest version of ABC, you may need to define "LIN" or "LIN64" 
+(depending on whether you are using 32- or 64-bit Linux). 
+For example, instead of
+    OPTFLAGS  := -g -O
+use
+    OPTFLAGS  := -g -O -DLIN64
+in Makefile.
 
 Finally, run regression test:
 abc>>> so regtest.script
diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c
index c939a38c..c5d0b39f 100644
--- a/src/aig/aig/aigInter.c
+++ b/src/aig/aig/aigInter.c
@@ -162,7 +162,17 @@ clk = clock();
     pRes = Inta_ManInterpolate( pManInter, pSatCnf, vVarsAB, fVerbose );
     Inta_ManFree( pManInter );
 timeInt += clock() - clk;
-
+/*
+    // test UNSAT core computation
+    {
+        Intp_Man_t * pManProof;
+        Vec_Int_t * vCore;
+        pManProof = Intp_ManAlloc();
+        vCore = Intp_ManUnsatCore( pManProof, pSatCnf, 0 );
+        Intp_ManFree( pManProof );
+        Vec_IntFree( vCore );
+    }
+*/
     Vec_IntFree( vVarsAB );
     Sto_ManFree( pSatCnf );
     return pRes;
diff --git a/src/aig/kit/cloud.c b/src/aig/kit/cloud.c
index 6e6691f0..f5c91fe7 100644
--- a/src/aig/kit/cloud.c
+++ b/src/aig/kit/cloud.c
@@ -105,8 +105,8 @@ clk2 = clock();
     dd->nSignCur          = 1;
     dd->tUnique[0].s      = dd->nSignCur;
     dd->tUnique[0].v      = CLOUD_CONST_INDEX;
-    dd->tUnique[0].e      = CLOUD_VOID;
-    dd->tUnique[0].t      = CLOUD_VOID;
+    dd->tUnique[0].e      = NULL;
+    dd->tUnique[0].t      = NULL;
     dd->one               = dd->tUnique;
     dd->zero              = Cloud_Not(dd->one);
     dd->nNodesCur         = 1;
@@ -256,7 +256,7 @@ CloudNode * Cloud_MakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudN
     if ( Cloud_IsComplement(t) )
     {
         pRes = cloudMakeNode( dd, v, Cloud_Not(t), Cloud_Not(e) );
-        if ( pRes != CLOUD_VOID )
+        if ( pRes != NULL )
             pRes = Cloud_Not(pRes);            
     }
     else
@@ -314,7 +314,7 @@ CloudNode * cloudMakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNo
         printf( "Cloud needs restart!\n" );
 //        fflush( stdout );
 //        exit(1);
-        return CLOUD_VOID;
+        return NULL;
     }
     // create the node
     entryUnique->s   = dd->nSignCur;
@@ -367,7 +367,7 @@ CloudNode * cloudBddAnd( CloudManager * dd, CloudNode * f, CloudNode * g )
     cacheEntry = dd->tCaches[CLOUD_OPER_AND] + cloudHashCudd2(f, g, dd->shiftCache[CLOUD_OPER_AND]);
 //    cacheEntry = dd->tCaches[CLOUD_OPER_AND] + cloudHashBuddy2(f, g, dd->shiftCache[CLOUD_OPER_AND]);
     r = cloudCacheLookup2( cacheEntry, dd->nSignCur, f, g );
-    if ( r != CLOUD_VOID )
+    if ( r != NULL )
     {
         dd->nCacheHits++;
         return r;
@@ -419,16 +419,16 @@ CloudNode * cloudBddAnd( CloudManager * dd, CloudNode * f, CloudNode * g )
     else
         t = cloudBddAnd( dd, gv, fv );
 
-    if ( t == CLOUD_VOID )
-        return CLOUD_VOID;
+    if ( t == NULL )
+        return NULL;
 
     if ( fnv <= gnv )
         e = cloudBddAnd( dd, fnv, gnv );
     else
         e = cloudBddAnd( dd, gnv, fnv );
 
-    if ( e == CLOUD_VOID )
-        return CLOUD_VOID;
+    if ( e == NULL )
+        return NULL;
 
     if ( t == e )
         r = t;
@@ -437,15 +437,15 @@ CloudNode * cloudBddAnd( CloudManager * dd, CloudNode * f, CloudNode * g )
         if ( Cloud_IsComplement(t) )
         {
             r = cloudMakeNode( dd, var, Cloud_Not(t), Cloud_Not(e) );
-            if ( r == CLOUD_VOID )
-                return CLOUD_VOID;
+            if ( r == NULL )
+                return NULL;
             r = Cloud_Not(r);
         }
         else
         {
             r = cloudMakeNode( dd, var, t, e );
-            if ( r == CLOUD_VOID )
-                return CLOUD_VOID;
+            if ( r == NULL )
+                return NULL;
         }
     }
     cloudCacheInsert2( cacheEntry, dd->nSignCur, f, g, r );
@@ -484,8 +484,8 @@ static inline CloudNode * cloudBddAnd_gate( CloudManager * dd, CloudNode * f, Cl
 ******************************************************************************/
 CloudNode * Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g )
 {
-    if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID )
-        return CLOUD_VOID;
+    if ( Cloud_Regular(f) == NULL || Cloud_Regular(g) == NULL )
+        return NULL;
     CLOUD_ASSERT(f);
     CLOUD_ASSERT(g);
     if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
@@ -507,14 +507,14 @@ CloudNode * Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g )
 CloudNode * Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g )
 {
     CloudNode * res;
-    if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID )
-        return CLOUD_VOID;
+    if ( Cloud_Regular(f) == NULL || Cloud_Regular(g) == NULL )
+        return NULL;
     CLOUD_ASSERT(f);
     CLOUD_ASSERT(g);
     if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
         cloudCacheAllocate( dd, CLOUD_OPER_AND );
     res = cloudBddAnd_gate( dd, Cloud_Not(f), Cloud_Not(g) );
-    res = Cloud_NotCond( res, res != CLOUD_VOID );
+    res = Cloud_NotCond( res, res != NULL );
     return res;
 }
 
@@ -532,18 +532,18 @@ CloudNode * Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g )
 CloudNode * Cloud_bddXor( CloudManager * dd, CloudNode * f, CloudNode * g )
 {
     CloudNode * t0, * t1, * r;
-    if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID )
-        return CLOUD_VOID;
+    if ( Cloud_Regular(f) == NULL || Cloud_Regular(g) == NULL )
+        return NULL;
     CLOUD_ASSERT(f);
     CLOUD_ASSERT(g);
     if ( dd->tCaches[CLOUD_OPER_AND] == NULL )
         cloudCacheAllocate( dd, CLOUD_OPER_AND );
     t0 = cloudBddAnd_gate( dd, f, Cloud_Not(g) );
-    if ( t0 == CLOUD_VOID )
-        return CLOUD_VOID;
+    if ( t0 == NULL )
+        return NULL;
     t1 = cloudBddAnd_gate( dd, Cloud_Not(f), g );
-    if ( t1 == CLOUD_VOID )
-        return CLOUD_VOID;
+    if ( t1 == NULL )
+        return NULL;
     r  = Cloud_bddOr( dd, t0, t1 );
     return r;
 }
@@ -631,7 +631,7 @@ CloudNode * Cloud_Support( CloudManager * dd, CloudNode * n )
         if ( support[i] == 1 )
         {
             res = Cloud_bddAnd( dd, res, dd->vars[i] );
-            if ( res == CLOUD_VOID )
+            if ( res == NULL )
                 break;
         }
     FREE( support );
@@ -831,8 +831,8 @@ CloudNode * Cloud_GetOneCube( CloudManager * dd, CloudNode * bFunc )
 
     // try to find the cube with the negative literal
     res = Cloud_GetOneCube( dd, bFunc0 );
-    if ( res == CLOUD_VOID )
-        return CLOUD_VOID;
+    if ( res == NULL )
+        return NULL;
 
     if ( res != dd->zero )
     {
@@ -842,8 +842,8 @@ CloudNode * Cloud_GetOneCube( CloudManager * dd, CloudNode * bFunc )
     {
         // try to find the cube with the positive literal
         res = Cloud_GetOneCube( dd, bFunc1 );
-        if ( res == CLOUD_VOID )
-            return CLOUD_VOID;
+        if ( res == NULL )
+            return NULL;
         assert( res != dd->zero );
         res = Cloud_bddAnd( dd, res, dd->vars[Cloud_V(bFunc)] );
     }
@@ -873,7 +873,7 @@ void Cloud_bddPrint( CloudManager * dd, CloudNode * Func )
         while ( 1 )
         {
             Cube = Cloud_GetOneCube( dd, Func );
-            if ( Cube == CLOUD_VOID || Cube == dd->zero )
+            if ( Cube == NULL || Cube == dd->zero )
                 break;
             if ( fFirst )       fFirst = 0;
             else                printf( " + " );
diff --git a/src/aig/kit/cloud.h b/src/aig/kit/cloud.h
index ac9d45f4..fa7f2fce 100644
--- a/src/aig/kit/cloud.h
+++ b/src/aig/kit/cloud.h
@@ -27,6 +27,7 @@ extern "C" {
 #include <stdlib.h>
 #include <assert.h>
 #include <time.h>
+#include "port_type.h"
 
 #ifdef _WIN32
 #define inline __inline // compatible with MS VS 6.0
@@ -162,9 +163,6 @@ struct cloudCacheEntry3  // the three-argument cache
 
 // parameters
 #define CLOUD_NODE_BITS              23
-#define CLOUD_ONE                    ((unsigned)0x00000001)
-#define CLOUD_NOT_ONE                ((unsigned)0xfffffffe)
-#define CLOUD_VOID                   ((unsigned)0x00000000)
 
 #define CLOUD_CONST_INDEX            ((unsigned)0x0fffffff)
 #define CLOUD_MARK_ON                ((unsigned)0x10000000)
@@ -182,10 +180,10 @@ struct cloudCacheEntry3  // the three-argument cache
 #define cloudHashCudd3(f,g,h,s)      (((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2 + (unsigned)(h)) * DD_P3) >> (s))
 
 // node complementation (using node)
-#define Cloud_Regular(p)             ((CloudNode*)(((unsigned)(p)) & CLOUD_NOT_ONE)) // get the regular node (w/o bubble)
-#define Cloud_Not(p)                 ((CloudNode*)(((unsigned)(p)) ^ CLOUD_ONE))     // complement the node
-#define Cloud_NotCond(p,c)           (((int)(c))? Cloud_Not(p):(p))                  // complement the node conditionally
-#define Cloud_IsComplement(p)        ((int)(((unsigned)(p)) & CLOUD_ONE))            // check if complemented
+#define Cloud_Regular(p)             ((CloudNode*)(((PORT_PTRUINT_T)(p)) & ~01))   // get the regular node (w/o bubble)
+#define Cloud_Not(p)                 ((CloudNode*)(((PORT_PTRUINT_T)(p)) ^  01))   // complement the node
+#define Cloud_NotCond(p,c)           ((CloudNode*)(((PORT_PTRUINT_T)(p)) ^ (c)))   // complement the node conditionally
+#define Cloud_IsComplement(p)        ((int)(((PORT_PTRUINT_T)(p)) & 01))           // check if complemented
 // checking constants (using node)
 #define Cloud_IsConstant(p)          (((Cloud_Regular(p))->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)
 #define cloudIsConstant(p)           (((p)->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX)
@@ -204,9 +202,9 @@ struct cloudCacheEntry3  // the three-argument cache
 #define cloudNodeIsMarked(p)         ((int)((p)->v &  CLOUD_MARK_ON))
 
 // cache lookups and inserts (using node)
-#define cloudCacheLookup1(p,sign,f)     (((p)->s == (sign) && (p)->a == (f))? ((p)->r): (CLOUD_VOID))
-#define cloudCacheLookup2(p,sign,f,g)   (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (CLOUD_VOID))
-#define cloudCacheLookup3(p,sign,f,g,h) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (CLOUD_VOID))
+#define cloudCacheLookup1(p,sign,f)     (((p)->s == (sign) && (p)->a == (f))? ((p)->r): (0))
+#define cloudCacheLookup2(p,sign,f,g)   (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (0))
+#define cloudCacheLookup3(p,sign,f,g,h) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (0))
 // cache inserts
 #define cloudCacheInsert1(p,sign,f,r)     (((p)->s = (sign)), ((p)->a = (f)), ((p)->r = (r)))
 #define cloudCacheInsert2(p,sign,f,g,r)   (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->r = (r)))
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index c14d0317..012b74cf 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -266,6 +266,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
         Abc_NtkAddDummyBoxNames( pNtkNew );
     else
     {
+/*
         {
             int i, k, iFlop, Counter = 0;
             FILE * pFile;
@@ -285,6 +286,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
             fclose( pFile );
             //printf( "\n" );
         }
+*/
         assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
         nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) );
         Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
@@ -1622,11 +1624,14 @@ timeInt = 0;
         }
         else
             pNtkInter1 = Abc_NtkInterOne( pNtkOn1, pNtkOff1, fVerbose );
-        Abc_NtkAppend( pNtkInter, pNtkInter1, 1 );
+        if ( pNtkInter1 )
+        {
+            Abc_NtkAppend( pNtkInter, pNtkInter1, 1 );
+            Abc_NtkDelete( pNtkInter1 );
+        }
 
         Abc_NtkDelete( pNtkOn1 );
         Abc_NtkDelete( pNtkOff1 );
-        Abc_NtkDelete( pNtkInter1 );
     }
 //    PRT( "CNF", timeCnf );
 //    PRT( "SAT", timeSat );
diff --git a/src/base/abci/abcDelay.c b/src/base/abci/abcDelay.c
index bb654b73..67e051f3 100644
--- a/src/base/abci/abcDelay.c
+++ b/src/base/abci/abcDelay.c
@@ -33,11 +33,12 @@ static inline void  Abc_ObjSetArrival( Abc_Obj_t * pNode, float Time )  { pNode-
 static inline void  Abc_ObjSetRequired( Abc_Obj_t * pNode, float Time ) { pNode->pNtk->pLutTimes[3*pNode->Id+1] = Time; }
 static inline void  Abc_ObjSetSlack( Abc_Obj_t * pNode, float Time )    { pNode->pNtk->pLutTimes[3*pNode->Id+2] = Time; }
 
+extern void * Abc_FrameReadLibLut();   
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-
 /**Function*************************************************************
 
   Synopsis    [Sorts the pins in the decreasing order of delays.]
@@ -95,7 +96,6 @@ void Abc_NtkDelayTraceSortPins( Abc_Obj_t * pNode, int * pPinPerm, float * pPinD
 ***********************************************************************/
 float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib )
 {
-    extern void * Abc_FrameReadLibLut();   
     int fUseSorting = 0;
     int pPinPerm[32];
     float pPinDelays[32];
diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c
index 7c18ca2c..e40c21d6 100644
--- a/src/base/abci/abcGen.c
+++ b/src/base/abci/abcGen.c
@@ -131,7 +131,7 @@ void Abc_GenSorter( char * pFileName, int nVars )
             fprintf( pFile, " y%02d=%0*d", k, nDigits, Counter++ );
         fprintf( pFile, "\n" );
         Counter -= nVars;
-        for ( i = 1; i < nVars-2; i++ )
+        for ( i = 1; i < 2*nVars-2; i++ )
         {
             fprintf( pFile, ".subckt Layer%d", (i&1) );
             for ( k = 0; k < nVars; k++ )
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 58614584..afdfbdeb 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -591,6 +591,16 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
         ASat_SolverSetPrefVars( pSat, pPrefVars, nVars );
     }
 */
+/*
+    Abc_NtkForEachObj( pNtk, pNode, i )
+    {
+        if ( !pNode->fMarkA )
+            continue;
+        printf( "%10s : ", Abc_ObjName(pNode) );
+        printf( "%3d\n", (int)pNode->pCopy );
+    }
+    printf( "\n" );
+*/
     RetValue = 1;
 Quits :
     // delete
@@ -876,6 +886,121 @@ finish:
 
 
 
+/**Function*************************************************************
+
+  Synopsis    [Writes CNF for the sorter with N inputs asserting Q ones.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens )
+{
+    extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
+    extern void * Abc_FrameGetGlobalFrame();
+    extern Abc_Ntk_t * Abc_FrameReadNtk( void * p );
+
+    char Command[100];
+    void * pAbc;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pObj, * ppNodes[2], * ppRoots[2];
+    Vec_Ptr_t * vNodes;
+    FILE * pFile;
+    int i, Counter;
+
+    if ( nQueens <= 0 && nQueens >= nVars )
+    {
+        printf( "The number of queens (Q = %d) should belong to the interval: 0 < Q < %d.\n", nQueens, nQueens, nVars );
+        return;
+    }
+    assert( nQueens > 0 && nQueens < nVars );
+    pAbc = Abc_FrameGetGlobalFrame();
+    // generate sorter
+    sprintf( Command, "gen -s -N %d sorter%d.blif", nVars, nVars );
+    if ( Cmd_CommandExecute( pAbc, Command ) )
+    {
+        fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
+        return;
+    }
+    // read the file
+    sprintf( Command, "read sorter%d.blif; strash", nVars );
+    if ( Cmd_CommandExecute( pAbc, Command ) )
+    {
+        fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
+        return;
+    }
+
+    // get the current network
+    pNtk = Abc_FrameReadNtk(pAbc);
+    // collect the nodes for the given two primary outputs
+    ppNodes[0] = Abc_NtkPo( pNtk, nVars - nQueens - 1 );
+    ppNodes[1] = Abc_NtkPo( pNtk, nVars - nQueens );
+    ppRoots[0] = Abc_ObjFanin0( ppNodes[0] );
+    ppRoots[1] = Abc_ObjFanin0( ppNodes[1] );
+    vNodes = Abc_NtkDfsNodes( pNtk, ppRoots, 2 );
+
+    // assign CNF variables
+    Counter = 0;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->pCopy = (void *)~0;
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pObj->pCopy = (void *)Counter++;
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = (void *)Counter++;
+
+/*
+        OutVar   = pCnf->pVarNums[ pObj->Id ];
+        pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
+        pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
+
+        // positive phase
+        *pClas++ = pLits;
+        *pLits++ = 2 * OutVar; 
+        *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj); 
+        *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj); 
+        // negative phase
+        *pClas++ = pLits;
+        *pLits++ = 2 * OutVar + 1; 
+        *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj); 
+        *pClas++ = pLits;
+        *pLits++ = 2 * OutVar + 1; 
+        *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj); 
+*/
+
+    // add clauses for these nodes
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "c CNF for %d-bit sorter with %d bits set to 1 generated by ABC.\n", nVars, nQueens );
+    fprintf( pFile, "p cnf %d %d\n", Counter, 3 * Vec_PtrSize(vNodes) + 2 );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // positive phase
+        fprintf( pFile, "%d %s%d %s%d 0\n", 1+(int)pObj->pCopy, 
+            Abc_ObjFaninC0(pObj)? "" : "-", 1+(int)Abc_ObjFanin0(pObj)->pCopy,
+            Abc_ObjFaninC1(pObj)? "" : "-", 1+(int)Abc_ObjFanin1(pObj)->pCopy );
+        // negative phase
+        fprintf( pFile, "-%d %s%d 0\n", 1+(int)pObj->pCopy, 
+            Abc_ObjFaninC0(pObj)? "-" : "", 1+(int)Abc_ObjFanin0(pObj)->pCopy );
+        fprintf( pFile, "-%d %s%d 0\n", 1+(int)pObj->pCopy, 
+            Abc_ObjFaninC1(pObj)? "-" : "", 1+(int)Abc_ObjFanin1(pObj)->pCopy );
+    }
+    Vec_PtrFree( vNodes );
+
+/*
+    *pClas++ = pLits;
+    *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
+*/
+    // assert the first literal to zero
+    fprintf( pFile, "%s%d 0\n", 
+        Abc_ObjFaninC0(ppNodes[0])? "" : "-", 1+(int)Abc_ObjFanin0(ppNodes[0])->pCopy );
+    // assert the second literal to one
+    fprintf( pFile, "%s%d 0\n", 
+        Abc_ObjFaninC0(ppNodes[1])? "-" : "", 1+(int)Abc_ObjFanin0(ppNodes[1])->pCopy );
+    fclose( pFile );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 4cac6190..fd57f430 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -168,17 +168,17 @@ int CmdCommandTime( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     pAbc->TimeTotal += pAbc->TimeCommand;
-    fprintf( pAbc->Out, "elapse: %3.2f seconds, total: %3.2f seconds\n",
-        (float)(1.0 * pAbc->TimeCommand / CLOCKS_PER_SEC), (float)(1.0 * pAbc->TimeTotal / CLOCKS_PER_SEC) );
+    fprintf( pAbc->Out, "elapse: %3.2f seconds, total: %3.2f seconds\n", 
+        pAbc->TimeCommand, pAbc->TimeTotal );
 /*
     {
         FILE * pTable;
         pTable = fopen( "runtimes.txt", "a+" );
-        fprintf( pTable, "%4.2f\n", (float)pAbc->TimeCommand / CLOCKS_PER_SEC );
+        fprintf( pTable, "%4.2f\n", pAbc->TimeCommand );
         fclose( pTable );
     }
 */
-    pAbc->TimeCommand = 0;
+    pAbc->TimeCommand = 0.0;
     return 0;
 
   usage:
diff --git a/src/base/cmd/cmdUtils.c b/src/base/cmd/cmdUtils.c
index 47e54bb3..6b4bdcbe 100644
--- a/src/base/cmd/cmdUtils.c
+++ b/src/base/cmd/cmdUtils.c
@@ -92,7 +92,7 @@ int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv )
     Abc_Command * pCommand;
     char * value;
     int fError;
-    int clk;
+    double clk;
 
     if ( argc == 0 )
         return 0;
@@ -121,10 +121,10 @@ int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     // execute the command
-    clk = Extra_CpuTime();
+    clk = Extra_CpuTimeDouble();
     pFunc = (int (*)(Abc_Frame_t *, int, char **))pCommand->pFunc;
     fError = (*pFunc)( pAbc, argc, argv );
-    pAbc->TimeCommand += (Extra_CpuTime() - clk);
+    pAbc->TimeCommand += Extra_CpuTimeDouble() - clk;
 
     // automatic execution of arbitrary command after each command 
     // usually this is a passive command ... 
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 628ef2b9..551feb0b 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -58,6 +58,7 @@ static int IoCommandWriteList   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWritePla    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteSortCnf( Abc_Frame_t * pAbc, int argc, char **argv );
 
 extern int glo_fMapped;
 
@@ -111,6 +112,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "write_pla",     IoCommandWritePla,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 );
 //    Cmd_CommandAdd( pAbc, "I/O", "write_verlib",  IoCommandWriteVerLib,  0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_sorter_cnf", IoCommandWriteSortCnf,  0 );
 }
 
 /**Function*************************************************************
@@ -2010,6 +2012,76 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandWriteSortCnf( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    char * pFileName;
+    int c;
+    int nVars = 16;
+    int nQueens = 4;
+    extern void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens );
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NQh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'N':
+                if ( globalUtilOptind >= argc )
+                {
+                    fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
+                    goto usage;
+                }
+                nVars = atoi(argv[globalUtilOptind]);
+                globalUtilOptind++;
+                if ( nVars <= 0 ) 
+                    goto usage;
+                break;
+            case 'Q':
+                if ( globalUtilOptind >= argc )
+                {
+                    fprintf( stdout, "Command line switch \"-Q\" should be followed by an integer.\n" );
+                    goto usage;
+                }
+                nQueens = atoi(argv[globalUtilOptind]);
+                globalUtilOptind++;
+                if ( nQueens <= 0 ) 
+                    goto usage;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 1 )
+        goto usage;
+    // get the output file name
+    pFileName = argv[globalUtilOptind];
+    Abc_NtkWriteSorterCnf( pFileName, nVars, nQueens );
+    // call the corresponding file writer
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_sorter_cnf [-N <num>] [-Q <num>] <file>\n" );
+    fprintf( pAbc->Err, "\t         write CNF for the sorter\n" );
+    fprintf( pAbc->Err, "\t-N num : the number of sorter bits [default = %d]\n", nVars );
+    fprintf( pAbc->Err, "\t-Q num : the number of bits to be asserted to 1 [default = %d]\n", nQueens );
+    fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 1d8cd70f..f82e12d6 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -61,8 +61,8 @@ struct Abc_Frame_t_
     FILE *          Err;
     FILE *          Hst;
     // used for runtime measurement
-    PORT_INT64_T    TimeCommand; // the runtime of the last command
-    PORT_INT64_T    TimeTotal;   // the total runtime of all commands
+    double          TimeCommand; // the runtime of the last command
+    double          TimeTotal;   // the total runtime of all commands
     // temporary storage for structural choices
     Vec_Ptr_t *     vStore;      // networks to be used by choice
     // decomposition package
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index dc2aac28..8f86fc32 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -607,6 +607,7 @@ extern unsigned    Extra_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux
 
 
 extern long        Extra_CpuTime();
+extern double      Extra_CpuTimeDouble();
 extern int         Extra_GetSoftDataLimit();
 extern void        Extra_UtilGetoptReset();
 extern int         Extra_UtilGetopt( int argc, char *argv[], char *optstring );
diff --git a/src/misc/extra/extraUtilUtil.c b/src/misc/extra/extraUtilUtil.c
index e2c407cd..abe08d7a 100644
--- a/src/misc/extra/extraUtilUtil.c
+++ b/src/misc/extra/extraUtilUtil.c
@@ -344,20 +344,36 @@ void (*Extra_UtilMMoutOfMemory)() = Extra_UtilMMout_Of_Memory;
   SeeAlso     []
 
 ***********************************************************************/
-#if defined(NT) || defined(NT64) || defined(WIN32)
 long Extra_CpuTime()
 {
     return clock();
 }
+
+/**Function*************************************************************
+
+  Synopsis    [util_cpu_time()]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+#if defined(NT) || defined(NT64) || defined(WIN32)
+double Extra_CpuTimeDouble()
+{
+    return (double)clock()/CLOCKS_PER_SEC;
+}
 #else
 #include <sys/time.h>
 #include <sys/resource.h>
 #include <unistd.h>
-long Extra_CpuTime()
+double Extra_CpuTimeDouble()
 {
     struct rusage ru;
     getrusage(RUSAGE_SELF, &ru);
-    return (long)(CLOCKS_PER_SEC * ((double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000)); 
+    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; 
 }
 #endif
 
diff --git a/src/sat/bsat/satInterP.c b/src/sat/bsat/satInterP.c
new file mode 100644
index 00000000..9559b39f
--- /dev/null
+++ b/src/sat/bsat/satInterP.c
@@ -0,0 +1,888 @@
+/**CFile****************************************************************
+
+  FileName    [satInter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT sat_solver.]
+
+  Synopsis    [Interpolation package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: satInter.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+#include "satStore.h"
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// variable assignments 
+static const lit    LIT_UNDEF = 0xffffffff;
+
+// interpolation manager
+struct Intp_Man_t_
+{
+    // clauses of the problems
+    Sto_Man_t *     pCnf;         // the set of CNF clauses for A and B
+    // various parameters
+    int             fVerbose;     // verbosiness flag
+    int             fProofVerif;  // verifies the proof
+    int             fProofWrite;  // writes the proof file
+    int             nVarsAlloc;   // the allocated size of var arrays
+    int             nClosAlloc;   // the allocated size of clause arrays
+    // internal BCP
+    int             nRootSize;    // the number of root level assignments
+    int             nTrailSize;   // the number of assignments made 
+    lit *           pTrail;       // chronological order of assignments (size nVars)
+    lit *           pAssigns;     // assignments by variable (size nVars) 
+    char *          pSeens;       // temporary mark (size nVars)
+    Sto_Cls_t **    pReasons;     // reasons for each assignment (size nVars)          
+    Sto_Cls_t **    pWatches;     // watched clauses for each literal (size 2*nVars)          
+    // proof data
+    Vec_Int_t *     vAnties;      // anticedents for all clauses
+    Vec_Int_t *     vBreaks;      // beginnings of anticedents for each clause
+    // proof recording
+    int             Counter;      // counter of resolved clauses
+    int *           pProofNums;   // the proof numbers for each clause (size nClauses)
+    FILE *          pFile;        // the file for proof recording
+    // internal verification
+    lit *           pResLits;     // the literals of the resolvent   
+    int             nResLits;     // the number of literals of the resolvent
+    int             nResLitsAlloc;// the number of literals of the resolvent
+    // runtime stats
+    int             timeBcp;      // the runtime for BCP
+    int             timeTrace;    // the runtime of trace construction
+    int             timeTotal;    // the total runtime of interpolation
+};
+
+// reading/writing the proof for a clause
+static inline int          Intp_ManProofGet( Intp_Man_t * p, Sto_Cls_t * pCls )                  { return p->pProofNums[pCls->Id];           }
+static inline void         Intp_ManProofSet( Intp_Man_t * p, Sto_Cls_t * pCls, int n )           { p->pProofNums[pCls->Id] = n;              }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Intp_Man_t * Intp_ManAlloc()
+{
+    Intp_Man_t * p;
+    // allocate the manager
+    p = (Intp_Man_t *)malloc( sizeof(Intp_Man_t) );
+    memset( p, 0, sizeof(Intp_Man_t) );
+    // verification
+    p->nResLitsAlloc = (1<<16);
+    p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
+    // proof recording
+    p->vAnties = Vec_IntAlloc( 1000 );
+    p->vBreaks = Vec_IntAlloc( 1000 );
+    // parameters
+    p->fProofWrite = 0;
+    p->fProofVerif = 1;
+    return p;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resize proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Intp_ManResize( Intp_Man_t * p )
+{
+    // check if resizing is needed
+    if ( p->nVarsAlloc < p->pCnf->nVars )
+    {
+        // find the new size
+        if ( p->nVarsAlloc == 0 )
+            p->nVarsAlloc = 1;
+        while ( p->nVarsAlloc < p->pCnf->nVars ) 
+            p->nVarsAlloc *= 2;
+        // resize the arrays
+        p->pTrail    = (lit *)       realloc( p->pTrail,    sizeof(lit) * p->nVarsAlloc );
+        p->pAssigns  = (lit *)       realloc( p->pAssigns,  sizeof(lit) * p->nVarsAlloc );
+        p->pSeens    = (char *)      realloc( p->pSeens,    sizeof(char) * p->nVarsAlloc );
+//        p->pVarTypes = (int *)       realloc( p->pVarTypes, sizeof(int) * p->nVarsAlloc );
+        p->pReasons  = (Sto_Cls_t **)realloc( p->pReasons,  sizeof(Sto_Cls_t *) * p->nVarsAlloc );
+        p->pWatches  = (Sto_Cls_t **)realloc( p->pWatches,  sizeof(Sto_Cls_t *) * p->nVarsAlloc*2 );
+    }
+
+    // clean the free space
+    memset( p->pAssigns , 0xff, sizeof(lit) * p->pCnf->nVars );
+    memset( p->pSeens   , 0,    sizeof(char) * p->pCnf->nVars );
+//    memset( p->pVarTypes, 0,    sizeof(int) * p->pCnf->nVars );
+    memset( p->pReasons , 0,    sizeof(Sto_Cls_t *) * p->pCnf->nVars );
+    memset( p->pWatches , 0,    sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 );
+
+    // check if resizing of clauses is needed
+    if ( p->nClosAlloc < p->pCnf->nClauses )
+    {
+        // find the new size
+        if ( p->nClosAlloc == 0 )
+            p->nClosAlloc = 1;
+        while ( p->nClosAlloc < p->pCnf->nClauses ) 
+            p->nClosAlloc *= 2;
+        // resize the arrays
+        p->pProofNums = (int *) realloc( p->pProofNums,  sizeof(int) * p->nClosAlloc );
+    }
+    memset( p->pProofNums, 0, sizeof(int) * p->pCnf->nClauses );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Intp_ManFree( Intp_Man_t * p )
+{
+/*
+    printf( "Runtime stats:\n" );
+PRT( "BCP     ", p->timeBcp   );
+PRT( "Trace   ", p->timeTrace );
+PRT( "TOTAL   ", p->timeTotal );
+*/
+    Vec_IntFree( p->vAnties );
+    Vec_IntFree( p->vBreaks );
+//    free( p->pInters );
+    free( p->pProofNums );
+    free( p->pTrail );
+    free( p->pAssigns );
+    free( p->pSeens );
+//    free( p->pVarTypes );
+    free( p->pReasons );
+    free( p->pWatches );
+    free( p->pResLits );
+    free( p );
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Intp_ManPrintClause( Intp_Man_t * p, Sto_Cls_t * pClause )
+{
+    int i;
+    printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Intp_ManProofGet(p, pClause) );
+    for ( i = 0; i < (int)pClause->nLits; i++ )
+        printf( " %d", pClause->pLits[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the resolvent.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Intp_ManPrintResolvent( lit * pResLits, int nResLits )
+{
+    int i;
+    printf( "Resolvent: {" );
+    for ( i = 0; i < nResLits; i++ )
+        printf( " %d", pResLits[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the interpolant for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Intp_ManPrintInterOne( Intp_Man_t * p, Sto_Cls_t * pClause )
+{
+    printf( "Clause %2d :  ", pClause->Id );
+//    Extra_PrintBinary___( stdout, Intp_ManAigRead(p, pClause), (1 << p->nVarsAB) );
+    printf( "\n" );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one clause to the watcher list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Intp_ManWatchClause( Intp_Man_t * p, Sto_Cls_t * pClause, lit Lit )
+{
+    assert( lit_check(Lit, p->pCnf->nVars) );
+    if ( pClause->pLits[0] == Lit )
+        pClause->pNext0 = p->pWatches[lit_neg(Lit)];  
+    else
+    {
+        assert( pClause->pLits[1] == Lit );
+        pClause->pNext1 = p->pWatches[lit_neg(Lit)];  
+    }
+    p->pWatches[lit_neg(Lit)] = pClause;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Records implication.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Intp_ManEnqueue( Intp_Man_t * p, lit Lit, Sto_Cls_t * pReason )
+{
+    int Var = lit_var(Lit);
+    if ( p->pAssigns[Var] != LIT_UNDEF )
+        return p->pAssigns[Var] == Lit;
+    p->pAssigns[Var] = Lit;
+    p->pReasons[Var] = pReason;
+    p->pTrail[p->nTrailSize++] = Lit;
+//printf( "assigning var %d value %d\n", Var, !lit_sign(Lit) );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records implication.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Intp_ManCancelUntil( Intp_Man_t * p, int Level )
+{
+    lit Lit;
+    int i, Var;
+    for ( i = p->nTrailSize - 1; i >= Level; i-- )
+    {
+        Lit = p->pTrail[i];
+        Var = lit_var( Lit );
+        p->pReasons[Var] = NULL;
+        p->pAssigns[Var] = LIT_UNDEF;
+//printf( "cancelling var %d\n", Var );
+    }
+    p->nTrailSize = Level;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagate one assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Sto_Cls_t * Intp_ManPropagateOne( Intp_Man_t * p, lit Lit )
+{
+    Sto_Cls_t ** ppPrev, * pCur, * pTemp;
+    lit LitF = lit_neg(Lit);
+    int i;
+    // iterate through the literals
+    ppPrev = p->pWatches + Lit;
+    for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev )
+    {
+        // make sure the false literal is in the second literal of the clause
+        if ( pCur->pLits[0] == LitF )
+        {
+            pCur->pLits[0] = pCur->pLits[1];
+            pCur->pLits[1] = LitF;
+            pTemp = pCur->pNext0;
+            pCur->pNext0 = pCur->pNext1;
+            pCur->pNext1 = pTemp;
+        }
+        assert( pCur->pLits[1] == LitF );
+
+        // if the first literal is true, the clause is satisfied
+        if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] )
+        {
+            ppPrev = &pCur->pNext1;
+            continue;
+        }
+
+        // look for a new literal to watch
+        for ( i = 2; i < (int)pCur->nLits; i++ )
+        {
+            // skip the case when the literal is false
+            if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] )
+                continue;
+            // the literal is either true or unassigned - watch it
+            pCur->pLits[1] = pCur->pLits[i];
+            pCur->pLits[i] = LitF;
+            // remove this clause from the watch list of Lit
+            *ppPrev = pCur->pNext1;
+            // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1])
+            Intp_ManWatchClause( p, pCur, pCur->pLits[1] );
+            break;
+        }
+        if ( i < (int)pCur->nLits ) // found new watch
+            continue;
+
+        // clause is unit - enqueue new implication
+        if ( Intp_ManEnqueue(p, pCur->pLits[0], pCur) )
+        {
+            ppPrev = &pCur->pNext1;
+            continue;
+        }
+
+        // conflict detected - return the conflict clause
+        return pCur;
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagate the current assignments.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sto_Cls_t * Intp_ManPropagate( Intp_Man_t * p, int Start )
+{
+    Sto_Cls_t * pClause;
+    int i;
+    int clk = clock();
+    for ( i = Start; i < p->nTrailSize; i++ )
+    {
+        pClause = Intp_ManPropagateOne( p, p->pTrail[i] );
+        if ( pClause )
+        {
+p->timeBcp += clock() - clk;
+            return pClause;
+        }
+    }
+p->timeBcp += clock() - clk;
+    return NULL;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Writes one root clause into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Intp_ManProofWriteOne( Intp_Man_t * p, Sto_Cls_t * pClause )
+{
+    Intp_ManProofSet( p, pClause, ++p->Counter );
+
+    if ( p->fProofWrite )
+    {
+        int v;
+        fprintf( p->pFile, "%d", Intp_ManProofGet(p, pClause) );
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+            fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) );
+        fprintf( p->pFile, " 0 0\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Traces the proof for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Intp_ManProofTraceOne( Intp_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFinal )
+{
+    Sto_Cls_t * pReason;
+    int i, v, Var, PrevId;
+    int fPrint = 0;
+    int clk = clock();
+
+    // collect resolvent literals
+    if ( p->fProofVerif )
+    {
+        assert( (int)pConflict->nLits <= p->nResLitsAlloc );
+        memcpy( p->pResLits, pConflict->pLits, sizeof(lit) * pConflict->nLits );
+        p->nResLits = pConflict->nLits;
+    }
+
+    // mark all the variables in the conflict as seen
+    for ( v = 0; v < (int)pConflict->nLits; v++ )
+        p->pSeens[lit_var(pConflict->pLits[v])] = 1;
+
+    // start the anticedents
+//    pFinal->pAntis = Vec_PtrAlloc( 32 );
+//    Vec_PtrPush( pFinal->pAntis, pConflict );
+    assert( pFinal->Id == Vec_IntSize(p->vBreaks) );
+    Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) );
+    Vec_IntPush( p->vAnties, pConflict->Id );
+
+//    if ( p->pCnf->nClausesA )
+//        Intp_ManAigCopy( p, Intp_ManAigRead(p, pFinal), Intp_ManAigRead(p, pConflict) );
+
+    // follow the trail backwards
+    PrevId = Intp_ManProofGet(p, pConflict);
+    for ( i = p->nTrailSize - 1; i >= 0; i-- )
+    {
+        // skip literals that are not involved
+        Var = lit_var(p->pTrail[i]);
+        if ( !p->pSeens[Var] )
+            continue;
+        p->pSeens[Var] = 0;
+
+        // skip literals of the resulting clause
+        pReason = p->pReasons[Var];
+        if ( pReason == NULL )
+            continue;
+        assert( p->pTrail[i] == pReason->pLits[0] );
+
+        // add the variables to seen
+        for ( v = 1; v < (int)pReason->nLits; v++ )
+            p->pSeens[lit_var(pReason->pLits[v])] = 1;
+
+
+        // record the reason clause
+        assert( Intp_ManProofGet(p, pReason) > 0 );
+        p->Counter++;
+        if ( p->fProofWrite )
+            fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Intp_ManProofGet(p, pReason) );
+        PrevId = p->Counter;
+
+//        if ( p->pCnf->nClausesA )
+//       {
+//            if ( p->pVarTypes[Var] == 1 ) // var of A
+//                Intp_ManAigOr( p, Intp_ManAigRead(p, pFinal), Intp_ManAigRead(p, pReason) );
+//            else
+//                Intp_ManAigAnd( p, Intp_ManAigRead(p, pFinal), Intp_ManAigRead(p, pReason) );
+//        }
+ 
+        // resolve the temporary resolvent with the reason clause
+        if ( p->fProofVerif )
+        {
+            int v1, v2; 
+            if ( fPrint )
+                Intp_ManPrintResolvent( p->pResLits, p->nResLits );
+            // check that the var is present in the resolvent
+            for ( v1 = 0; v1 < p->nResLits; v1++ )
+                if ( lit_var(p->pResLits[v1]) == Var )
+                    break;
+            if ( v1 == p->nResLits )
+                printf( "Recording clause %d: Cannot find variable %d in the temporary resolvent.\n", pFinal->Id, Var );
+            if ( p->pResLits[v1] != lit_neg(pReason->pLits[0]) )
+                printf( "Recording clause %d: The resolved variable %d is in the wrong polarity.\n", pFinal->Id, Var );
+            // remove this variable from the resolvent
+            assert( lit_var(p->pResLits[v1]) == Var );
+            p->nResLits--;
+            for ( ; v1 < p->nResLits; v1++ )
+                p->pResLits[v1] = p->pResLits[v1+1];
+            // add variables of the reason clause
+            for ( v2 = 1; v2 < (int)pReason->nLits; v2++ )
+            {
+                for ( v1 = 0; v1 < p->nResLits; v1++ )
+                    if ( lit_var(p->pResLits[v1]) == lit_var(pReason->pLits[v2]) )
+                        break;
+                // if it is a new variable, add it to the resolvent
+                if ( v1 == p->nResLits ) 
+                {
+                    if ( p->nResLits == p->nResLitsAlloc )
+                        printf( "Recording clause %d: Ran out of space for intermediate resolvent.\n", pFinal->Id );
+                    p->pResLits[ p->nResLits++ ] = pReason->pLits[v2];
+                    continue;
+                }
+                // if the variable is the same, the literal should be the same too
+                if ( p->pResLits[v1] == pReason->pLits[v2] )
+                    continue;
+                // the literal is different
+                printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id );
+            }
+        }
+
+//        Vec_PtrPush( pFinal->pAntis, pReason );
+        Vec_IntPush( p->vAnties, pReason->Id );
+    }
+
+    // unmark all seen variables
+//    for ( i = p->nTrailSize - 1; i >= 0; i-- )
+//        p->pSeens[lit_var(p->pTrail[i])] = 0;
+    // check that the literals are unmarked
+//    for ( i = p->nTrailSize - 1; i >= 0; i-- )
+//        assert( p->pSeens[lit_var(p->pTrail[i])] == 0 );
+
+    // use the resulting clause to check the correctness of resolution
+    if ( p->fProofVerif )
+    {
+        int v1, v2; 
+        if ( fPrint )
+            Intp_ManPrintResolvent( p->pResLits, p->nResLits );
+        for ( v1 = 0; v1 < p->nResLits; v1++ )
+        {
+            for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ )
+                if ( pFinal->pLits[v2] == p->pResLits[v1] )
+                    break;
+            if ( v2 < (int)pFinal->nLits )
+                continue;
+            break;
+        }
+        if ( v1 < p->nResLits )
+        {
+            printf( "Recording clause %d: The final resolvent is wrong.\n", pFinal->Id );
+            Intp_ManPrintClause( p, pConflict );
+            Intp_ManPrintResolvent( p->pResLits, p->nResLits );
+            Intp_ManPrintClause( p, pFinal );
+        }
+    }
+p->timeTrace += clock() - clk;
+
+    // return the proof pointer 
+//    if ( p->pCnf->nClausesA )
+//    {
+//        Intp_ManPrintInterOne( p, pFinal );
+//    }
+    Intp_ManProofSet( p, pFinal, p->Counter );
+    return p->Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Intp_ManProofRecordOne( Intp_Man_t * p, Sto_Cls_t * pClause )
+{
+    Sto_Cls_t * pConflict;
+    int i;
+
+    // empty clause never ends up there
+    assert( pClause->nLits > 0 );
+    if ( pClause->nLits == 0 )
+        printf( "Error: Empty clause is attempted.\n" );
+
+    // add assumptions to the trail
+    assert( !pClause->fRoot );
+    assert( p->nTrailSize == p->nRootSize );
+    for ( i = 0; i < (int)pClause->nLits; i++ )
+        if ( !Intp_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
+        {
+            assert( 0 ); // impossible
+            return 0;
+        }
+
+    // propagate the assumptions
+    pConflict = Intp_ManPropagate( p, p->nRootSize );
+    if ( pConflict == NULL )
+    {
+        assert( 0 ); // cannot prove
+        return 0;
+    }
+
+    // construct the proof
+    Intp_ManProofTraceOne( p, pConflict, pClause );
+
+    // undo to the root level
+    Intp_ManCancelUntil( p, p->nRootSize );
+
+    // add large clauses to the watched lists
+    if ( pClause->nLits > 1 )
+    {
+        Intp_ManWatchClause( p, pClause, pClause->pLits[0] );
+        Intp_ManWatchClause( p, pClause, pClause->pLits[1] );
+        return 1;
+    }
+    assert( pClause->nLits == 1 );
+
+    // if the clause proved is unit, add it and propagate
+    if ( !Intp_ManEnqueue( p, pClause->pLits[0], pClause ) )
+    {
+        assert( 0 ); // impossible
+        return 0;
+    }
+
+    // propagate the assumption
+    pConflict = Intp_ManPropagate( p, p->nRootSize );
+    if ( pConflict )
+    {
+        // construct the proof
+        Intp_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty );
+//        if ( p->fVerbose )
+//            printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id );
+        return 0;
+    }
+
+    // update the root level
+    p->nRootSize = p->nTrailSize;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagate the root clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Intp_ManProcessRoots( Intp_Man_t * p )
+{
+    Sto_Cls_t * pClause;
+    int Counter;
+
+    // make sure the root clauses are preceeding the learnt clauses
+    Counter = 0;
+    Sto_ManForEachClause( p->pCnf, pClause )
+    {
+        assert( (int)pClause->fA    == (Counter < (int)p->pCnf->nClausesA) );
+        assert( (int)pClause->fRoot == (Counter < (int)p->pCnf->nRoots)    );
+        Counter++;
+    }
+    assert( p->pCnf->nClauses == Counter );
+
+    // make sure the last clause if empty
+    assert( p->pCnf->pTail->nLits == 0 );
+
+    // go through the root unit clauses
+    p->nTrailSize = 0;
+    Sto_ManForEachClauseRoot( p->pCnf, pClause )
+    {
+        // create watcher lists for the root clauses
+        if ( pClause->nLits > 1 )
+        {
+            Intp_ManWatchClause( p, pClause, pClause->pLits[0] );
+            Intp_ManWatchClause( p, pClause, pClause->pLits[1] );
+        }
+        // empty clause and large clauses
+        if ( pClause->nLits != 1 )
+            continue;
+        // unit clause
+        assert( lit_check(pClause->pLits[0], p->pCnf->nVars) );
+        if ( !Intp_ManEnqueue( p, pClause->pLits[0], pClause ) )
+        {
+            // detected root level conflict
+            printf( "Error in Intp_ManProcessRoots(): Detected a root-level conflict too early!\n" );
+            assert( 0 );
+            return 0;
+        }
+    }
+
+    // propagate the root unit clauses
+    pClause = Intp_ManPropagate( p, 0 );
+    if ( pClause )
+    {
+        // detected root level conflict
+        Intp_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
+        if ( p->fVerbose )
+            printf( "Found root level conflict!\n" );
+        return 0;
+    }
+
+    // set the root level
+    p->nRootSize = p->nTrailSize;
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively computes the UNSAT core.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Intp_ManUnsatCore_rec( Vec_Int_t * vAnties, Vec_Int_t * vBreaks, int iThis, Vec_Int_t * vCore, int nRoots )
+{
+    int i, iStop, iStart;
+    // skip of this clause was visited
+    iStart = Vec_IntEntry( vBreaks, iThis );
+    if ( iStart == -1 )
+        return;
+    // mark this clause as visited
+    Vec_IntWriteEntry( vBreaks, iThis, -1 );
+    // add a root clause to the core
+    if ( iThis < nRoots )
+    {
+        Vec_IntPush( vCore, iThis );
+        return;
+    }
+    // iterate through the clauses
+    iStop = Vec_IntEntry( vBreaks, iThis+1 );
+    for ( i = iStart; i < iStop; i++ )
+        Intp_ManUnsatCore_rec( vAnties, vBreaks, Vec_IntEntry(vAnties, i), vCore, nRoots );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes UNSAT core of the satisfiablity problem.]
+
+  Description [Takes the interpolation manager, the CNF deriving by the SAT
+  solver, which includes the root clauses and the learned clauses. Returns
+  the array of integers representing the number of root clauses that are in
+  the UNSAT core.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
+{
+    Vec_Int_t * vCore;
+    Sto_Cls_t * pClause;
+    int RetValue = 1;
+    int clkTotal = clock();
+
+    // check that the CNF makes sense
+    assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
+    p->pCnf = pCnf;
+    p->fVerbose = fVerbose;
+
+    // adjust the manager
+    Intp_ManResize( p );
+
+    // construct proof for each clause
+    // start the proof
+    if ( p->fProofWrite )
+    {
+        p->pFile = fopen( "proof.cnf_", "w" );
+        p->Counter = 0;
+    }
+
+    // write the root clauses
+    Vec_IntClear( p->vAnties );
+    Vec_IntFill( p->vBreaks, p->pCnf->nRoots, 0 );
+    Sto_ManForEachClauseRoot( p->pCnf, pClause )
+        Intp_ManProofWriteOne( p, pClause );
+
+    // propagate root level assignments
+    if ( Intp_ManProcessRoots( p ) )
+    {
+        // if there is no conflict, consider learned clauses
+        Sto_ManForEachClause( p->pCnf, pClause )
+        {
+            if ( pClause->fRoot )
+                continue;
+            if ( !Intp_ManProofRecordOne( p, pClause ) )
+            {
+                RetValue = 0;
+                break;
+            }
+        }
+    }
+
+    // add the last breaker
+    assert( p->pCnf->pEmpty->Id == Vec_IntSize(p->vBreaks) - 1 );
+    Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) );
+
+    // stop the proof
+    if ( p->fProofWrite )
+    {
+        fclose( p->pFile );
+        p->pFile = NULL;    
+    }
+
+    if ( fVerbose )
+    {
+        PRT( "Core", clock() - clkTotal );
+    printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f Mb\n", 
+        p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
+        1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 
+        1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
+p->timeTotal += clock() - clkTotal;
+    }
+
+    // derive the UNSAT core
+    vCore = Vec_IntAlloc( 1000 );
+    Intp_ManUnsatCore_rec( p->vAnties, p->vBreaks, p->pCnf->pEmpty->Id, vCore, p->pCnf->nRoots );
+    if ( fVerbose )
+        printf( "Root clauses = %d. Learned clauses = %d. UNSAT core size = %d.\n", 
+            p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, Vec_IntSize(vCore) );
+    return vCore;   
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h
index bbd7b28b..027afcb4 100644
--- a/src/sat/bsat/satStore.h
+++ b/src/sat/bsat/satStore.h
@@ -135,6 +135,12 @@ extern Inta_Man_t * Inta_ManAlloc();
 extern void         Inta_ManFree( Inta_Man_t * p );
 extern void *       Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose );
 
+/*=== satInterP.c ==========================================================*/
+typedef struct Intp_Man_t_ Intp_Man_t;
+extern Intp_Man_t * Intp_ManAlloc();
+extern void         Intp_ManFree( Intp_Man_t * p );
+extern void *       Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose );
+
 #ifdef __cplusplus
 }
 #endif