Version abc80116

15 files changed, 1328 insertions, 20 deletions

diff --git a/abc.dsp b/abc.dsp
index 60827bb2..b731f58f 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -1170,6 +1170,10 @@ SOURCE=.\src\sat\bsat\satInter.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\bsat\satInterA.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\bsat\satMem.c
 # End Source File
 # Begin Source File
@@ -2870,6 +2874,10 @@ SOURCE=.\src\aig\aig\aigHaig.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\aig\aigInter.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\aig\aigMan.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c
new file mode 100644
index 00000000..b3bc28b2
--- /dev/null
+++ b/src/aig/aig/aigInter.c
@@ -0,0 +1,174 @@
+/**CFile****************************************************************
+
+  FileName    [aigInter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Interpolate two AIGs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigInter.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+#include "cnf.h"
+#include "satStore.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose )
+{
+    void * pSatCnf = NULL;
+    Inta_Man_t * pManInter;
+    Aig_Man_t * pRes;
+    sat_solver * pSat;
+    Cnf_Dat_t * pCnfOn, * pCnfOff;
+    Vec_Int_t * vVarsAB;
+    Aig_Obj_t * pObj, * pObj2;
+    int Lits[3], status, i;
+    int clk = clock();
+
+    assert( Aig_ManPiNum(pManOn) == Aig_ManPiNum(pManOff) );
+
+    // derive CNFs
+    pCnfOn  = Cnf_Derive( pManOn, 0 );
+    pCnfOff = Cnf_Derive( pManOff, 0 );
+//    pCnfOn  = Cnf_DeriveSimple( pManOn, 0 );
+//    pCnfOff = Cnf_DeriveSimple( pManOff, 0 );
+    Cnf_DataLift( pCnfOff, pCnfOn->nVars );
+
+    // start the solver
+    pSat = sat_solver_new();
+    sat_solver_store_alloc( pSat );
+    sat_solver_setnvars( pSat, pCnfOn->nVars + pCnfOff->nVars );
+
+    // add clauses of A
+    for ( i = 0; i < pCnfOn->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnfOn->pClauses[i], pCnfOn->pClauses[i+1] ) )
+        {
+            Cnf_DataFree( pCnfOn );
+            Cnf_DataFree( pCnfOff );
+            sat_solver_delete( pSat );
+            return NULL;
+        }
+    }
+    sat_solver_store_mark_clauses_a( pSat );
+
+    // add clauses of B
+    for ( i = 0; i < pCnfOff->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnfOff->pClauses[i], pCnfOff->pClauses[i+1] ) )
+        {
+            Cnf_DataFree( pCnfOn );
+            Cnf_DataFree( pCnfOff );
+            sat_solver_delete( pSat );
+            return NULL;
+        }
+    }
+
+    // add PI clauses
+    // collect the common variables
+    vVarsAB = Vec_IntAlloc( Aig_ManPiNum(pManOn) );
+    Aig_ManForEachPi( pManOn, pObj, i )
+    {
+        Vec_IntPush( vVarsAB, pCnfOn->pVarNums[pObj->Id] );
+        pObj2 = Aig_ManPi( pManOff, i );
+
+        Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 0 );
+        Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 1 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 1 );
+        Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 0 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+    }
+    Cnf_DataFree( pCnfOn );
+    Cnf_DataFree( pCnfOff );
+    sat_solver_store_mark_roots( pSat );
+    if ( fVerbose )
+    {
+        PRT( "Prepare", clock() - clk );
+    }
+
+/*
+    status = sat_solver_simplify(pSat);
+    if ( status == 0 )
+    {
+        Vec_IntFree( vVarsAB );
+        Cnf_DataFree( pCnfOn );
+        Cnf_DataFree( pCnfOff );
+        sat_solver_delete( pSat );
+        return NULL;
+    }
+*/
+
+    // solve the problem
+    clk = clock();
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+    if ( fVerbose )
+    {
+        PRT( "Solving", clock() - clk );
+    }
+    if ( status == l_False )
+    {
+        pSatCnf = sat_solver_store_release( pSat );
+//        printf( "unsat\n" );
+    }
+    else if ( status == l_True )
+    {
+//        printf( "sat\n" );
+    }
+    else
+    {
+//        printf( "undef\n" );
+    }
+    sat_solver_delete( pSat );
+    if ( pSatCnf == NULL )
+    {
+        printf( "The SAT problem is not unsat.\n" );
+        Vec_IntFree( vVarsAB );
+        return NULL;
+    }
+
+    // create the resulting manager
+    pManInter = Inta_ManAlloc();
+    pRes = Inta_ManInterpolate( pManInter, pSatCnf, vVarsAB, fVerbose );
+    Inta_ManFree( pManInter );
+
+    Vec_IntFree( vVarsAB );
+    Sto_ManFree( pSatCnf );
+    return pRes;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index 667ceec1..ffe6141c 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -3,6 +3,7 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigFanout.c \
     src/aig/aig/aigFrames.c \
     src/aig/aig/aigHaig.c \
