initial commit of public abc

20 files changed, 3653 insertions, 113 deletions

diff --git a/src/sat/bsat/satChecker.c b/src/sat/bsat/satChecker.c
index 1488fe2f..041bc9ed 100644
--- a/src/sat/bsat/satChecker.c
+++ b/src/sat/bsat/satChecker.c
@@ -25,6 +25,9 @@
 #include <time.h>
 #include "vec.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -185,3 +188,5 @@ void Sat_ProofChecker( char * pFileName )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c
index 849ceb71..8617def9 100644
--- a/src/sat/bsat/satInter.c
+++ b/src/sat/bsat/satInter.c
@@ -25,6 +25,9 @@
 #include <time.h>
 #include "satStore.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -222,7 +225,7 @@ void Int_ManResize( Int_Man_t * p )
         p->pWatches  = ABC_REALLOC(Sto_Cls_t *, p->pWatches,  p->nVarsAlloc*2 );
     }
 
-    // clean the ABC_FREE space
+    // 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 );
@@ -1070,3 +1073,5 @@ p->timeTotal += clock() - clkTotal;
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
index 5dcc7f0b..a635516c 100644
--- a/src/sat/bsat/satInterA.c
+++ b/src/sat/bsat/satInterA.c
@@ -26,6 +26,9 @@
 #include "satStore.h"
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -186,6 +189,7 @@ int Inta_ManGlobalVars( Inta_Man_t * p )
 ***********************************************************************/
 void Inta_ManResize( Inta_Man_t * p )
 {
+    p->Counter = 0;
     // check if resizing is needed
     if ( p->nVarsAlloc < p->pCnf->nVars )
     {
@@ -203,7 +207,7 @@ void Inta_ManResize( Inta_Man_t * p )
         p->pWatches  = ABC_REALLOC(Sto_Cls_t *, p->pWatches,  p->nVarsAlloc*2 );
     }
 
-    // clean the ABC_FREE space
+    // 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 );
@@ -956,7 +960,7 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
     assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
     p->pCnf = pCnf;
     p->fVerbose = fVerbose;
-    p->vVarsAB = vVarsAB;
+    p->vVarsAB = (Vec_Int_t *)vVarsAB;
     p->pAig = pRes = Aig_ManStart( 10000 );
     Aig_IthVar( p->pAig, Vec_IntSize(p->vVarsAB) - 1 );
 
@@ -1071,3 +1075,5 @@ Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fCla
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satInterA_mod.c b/src/sat/bsat/satInterA_mod.c
index faf396a6..199e9bd3 100644
--- a/src/sat/bsat/satInterA_mod.c
+++ b/src/sat/bsat/satInterA_mod.c
@@ -26,6 +26,9 @@
 #include "satStore.h"
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -1102,3 +1105,5 @@ Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fCla
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satInterA_old.c b/src/sat/bsat/satInterA_old.c
index 57628989..02db6c79 100644
--- a/src/sat/bsat/satInterA_old.c
+++ b/src/sat/bsat/satInterA_old.c
@@ -26,6 +26,9 @@
 #include "satStore.h"
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -1045,3 +1048,5 @@ Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fCla
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satInterA_yu_hu.c b/src/sat/bsat/satInterA_yu_hu.c
index aa2289f2..9afd2dd8 100644
--- a/src/sat/bsat/satInterA_yu_hu.c
+++ b/src/sat/bsat/satInterA_yu_hu.c
@@ -26,6 +26,9 @@
 #include "satStore.h"
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -1079,3 +1082,5 @@ Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fCla
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satInterB.c b/src/sat/bsat/satInterB.c
index cb7f7828..1ffb0dc5 100644
--- a/src/sat/bsat/satInterB.c
+++ b/src/sat/bsat/satInterB.c
@@ -26,6 +26,9 @@
 #include "satStore.h"
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -188,6 +191,7 @@ int Intb_ManGlobalVars( Intb_Man_t * p )
 ***********************************************************************/
 void Intb_ManResize( Intb_Man_t * p )
 {
+    p->Counter = 0;
     // check if resizing is needed
     if ( p->nVarsAlloc < p->pCnf->nVars )
     {
@@ -205,7 +209,7 @@ void Intb_ManResize( Intb_Man_t * p )
         p->pWatches  = ABC_REALLOC(Sto_Cls_t *, p->pWatches,  p->nVarsAlloc*2 );
     }
 
-    // clean the ABC_FREE space
+    // 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 );
@@ -232,7 +236,7 @@ void Intb_ManResize( Intb_Man_t * p )
     if ( p->nIntersAlloc < p->pCnf->nClauses )
     {
         p->nIntersAlloc = p->pCnf->nClauses;
-        p->pInters = ABC_REALLOC(Aig_Obj_t *, p->pInters, p->nIntersAlloc );
+        p->pInters = ABC_REALLOC( Aig_Obj_t *, p->pInters, p->nIntersAlloc );
     }
     memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses );
 }
@@ -550,7 +554,6 @@ int Intb_ManGetGlobalVar( Intb_Man_t * p, int Var )
     return VarAB;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Traces the proof for one clause.]
@@ -608,7 +611,6 @@ int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
         for ( v = 1; v < (int)pReason->nLits; v++ )
             p->pSeens[lit_var(pReason->pLits[v])] = 1;
 
-
         // record the reason clause
         assert( Intb_ManProofGet(p, pReason) > 0 );
         p->Counter++;
@@ -677,7 +679,6 @@ int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
                 printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id );
             }
         }
-
 //        Vec_PtrPush( pFinal->pAntis, pReason );
     }
 
@@ -710,6 +711,27 @@ int Intb_ManProofTraceOne( Intb_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
             Intb_ManPrintResolvent( p->pResLits, p->nResLits );
             Intb_ManPrintClause( p, pFinal );
         }
+
+        // if there are literals in the clause that are not in the resolvent
+        // it means that the derived resolvent is stronger than the clause
+        // we can replace the clause with the resolvent by removing these literals
+        if ( p->nResLits != (int)pFinal->nLits )
+        {
+            for ( v1 = 0; v1 < (int)pFinal->nLits; v1++ )
+            {
+                for ( v2 = 0; v2 < p->nResLits; v2++ )
+                    if ( pFinal->pLits[v1] == p->pResLits[v2] )
+                        break;
+                if ( v2 < p->nResLits )
+                    continue;
+                // remove literal v1 from the final clause
+                pFinal->nLits--;
+                for ( v2 = v1; v2 < (int)pFinal->nLits; v2++ )
+                    pFinal->pLits[v2] = pFinal->pLits[v2+1];
+                v1--;
+            }
+            assert( p->nResLits == (int)pFinal->nLits );
+        }
     }
 p->timeTrace += clock() - clk;
 
@@ -719,6 +741,10 @@ p->timeTrace += clock() - clk;
 //        Intb_ManPrintInterOne( p, pFinal );
     }
     Intb_ManProofSet( p, pFinal, p->Counter );
+    // make sure the same proof ID is not asssigned to two consecutive clauses
+    assert( p->pProofNums[pFinal->Id-1] != p->Counter );
+//    if ( p->pProofNums[pFinal->Id] == p->pProofNums[pFinal->Id-1] )
+//        p->pProofNums[pFinal->Id] = p->pProofNums[pConflict->Id];
     return p->Counter;
 }
 
@@ -743,9 +769,16 @@ int Intb_ManProofRecordOne( Intb_Man_t * p, Sto_Cls_t * pClause )
     if ( pClause->nLits == 0 )
         printf( "Error: Empty clause is attempted.\n" );
 
-    // add assumptions to the trail
     assert( !pClause->fRoot );
     assert( p->nTrailSize == p->nRootSize );
+
+    // if any of the clause literals are already assumed
+    // it means that the clause is redundant and can be skipped
+    for ( i = 0; i < (int)pClause->nLits; i++ )
+        if ( p->pAssigns[lit_var(pClause->pLits[i])] == pClause->pLits[i] )
+            return 1;
+
+    // add assumptions to the trail
     for ( i = 0; i < (int)pClause->nLits; i++ )
         if ( !Intb_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
         {
@@ -759,6 +792,27 @@ int Intb_ManProofRecordOne( Intb_Man_t * p, Sto_Cls_t * pClause )
     {
         assert( 0 ); // cannot prove
         return 0;
+    } 
+
+    // skip the clause if it is weaker or the same as the conflict clause
+    if ( pClause->nLits >= pConflict->nLits )
+    {
+        // check if every literal of conflict clause can be found in the given clause
+        int j;
+        for ( i = 0; i < (int)pConflict->nLits; i++ )
+        {
+            for ( j = 0; j < (int)pClause->nLits; j++ )
+                if ( pConflict->pLits[i] == pClause->pLits[j] )
+                    break;
+            if ( j == (int)pClause->nLits ) // literal pConflict->pLits[i] is not found
+                break;
+        }
+        if ( i == (int)pConflict->nLits ) // all lits are found
+        {
+            // undo to the root level
+            Intb_ManCancelUntil( p, p->nRootSize );
+            return 1;
+        }
     }
 
     // construct the proof
@@ -846,8 +900,12 @@ int Intb_ManProcessRoots( Intb_Man_t * p )
         if ( !Intb_ManEnqueue( p, pClause->pLits[0], pClause ) )
         {
             // detected root level conflict
-            printf( "Error in Intb_ManProcessRoots(): Detected a root-level conflict too early!\n" );
-            assert( 0 );
+//            printf( "Error in Intb_ManProcessRoots(): Detected a root-level conflict too early!\n" );
+//            assert( 0 );
+            // detected root level conflict
+            Intb_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
+            if ( p->fVerbose )
+                printf( "Found root level conflict!\n" );
             return 0;
         }
     }
@@ -895,7 +953,6 @@ void Intb_ManPrepareInter( Intb_Man_t * p )
         }
         // clause of A
         Intb_ManAigClear( p, Intb_ManAigRead(p, pClause) );
-
         for ( v = 0; v < (int)pClause->nLits; v++ )
         {
             Var = lit_var(pClause->pLits[v]);
@@ -909,7 +966,6 @@ void Intb_ManPrepareInter( Intb_Man_t * p )
                     Intb_ManAigOrVar( p, Intb_ManAigRead(p, pClause), VarAB );
             }
         }
-
 //        Intb_ManPrintInterOne( p, pClause );
     }
 }
@@ -940,7 +996,7 @@ void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
     assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
     p->pCnf = pCnf;
     p->fVerbose = fVerbose;
-    p->vVarsAB = vVarsAB;
+    p->vVarsAB = (Vec_Int_t *)vVarsAB;
     p->pAig = pRes = Aig_ManStart( 10000 );
     Aig_IthVar( p->pAig, Vec_IntSize(p->vVarsAB) - 1 );
 
@@ -980,8 +1036,9 @@ void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
 
     // stop the proof
     if ( p->fProofWrite )
-    {
+    { 
         fclose( p->pFile );
+//        Sat_ProofChecker( "proof.cnf_" );
         p->pFile = NULL;    
     }
 
@@ -1004,6 +1061,7 @@ p->timeTotal += clock() - clkTotal;
     
 }
 
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -1053,3 +1111,5 @@ Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fCla
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satInterB_.c b/src/sat/bsat/satInterB_.c
new file mode 100644
index 00000000..ac005422
--- /dev/null
+++ b/src/sat/bsat/satInterB_.c
@@ -0,0 +1,1060 @@
+/**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"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        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))); }
+static inline void         Inta_ManAigMux0( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q, int v){ *p = Aig_Mux(pMan->pAig, Aig_IthVar(pMan->pAig, v), *q, *p);     }
+static inline void         Inta_ManAigMux1( Inta_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q, int v){ *p = Aig_Mux(pMan->pAig, Aig_IthVar(pMan->pAig, v), *p, *q);     }
+
+// 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 *)ABC_ALLOC( char, sizeof(Inta_Man_t) );
+    memset( p, 0, sizeof(Inta_Man_t) );
+    // verification
+    p->nResLitsAlloc = (1<<16);
+    p->pResLits = ABC_ALLOC( 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    = ABC_REALLOC(lit,         p->pTrail,    p->nVarsAlloc );
+        p->pAssigns  = ABC_REALLOC(lit,         p->pAssigns,  p->nVarsAlloc );
+        p->pSeens    = ABC_REALLOC(char,        p->pSeens,    p->nVarsAlloc );
+        p->pVarTypes = ABC_REALLOC(int,         p->pVarTypes, p->nVarsAlloc );
+        p->pReasons  = ABC_REALLOC(Sto_Cls_t *, p->pReasons,  p->nVarsAlloc );
+        p->pWatches  = ABC_REALLOC(Sto_Cls_t *, p->pWatches,  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 = ABC_REALLOC( int, p->pProofNums,  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 = ABC_REALLOC(Aig_Obj_t *, p->pInters, 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" );
+ABC_PRT( "BCP     ", p->timeBcp   );
+ABC_PRT( "Trace   ", p->timeTrace );
+ABC_PRT( "TOTAL   ", p->timeTotal );
+*/
+    ABC_FREE( p->pInters );
+    ABC_FREE( p->pProofNums );
+    ABC_FREE( p->pTrail );
+    ABC_FREE( p->pAssigns );
+    ABC_FREE( p->pSeens );
+    ABC_FREE( p->pVarTypes );
+    ABC_FREE( p->pReasons );
+    ABC_FREE( p->pWatches );
+    ABC_FREE( p->pResLits );
+    ABC_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_ManGetGlobalVar( Inta_Man_t * p, int Var )
+{
+    int VarAB;
+    if ( p->pVarTypes[Var] >= 0 ) // global var
+        return -1;
+    VarAB = -p->pVarTypes[Var]-1;
+    assert( VarAB >= 0 && VarAB < Vec_IntSize(p->vVarsAB) );
+    return VarAB;
+}
+
+
+/**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 )// || rand() % 10 == 0 ) // var of A
+                Inta_ManAigOr( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason) );
+            else if ( p->pVarTypes[Var] == 0 ) // var of B
+                Inta_ManAigAnd( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason) );
+            else
+            {
+                int VarAB = Inta_ManGetGlobalVar(p, Var);
+                // check that the var is present in the reason
+                for ( v = 0; v < (int)pReason->nLits; v++ )
+                    if ( lit_var(pReason->pLits[v]) == Var )
+                        break;
+                assert( v < (int)pReason->nLits );
+                if ( lit_sign(pReason->pLits[v]) ) // negative polarity
+                    Inta_ManAigMux0( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason), VarAB );
+                else
+                    Inta_ManAigMux1( p, Inta_ManAigRead(p, pFinal), Inta_ManAigRead(p, pReason), VarAB );
+            }
+        }
+ 
+        // 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;
+    Aig_Obj_t * pObj;
+    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 )
+    {
+//        ABC_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;
+    }
+
+    pObj = *Inta_ManAigRead( p, p->pCnf->pTail );
+    Aig_ObjCreatePo( pRes, pObj );
+    Aig_ManCleanup( pRes );
+
+    p->pAig = NULL;
+    return pRes;
+    
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA )
+{
+    Aig_Man_t * p;
+    Aig_Obj_t * pMiter, * pSum, * pLit;
+    Sto_Cls_t * pClause;
+    int Var, VarAB, v;
+    p = Aig_ManStart( 10000 );
+    pMiter = Aig_ManConst1(p);
+    Sto_ManForEachClauseRoot( pCnf, pClause )
+    {
+        if ( fClausesA ^ pClause->fA ) // clause of B
+            continue;
+        // clause of A
+        pSum = Aig_ManConst0(p);
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+        {
+            Var = lit_var(pClause->pLits[v]);
+            if ( pMan->pVarTypes[Var] < 0 ) // global var
+            {
+                VarAB = -pMan->pVarTypes[Var]-1;
+                assert( VarAB >= 0 && VarAB < Vec_IntSize(pMan->vVarsAB) );
+                pLit = Aig_NotCond( Aig_IthVar(p, VarAB), lit_sign(pClause->pLits[v]) );
+            }
+            else
+                pLit = Aig_NotCond( Aig_IthVar(p, Vec_IntSize(pMan->vVarsAB)+1+Var), lit_sign(pClause->pLits[v]) );
+            pSum = Aig_Or( p, pSum, pLit );
+        }
+        pMiter = Aig_And( p, pMiter, pSum );
+    }
+    Aig_ObjCreatePo( p, pMiter );
+    return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satInterB_new.c b/src/sat/bsat/satInterB_new.c
new file mode 100644
index 00000000..f6f54c8c
--- /dev/null
+++ b/src/sat/bsat/satInterB_new.c
@@ -0,0 +1,1115 @@
+/**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"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// variable assignments 
+static const lit    LIT_UNDEF = 0xffffffff;
+
+// interpolation manager
+struct Intb_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 ** Intb_ManAigRead( Intb_Man_t * pMan, Sto_Cls_t * pCls )                   { return pMan->pInters + pCls->Id;          }
+static inline void         Intb_ManAigClear( Intb_Man_t * pMan, Aig_Obj_t ** p )                    { *p = Aig_ManConst0(pMan->pAig);           }
+static inline void         Intb_ManAigFill( Intb_Man_t * pMan, Aig_Obj_t ** p )                     { *p = Aig_ManConst1(pMan->pAig);           }
+static inline void         Intb_ManAigCopy( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q )     { *p = *q;                                  }
+static inline void         Intb_ManAigAnd( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q )      { *p = Aig_And(pMan->pAig, *p, *q);         }
+static inline void         Intb_ManAigOr( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q )       { *p = Aig_Or(pMan->pAig, *p, *q);          }
+static inline void         Intb_ManAigOrNot( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q )    { *p = Aig_Or(pMan->pAig, *p, Aig_Not(*q)); }
+static inline void         Intb_ManAigOrVar( Intb_Man_t * pMan, Aig_Obj_t ** p, int v )             { *p = Aig_Or(pMan->pAig, *p, Aig_IthVar(pMan->pAig, v));          }
+static inline void         Intb_ManAigOrNotVar( Intb_Man_t * pMan, Aig_Obj_t ** p, int v )          { *p = Aig_Or(pMan->pAig, *p, Aig_Not(Aig_IthVar(pMan->pAig, v))); }
+static inline void         Intb_ManAigMux0( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q, int v){ *p = Aig_Mux(pMan->pAig, Aig_IthVar(pMan->pAig, v), *q, *p);     }
+static inline void         Intb_ManAigMux1( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q, int v){ *p = Aig_Mux(pMan->pAig, Aig_IthVar(pMan->pAig, v), *p, *q);     }
+
+// reading/writing the proof for a clause
+static inline int          Intb_ManProofGet( Intb_Man_t * p, Sto_Cls_t * pCls )                  { return p->pProofNums[pCls->Id];           }
+static inline void         Intb_ManProofSet( Intb_Man_t * p, Sto_Cls_t * pCls, int n )           { p->pProofNums[pCls->Id] = n;              }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Intb_Man_t * Intb_ManAlloc()
+{
+    Intb_Man_t * p;
+    // allocate the manager
+    p = (Intb_Man_t *)ABC_ALLOC( char, sizeof(Intb_Man_t) );
+    memset( p, 0, sizeof(Intb_Man_t) );
+    // verification
+    p->nResLitsAlloc = (1<<16);
+    p->pResLits = ABC_ALLOC( 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 Intb_ManGlobalVars( Intb_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 Intb_ManResize( Intb_Man_t * p )
+{
+    p->Counter = 0;
+    // 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    = ABC_REALLOC(lit,         p->pTrail,    p->nVarsAlloc );
+        p->pAssigns  = ABC_REALLOC(lit,         p->pAssigns,  p->nVarsAlloc );
+        p->pSeens    = ABC_REALLOC(char,        p->pSeens,    p->nVarsAlloc );
+        p->pVarTypes = ABC_REALLOC(int,         p->pVarTypes, p->nVarsAlloc );
+        p->pReasons  = ABC_REALLOC(Sto_Cls_t *, p->pReasons,  p->nVarsAlloc );
+        p->pWatches  = ABC_REALLOC(Sto_Cls_t *, p->pWatches,  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
+    Intb_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 = ABC_REALLOC( int, p->pProofNums,  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 = ABC_REALLOC( Aig_Obj_t *, p->pInters, p->nIntersAlloc );
+    }
+    memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Intb_ManFree( Intb_Man_t * p )
+{
+/*
+    printf( "Runtime stats:\n" );
+ABC_PRT( "BCP     ", p->timeBcp   );
+ABC_PRT( "Trace   ", p->timeTrace );
+ABC_PRT( "TOTAL   ", p->timeTotal );
+*/
+    ABC_FREE( p->pInters );
+    ABC_FREE( p->pProofNums );
+    ABC_FREE( p->pTrail );
+    ABC_FREE( p->pAssigns );
+    ABC_FREE( p->pSeens );
+    ABC_FREE( p->pVarTypes );
+    ABC_FREE( p->pReasons );
+    ABC_FREE( p->pWatches );
+    ABC_FREE( p->pResLits );
+    ABC_FREE( p );
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Intb_ManPrintClause( Intb_Man_t * p, Sto_Cls_t * pClause )
+{
+    int i;
+    printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Intb_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 Intb_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 Intb_ManPrintInterOne( Intb_Man_t * p, Sto_Cls_t * pClause )
+{
+    printf( "Clause %2d :  ", pClause->Id );
+//    Extra_PrintBinary___( stdout, Intb_ManAigRead(p, pClause), (1 << p->nVarsAB) );
+    printf( "\n" );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one clause to the watcher list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Intb_ManWatchClause( Intb_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 Intb_ManEnqueue( Intb_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 Intb_ManCancelUntil( Intb_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 * Intb_ManPropagateOne( Intb_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])
+            Intb_ManWatchClause( p, pCur, pCur->pLits[1] );
+            break;
+        }
+        if ( i < (int)pCur->nLits ) // found new watch
+            continue;
+
+        // clause is unit - enqueue new implication
+        if ( Intb_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 * Intb_ManPropagate( Intb_Man_t * p, int Start )
+{
+    Sto_Cls_t * pClause;
+    int i;
+    int clk = clock();
+    for ( i = Start; i < p->nTrailSize; i++ )
+    {
+        pClause = Intb_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 Intb_ManProofWriteOne( Intb_Man_t * p, Sto_Cls_t * pClause )
+{
+    Intb_ManProofSet( p, pClause, ++p->Counter );
+
+    if ( p->fProofWrite )
+    {
+        int v;
+        fprintf( p->pFile, "%d", Intb_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 Intb_ManGetGlobalVar( Intb_Man_t * p, int Var )
+{
+    int VarAB;
+    if ( p->pVarTypes[Var] >= 0 ) // global var
+        return -1;
+    VarAB = -p->pVarTypes[Var]-1;
+    assert( VarAB >= 0 && VarAB < Vec_IntSize(p->vVarsAB) );
+    return VarAB;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Traces the proof for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Intb_ManProofTraceOne( Intb_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 )
+        Intb_ManAigCopy( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pConflict) );
+
+    // follow the trail backwards
+    PrevId = Intb_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( Intb_ManProofGet(p, pReason) > 0 );
+        p->Counter++;
+        if ( p->fProofWrite )
+            fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Intb_ManProofGet(p, pReason) );
+        PrevId = p->Counter;
+
+        if ( p->pCnf->nClausesA )
+        {
+            if ( p->pVarTypes[Var] == 1 )// || rand() % 10 == 0 ) // var of A
+                Intb_ManAigOr( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason) );
+            else if ( p->pVarTypes[Var] == 0 ) // var of B
+                Intb_ManAigAnd( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason) );
+            else
+            {
+                int VarAB = Intb_ManGetGlobalVar(p, Var);
+                // check that the var is present in the reason
+                for ( v = 0; v < (int)pReason->nLits; v++ )
+                    if ( lit_var(pReason->pLits[v]) == Var )
+                        break;
+                assert( v < (int)pReason->nLits );
+                if ( lit_sign(pReason->pLits[v]) ) // negative polarity
+                    Intb_ManAigMux0( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason), VarAB );
+                else
+                    Intb_ManAigMux1( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason), VarAB );
+            }
+        }
+ 
+        // resolve the temporary resolvent with the reason clause
+        if ( p->fProofVerif )
+        {
+            int v1, v2; 
+            if ( fPrint )
+                Intb_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 )
+            Intb_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 );
+            Intb_ManPrintClause( p, pConflict );
+            Intb_ManPrintResolvent( p->pResLits, p->nResLits );
+            Intb_ManPrintClause( p, pFinal );
+        }
+
+        // if there are literals in the clause that are not in the resolvent
+        // it means that the derived resolvent is stronger than the clause
+        // we can replace the clause with the resolvent by removing these literals
+        if ( p->nResLits != (int)pFinal->nLits )
+        {
+            for ( v1 = 0; v1 < (int)pFinal->nLits; v1++ )
+            {
+                for ( v2 = 0; v2 < p->nResLits; v2++ )
+                    if ( pFinal->pLits[v1] == p->pResLits[v2] )
+                        break;
+                if ( v2 < p->nResLits )
+                    continue;
+                // remove literal v1 from the final clause
+                pFinal->nLits--;
+                for ( v2 = v1; v2 < (int)pFinal->nLits; v2++ )
+                    pFinal->pLits[v2] = pFinal->pLits[v2+1];
+                v1--;
+            }
+            assert( p->nResLits == (int)pFinal->nLits );
+        }
+    }
+p->timeTrace += clock() - clk;
+
+    // return the proof pointer 
+    if ( p->pCnf->nClausesA )
+    {
+//        Intb_ManPrintInterOne( p, pFinal );
+    }
+    Intb_ManProofSet( p, pFinal, p->Counter );
+    // make sure the same proof ID is not asssigned to two consecutive clauses
+    assert( p->pProofNums[pFinal->Id-1] != p->Counter );
+//    if ( p->pProofNums[pFinal->Id] == p->pProofNums[pFinal->Id-1] )
+//        p->pProofNums[pFinal->Id] = p->pProofNums[pConflict->Id];
+    return p->Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Intb_ManProofRecordOne( Intb_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" );
+
+    assert( !pClause->fRoot );
+    assert( p->nTrailSize == p->nRootSize );
+
+    // if any of the clause literals are already assumed
+    // it means that the clause is redundant and can be skipped
+    for ( i = 0; i < (int)pClause->nLits; i++ )
+        if ( p->pAssigns[lit_var(pClause->pLits[i])] == pClause->pLits[i] )
+            return 1;
+
+    // add assumptions to the trail
+    for ( i = 0; i < (int)pClause->nLits; i++ )
+        if ( !Intb_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
+        {
+            assert( 0 ); // impossible
+            return 0;
+        }
+
+    // propagate the assumptions
+    pConflict = Intb_ManPropagate( p, p->nRootSize );
+    if ( pConflict == NULL )
+    {
+        assert( 0 ); // cannot prove
+        return 0;
+    } 
+
+    // skip the clause if it is weaker or the same as the conflict clause
+    if ( pClause->nLits >= pConflict->nLits )
+    {
+        // check if every literal of conflict clause can be found in the given clause
+        int j;
+        for ( i = 0; i < (int)pConflict->nLits; i++ )
+        {
+            for ( j = 0; j < (int)pClause->nLits; j++ )
+                if ( pConflict->pLits[i] == pClause->pLits[j] )
+                    break;
+            if ( j == (int)pClause->nLits ) // literal pConflict->pLits[i] is not found
+                break;
+        }
+        if ( i == (int)pConflict->nLits ) // all lits are found
+        {
+            // undo to the root level
+            Intb_ManCancelUntil( p, p->nRootSize );
+            return 1;
+        }
+    }
+
+    // construct the proof
+    Intb_ManProofTraceOne( p, pConflict, pClause );
+
+    // undo to the root level
+    Intb_ManCancelUntil( p, p->nRootSize );
+
+    // add large clauses to the watched lists
+    if ( pClause->nLits > 1 )
+    {
+        Intb_ManWatchClause( p, pClause, pClause->pLits[0] );
+        Intb_ManWatchClause( p, pClause, pClause->pLits[1] );
+        return 1;
+    }
+    assert( pClause->nLits == 1 );
+
+    // if the clause proved is unit, add it and propagate
+    if ( !Intb_ManEnqueue( p, pClause->pLits[0], pClause ) )
+    {
+        assert( 0 ); // impossible
+        return 0;
+    }
+
+    // propagate the assumption
+    pConflict = Intb_ManPropagate( p, p->nRootSize );
+    if ( pConflict )
+    {
+        // construct the proof
+        Intb_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 Intb_ManProcessRoots( Intb_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 )
+        {
+            Intb_ManWatchClause( p, pClause, pClause->pLits[0] );
+            Intb_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 ( !Intb_ManEnqueue( p, pClause->pLits[0], pClause ) )
+        {
+            // detected root level conflict
+//            printf( "Error in Intb_ManProcessRoots(): Detected a root-level conflict too early!\n" );
+//            assert( 0 );
+            // detected root level conflict
+            Intb_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
+            if ( p->fVerbose )
+                printf( "Found root level conflict!\n" );
+            return 0;
+        }
+    }
+
+    // propagate the root unit clauses
+    pClause = Intb_ManPropagate( p, 0 );
+    if ( pClause )
+    {
+        // detected root level conflict
+        Intb_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 Intb_ManPrepareInter( Intb_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
+        {
+            Intb_ManAigFill( p, Intb_ManAigRead(p, pClause) );
+//            Intb_ManPrintInterOne( p, pClause );
+            continue;
+        }
+        // clause of A
+        Intb_ManAigClear( p, Intb_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
+                    Intb_ManAigOrNotVar( p, Intb_ManAigRead(p, pClause), VarAB );
+                else
+                    Intb_ManAigOrVar( p, Intb_ManAigRead(p, pClause), VarAB );
+            }
+        }
+//        Intb_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 * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose )
+{
+    Aig_Man_t * pRes;
+    Aig_Obj_t * pObj;
+    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
+    Intb_ManResize( p );
+
+    // prepare the interpolant computation
+    Intb_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 )
+        Intb_ManProofWriteOne( p, pClause );
+
+    // propagate root level assignments
+    if ( Intb_ManProcessRoots( p ) )
+    {
+        // if there is no conflict, consider learned clauses
+        Sto_ManForEachClause( p->pCnf, pClause )
+        {
+            if ( pClause->fRoot )
+                continue;
+            if ( !Intb_ManProofRecordOne( p, pClause ) )
+            {
+                RetValue = 0;
+                break;
+            }
+        }
+    }
+
+    // stop the proof
+    if ( p->fProofWrite )
+    { 
+        fclose( p->pFile );
+//        Sat_ProofChecker( "proof.cnf_" );
+        p->pFile = NULL;    
+    }
+
+    if ( fVerbose )
+    {
+//        ABC_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;
+    }
+
+    pObj = *Intb_ManAigRead( p, p->pCnf->pTail );
+    Aig_ObjCreatePo( pRes, pObj );
+    Aig_ManCleanup( pRes );
+
+    p->pAig = NULL;
+    return pRes;
+    
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA )
+{
+    Aig_Man_t * p;
+    Aig_Obj_t * pMiter, * pSum, * pLit;
+    Sto_Cls_t * pClause;
+    int Var, VarAB, v;
+    p = Aig_ManStart( 10000 );
+    pMiter = Aig_ManConst1(p);
+    Sto_ManForEachClauseRoot( pCnf, pClause )
+    {
+        if ( fClausesA ^ pClause->fA ) // clause of B
+            continue;
+        // clause of A
+        pSum = Aig_ManConst0(p);
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+        {
+            Var = lit_var(pClause->pLits[v]);
+            if ( pMan->pVarTypes[Var] < 0 ) // global var
+            {
+                VarAB = -pMan->pVarTypes[Var]-1;
+                assert( VarAB >= 0 && VarAB < Vec_IntSize(pMan->vVarsAB) );
+                pLit = Aig_NotCond( Aig_IthVar(p, VarAB), lit_sign(pClause->pLits[v]) );
+            }
+            else
+                pLit = Aig_NotCond( Aig_IthVar(p, Vec_IntSize(pMan->vVarsAB)+1+Var), lit_sign(pClause->pLits[v]) );
+            pSum = Aig_Or( p, pSum, pLit );
+        }
+        pMiter = Aig_And( p, pMiter, pSum );
+    }
+    Aig_ObjCreatePo( p, pMiter );
+    return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satInterB_old.c b/src/sat/bsat/satInterB_old.c
new file mode 100644
index 00000000..2afc9855
--- /dev/null
+++ b/src/sat/bsat/satInterB_old.c
@@ -0,0 +1,1061 @@
+/**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"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// variable assignments 
+static const lit    LIT_UNDEF = 0xffffffff;
+
+// interpolation manager
+struct Intb_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 ** Intb_ManAigRead( Intb_Man_t * pMan, Sto_Cls_t * pCls )                   { return pMan->pInters + pCls->Id;          }
+static inline void         Intb_ManAigClear( Intb_Man_t * pMan, Aig_Obj_t ** p )                    { *p = Aig_ManConst0(pMan->pAig);           }
+static inline void         Intb_ManAigFill( Intb_Man_t * pMan, Aig_Obj_t ** p )                     { *p = Aig_ManConst1(pMan->pAig);           }
+static inline void         Intb_ManAigCopy( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q )     { *p = *q;                                  }
+static inline void         Intb_ManAigAnd( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q )      { *p = Aig_And(pMan->pAig, *p, *q);         }
+static inline void         Intb_ManAigOr( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q )       { *p = Aig_Or(pMan->pAig, *p, *q);          }
+static inline void         Intb_ManAigOrNot( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q )    { *p = Aig_Or(pMan->pAig, *p, Aig_Not(*q)); }
+static inline void         Intb_ManAigOrVar( Intb_Man_t * pMan, Aig_Obj_t ** p, int v )             { *p = Aig_Or(pMan->pAig, *p, Aig_IthVar(pMan->pAig, v));          }
+static inline void         Intb_ManAigOrNotVar( Intb_Man_t * pMan, Aig_Obj_t ** p, int v )          { *p = Aig_Or(pMan->pAig, *p, Aig_Not(Aig_IthVar(pMan->pAig, v))); }
+static inline void         Intb_ManAigMux0( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q, int v){ *p = Aig_Mux(pMan->pAig, Aig_IthVar(pMan->pAig, v), *q, *p);     }
+static inline void         Intb_ManAigMux1( Intb_Man_t * pMan, Aig_Obj_t ** p, Aig_Obj_t ** q, int v){ *p = Aig_Mux(pMan->pAig, Aig_IthVar(pMan->pAig, v), *p, *q);     }
+
+// reading/writing the proof for a clause
+static inline int          Intb_ManProofGet( Intb_Man_t * p, Sto_Cls_t * pCls )                  { return p->pProofNums[pCls->Id];           }
+static inline void         Intb_ManProofSet( Intb_Man_t * p, Sto_Cls_t * pCls, int n )           { p->pProofNums[pCls->Id] = n;              }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Intb_Man_t * Intb_ManAlloc()
+{
+    Intb_Man_t * p;
+    // allocate the manager
+    p = (Intb_Man_t *)ABC_ALLOC( char, sizeof(Intb_Man_t) );
+    memset( p, 0, sizeof(Intb_Man_t) );
+    // verification
+    p->nResLitsAlloc = (1<<16);
+    p->pResLits = ABC_ALLOC( 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 Intb_ManGlobalVars( Intb_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 Intb_ManResize( Intb_Man_t * p )
+{
+    p->Counter = 0;
+    // 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    = ABC_REALLOC(lit,         p->pTrail,    p->nVarsAlloc );
+        p->pAssigns  = ABC_REALLOC(lit,         p->pAssigns,  p->nVarsAlloc );
+        p->pSeens    = ABC_REALLOC(char,        p->pSeens,    p->nVarsAlloc );
+        p->pVarTypes = ABC_REALLOC(int,         p->pVarTypes, p->nVarsAlloc );
+        p->pReasons  = ABC_REALLOC(Sto_Cls_t *, p->pReasons,  p->nVarsAlloc );
+        p->pWatches  = ABC_REALLOC(Sto_Cls_t *, p->pWatches,  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
+    Intb_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 = ABC_REALLOC( int, p->pProofNums,  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 = ABC_REALLOC(Aig_Obj_t *, p->pInters, p->nIntersAlloc );
+    }
+    memset( p->pInters, 0, sizeof(Aig_Obj_t *) * p->pCnf->nClauses );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Intb_ManFree( Intb_Man_t * p )
+{
+/*
+    printf( "Runtime stats:\n" );
+ABC_PRT( "BCP     ", p->timeBcp   );
+ABC_PRT( "Trace   ", p->timeTrace );
+ABC_PRT( "TOTAL   ", p->timeTotal );
+*/
+    ABC_FREE( p->pInters );
+    ABC_FREE( p->pProofNums );
+    ABC_FREE( p->pTrail );
+    ABC_FREE( p->pAssigns );
+    ABC_FREE( p->pSeens );
+    ABC_FREE( p->pVarTypes );
+    ABC_FREE( p->pReasons );
+    ABC_FREE( p->pWatches );
+    ABC_FREE( p->pResLits );
+    ABC_FREE( p );
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Intb_ManPrintClause( Intb_Man_t * p, Sto_Cls_t * pClause )
+{
+    int i;
+    printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Intb_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 Intb_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 Intb_ManPrintInterOne( Intb_Man_t * p, Sto_Cls_t * pClause )
+{
+    printf( "Clause %2d :  ", pClause->Id );
+//    Extra_PrintBinary___( stdout, Intb_ManAigRead(p, pClause), (1 << p->nVarsAB) );
+    printf( "\n" );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one clause to the watcher list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Intb_ManWatchClause( Intb_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 Intb_ManEnqueue( Intb_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 Intb_ManCancelUntil( Intb_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 * Intb_ManPropagateOne( Intb_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])
+            Intb_ManWatchClause( p, pCur, pCur->pLits[1] );
+            break;
+        }
+        if ( i < (int)pCur->nLits ) // found new watch
+            continue;
+
+        // clause is unit - enqueue new implication
+        if ( Intb_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 * Intb_ManPropagate( Intb_Man_t * p, int Start )
+{
+    Sto_Cls_t * pClause;
+    int i;
+    int clk = clock();
+    for ( i = Start; i < p->nTrailSize; i++ )
+    {
+        pClause = Intb_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 Intb_ManProofWriteOne( Intb_Man_t * p, Sto_Cls_t * pClause )
+{
+    Intb_ManProofSet( p, pClause, ++p->Counter );
+
+    if ( p->fProofWrite )
+    {
+        int v;
+        fprintf( p->pFile, "%d", Intb_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 Intb_ManGetGlobalVar( Intb_Man_t * p, int Var )
+{
+    int VarAB;
+    if ( p->pVarTypes[Var] >= 0 ) // global var
+        return -1;
+    VarAB = -p->pVarTypes[Var]-1;
+    assert( VarAB >= 0 && VarAB < Vec_IntSize(p->vVarsAB) );
+    return VarAB;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Traces the proof for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Intb_ManProofTraceOne( Intb_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 )
+        Intb_ManAigCopy( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pConflict) );
+
+    // follow the trail backwards
+    PrevId = Intb_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( Intb_ManProofGet(p, pReason) > 0 );
+        p->Counter++;
+        if ( p->fProofWrite )
+            fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Intb_ManProofGet(p, pReason) );
+        PrevId = p->Counter;
+
+        if ( p->pCnf->nClausesA )
+        {
+            if ( p->pVarTypes[Var] == 1 )// || rand() % 10 == 0 ) // var of A
+                Intb_ManAigOr( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason) );
+            else if ( p->pVarTypes[Var] == 0 ) // var of B
+                Intb_ManAigAnd( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason) );
+            else
+            {
+                int VarAB = Intb_ManGetGlobalVar(p, Var);
+                // check that the var is present in the reason
+                for ( v = 0; v < (int)pReason->nLits; v++ )
+                    if ( lit_var(pReason->pLits[v]) == Var )
+                        break;
+                assert( v < (int)pReason->nLits );
+                if ( lit_sign(pReason->pLits[v]) ) // negative polarity
+                    Intb_ManAigMux0( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason), VarAB );
+                else
+                    Intb_ManAigMux1( p, Intb_ManAigRead(p, pFinal), Intb_ManAigRead(p, pReason), VarAB );
+            }
+        }
+ 
+        // resolve the temporary resolvent with the reason clause
+        if ( p->fProofVerif )
+        {
+            int v1, v2; 
+            if ( fPrint )
+                Intb_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 )
+            Intb_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 );
+            Intb_ManPrintClause( p, pConflict );
+            Intb_ManPrintResolvent( p->pResLits, p->nResLits );
+            Intb_ManPrintClause( p, pFinal );
+        }
+    }
+p->timeTrace += clock() - clk;
+
+    // return the proof pointer 
+    if ( p->pCnf->nClausesA )
+    {
+//        Intb_ManPrintInterOne( p, pFinal );
+    }
+    Intb_ManProofSet( p, pFinal, p->Counter );
+    return p->Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Intb_ManProofRecordOne( Intb_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 ( !Intb_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
+        {
+            assert( 0 ); // impossible
+            return 0;
+        }
+
+    // propagate the assumptions
+    pConflict = Intb_ManPropagate( p, p->nRootSize );
+    if ( pConflict == NULL )
+    {
+        assert( 0 ); // cannot prove
+        return 0;
+    }
+
+    // construct the proof
+    Intb_ManProofTraceOne( p, pConflict, pClause );
+
+    // undo to the root level
+    Intb_ManCancelUntil( p, p->nRootSize );
+
+    // add large clauses to the watched lists
+    if ( pClause->nLits > 1 )
+    {
+        Intb_ManWatchClause( p, pClause, pClause->pLits[0] );
+        Intb_ManWatchClause( p, pClause, pClause->pLits[1] );
+        return 1;
+    }
+    assert( pClause->nLits == 1 );
+
+    // if the clause proved is unit, add it and propagate
+    if ( !Intb_ManEnqueue( p, pClause->pLits[0], pClause ) )
+    {
+        assert( 0 ); // impossible
+        return 0;
+    }
+
+    // propagate the assumption
+    pConflict = Intb_ManPropagate( p, p->nRootSize );
+    if ( pConflict )
+    {
+        // construct the proof
+        Intb_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 Intb_ManProcessRoots( Intb_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 )
+        {
+            Intb_ManWatchClause( p, pClause, pClause->pLits[0] );
+            Intb_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 ( !Intb_ManEnqueue( p, pClause->pLits[0], pClause ) )
+        {
+            // detected root level conflict
+            printf( "Error in Intb_ManProcessRoots(): Detected a root-level conflict too early!\n" );
+            assert( 0 );
+            return 0;
+        }
+    }
+
+    // propagate the root unit clauses
+    pClause = Intb_ManPropagate( p, 0 );
+    if ( pClause )
+    {
+        // detected root level conflict
+        Intb_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 Intb_ManPrepareInter( Intb_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
+        {
+            Intb_ManAigFill( p, Intb_ManAigRead(p, pClause) );
+//            Intb_ManPrintInterOne( p, pClause );
+            continue;
+        }
+        // clause of A
+        Intb_ManAigClear( p, Intb_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
+                    Intb_ManAigOrNotVar( p, Intb_ManAigRead(p, pClause), VarAB );
+                else
+                    Intb_ManAigOrVar( p, Intb_ManAigRead(p, pClause), VarAB );
+            }
+        }
+
+//        Intb_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 * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose )
+{
+    Aig_Man_t * pRes;
+    Aig_Obj_t * pObj;
+    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
+    Intb_ManResize( p );
+
+    // prepare the interpolant computation
+    Intb_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 )
+        Intb_ManProofWriteOne( p, pClause );
+
+    // propagate root level assignments
+    if ( Intb_ManProcessRoots( p ) )
+    {
+        // if there is no conflict, consider learned clauses
+        Sto_ManForEachClause( p->pCnf, pClause )
+        {
+            if ( pClause->fRoot )
+                continue;
+            if ( !Intb_ManProofRecordOne( p, pClause ) )
+            {
+                RetValue = 0;
+                break;
+            }
+        }
+    }
+
+    // stop the proof
+    if ( p->fProofWrite )
+    {
+        fclose( p->pFile );
+        p->pFile = NULL;    
+    }
+
+    if ( fVerbose )
+    {
+//        ABC_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;
+    }
+
+    pObj = *Intb_ManAigRead( p, p->pCnf->pTail );
+    Aig_ObjCreatePo( pRes, pObj );
+    Aig_ManCleanup( pRes );
+
+    p->pAig = NULL;
+    return pRes;
+    
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA )
+{
+    Aig_Man_t * p;
+    Aig_Obj_t * pMiter, * pSum, * pLit;
+    Sto_Cls_t * pClause;
+    int Var, VarAB, v;
+    p = Aig_ManStart( 10000 );
+    pMiter = Aig_ManConst1(p);
+    Sto_ManForEachClauseRoot( pCnf, pClause )
+    {
+        if ( fClausesA ^ pClause->fA ) // clause of B
+            continue;
+        // clause of A
+        pSum = Aig_ManConst0(p);
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+        {
+            Var = lit_var(pClause->pLits[v]);
+            if ( pMan->pVarTypes[Var] < 0 ) // global var
+            {
+                VarAB = -pMan->pVarTypes[Var]-1;
+                assert( VarAB >= 0 && VarAB < Vec_IntSize(pMan->vVarsAB) );
+                pLit = Aig_NotCond( Aig_IthVar(p, VarAB), lit_sign(pClause->pLits[v]) );
+            }
+            else
+                pLit = Aig_NotCond( Aig_IthVar(p, Vec_IntSize(pMan->vVarsAB)+1+Var), lit_sign(pClause->pLits[v]) );
+            pSum = Aig_Or( p, pSum, pLit );
+        }
+        pMiter = Aig_And( p, pMiter, pSum );
+    }
+    Aig_ObjCreatePo( p, pMiter );
+    return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satInterP.c b/src/sat/bsat/satInterP.c
index 57fb79d2..76f6982d 100644
--- a/src/sat/bsat/satInterP.c
+++ b/src/sat/bsat/satInterP.c
@@ -27,6 +27,9 @@
 #include "satStore.h"
 #include "vec.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -54,8 +57,10 @@ struct Intp_Man_t_
     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
+//    Vec_Int_t *     vAnties;      // anticedents for all clauses
+//    Vec_Int_t *     vBreaks;      // beginnings of anticedents for each clause
+    Vec_Ptr_t *     vAntClas;     // anticedant clauses
+    int             nAntStart;    // starting antecedant clause
     // proof recording
     int             Counter;      // counter of resolved clauses
     int *           pProofNums;   // the proof numbers for each clause (size nClauses)
@@ -99,8 +104,10 @@ Intp_Man_t * Intp_ManAlloc()
     p->nResLitsAlloc = (1<<16);
     p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc );
     // proof recording
-    p->vAnties = Vec_IntAlloc( 1000 );
-    p->vBreaks = Vec_IntAlloc( 1000 );
+//    p->vAnties = Vec_IntAlloc( 1000 );
+//    p->vBreaks = Vec_IntAlloc( 1000 );
+    p->vAntClas = Vec_PtrAlloc( 1000 );
+    p->nAntStart = 0;
     // parameters
     p->fProofWrite = 0;
     p->fProofVerif = 1;
@@ -137,7 +144,7 @@ void Intp_ManResize( Intp_Man_t * p )
         p->pWatches  = ABC_REALLOC(Sto_Cls_t *, p->pWatches,  p->nVarsAlloc*2 );
     }
 
-    // clean the ABC_FREE space
+    // 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 );
@@ -177,8 +184,9 @@ ABC_PRT( "BCP     ", p->timeBcp   );
 ABC_PRT( "Trace   ", p->timeTrace );
 ABC_PRT( "TOTAL   ", p->timeTotal );
 */
-    Vec_IntFree( p->vAnties );
-    Vec_IntFree( p->vBreaks );
+//    Vec_IntFree( p->vAnties );
+//    Vec_IntFree( p->vBreaks );
+    Vec_VecFree( (Vec_Vec_t *)p->vAntClas );
 //    ABC_FREE( p->pInters );
     ABC_FREE( p->pProofNums );
     ABC_FREE( p->pTrail );
@@ -485,9 +493,16 @@ int Intp_ManProofTraceOne( Intp_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
     // 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 );
+
+//    assert( pFinal->Id == Vec_IntSize(p->vBreaks) );
+//    Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) );
+//    Vec_IntPush( p->vAnties, pConflict->Id );
+    {
+        Vec_Int_t * vAnts = Vec_IntAlloc( 16 );
+        assert( Vec_PtrSize(p->vAntClas) == pFinal->Id - p->nAntStart );
+        Vec_IntPush( vAnts, pConflict->Id );
+        Vec_PtrPush( p->vAntClas, vAnts );
+    }
 
 //    if ( p->pCnf->nClausesA )
 //        Intp_ManAigCopy( p, Intp_ManAigRead(p, pFinal), Intp_ManAigRead(p, pConflict) );
@@ -570,7 +585,8 @@ int Intp_ManProofTraceOne( Intp_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
         }
 
 //        Vec_PtrPush( pFinal->pAntis, pReason );
-        Vec_IntPush( p->vAnties, pReason->Id );
+//        Vec_IntPush( p->vAnties, pReason->Id );
+        Vec_IntPush( (Vec_Int_t *)Vec_PtrEntryLast(p->vAntClas), pReason->Id );
     }
 
     // unmark all seen variables
@@ -668,7 +684,8 @@ int Intp_ManProofRecordOne( Intp_Man_t * p, Sto_Cls_t * pClause )
     for ( i = 0; i < (int)pClause->nLits; i++ )
         if ( p->pAssigns[lit_var(pClause->pLits[i])] == pClause->pLits[i] )
         {
-            Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) );
+//            Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) );
+            Vec_PtrPush( p->vAntClas, Vec_IntAlloc(0) );
             return 1;
         }
 
@@ -705,7 +722,8 @@ int Intp_ManProofRecordOne( Intp_Man_t * p, Sto_Cls_t * pClause )
         {
             // undo to the root level
             Intp_ManCancelUntil( p, p->nRootSize );
-            Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) );
+//            Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) );
+            Vec_PtrPush( p->vAntClas, Vec_IntAlloc(0) );
             return 1;
         }
     }
@@ -736,7 +754,10 @@ int Intp_ManProofRecordOne( Intp_Man_t * p, Sto_Cls_t * pClause )
     pConflict = Intp_ManPropagate( p, p->nRootSize );
     if ( pConflict )
     {
-        // construct the proof
+        // insert place-holders till the empty clause
+        while ( Vec_PtrSize(p->vAntClas) < p->pCnf->pEmpty->Id - p->nAntStart )
+            Vec_PtrPush( p->vAntClas, Vec_IntAlloc(0) );
+        // construct the proof for the empty clause
         Intp_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty );
 //        if ( p->fVerbose )
 //            printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id );
@@ -856,7 +877,7 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore )
 //    sat_solver_setnvars( pSat, nSatVars );
     Vec_IntForEachEntry( vCore, iClause, i )
     {
-        pClause = Vec_PtrEntry( vClauses, iClause );
+        pClause = (Sto_Cls_t *)Vec_PtrEntry( vClauses, iClause );
         if ( !sat_solver_addclause( pSat, pClause->pLits, pClause->pLits+pClause->nLits ) )
         {
             printf( "The core verification problem is trivially UNSAT.\n" );
@@ -895,9 +916,11 @@ void Intp_ManUnsatCoreVerify( Sto_Man_t * pCnf, Vec_Int_t * vCore )
   SeeAlso     []
 
 ***********************************************************************/
-void Intp_ManUnsatCore_rec( Vec_Int_t * vAnties, Vec_Int_t * vBreaks, int iThis, Vec_Int_t * vCore, int nRoots, Vec_Int_t * vVisited )
+void Intp_ManUnsatCore_rec( Vec_Ptr_t * vAntClas, int iThis, Vec_Int_t * vCore, int nRoots, Vec_Int_t * vVisited )
 {
-    int i, iStop, iStart;
+//    int i, iStop, iStart;
+    Vec_Int_t * vAnt;
+    int i, Entry;
     // skip visited clauses
     if ( Vec_IntEntry( vVisited, iThis ) )
         return;
@@ -906,14 +929,17 @@ void Intp_ManUnsatCore_rec( Vec_Int_t * vAnties, Vec_Int_t * vBreaks, int iThis,
     if ( iThis < nRoots )
     {
         Vec_IntPush( vCore, iThis );
-        return;
+        return; 
     }
     // iterate through the clauses
-    iStart = Vec_IntEntry( vBreaks, iThis );
-    iStop = Vec_IntEntry( vBreaks, iThis+1 );
-    assert( iStop != -1 );
-    for ( i = iStart; i < iStop; i++ )
-        Intp_ManUnsatCore_rec( vAnties, vBreaks, Vec_IntEntry(vAnties, i), vCore, nRoots, vVisited );
+//    iStart = Vec_IntEntry( vBreaks, iThis );
+//    iStop = Vec_IntEntry( vBreaks, iThis+1 );
+//    assert( iStop != -1 );
+//    for ( i = iStart; i < iStop; i++ )
+    vAnt = (Vec_Int_t *)Vec_PtrEntry( vAntClas, iThis - nRoots );
+    Vec_IntForEachEntry( vAnt, Entry, i )
+//        Intp_ManUnsatCore_rec( vAntClas, Vec_IntEntry(vAnties, i), vCore, nRoots, vVisited );
+        Intp_ManUnsatCore_rec( vAntClas, Entry, vCore, nRoots, vVisited );
 }
 
 /**Function*************************************************************
@@ -944,7 +970,7 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
     p->fVerbose = fVerbose;
 
     // adjust the manager
-    Intp_ManResize( p );
+    Intp_ManResize( p ); 
 
     // construct proof for each clause
     // start the proof
@@ -955,8 +981,11 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
     }
 
     // write the root clauses
-    Vec_IntClear( p->vAnties );
-    Vec_IntFill( p->vBreaks, p->pCnf->nRoots, 0 );
+//    Vec_IntClear( p->vAnties );
+//    Vec_IntFill( p->vBreaks, p->pCnf->nRoots, 0 );
+    Vec_PtrClear( p->vAntClas );
+    p->nAntStart = p->pCnf->nRoots;
+
     Sto_ManForEachClauseRoot( p->pCnf, pClause )
         Intp_ManProofWriteOne( p, pClause );
 
@@ -977,8 +1006,10 @@ void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fVerbose )
     }
 
     // add the last breaker
-    assert( p->pCnf->pEmpty->Id == Vec_IntSize(p->vBreaks) - 1 );
-    Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) );
+//    assert( p->pCnf->pEmpty->Id == Vec_IntSize(p->vBreaks) - 1 );
+//    Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) );
+    assert( p->pCnf->pEmpty->Id - p->nAntStart == Vec_PtrSize(p->vAntClas) - 1 );
+    Vec_PtrPush( p->vAntClas, Vec_IntAlloc(0) );
 
     // stop the proof
     if ( p->fProofWrite )
@@ -1001,7 +1032,7 @@ p->timeTotal += clock() - clkTotal;
     // derive the UNSAT core
     vCore = Vec_IntAlloc( 1000 );
     vVisited = Vec_IntStart( p->pCnf->pEmpty->Id+1 );
-    Intp_ManUnsatCore_rec( p->vAnties, p->vBreaks, p->pCnf->pEmpty->Id, vCore, p->pCnf->nRoots, vVisited );
+    Intp_ManUnsatCore_rec( p->vAntClas, p->pCnf->pEmpty->Id, vCore, p->pCnf->nRoots, vVisited );
     Vec_IntFree( vVisited );
     if ( fVerbose )
         printf( "Root clauses = %d. Learned clauses = %d. UNSAT core size = %d.\n", 
@@ -1015,3 +1046,5 @@ p->timeTotal += clock() - clkTotal;
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satMem.c b/src/sat/bsat/satMem.c
index f789f927..30861993 100644
--- a/src/sat/bsat/satMem.c
+++ b/src/sat/bsat/satMem.c
@@ -21,9 +21,11 @@
 #include <string.h>
 #include <assert.h>
 
-#include "abc_global.h"
 #include "satMem.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -35,7 +37,7 @@ struct Sat_MmFixed_t_
     int           nEntriesAlloc; // the total number of entries allocated
     int           nEntriesUsed;  // the number of entries in use
     int           nEntriesMax;   // the max number of entries in use
-    char *        pEntriesFree;  // the linked list of ABC_FREE entries
+    char *        pEntriesFree;  // the linked list of free entries
 
     // this is where the memory is stored
     int           nChunkSize;    // the size of one chunk
@@ -52,8 +54,8 @@ struct Sat_MmFlex_t_
 {
     // information about individual entries
     int           nEntriesUsed;  // the number of entries allocated
-    char *        pCurrent;      // the current pointer to ABC_FREE memory
-    char *        pEnd;          // the first entry outside the ABC_FREE memory
+    char *        pCurrent;      // the current pointer to free memory
+    char *        pEnd;          // the first entry outside the free memory
 
     // this is where the memory is stored
     int           nChunkSize;    // the size of one chunk
@@ -167,7 +169,7 @@ char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p )
     char * pTemp;
     int i;
 
-    // check if there are still ABC_FREE entries
+    // check if there are still free entries
     if ( p->nEntriesUsed == p->nEntriesAlloc )
     { // need to allocate more entries
         assert( p->pEntriesFree == NULL );
@@ -196,7 +198,7 @@ char * Sat_MmFixedEntryFetch( Sat_MmFixed_t * p )
     p->nEntriesUsed++;
     if ( p->nEntriesMax < p->nEntriesUsed )
         p->nEntriesMax = p->nEntriesUsed;
-    // return the first entry in the ABC_FREE entry list
+    // return the first entry in the free entry list
     pTemp = p->pEntriesFree;
     p->pEntriesFree = *((char **)pTemp);
     return pTemp;
@@ -217,7 +219,7 @@ void Sat_MmFixedEntryRecycle( Sat_MmFixed_t * p, char * pEntry )
 {
     // decrement the counter of used entries
     p->nEntriesUsed--;
-    // add the entry to the linked list of ABC_FREE entries
+    // add the entry to the linked list of free entries
     *((char **)pEntry) = p->pEntriesFree;
     p->pEntriesFree = pEntry;
 }
@@ -251,7 +253,7 @@ void Sat_MmFixedRestart( Sat_MmFixed_t * p )
     }
     // set the last link
     *((char **)pTemp) = NULL;
-    // set the ABC_FREE entry list
+    // set the free entry list
     p->pEntriesFree  = p->pChunks[0];
     // set the correct statistics
     p->nMemoryAlloc  = p->nEntrySize * p->nChunkSize;
@@ -353,7 +355,7 @@ void Sat_MmFlexStop( Sat_MmFlex_t * p, int fVerbose )
 char * Sat_MmFlexEntryFetch( Sat_MmFlex_t * p, int nBytes )
 {
     char * pTemp;
-    // check if there are still ABC_FREE entries
+    // check if there are still free entries
     if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
     { // need to allocate more entries
         if ( p->nChunks == p->nChunksAlloc )
@@ -548,3 +550,5 @@ int Sat_MmStepReadMemUsage( Sat_MmStep_t * p )
         nMemTotal += p->pMems[i]->nMemoryAlloc;
     return nMemTotal;
 }
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satMem.h b/src/sat/bsat/satMem.h
index b6d93807..13afa9b9 100644
--- a/src/sat/bsat/satMem.h
+++ b/src/sat/bsat/satMem.h
@@ -23,6 +23,10 @@
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
+#include "abc_global.h"
+
+ABC_NAMESPACE_HEADER_START
+
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
@@ -66,6 +70,10 @@ extern char *              Sat_MmStepEntryFetch( Sat_MmStep_t * p, int nBytes );
 extern void                Sat_MmStepEntryRecycle( Sat_MmStep_t * p, char * pEntry, int nBytes );
 extern int                 Sat_MmStepReadMemUsage( Sat_MmStep_t * p );
 
+
+
+ABC_NAMESPACE_HEADER_END
+
 #endif
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index df04cd1f..10dea1e3 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -2,7 +2,7 @@
 MiniSat -- Copyright (c) 2005, Niklas Sorensson
 http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
 
-Permission is hereby granted, ABC_FREE of charge, to any person obtaining a copy of this software and
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
 associated documentation files (the "Software"), to deal in the Software without restriction,
 including without limitation the rights to use, copy, modify, merge, publish, distribute,
 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
@@ -25,7 +25,21 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <math.h>
 
 #include "satSolver.h"
-
+#include "satStore.h"
+
+ABC_NAMESPACE_IMPL_START
+/*
+extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
+extern void * Sto_ManAlloc();
+extern void Sto_ManDumpClauses( void * p, char * pFileName );
+extern void Sto_ManFree( void * p );
+extern int Sto_ManChangeLastClause( void * p );
+extern void Sto_ManMarkRoots( void * p );
+extern void Sto_ManMarkClausesA( void * p );
+*/
 //#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
 
 //=================================================================================================
@@ -91,7 +105,7 @@ static inline void  clause_setactivity(clause* c, float a) { *((float*)&c->lits[
 // Encode literals in clause pointers:
 
 static inline clause* clause_from_lit (lit l)     { return (clause*)((ABC_PTRUINT_T)l + (ABC_PTRUINT_T)l + 1); }
-static inline bool    clause_is_lit   (clause* c) { return ((ABC_PTRUINT_T)c & 1);                              }
+static inline int     clause_is_lit   (clause* c) { return ((ABC_PTRUINT_T)c & 1);                              }
 static inline lit     clause_read_lit (clause* c) { return (lit)((ABC_PTRUINT_T)c >> 1);                        }
 
 //=================================================================================================
@@ -386,6 +400,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
         s->levels    = ABC_REALLOC(int,    s->levels,   s->cap);
         s->tags      = ABC_REALLOC(lbool,  s->tags,     s->cap);
         s->trail     = ABC_REALLOC(lit,    s->trail,    s->cap);
+        s->polarity  = ABC_REALLOC(char,   s->polarity, s->cap);
     }
 
     for (var = s->size; var < n; var++){
@@ -398,6 +413,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
         s->reasons  [var] = (clause*)0;
         s->levels   [var] = 0;
         s->tags     [var] = l_Undef;
+        s->polarity [var] = 0;
         
         /* does not hold because variables enqueued at top level will not be reinserted in the heap
            assert(veci_size(&s->order) == var); 
@@ -410,7 +426,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
 }
 
 
-static inline bool enqueue(sat_solver* s, lit l, clause* from)
+static inline int enqueue(sat_solver* s, lit l, clause* from)
 {
     lbool* values = s->assigns;
     int    v      = lit_var(l);
@@ -457,6 +473,7 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
     lbool*   values;  
     clause** reasons; 
     int      bound;
+    int      lastLev;
     int      c;
     
     if (sat_solver_dlevel(s) <= level)
@@ -466,6 +483,7 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
     values  = s->assigns;
     reasons = s->reasons;
     bound   = (veci_begin(&s->trail_lim))[level];
+    lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1];
 
     ////////////////////////////////////////
     // added to cancel all assignments
@@ -477,6 +495,8 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
         int     x  = lit_var(trail[c]);
         values [x] = l_Undef;
         reasons[x] = (clause*)0;
+        if ( c < lastLev )
+            s->polarity[x] = !lit_sign(trail[c]);
     }
 
     for (c = s->qhead-1; c >= bound; c--)
@@ -497,8 +517,7 @@ static void sat_solver_record(sat_solver* s, veci* cls)
     // add clause to internal storage
     if ( s->pStore )
     {
-        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
-        int RetValue = Sto_ManAddClause( s->pStore, begin, end );
+        int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
         assert( RetValue );
     }
     ///////////////////////////////////
@@ -531,7 +550,7 @@ static double sat_solver_progress(sat_solver* s)
 //=================================================================================================
 // Major methods:
 
-static bool sat_solver_lit_removable(sat_solver* s, lit l, int minl)
+static int sat_solver_lit_removable(sat_solver* s, lit l, int minl)
 {
     lbool*   tags    = s->tags;
     clause** reasons = s->reasons;
@@ -594,6 +613,92 @@ static bool sat_solver_lit_removable(sat_solver* s, lit l, int minl)
     return true;
 }
 
+
+/*_________________________________________________________________________________________________
+|
+|  analyzeFinal : (p : Lit)  ->  [void]
+|  
+|  Description:
+|    Specialized analysis procedure to express the final conflict in terms of assumptions.
+|    Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
+|    stores the result in 'out_conflict'.
+|________________________________________________________________________________________________@*/
+/*
+void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
+{
+    out_conflict.clear();
+    out_conflict.push(p);
+
+    if (decisionLevel() == 0)
+        return;
+
+    seen[var(p)] = 1;
+
+    for (int i = trail.size()-1; i >= trail_lim[0]; i--){
+        Var x = var(trail[i]);
+        if (seen[x]){
+            if (reason(x) == GClause_NULL){
+                assert(level(x) > 0);
+                out_conflict.push(~trail[i]);
+            }else{
+                Clause& c = ca.deref(smartReason(x));
+                for (int j = 1; j < c.size(); j++)
+                    if (level(var(c[j])) > 0)
+                        seen[var(c[j])] = 1;
+            }
+            seen[x] = 0;
+        }
+    }
+
+    seen[var(p)] = 0;
+}
+*/
+
+static void sat_solver_analyze_final(sat_solver* s, lit p, veci* out_conflict)
+{
+    int i, j;
+    veci_resize(out_conflict,0);
+//    veci_push(out_conflict,p); // do not write conflict literal
+    if ( sat_solver_dlevel(s) == 0 )
+        return;
+    assert( veci_size(&s->tagged) == 0 );
+    assert( s->tags[lit_var(p)] == l_Undef );
+    s->tags[lit_var(p)] = l_True;
+    for (i = s->qtail-1; i >= (veci_begin(&s->trail_lim))[0]; i--){
+        int x = lit_var(s->trail[i]);
+        if (s->tags[x] == l_True){
+            if (s->reasons[x] == NULL){
+                assert(s->levels[x] > 0);
+                veci_push(out_conflict,lit_neg(s->trail[i]));
+            }else{
+                clause* c = s->reasons[x];
+                if (clause_is_lit(c)){
+                    lit q = clause_read_lit(c);
+                    assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+                    if (s->levels[lit_var(q)] > 0)
+                    {
+                        s->tags[lit_var(q)] = l_True;
+                        veci_push(&s->tagged,lit_var(q));
+                    }
+                }
+                else{
+                    int* lits = clause_begin(c);
+                    for (j = 1; j < clause_size(c); j++)
+                        if (s->levels[lit_var(lits[j])] > 0)
+                        {
+                            s->tags[lit_var(lits[j])] = l_True;
+                            veci_push(&s->tagged,lit_var(lits[j]));
+                        }
+                }
+            }
+        }
+    }
+    for (i = 0; i < veci_size(&s->tagged); i++)
+        s->tags[veci_begin(&s->tagged)[i]] = l_Undef;
+    veci_resize(&s->tagged,0);
+}
+
+
 static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
 {
     lit*     trail   = s->trail;
@@ -871,6 +976,8 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
 #endif
             s->stats.conflicts++; conflictC++;
             if (sat_solver_dlevel(s) == s->root_level){
+//                lit p = clause_is_lit(confl)? clause_read_lit(confl) : clause_begin(confl)[0];
+//                sat_solver_analyze_final(s, lit_neg(p), &s->conf_final);
                 veci_delete(&learnt_clause);
                 return l_False;
             }
@@ -896,7 +1003,8 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
                 return l_Undef; }
 
             if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) ||
-                 (s->nInsLimit  && s->stats.inspects  > s->nInsLimit) )
+//                 (s->nInsLimit  && s->stats.inspects  > s->nInsLimit) )
+                 (s->nInsLimit  && s->stats.propagations > s->nInsLimit) )
             {
                 // Reached bound on number of conflicts:
                 s->progress_estimate = sat_solver_progress(s);
@@ -938,7 +1046,10 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
                 return l_True;
             }
 
-            assume(s,lit_neg(toLit(next)));
+            if ( s->polarity[next] ) // positive polarity
+                assume(s,toLit(next));
+            else
+                assume(s,lit_neg(toLit(next)));
         }
     }
 
@@ -963,6 +1074,7 @@ sat_solver* sat_solver_new(void)
     veci_new(&s->model);
     veci_new(&s->act_vars);
     veci_new(&s->temp_clause);
+    veci_new(&s->conf_final);
 
     // initialize arrays
     s->wlists    = 0;
@@ -1038,6 +1150,7 @@ void sat_solver_delete(sat_solver* s)
     veci_delete(&s->model);
     veci_delete(&s->act_vars);
     veci_delete(&s->temp_clause);
+    veci_delete(&s->conf_final);
     ABC_FREE(s->binary);
 
     // delete arrays
@@ -1056,6 +1169,7 @@ void sat_solver_delete(sat_solver* s)
         ABC_FREE(s->levels   );
         ABC_FREE(s->trail    );
         ABC_FREE(s->tags     );
+        ABC_FREE(s->polarity );
     }
 
     sat_solver_store_free(s);
@@ -1063,7 +1177,7 @@ void sat_solver_delete(sat_solver* s)
 }
 
 
-bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
+int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
 {
     lit *i,*j;
     int maxvar;
@@ -1096,8 +1210,7 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
     // add clause to internal storage
     if ( s->pStore )
     {
-        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
-        int RetValue = Sto_ManAddClause( s->pStore, begin, end );
+        int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
         assert( RetValue );
     }
     ///////////////////////////////////
@@ -1135,7 +1248,7 @@ bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
 }
 
 
-bool sat_solver_simplify(sat_solver* s)
+int sat_solver_simplify(sat_solver* s)
 {
     clause** reasons;
     int type;
@@ -1171,10 +1284,30 @@ bool sat_solver_simplify(sat_solver* s)
     return true;
 }
 
+double luby(double y, int x)
+{
+    int size, seq;
+    for (size = 1, seq = 0; size < x+1; seq++, size = 2*size + 1);
+    while (size-1 != x){
+        size = (size-1) >> 1;
+        seq--;
+        x = x % size;
+    }
+    return pow(y, (double)seq);
+} 
+
+void luby_test()
+{
+    int i;
+    for ( i = 0; i < 20; i++ )
+        printf( "%d ", (int)luby(2,i) );
+    printf( "\n" );
+}
 
 int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
 {
-    ABC_INT64_T  nof_conflicts = 100;
+    int restart_iter = 0;
+    ABC_INT64_T  nof_conflicts;
     ABC_INT64_T  nof_learnts   = sat_solver_nclauses(s) / 3;
     lbool   status        = l_Undef;
     lbool*  values        = s->assigns;
@@ -1185,8 +1318,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
     {
         if ( s->pStore )
         {
-            extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
-            int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL );
+            int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
             assert( RetValue );
         }
         return l_False;
@@ -1201,7 +1333,8 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
     if ( nConfLimit )
         s->nConfLimit = s->stats.conflicts + nConfLimit;
     if ( nInsLimit )
-        s->nInsLimit = s->stats.inspects + nInsLimit;
+//        s->nInsLimit = s->stats.inspects + nInsLimit;
+        s->nInsLimit = s->stats.propagations + nInsLimit;
     if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) )
         s->nConfLimit = nConfLimitGlobal;
     if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
@@ -1250,9 +1383,11 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
                 s->progress_estimate*100);
             fflush(stdout);
         }