+    src/aig/aig/aigInter.c \
     src/aig/aig/aigMan.c \
     src/aig/aig/aigMem.c \
     src/aig/aig/aigMffc.c \
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index 77c87f3f..5726469f 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -133,6 +133,7 @@ extern Cnf_Man_t *     Cnf_ManStart();
 extern void            Cnf_ManStop( Cnf_Man_t * p );
 extern Vec_Int_t *     Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
 extern void            Cnf_DataFree( Cnf_Dat_t * p );
+extern void            Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
 extern void            Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
 void *                 Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
 /*=== cnfMap.c ========================================================*/
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index 4ac06b48..47bc0b67 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -139,6 +139,28 @@ void Cnf_DataFree( Cnf_Dat_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus )
+{
+    Aig_Obj_t * pObj;
+    int v;
+    Aig_ManForEachObj( p->pMan, pObj, v )
+        if ( p->pVarNums[pObj->Id] )
+            p->pVarNums[pObj->Id] += nVarsPlus;
+    for ( v = 0; v < p->nLiterals; v++ )
+        p->pClauses[0][v] += 2*nVarsPlus;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes CNF into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
 {
     FILE * pFile;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1108238c..0a27ee15 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -104,6 +104,7 @@ static int Abc_CommandEspresso       ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandGen            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandXyz            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDouble         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInter          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTest           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandQuaVar         ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -281,6 +282,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "gen",           Abc_CommandGen,              0 );
 //    Cmd_CommandAdd( pAbc, "Various",      "xyz",           Abc_CommandXyz,              1 );
     Cmd_CommandAdd( pAbc, "Various",      "double",        Abc_CommandDouble,           1 );
+    Cmd_CommandAdd( pAbc, "Various",      "inter",         Abc_CommandInter,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "test",          Abc_CommandTest,             0 );
 
     Cmd_CommandAdd( pAbc, "Various",      "qvar",          Abc_CommandQuaVar,           1 );
@@ -6209,6 +6211,77 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandInter( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes, * pNtk1, * pNtk2;
+    char ** pArgvNew;
+    int nArgcNew;
+    int c, fDelete1, fDelete2;
+    int fVerbose;
+    extern Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose   =  0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    pArgvNew = argv + globalUtilOptind;
+    nArgcNew = argc - globalUtilOptind;
+    if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
+        return 1;
+    if ( nArgcNew == 0 )
+    {
+        printf( "Deriving new circuit structure for the current network.\n" );
+        Abc_ObjXorFaninC( Abc_NtkPo(pNtk2,0), 0 );
+    }
+    pNtkRes = Abc_NtkInter( pNtk1, pNtk2, fVerbose );
+    if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
+    if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
+
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: inter [-vh] <fileOnSet> <fileOffSet>\n" );
+    fprintf( pErr, "\t         derives interpolant of two networks (onset and offset)\n" );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandDouble( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -6311,7 +6384,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
     extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
-    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
+//    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
     extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
     extern void Abc_NtkDarTestBlif( char * pFileName );
 
@@ -6464,7 +6537,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
 */
-
+/*
     if ( Abc_NtkIsStrash(pNtk) )
     {
         fprintf( stdout, "Currently only works for logic circuits.\n" );
@@ -6482,7 +6555,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-
+*/
 
 //    Abc_NtkDarHaigRecord( pNtk );
 //    Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 439c3383..16a772ce 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1482,6 +1482,54 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
     return pNtkAig;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Interplates two networks.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
+{
+    extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose );
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pManOn, * pManOff, * pManAig;
+    if ( Abc_NtkCoNum(pNtkOn) != 1 || Abc_NtkCoNum(pNtkOff) != 1 )
+    {
+        printf( "Currently works only for single output networks.\n" );
+        return NULL;
+    }
+    if ( Abc_NtkCiNum(pNtkOn) != Abc_NtkCiNum(pNtkOff) )
+    {
+        printf( "The number of PIs should be the same.\n" );
+        return NULL;
+    }
+    // create internal AIGs
+    pManOn = Abc_NtkToDar( pNtkOn, 0 );
+    if ( pManOn == NULL )
+        return NULL;
+    pManOff = Abc_NtkToDar( pNtkOff, 0 );
+    if ( pManOff == NULL )
+        return NULL;
+    // derive the interpolant
+    pManAig = Aig_ManInter( pManOn, pManOff, fVerbose );
+    if ( pManAig == NULL )
+    {
+        printf( "Interpolant computation failed.\n" );
+        return NULL;
+    }
+    Aig_ManStop( pManOn );
+    Aig_ManStop( pManOff );
+    // create logic network
+    pNtkAig = Abc_NtkFromDar( pNtkOn, pManAig );
+    Aig_ManStop( pManAig );
+    return pNtkAig;
+}
+
 
 #include "ntl.h"
 
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/pcm/module.make
+++ /dev/null
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/ply/module.make
+++ /dev/null
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index b22f0f5e..cb448fc0 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -100,7 +100,7 @@ Res_Man_t * Res_ManAlloc( Res_Par_t * pPars )
     p->pPars = pPars;
     p->pWin = Res_WinAlloc();
     p->pSim = Res_SimAlloc( pPars->nSimWords );
-    p->pMan = Int_ManAlloc( 512 );
+    p->pMan = Int_ManAlloc();
     p->vMem = Vec_IntAlloc( 0 );
     p->vResubs  = Vec_VecStart( pPars->nCands );
     p->vResubsW = Vec_VecStart( pPars->nCands );
diff --git a/src/sat/bsat/module.make b/src/sat/bsat/module.make
index 563c8dfc..1e52cc0a 100644
--- a/src/sat/bsat/module.make
+++ b/src/sat/bsat/module.make
@@ -1,5 +1,6 @@
 SRC +=  src/sat/bsat/satMem.c \
     src/sat/bsat/satInter.c \
+    src/sat/bsat/satInterA.c \
     src/sat/bsat/satSolver.c \
     src/sat/bsat/satStore.c \
     src/sat/bsat/satTrace.c \
diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c
index 8759aa09..8e07e9f6 100644
--- a/src/sat/bsat/satInter.c
+++ b/src/sat/bsat/satInter.c
@@ -99,7 +99,7 @@ static inline void       Int_ManProofSet( Int_Man_t * p, Sto_Cls_t * pCls, int n
   SeeAlso     []
 
 ***********************************************************************/
-Int_Man_t * Int_ManAlloc( int nVarsAlloc )
+Int_Man_t * Int_ManAlloc()
 {
     Int_Man_t * p;
     // allocate the manager
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
new file mode 100644
index 00000000..513a9044
--- /dev/null
+++ b/src/sat/bsat/satInterA.c
@@ -0,0 +1,970 @@
+/**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 "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// variable assignments 
+static const lit    LIT_UNDEF = 0xffffffff;
+
+// interpolation manager
+struct Inta_Man_t_
+{
+    // clauses of the problems
+    Sto_Man_t *     pCnf;         // the set of CNF clauses for A and B
+    Vec_Int_t *     vVarsAB;      // the array of global variables
+    // 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)          
+    // interpolation data
+    Aig_Man_t *     pAig;         // the AIG manager for recording the interpolant
+    int *           pVarTypes;    // variable type (size nVars) [1=A, 0=B, <0=AB]
+    Aig_Obj_t **    pInters;      // storage for interpolants as truth tables (size nClauses)
+    int             nIntersAlloc; // the allocated size of truth table array
+    // 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
+};
+
+// procedure to get hold of the clauses' truth table 
+static inline Aig_Obj_t ** Inta_ManAigRead( Inta_Man_t * pMan, Sto_Cls_t * pCls )                   { return pMan->pInters + pCls->Id;          }
+static inline void         Inta_ManAigClear( Inta_Man_t * pMan, Aig_Obj_t ** p )                    { *p = Aig_ManConst0(pMan->pAig);           }
+static inline void         Inta_ManAigFill( Inta_Man_t * pMan, Aig_Obj_t ** p )                     { *p = Aig_ManConst1(pMan->pAig);           }
+static inline void         Inta_ManAigCopy( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q )     { *p = *q;                                  }
+static inline void         Inta_ManAigAnd( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q )      { *p = Aig_And(pMan->pAig, *p, *q);         }
+static inline void         Inta_ManAigOr( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q )       { *p = Aig_Or(pMan->pAig, *p, *q);          }
+static inline void         Inta_ManAigOrNot( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q )    { *p = Aig_Or(pMan->pAig, *p, Aig_Not(*q)); }
+static inline void         Inta_ManAigOrVar( Inta_Man_t * pMan, Aig_Obj_t ** p, int v )             { *p = Aig_Or(pMan->pAig, *p, Aig_IthVar(pMan->pAig, v));          }
+static inline void         Inta_ManAigOrNotVar( Inta_Man_t * pMan, Aig_Obj_t ** p, int v )          { *p = Aig_Or(pMan->pAig, *p, Aig_Not(Aig_IthVar(pMan->pAig, v))); }
+
+// reading/writing the proof for a clause
+static inline int          Inta_ManProofGet( Inta_Man_t * p, Sto_Cls_t * pCls )                  { return p->pProofNums[pCls->Id];           }
+static inline void         Inta_ManProofSet( Inta_Man_t * p, Sto_Cls_t * pCls, int n )           { p->pProofNums[pCls->Id] = n;              }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Inta_Man_t * Inta_ManAlloc()
+{
+    Inta_Man_t * p;
+    // allocate the manager
+    p = (Inta_Man_t *)malloc( sizeof(Inta_Man_t) );
+    memset( p, 0, sizeof(Inta_Man_t) );
+    // verification
+    p->nResLitsAlloc = (1<<16);
+    p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
+    // parameters
+    p->fProofWrite = 0;
+    p->fProofVerif = 1;
+    return p;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count common variables in the clauses of A and B.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Inta_ManGlobalVars( Inta_Man_t * p )
+{
+    Sto_Cls_t * pClause;
+    int LargeNum = -100000000;
+    int Var, nVarsAB, v;
+
+    // mark the variable encountered in the clauses of A
+    Sto_ManForEachClauseRoot( p->pCnf, pClause )
+    {
+        if ( !pClause->fA )
+            break;
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+            p->pVarTypes[lit_var(pClause->pLits[v])] = 1;
+    }
+
+    // check variables that appear in clauses of B
+    nVarsAB = 0;
+    Sto_ManForEachClauseRoot( p->pCnf, pClause )
+    {
+        if ( pClause->fA )
+            continue;
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+        {
+            Var = lit_var(pClause->pLits[v]);
+            if ( p->pVarTypes[Var] == 1 ) // var of A
+            {
+                // change it into a global variable
+                nVarsAB++;
+                p->pVarTypes[Var] = LargeNum;
+            }
+        }
+    }
+    assert( nVarsAB <= Vec_IntSize(p->vVarsAB) );
+
+    // order global variables
+    nVarsAB = 0;
+    Vec_IntForEachEntry( p->vVarsAB, Var, v )
+        p->pVarTypes[Var] = -(1+nVarsAB++);
+
+    // check that there is no extra global variables
+    for ( v = 0; v < p->pCnf->nVars; v++ )
+        assert( p->pVarTypes[v] != LargeNum );
+    return nVarsAB;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resize proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Inta_ManResize( Inta_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 );
+
+    // compute the number of common variables
+    Inta_ManGlobalVars( p );
+
+    // 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 );
+
+    // check if resizing of truth tables is needed
+    if ( p->nIntersAlloc < p->pCnf->nClauses )
+    {
+        p->nIntersAlloc = p->pCnf->nClauses;
+        p->pInters = (Aig_Obj_t **) realloc( p->pInters, sizeof(Aig_Obj_t *) * p->nIntersAlloc );
+    }
+    memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Inta_ManFree( Inta_Man_t * p )
+{
+/*
+    printf( "Runtime stats:\n" );
+PRT( "BCP     ", p->timeBcp   );
+PRT( "Trace   ", p->timeTrace );
+PRT( "TOTAL   ", p->timeTotal );
+*/
+    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 Inta_ManPrintClause( Inta_Man_t * p, Sto_Cls_t * pClause )
+{
+    int i;
+    printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Inta_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 Inta_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 Inta_ManPrintInterOne( Inta_Man_t * p, Sto_Cls_t * pClause )
+{
+    printf( "Clause %2d :  ", pClause->Id );
+//    Extra_PrintBinary___( stdout, Inta_ManAigRead(p, pClause), (1 << p->nVarsAB) );
+    printf( "\n" );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one clause to the watcher list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Inta_ManWatchClause( Inta_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 Inta_ManEnqueue( Inta_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 Inta_ManCancelUntil( Inta_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 * Inta_ManPropagateOne( Inta_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])
+            Inta_ManWatchClause( p, pCur, pCur->pLits[1] );
+            break;
+        }
+        if ( i < (int)pCur->nLits ) // found new watch
+            continue;
+
+        // clause is unit - enqueue new implication
+        if ( Inta_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 * Inta_ManPropagate( Inta_Man_t * p, int Start )
+{
+    Sto_Cls_t * pClause;
+    int i;
+    int clk = clock();
+    for ( i = Start; i < p->nTrailSize; i++ )
+    {
+        pClause = Inta_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 Inta_ManProofWriteOne( Inta_Man_t * p, Sto_Cls_t * pClause )
+{
+    Inta_ManProofSet( p, pClause, ++p->Counter );
+
+    if ( p->fProofWrite )
+    {
+        int v;
+        fprintf( p->pFile, "%d", Inta_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 Inta_ManProofTraceOne( Inta_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 );
+
+    if ( p->pCnf->nClausesA )
+        Inta_ManAigCopy( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pConflict) );
+
+    // follow the trail backwards
+    PrevId = Inta_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( Inta_ManProofGet(p, pReason) > 0 );
+        p->Counter++;
+        if ( p->fProofWrite )
+            fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Inta_ManProofGet(p, pReason) );
+        PrevId = p->Counter;
+
+        if ( p->pCnf->nClausesA )
+        {
+            if ( p->pVarTypes[Var] == 1 ) // var of A
+                Inta_ManAigOr( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason) );
+            else
+                Inta_ManAigAnd( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason) );
+        }
+ 
+        // resolve the temporary resolvent with the reason clause
+        if ( p->fProofVerif )
+        {
+            int v1, v2; 
+            if ( fPrint )
+                Inta_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 );
+    }
+
+    // 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 )
+            Inta_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 );
+            Inta_ManPrintClause( p, pConflict );
+            Inta_ManPrintResolvent( p->pResLits, p->nResLits );
+            Inta_ManPrintClause( p, pFinal );
+        }
+    }
+p->timeTrace += clock() - clk;
+
+    // return the proof pointer 
+    if ( p->pCnf->nClausesA )
+    {
+//        Inta_ManPrintInterOne( p, pFinal );
+    }
+    Inta_ManProofSet( p, pFinal, p->Counter );
+    return p->Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Inta_ManProofRecordOne( Inta_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 ( !Inta_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
+        {
+            assert( 0 ); // impossible
+            return 0;
+        }
+
+    // propagate the assumptions
+    pConflict = Inta_ManPropagate( p, p->nRootSize );
+    if ( pConflict == NULL )
+    {
+        assert( 0 ); // cannot prove
+        return 0;
+    }
+
+    // construct the proof
+    Inta_ManProofTraceOne( p, pConflict, pClause );
+
+    // undo to the root level
+    Inta_ManCancelUntil( p, p->nRootSize );
+
+    // add large clauses to the watched lists
+    if ( pClause->nLits > 1 )
+    {
+        Inta_ManWatchClause( p, pClause, pClause->pLits[0] );
+        Inta_ManWatchClause( p, pClause, pClause->pLits[1] );
+        return 1;
+    }
+    assert( pClause->nLits == 1 );
+
+    // if the clause proved is unit, add it and propagate
+    if ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) )
+    {
+        assert( 0 ); // impossible
+        return 0;
+    }
+
+    // propagate the assumption
+    pConflict = Inta_ManPropagate( p, p->nRootSize );
+    if ( pConflict )
+    {
+        // construct the proof
+        Inta_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 Inta_ManProcessRoots( Inta_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 )
+        {
+            Inta_ManWatchClause( p, pClause, pClause->pLits[0] );
+            Inta_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 ( !Inta_ManEnqueue( p, pClause->pLits[0], pClause ) )
+        {
+            // detected root level conflict
+            printf( "Error in Inta_ManProcessRoots(): Detected a root-level conflict too early!\n" );
+            assert( 0 );
+            return 0;
+        }
+    }
+
+    // propagate the root unit clauses
+    pClause = Inta_ManPropagate( p, 0 );
+    if ( pClause )
+    {
+        // detected root level conflict
+        Inta_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    [Records the proof.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Inta_ManPrepareInter( Inta_Man_t * p )
+{
+    Sto_Cls_t * pClause;
+    int Var, VarAB, v;
+
+    // set interpolants for root clauses
+    Sto_ManForEachClauseRoot( p->pCnf, pClause )
+    {
+        if ( !pClause->fA ) // clause of B
+        {
+            Inta_ManAigFill( p, Inta_ManAigRead(p, pClause) );
+//            Inta_ManPrintInterOne( p, pClause );
+            continue;
+        }
+        // clause of A
+        Inta_ManAigClear( p, Inta_ManAigRead(p, pClause) );
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+        {
+            Var = lit_var(pClause->pLits[v]);
+            if ( p->pVarTypes[Var] < 0 ) // global var
+            {
+                VarAB = -p->pVarTypes[Var]-1;
+                assert( VarAB >= 0 && VarAB < Vec_IntSize(p->vVarsAB) );
+                if ( lit_sign(pClause->pLits[v]) ) // negative var
+                    Inta_ManAigOrNotVar( p, Inta_ManAigRead(p, pClause), VarAB );
+                else
+                    Inta_ManAigOrVar( p, Inta_ManAigRead(p, pClause), VarAB );
+            }
+        }
+//        Inta_ManPrintInterOne( p, pClause );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes interpolant for the given CNF.]
+
+  Description [Takes the interpolation manager, the CNF deriving by the SAT
+  solver, which includes ClausesA, ClausesB, and learned clauses. Additional
+  arguments are the vector of variables common to AB and the verbosiness flag.
+  Returns the AIG manager with a single output, containing the interpolant.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose )
+{
+    Aig_Man_t * pRes;
+    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;
+    p->vVarsAB = vVarsAB;
+    p->pAig = pRes = Aig_ManStart( 10000 );
+    Aig_IthVar( p->pAig, Vec_IntSize(p->vVarsAB) - 1 );
+
+    // adjust the manager
+    Inta_ManResize( p );
+
+    // prepare the interpolant computation
+    Inta_ManPrepareInter( 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
+    Sto_ManForEachClauseRoot( p->pCnf, pClause )
+        Inta_ManProofWriteOne( p, pClause );
+
+    // propagate root level assignments
+    if ( Inta_ManProcessRoots( p ) )
+    {
+        // if there is no conflict, consider learned clauses
+        Sto_ManForEachClause( p->pCnf, pClause )
+        {
+            if ( pClause->fRoot )
+                continue;
+            if ( !Inta_ManProofRecordOne( p, pClause ) )
+            {
+                RetValue = 0;
+                break;
+            }
+        }
+    }
+
+    // stop the proof
+    if ( p->fProofWrite )
+    {
+        fclose( p->pFile );
+        p->pFile = NULL;    
+    }
+
+    if ( fVerbose )
+    {
+        PRT( "Interpo", 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;
+    }
+
+    Aig_ObjCreatePo( pRes, *Inta_ManAigRead( p, p->pCnf->pTail ) );
+    Aig_ManCleanup( pRes );
+
+    p->pAig = NULL;
+    return pRes;
+    
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index ca2954d2..c1bf32a7 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -71,6 +71,7 @@ static inline int  lit_var  (lit l)        { return l >> 1; }
 static inline int  lit_sign (lit l)        { return l & 1; }
 static inline int  lit_print(lit l)        { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
 static inline lit  lit_read (int s)        { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
+static inline int  lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n;                  }
 
 
 //=================================================================================================
diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h
index 346b59df..b66abc8f 100644
--- a/src/sat/bsat/satStore.h
+++ b/src/sat/bsat/satStore.h
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [pr.h]
+  FileName    [satStore.h]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -18,11 +18,13 @@
 
 ***********************************************************************/
  
-#ifndef __PR_H__
-#define __PR_H__
+#ifndef __SAT_STORE_H__
+#define __SAT_STORE_H__
+
+#include "satSolver.h"
 
 /*
-    The trace of SAT solving contains the original clause of the problem
+    The trace of SAT solving contains the original clauses of the problem
     along with the learned clauses derived during SAT solving.
     The first line of the resulting file contains 3 numbers instead of 2:
     c <num_vars> <num_all_clauses> <num_root_clauses>
@@ -54,7 +56,18 @@ extern "C" {
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
+/*
 typedef unsigned lit;
+// variable/literal conversions (taken from MiniSat)
+static inline lit   toLit    (int v)        { return v + v;  }
+static inline lit   toLitCond(int v, int c) { return v + v + (c != 0); }
+static inline lit   lit_neg  (lit l)        { return l ^ 1;  }
+static inline int   lit_var  (lit l)        { return l >> 1; }
+static inline int   lit_sign (lit l)        { return l & 1;  }
+static inline int   lit_print(lit l)        { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
+static inline lit   lit_read (int s)        { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
+static inline int   lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n;                  }
+*/
 
 typedef struct Sto_Cls_t_ Sto_Cls_t;
 struct Sto_Cls_t_
@@ -87,16 +100,6 @@ struct Sto_Man_t_
     char *          pChunkLast;   // the last memory chunk
 };
 
-// variable/literal conversions (taken from MiniSat)
-static inline lit   toLit    (int v)        { return v + v;  }
-static inline lit   toLitCond(int v, int c) { return v + v + (c != 0); }
-static inline lit   lit_neg  (lit l)        { return l ^ 1;  }
-static inline int   lit_var  (lit l)        { return l >> 1; }
-static inline int   lit_sign (lit l)        { return l & 1;  }
-static inline int   lit_print(lit l)        { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
-static inline lit   lit_read (int s)        { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
-static inline int   lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n;                  }
-
 // iterators through the clauses
 #define Sto_ManForEachClause( p, pCls )      for( pCls = p->pHead; pCls; pCls = pCls->pNext )
 #define Sto_ManForEachClauseRoot( p, pCls )  for( pCls = p->pHead; pCls && pCls->fRoot; pCls = pCls->pNext )
@@ -121,10 +124,16 @@ extern Sto_Man_t *  Sto_ManLoadClauses( char * pFileName );
 
 /*=== satInter.c ==========================================================*/
 typedef struct Int_Man_t_ Int_Man_t;
-extern Int_Man_t *  Int_ManAlloc( int nVarsAlloc );
+extern Int_Man_t *  Int_ManAlloc();
 extern void         Int_ManFree( Int_Man_t * p );
 extern int          Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult );
 
+/*=== satInterA.c ==========================================================*/
+typedef struct Inta_Man_t_ Inta_Man_t;
+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 );
+
 #ifdef __cplusplus
 }
 #endif