+        nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) );
+//printf( "%d ", (int)nof_conflicts );
         status = sat_solver_search(s, nof_conflicts, nof_learnts);
-        nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
-        nof_learnts   = nof_learnts * 11 / 10; //*= 1.1;
+//        nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
+        nof_learnts    = nof_learnts * 11 / 10; //*= 1.1;
 
         // quit the loop if reached an external limit
         if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
@@ -1260,7 +1395,8 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
 //            printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
             break;
         }
-        if ( s->nInsLimit  && s->stats.inspects > s->nInsLimit )
+//        if ( s->nInsLimit  && s->stats.inspects > s->nInsLimit )
+        if ( s->nInsLimit  && s->stats.propagations > s->nInsLimit )
         {
 //            printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
             break;
@@ -1274,8 +1410,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
     ////////////////////////////////////////////////
     if ( status == l_False && s->pStore )
     {
-        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
-        int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL );
+        int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
         assert( RetValue );
     }
     ////////////////////////////////////////////////
@@ -1305,41 +1440,35 @@ int sat_solver_nconflicts(sat_solver* s)
 
 void sat_solver_store_alloc( sat_solver * s )
 {
-    extern void * Sto_ManAlloc();
     assert( s->pStore == NULL );
     s->pStore = Sto_ManAlloc();
 }
 
 void sat_solver_store_write( sat_solver * s, char * pFileName )
 {
-    extern void Sto_ManDumpClauses( void * p, char * pFileName );
-    if ( s->pStore ) Sto_ManDumpClauses( s->pStore, pFileName );
+    if ( s->pStore ) Sto_ManDumpClauses( (Sto_Man_t *)s->pStore, pFileName );
 }
 
 void sat_solver_store_free( sat_solver * s )
 {
-    extern void Sto_ManFree( void * p );
-    if ( s->pStore ) Sto_ManFree( s->pStore );
+    if ( s->pStore ) Sto_ManFree( (Sto_Man_t *)s->pStore );
     s->pStore = NULL;
 }
 
 int sat_solver_store_change_last( sat_solver * s )
 {
-    extern int Sto_ManChangeLastClause( void * p );
-    if ( s->pStore ) return Sto_ManChangeLastClause( s->pStore );
+    if ( s->pStore ) return Sto_ManChangeLastClause( (Sto_Man_t *)s->pStore );
     return -1;
 }
  
 void sat_solver_store_mark_roots( sat_solver * s )
 {
-    extern void Sto_ManMarkRoots( void * p );
-    if ( s->pStore ) Sto_ManMarkRoots( s->pStore );
+    if ( s->pStore ) Sto_ManMarkRoots( (Sto_Man_t *)s->pStore );
 }
 
 void sat_solver_store_mark_clauses_a( sat_solver * s )
 {
-    extern void Sto_ManMarkClausesA( void * p );
-    if ( s->pStore ) Sto_ManMarkClausesA( s->pStore );
+    if ( s->pStore ) Sto_ManMarkClausesA( (Sto_Man_t *)s->pStore );
 }
 
 void * sat_solver_store_release( sat_solver * s )
@@ -1404,3 +1533,5 @@ void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void
 //    for ( i = 1; i < size; i++ )
 //        assert(comp(array[i-1], array[i])<0);
 }
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index f37c1738..2e435c59 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -2,7 +2,7 @@
 MiniSat -- Copyright (c) 2005, Niklas Sorensson
 http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
 
-Permission is hereby granted, ABC_FREE of charge, to any person obtaining a copy of this software and
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
 associated documentation files (the "Software"), to deal in the Software without restriction,
 including without limitation the rights to use, copy, modify, merge, publish, distribute,
 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
@@ -22,28 +22,29 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef satSolver_h
 #define satSolver_h
 
+
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
 
-#include "abc_global.h"
 #include "satVec.h"
 #include "satMem.h"
 
+ABC_NAMESPACE_HEADER_START
+
+
 //=================================================================================================
 // Simple types:
 
-// does not work for c++
-//typedef int                   bool;
 #ifndef __cplusplus
-#ifndef bool
-#define bool int
+#ifndef false
+#  define false 0
+#endif
+#ifndef true
+#  define true 1
 #endif
 #endif
-
-static const bool  true      = 1;
-static const bool  false     = 0;
 
 typedef int                lit;
 typedef char               lbool;
@@ -74,8 +75,8 @@ typedef struct sat_solver_t sat_solver;
 extern sat_solver* sat_solver_new(void);
 extern void        sat_solver_delete(sat_solver* s);
 
-extern bool        sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
-extern bool        sat_solver_simplify(sat_solver* s);
+extern int         sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
+extern int         sat_solver_simplify(sat_solver* s);
 extern int         sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
 
 extern int         sat_solver_nvars(sat_solver* s);
@@ -89,7 +90,7 @@ struct stats_t
     ABC_INT64_T   starts, decisions, propagations, inspects, conflicts;
     ABC_INT64_T   clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
 };
-typedef struct stats_t stats;
+typedef struct stats_t stats_t;
 
 extern void        Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
 extern void        Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
@@ -139,6 +140,7 @@ struct sat_solver_t
     clause** reasons;       //
     int*     levels;        //
     lit*     trail;
+    char*    polarity;
 
     clause*  binary;        // A temporary binary clause
     lbool*   tags;          //
@@ -148,6 +150,8 @@ struct sat_solver_t
     veci     order;         // Variable order. (heap) (contains: var)
     veci     trail_lim;     // Separator indices for different decision levels in 'trail'. (contains: int)
     veci     model;         // If problem is solved, this vector contains the model (contains: lbool).
+    veci     conf_final;    // If problem is unsatisfiable (possibly under assumptions),
+                            // this vector represent the final conflict clause expressed in the assumptions.
 
     int      root_level;    // Level of first proper decision.
     int      simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
@@ -156,7 +160,7 @@ struct sat_solver_t
     double   progress_estimate;
     int      verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
 
-    stats    stats;
+    stats_t    stats;
 
     ABC_INT64_T   nConfLimit;    // external limit on the number of conflicts
     ABC_INT64_T   nInsLimit;     // external limit on the number of implications
@@ -210,4 +214,8 @@ static void sat_solver_compress(sat_solver* s)
     }
 }
 
+
+
+ABC_NAMESPACE_HEADER_END
+
 #endif
diff --git a/src/sat/bsat/satStore.c b/src/sat/bsat/satStore.c
index fff8a836..ac74c4a6 100644
--- a/src/sat/bsat/satStore.c
+++ b/src/sat/bsat/satStore.c
@@ -26,6 +26,9 @@
 
 #include "satStore.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -185,6 +188,7 @@ int Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd )
 
     // get memory for the clause
     nSize = sizeof(Sto_Cls_t) + sizeof(lit) * (pEnd - pBeg);
+    nSize = (nSize / sizeof(char*) + ((nSize % sizeof(char*)) > 0)) * sizeof(char*); // added by Saurabh on Sep 3, 2009
     pClause = (Sto_Cls_t *)Sto_ManMemoryFetch( p, nSize );
     memset( pClause, 0, sizeof(Sto_Cls_t) );
 
@@ -192,6 +196,7 @@ int Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd )
     pClause->Id = p->nClauses++;
     pClause->nLits = pEnd - pBeg;
     memcpy( pClause->pLits, pBeg, sizeof(lit) * (pEnd - pBeg) );
+//    assert( pClause->pLits[0] >= 0 );
 
     // add the clause to the list
     if ( p->pHead == NULL )
@@ -461,3 +466,5 @@ Sto_Man_t * Sto_ManLoadClauses( char * pFileName )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h
index ea11f46a..0293aea7 100644
--- a/src/sat/bsat/satStore.h
+++ b/src/sat/bsat/satStore.h
@@ -21,6 +21,7 @@
 #ifndef __SAT_STORE_H__
 #define __SAT_STORE_H__
 
+
 /*
     The trace of SAT solving contains the original clauses of the problem
     along with the learned clauses derived during SAT solving.
@@ -38,9 +39,7 @@
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef __cplusplus
-extern "C" {
-#endif
+ABC_NAMESPACE_HEADER_START
 
 #ifdef _WIN32
 #define inline __inline // compatible with MS VS 6.0
@@ -116,8 +115,10 @@ extern int          Sto_ManMemoryReport( Sto_Man_t * p );
 extern void         Sto_ManMarkRoots( Sto_Man_t * p );
 extern void         Sto_ManMarkClausesA( Sto_Man_t * p );
 extern void         Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName );
+extern int          Sto_ManChangeLastClause( Sto_Man_t * p );
 extern Sto_Man_t *  Sto_ManLoadClauses( char * pFileName );
 
+
 /*=== satInter.c ==========================================================*/
 typedef struct Int_Man_t_ Int_Man_t;
 extern Int_Man_t *  Int_ManAlloc();
@@ -143,9 +144,11 @@ 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
+
+
+ABC_NAMESPACE_HEADER_END
+
+
 
 #endif
 
diff --git a/src/sat/bsat/satTrace.c b/src/sat/bsat/satTrace.c
index 08cfadf6..ae701ce9 100644
--- a/src/sat/bsat/satTrace.c
+++ b/src/sat/bsat/satTrace.c
@@ -20,6 +20,9 @@
 
 #include "satSolver.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /*
     The trace of SAT solving contains the original clause of the problem
     along with the learned clauses derived during SAT solving.
@@ -105,3 +108,5 @@ void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 5f8008bb..0ce40acd 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -22,6 +22,9 @@
 #include <assert.h>
 #include "satSolver.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -35,7 +38,7 @@ struct clause_t
 static inline int  clause_size( clause* c )  { return c->size_learnt >> 1; }
 static inline lit* clause_begin( clause* c ) { return c->lits;             }
 
-static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement );
+static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -78,13 +81,13 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBe
     nClauses = p->clauses.size;
     pClauses = p->clauses.ptr;
     for ( i = 0; i < nClauses; i++ )
-        Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars );
+        Sat_SolverClauseWriteDimacs( pFile, (clause *)pClauses[i], incrementVars );
 
     // write the learned clauses
     nClauses = p->learnts.size;
     pClauses = p->learnts.ptr;
     for ( i = 0; i < nClauses; i++ )
-        Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars );
+        Sat_SolverClauseWriteDimacs( pFile, (clause *)pClauses[i], incrementVars );
 
     // write zero-level assertions
     for ( i = 0; i < p->size; i++ )
@@ -119,14 +122,14 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBe
   SeeAlso     []
 
 ***********************************************************************/
-void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement )
+void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement )
 {
     lit * pLits = clause_begin(pC);
     int nLits = clause_size(pC);
     int i;
 
     for ( i = 0; i < nLits; i++ )
-        fprintf( pFile, "%s%d ", (lit_sign(pLits[i])? "-": ""),  lit_var(pLits[i]) + (int)(fIncrement>0) );
+        fprintf( pFile, "%s%d ", (lit_sign(pLits[i])? "-": ""),  lit_var(pLits[i]) + (fIncrement>0) );
     if ( fIncrement )
         fprintf( pFile, "0" );
     fprintf( pFile, "\n" );
@@ -169,7 +172,7 @@ int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars )
 {
     int * pModel;
     int i;
-    pModel = ABC_ALLOC( int, nVars+1 );
+    pModel = ABC_CALLOC( int, nVars+1 );
     for ( i = 0; i < nVars; i++ )
     {
         assert( pVars[i] >= 0 && pVars[i] < p->size );
@@ -213,7 +216,7 @@ void Sat_SolverDoubleClauses( sat_solver * p, int iVar )
     nClauses = vecp_size(&p->clauses);
     for ( c = 0; c < nClauses; c++ )
     {
-        pClause = p->clauses.ptr[c];
+        pClause = (clause *)p->clauses.ptr[c];
         nLits = clause_size(pClause);
         pLits = clause_begin(pClause);
         for ( v = 0; v < nLits; v++ )
@@ -231,3 +234,5 @@ void Sat_SolverDoubleClauses( sat_solver * p, int iVar )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h
index f017c90b..4c3763e3 100644
--- a/src/sat/bsat/satVec.h
+++ b/src/sat/bsat/satVec.h
@@ -2,7 +2,7 @@
 MiniSat -- Copyright (c) 2005, Niklas Sorensson
 http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
 
-Permission is hereby granted, ABC_FREE of charge, to any person obtaining a copy of this software and
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
 associated documentation files (the "Software"), to deal in the Software without restriction,
 including without limitation the rights to use, copy, modify, merge, publish, distribute,
 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
@@ -22,6 +22,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef satVec_h
 #define satVec_h
 
+#include "abc_global.h"
+
+ABC_NAMESPACE_HEADER_START
+
+
 // vector of 32-bit intergers (added for 64-bit portability)
 struct veci_t {
     int    size;
@@ -78,4 +83,8 @@ static inline void   vecp_push   (vecp* v, void* e)
 }
 
 
+
+
+ABC_NAMESPACE_HEADER_END
+
 #endif