Started SAT-based reparameterization.

6 files changed, 474 insertions, 151 deletions

diff --git a/src/aig/aig/aigRepar.c b/src/aig/aig/aigRepar.c
new file mode 100644
index 00000000..d10471d7
--- /dev/null
+++ b/src/aig/aig/aigRepar.c
@@ -0,0 +1,397 @@
+/**CFile****************************************************************
+
+  FileName    [aigRepar.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Interpolation-based reparametrization.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigRepar.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+#include "cnf.h"
+#include "satSolver2.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Adds buffer to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Aig_ManInterAddBuffer( sat_solver2 * pSat, int iVarA, int iVarB, int fCompl, int fMark )
+{
+    lit Lits[2];
+    int Cid;
+    assert( iVarA >= 0 && iVarB >= 0 );
+
+    Lits[0] = toLitCond( iVarA, 0 );
+    Lits[1] = toLitCond( iVarB, !fCompl );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+
+    Lits[0] = toLitCond( iVarA, 1 );
+    Lits[1] = toLitCond( iVarB, fCompl );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 2 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds constraints for the two-input AND-gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Aig_ManInterAddXor( sat_solver2 * pSat, int iVarA, int iVarB, int iVarC, int fCompl, int fMark )
+{
+    lit Lits[3];
+    int Cid;
+    assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
+
+    Lits[0] = toLitCond( iVarA, !fCompl );
+    Lits[1] = toLitCond( iVarB, 1 );
+    Lits[2] = toLitCond( iVarC, 1 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+
+    Lits[0] = toLitCond( iVarA, !fCompl );
+    Lits[1] = toLitCond( iVarB, 0 );
+    Lits[2] = toLitCond( iVarC, 0 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+
+    Lits[0] = toLitCond( iVarA, fCompl );
+    Lits[1] = toLitCond( iVarB, 1 );
+    Lits[2] = toLitCond( iVarC, 0 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+
+    Lits[0] = toLitCond( iVarA, fCompl );
+    Lits[1] = toLitCond( iVarB, 0 );
+    Lits[2] = toLitCond( iVarC, 1 );
+    Cid = sat_solver2_addclause( pSat, Lits, Lits + 3 );
+    if ( fMark )
+        clause_set_partA( pSat, Cid, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManInterTest( Aig_Man_t * pMan, int fVerbose )
+{
+    sat_solver2 * pSat;
+    Aig_Man_t * pInter;
+    Vec_Int_t * vVars;
+    Cnf_Dat_t * pCnf;
+    Aig_Obj_t * pObj;
+    int Lit, Cid, Var, status, i;
+    int clk = clock();
+    assert( Aig_ManRegNum(pMan) == 0 );
+    assert( Aig_ManPoNum(pMan) == 1 );
+
+    // derive CNFs
+    pCnf = Cnf_Derive( pMan, 1 );
+
+    // start the solver
+    pSat = sat_solver2_new();
+    sat_solver2_setnvars( pSat, 2*pCnf->nVars+1 );
+    // set A-variables (all used except PI/PO)
+    Aig_ManForEachObj( pMan, pObj, i )
+    {
+        if ( pCnf->pVarNums[pObj->Id] < 0 )
+            continue;
+        if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsPo(pObj) )
+            var_set_partA( pSat, pCnf->pVarNums[pObj->Id], 1 );
+    }
+
+    // add clauses of A
+    for ( i = 0; i < pCnf->nClauses; i++ )
+    {
+        Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
+        clause_set_partA( pSat, Cid, 1 );
+    }
+
+    // add clauses of B
+    Cnf_DataLift( pCnf, pCnf->nVars );
+    for ( i = 0; i < pCnf->nClauses; i++ )
+        sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
+    Cnf_DataLift( pCnf, -pCnf->nVars );
+
+    // add PI equality clauses
+    vVars = Vec_IntAlloc( Aig_ManPoNum(pMan)+1 );
+    Aig_ManForEachPi( pMan, pObj, i )
+    {
+        if ( Aig_ObjRefs(pObj) == 0 )
+            continue;
+        Var = pCnf->pVarNums[pObj->Id];
+        Aig_ManInterAddBuffer( pSat, Var, pCnf->nVars + Var, 0, 0 );
+        Vec_IntPush( vVars, Var );
+    }
+
+    // add an XOR clause in the end
+    Var = pCnf->pVarNums[Aig_ManPo(pMan,0)->Id];
+    Aig_ManInterAddXor( pSat, Var, pCnf->nVars + Var, 2*pCnf->nVars, 0, 0 );
+    Vec_IntPush( vVars, Var );
+
+    // solve the problem
+    Lit = toLitCond( 2*pCnf->nVars, 0 );
+    status = sat_solver2_solve( pSat, &Lit, &Lit + 1, 0, 0, 0, 0 );
+    assert( status == l_False );
+    Sat_Solver2PrintStats( stdout, pSat );
+
+    // derive interpolant
+    pInter = Sat_ProofInterpolant( pSat, vVars );
+    Aig_ManPrintStats( pInter );
+    Aig_ManDumpBlif( pInter, "int.blif", NULL, NULL );
+
+    // clean up
+    Aig_ManStop( pInter );
+    Vec_IntFree( vVars );
+    Cnf_DataFree( pCnf );
+    sat_solver2_delete( pSat );
+    ABC_PRT( "Total interpolation time", clock() - clk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while mapping PIs into the given array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManAppend( Aig_Man_t * pBase, Aig_Man_t * pNew )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    assert( Aig_ManPoNum(pNew) == 1 );
+    assert( Aig_ManPiNum(pNew) == Aig_ManPiNum(pBase) );
+    // create the PIs
+    Aig_ManCleanData( pNew );
+    Aig_ManConst1(pNew)->pData = Aig_ManConst1(pBase);
+    Aig_ManForEachPi( pNew, pObj, i )
+        pObj->pData = Aig_IthVar(pBase, i);
+    // duplicate internal nodes
+    Aig_ManForEachNode( pNew, pObj, i )
+        pObj->pData = Aig_And( pBase, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // add one PO to base
+    pObj = Aig_ManPo( pNew, 0 );
+    Aig_ObjCreatePo( pBase, Aig_ObjChild0Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
+{
+    Aig_Man_t * pAigTemp, * pInter, * pBase = NULL;
+    sat_solver2 * pSat;
+    Vec_Int_t * vVars;
+    Cnf_Dat_t * pCnf, * pCnfInter;
+    Aig_Obj_t * pObj;
+    int nOuts = Aig_ManPoNum(pMan);
+    int ShiftP[2], ShiftCnf[2], ShiftOr[2], ShiftAssume;
+    int Cid, Lit, status, i, k, c;
+    int clk = clock();
+    assert( Aig_ManRegNum(pMan) == 0 );
+
+    // derive CNFs
+    pCnf = Cnf_Derive( pMan, nOuts );
+
+    // start the solver
+    pSat = sat_solver2_new();
+    sat_solver2_setnvars( pSat, 4*pCnf->nVars + 6*nOuts );
+    // vars: pGlobal + (p0 + A1 + A2 + or0) + (p1 + B1 + B2 + or1) + pAssume;
+    ShiftP[0] = nOuts;
+    ShiftP[1] = 2*pCnf->nVars + 3*nOuts;
+    ShiftCnf[0] = ShiftP[0] + nOuts;
+    ShiftCnf[1] = ShiftP[1] + nOuts;
+    ShiftOr[0] = ShiftCnf[0] + 2*pCnf->nVars;
+    ShiftOr[1] = ShiftCnf[1] + 2*pCnf->nVars;
+    ShiftAssume = ShiftOr[1] + nOuts;
+    assert( ShiftAssume + nOuts == pSat->size );
+
+    // mark variables of A
+    for ( i = ShiftCnf[0]; i < ShiftP[1]; i++ )
+        var_set_partA( pSat, i, 1 );
+
+    // add clauses of A, then B
+    vVars = Vec_IntAlloc( 2*nOuts );
+    for ( k = 0; k < 2; k++ )
+    {
+        // copy A1
+        Cnf_DataLift( pCnf, ShiftCnf[k] );
+        for ( i = 0; i < pCnf->nClauses; i++ )
+        {
+            Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
+            clause_set_partA( pSat, Cid, k==0 );
+        }
+        // add equality p[k] == A1/B1
+        Aig_ManForEachPo( pMan, pObj, i )
+            Aig_ManInterAddBuffer( pSat, ShiftP[k] + i, pCnf->pVarNums[pObj->Id], k==1, k==0 );
+        // copy A2
+        Cnf_DataLift( pCnf, pCnf->nVars );
+        for ( i = 0; i < pCnf->nClauses; i++ )
+        {
+            Cid = sat_solver2_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] );
+            clause_set_partA( pSat, Cid, k==0 );
+        }
+        // add comparator (!p[k] ^ A2/B2) == or[k]
+        Vec_IntClear( vVars );
+        Aig_ManForEachPo( pMan, pObj, i )
+        {
+            Aig_ManInterAddXor( pSat, ShiftP[k] + i, pCnf->pVarNums[pObj->Id], ShiftOr[k] + i, k==1, k==0 );
+            Vec_IntPush( vVars, toLitCond(ShiftOr[k] + i, 1) );
+        }
+        Cid = sat_solver2_addclause( pSat, Vec_IntArray(vVars), Vec_IntArray(vVars) + Vec_IntSize(vVars) );
+        clause_set_partA( pSat, Cid, k==0 );
+        // return to normal
+        Cnf_DataLift( pCnf, -ShiftCnf[k]-pCnf->nVars );
+    }
+    // add clauses to constrain p[0] and p[1]
+    for ( k = 0; k < nOuts; k++ )
+        Aig_ManInterAddXor( pSat, ShiftP[0] + k, ShiftP[1] + k, ShiftAssume + k, 0, 0 );
+
+    // start the interpolant
+    pBase = Aig_ManStart( 1000 );
+    pBase->pName = Aig_UtilStrsav( "repar" );
+    for ( k = 0; k < 2*nOuts; k++ )
+        Aig_IthVar(pBase, i);
+
+    // start global variables (pGlobal and p[0])
+    Vec_IntClear( vVars );
+    for ( k = 0; k < 2*nOuts; k++ )
+        Vec_IntPush( vVars, k );
+
+    // perform iterative solving
+    // vars: pGlobal + (p0 + A1 + A2 + or0) + (p1 + B1 + B2 + or1) + pAssume;
+    for ( k = 0; k < nOuts; k++ )
+    {
+        // swap k-th variables
+        int Temp = Vec_IntEntry( vVars, k );
+        Vec_IntWriteEntry( vVars, k, Vec_IntEntry(vVars, nOuts+k) );
+        Vec_IntWriteEntry( vVars, nOuts+k, Temp );
+
+        // solve incrementally 
+        Lit = toLitCond( ShiftAssume + k, 1 ); // XOR output is 0 ==> p1 == p2
+        status = sat_solver2_solve( pSat, &Lit, &Lit + 1, 0, 0, 0, 0 );
+        assert( status == l_False );
+        Sat_Solver2PrintStats( stdout, pSat );
+
+        // derive interpolant
+        pInter = Sat_ProofInterpolant( pSat, vVars );
+        Aig_ManPrintStats( pInter );
+        // make sure interpolant does not depend on useless vars
+        Aig_ManForEachPi( pInter, pObj, i )
+            assert( i <= k || Aig_ObjRefs(pObj) == 0 );
+
+        // simplify
+        pInter = Dar_ManRwsat( pAigTemp = pInter, 1, 0 );
+        Aig_ManStop( pAigTemp );
+
+        // add interpolant to the solver
+        pCnfInter = Cnf_Derive( pInter, 1 );
+        Cnf_DataLift( pCnfInter, pSat->size );
+        sat_solver2_setnvars( pSat, pSat->size + 2*pCnfInter->nVars );
+        for ( i = 0; i < pCnfInter->nVars; i++ )
+            var_set_partA( pSat, pSat->size-2*pCnfInter->nVars + i, 1 );
+        for ( c = 0; c < 2; c++ )
+        {
+            if ( c == 1 )
+                Cnf_DataLift( pCnfInter, pCnfInter->nVars );
+            // add to A
+            for ( i = 0; i < pCnfInter->nClauses; i++ )
+            {
+                Cid = sat_solver2_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] );
+                clause_set_partA( pSat, Cid, c==0 );
+            }
+            // connect to the inputs
+            Aig_ManForEachPi( pInter, pObj, i )
+                if ( i <= k )
+                    Aig_ManInterAddBuffer( pSat, i, pCnf->pVarNums[pObj->Id], 0, c==0 );
+            // connect to the outputs
+            pObj = Aig_ManPo(pInter, 0);
+            Aig_ManInterAddBuffer( pSat, ShiftP[c] + k, pCnf->pVarNums[pObj->Id], 0, c==0 );
+            if ( c == 1 )
+                Cnf_DataLift( pCnfInter, -pCnfInter->nVars );
+        }
+        Cnf_DataFree( pCnfInter );
+
+        // accumulate
+        Aig_ManAppend( pBase, pInter );
+        Aig_ManStop( pInter );
+
+        // update global variables
+        Temp = Vec_IntEntry( vVars, k );
+        Vec_IntWriteEntry( vVars, k, Vec_IntEntry(vVars, nOuts+k) );
+        Vec_IntWriteEntry( vVars, nOuts+k, Temp );
+    }
+
+    Vec_IntFree( vVars );
+    Cnf_DataFree( pCnf );
+    sat_solver2_delete( pSat );
+    ABC_PRT( "Reparameterization time", clock() - clk );
+    return pBase;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index c291433f..aaf5bf6d 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -17,6 +17,7 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigPart.c \
     src/aig/aig/aigPartReg.c \
     src/aig/aig/aigPartSat.c \
+    src/aig/aig/aigRepar.c \
     src/aig/aig/aigRepr.c \
     src/aig/aig/aigRet.c \
     src/aig/aig/aigRetF.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9042d1ed..862288fd 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8891,12 +8891,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 */
 
 {
-    extern void Abs_VfaManTest( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose );
+//    extern void Abs_VfaManTest( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose );
+    extern void Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose );
     extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
     if ( pNtk )
     {
         Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
-        Abs_VfaManTest( pAig, 32, 1000000, 1 );
+        Aig_ManInterRepar( pAig, 1 );
         Aig_ManStop( pAig );
     }
 }
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 337fe3ca..ded11f1e 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -133,10 +133,10 @@ static inline satset* Proof_ResolveRead (Rec_Int_t* p, cla h )    { return (sats
 // iterating through fanins of a proof node
 #define Proof_NodeForeachFanin( p, pNode, pFanin, i )        \
     for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 2)), 1); i++ )
-#define Proof_NodeForeachLeaf( pLeaves, pNode, pLeaf, i )    \
-    for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pLeaves, pNode->pEnts[i] >> 2) : NULL), 1); i++ )
-#define Proof_NodeForeachFaninLeaf( p, pLeaves, pNode, pFanin, i )    \
-    for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pLeaves, pNode->pEnts[i] >> 2) : Proof_NodeRead(p, pNode->pEnts[i] >> 2)); i++ )
+#define Proof_NodeForeachLeaf( pClauses, pNode, pLeaf, i )   \
+    for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pClauses, pNode->pEnts[i] >> 2) : NULL), 1); i++ )
+#define Proof_NodeForeachFaninLeaf( p, pClauses, pNode, pFanin, i )    \
+    for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pClauses, pNode->pEnts[i] >> 2) : Proof_NodeRead(p, pNode->pEnts[i] >> 2)); i++ )
 
 
 ////////////////////////////////////////////////////////////////////////
@@ -420,135 +420,6 @@ void Sat_ProofReduce( sat_solver2 * s )
 
 
 
-#if 0
- 
-/**Function*************************************************************
-
-  Synopsis    [Performs one resultion step.]
-
-  Description [Returns ID of the resolvent if success, and -1 if failure.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-satset * Sat_ProofCheckResolveOne( Vec_Int_t * p, satset * c1, satset * c2, Vec_Int_t * vTemp )
-{
-    satset * c;
-    int i, k, hNode, Var = -1, Count = 0;
-    // find resolution variable
-    for ( i = 0; i < (int)c1->nEnts; i++ )
-    for ( k = 0; k < (int)c2->nEnts; k++ )
-        if ( (c1->pEnts[i] ^ c2->pEnts[k]) == 1 )
-        {
-            Var = (c1->pEnts[i] >> 1);
-            Count++;
-        }
-    if ( Count == 0 )
-    {
-        printf( "Cannot find resolution variable\n" );
-        return NULL;
-    }
-    if ( Count > 1 )
-    {
-        printf( "Found more than 1 resolution variables\n" );
-        return NULL;
-    }
-    // perform resolution
-    Vec_IntClear( vTemp );
-    for ( i = 0; i < (int)c1->nEnts; i++ )
-        if ( (c1->pEnts[i] >> 1) != Var )
-            Vec_IntPush( vTemp, c1->pEnts[i] );
-    for ( i = 0; i < (int)c2->nEnts; i++ )
-        if ( (c2->pEnts[i] >> 1) != Var )
-            Vec_IntPushUnique( vTemp, c2->pEnts[i] );
-    // move to the new one
-    hNode = Vec_IntSize( p );
-    Vec_IntPush( p, 0 ); // placeholder
-    Vec_IntPush( p, 0 );
-    Vec_IntForEachEntry( vTemp, Var, i )
-        Vec_IntPush( p, Var );
-    c = Proof_NodeRead( p, hNode );
-    c->nEnts = Vec_IntSize(vTemp);
-    return c;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks the proof for consitency.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-satset * Sat_ProofCheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vResolves, int iAnt )
-{
-    satset * pAnt;
-    if ( iAnt & 1 )
-        return Proof_NodeRead( vClauses, iAnt >> 2 );
-    assert( iAnt > 0 );
-    pAnt = Proof_NodeRead( vProof, iAnt >> 2 );
-    assert( pAnt->Id > 0 );
-    return Proof_NodeRead( vResolves, pAnt->Id );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks the proof for consitency.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sat_ProofCheck( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot )
-{
-    Vec_Int_t * vUsed, * vResolves, * vTemp;
-    satset * pSet, * pSet0, * pSet1;
-    int i, k, Counter = 0, clk = clock(); 
-    // collect visited clauses
-    vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
-    Proof_CleanCollected( vProof, vUsed );
-    // perform resolution steps
-    vTemp = Vec_IntAlloc( 1000 );
-    vResolves = Vec_IntAlloc( 1000 );
-    Vec_IntPush( vResolves, -1 );
-    Proof_ForeachNodeVec( vUsed, vProof, pSet, i )
-    {
-        pSet0 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] );
-        for ( k = 1; k < (int)pSet->nEnts; k++ )
-        {
-            pSet1 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[k] );
-            pSet0 = Sat_ProofCheckResolveOne( vResolves, pSet0, pSet1, vTemp );
-        }
-        pSet->Id = Proof_NodeHandle( vResolves, pSet0 );
-//printf( "Clause for proof %d: ", Vec_IntEntry(vUsed, i) );
-//satset_print( pSet0 );
-        Counter++;
-    }
-    Vec_IntFree( vTemp );
-    // clean the proof
-    Proof_CleanCollected( vProof, vUsed );
-    // compare the final clause
-    printf( "Used %6.2f Mb for resolvents.\n", 4.0 * Vec_IntSize(vResolves) / (1<<20) );
-    if ( pSet0->nEnts > 0 )
-        printf( "Cound not derive the empty clause.  " );
-    else
-        printf( "Proof verification successful.  " );
-    Abc_PrintTime( 1, "Time", clock() - clk );
-    // cleanup
-    Vec_IntFree( vResolves );
-    Vec_IntFree( vUsed );
-}
-
-#endif
-
 /**Function*************************************************************
 
   Synopsis    [Performs one resultion step.]
@@ -669,7 +540,7 @@ void Sat_ProofCheck( sat_solver2 * s )
     // compare the final clause
     printf( "Used %6.2f Mb for resolvents.\n", 4.0 * Rec_IntSize(vResolves) / (1<<20) );
     if ( pSet0->nEnts > 0 )
-        printf( "Cound not derive the empty clause.  " );
+        printf( "Derived clause with %d lits instead of the empty clause.  ", pSet0->nEnts );
     else
         printf( "Proof verification successful.  " );
     Abc_PrintTime( 1, "Time", clock() - clk );
@@ -689,7 +560,7 @@ void Sat_ProofCheck( sat_solver2 * s )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vUsed )
+Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t * vUsed, int fUseIds )
 {
     Vec_Int_t * vCore;
     satset * pNode, * pFanin;
@@ -709,11 +580,59 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_
     Proof_ForeachNodeVec( vCore, vClauses, pNode, i )
     {
         pNode->mark = 0;
-        Vec_IntWriteEntry( vCore, i, pNode->Id - 1 );
+        if ( fUseIds )
+            Vec_IntWriteEntry( vCore, i, pNode->Id - 1 );
     }
     return vCore;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Verifies that variables are labeled correctly.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_ProofInterpolantCheckVars( sat_solver2 * s, Vec_Int_t * vGloVars )
+{
+    satset* c; 
+    Vec_Int_t * vVarMap;
+    int i, k, Entry, * pMask;
+    int Counts[5] = {0};
+    // map variables into their type (A, B, or AB)
+    vVarMap = Vec_IntStart( s->size );
+    sat_solver_foreach_clause( s, c, i )
+        for ( k = 0; k < (int)c->nEnts; k++ )
+            *Vec_IntEntryP(vVarMap, lit_var(c->pEnts[k])) |= 2 - c->partA;
+    // analyze variables
+    Vec_IntForEachEntry( vGloVars, Entry, i )
+    {
+        pMask = Vec_IntEntryP(vVarMap, Entry);
+        assert( *pMask >= 0 && *pMask <= 3 );
+        Counts[(*pMask & 3)]++;
+        *pMask = 0;
+    }
+    // count the number of global variables not listed
+    Vec_IntForEachEntry( vVarMap, Entry, i )
+        if ( Entry == 3 )
+            Counts[4]++;
+    Vec_IntFree( vVarMap );
+    // report
+    if ( Counts[0] )
+        printf( "Warning: %6d variables listed as global do not appear in clauses (this is normal)\n", Counts[0] );
+    if ( Counts[1] )
+        printf( "Warning: %6d variables listed as global appear only in A-clauses (this is a BUG)\n", Counts[1] );
+    if ( Counts[2] )
+        printf( "Warning: %6d variables listed as global appear only in B-clauses (this is a BUG)\n", Counts[2] );
+    if ( Counts[3] )
+        printf( "Warning: %6d (out of %d) variables listed as global appear in both A- and B-clauses (this is normal)\n", Counts[3], Vec_IntSize(vGloVars) );
+    if ( Counts[4] )
+        printf( "Warning: %6d variables not listed as global appear in both A- and B-clauses (this is a BUG)\n", Counts[4] );
+}
 
 /**Function*************************************************************
 
@@ -737,15 +656,17 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
     satset * pNode, * pFanin;
     Aig_Man_t * pAig;
     Aig_Obj_t * pObj;
-    int i, k, iVar, Entry;
+    int i, k, iVar, Lit, Entry;
+
+    Sat_ProofInterpolantCheckVars( s, vGlobVars );
 
     // collect visited nodes
     vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
     // collect core clauses (cleans vUsed and vCore)
-    vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed );
+    vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 0 );
 
     // map variables into their global numbers
-    vVarMap = Vec_IntStartFull( Vec_IntFindMax(vGlobVars) + 1 );
+    vVarMap = Vec_IntStartFull( s->size );
     Vec_IntForEachEntry( vGlobVars, Entry, i )
         Vec_IntWriteEntry( vVarMap, Entry, i );
 
@@ -762,9 +683,9 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
         if ( pNode->partA )
         {
             pObj = Aig_ManConst0( pAig );
-            satset_foreach_var( pNode, iVar, k, 0 )
-                if ( iVar < Vec_IntSize(vVarMap) && Vec_IntEntry(vVarMap, iVar) >= 0 )
-                    pObj = Aig_Or( pAig, pObj, Aig_IthVar(pAig, iVar) );
+            satset_foreach_lit( pNode, Lit, k, 0 )
+                if ( (iVar = Vec_IntEntry(vVarMap, lit_var(Lit))) >= 0 )
+                    pObj = Aig_Or( pAig, pObj, Aig_NotCond(Aig_IthVar(pAig, iVar), lit_sign(Lit)) );
         }
         else
             pObj = Aig_ManConst1( pAig );
@@ -777,9 +698,11 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
     // copy the numbers out and derive interpol for resolvents
     Proof_ForeachNodeVec( vUsed, vProof, pNode, i )
     {
+//        satset_print( pNode );
         assert( pNode->nEnts > 1 );
         Proof_NodeForeachFaninLeaf( vProof, vClauses, pNode, pFanin, k )
         {
+            assert( pFanin->Id < 2*Aig_ManObjNumMax(pAig) );
             if ( k == 0 )
                 pObj = Aig_ObjFromLit( pAig, pFanin->Id );
             else if ( pNode->pEnts[k] & 2 ) // variable of A
@@ -828,7 +751,7 @@ void * Sat_ProofCore( sat_solver2 * s )
     // collect visited clauses
     vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot );
     // collect core clauses 
-    vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed );
+    vCore = Sat_ProofCollectCore( vClauses, vProof, vUsed, 1 );
     Vec_IntFree( vUsed );
     return vCore;
 }
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index e2bea751..5eb65132 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -144,11 +144,9 @@ static inline void    solver2_clear_marks(sat_solver2* s)              {
 static inline satset* clause_read   (sat_solver2* s, cla h)      { return (h & 1) ? satset_read(&s->learnts, h>>1)  : satset_read(&s->clauses, h>>1);          }
 static inline cla     clause_handle (sat_solver2* s, satset* c)  { return c->learnt ? (satset_handle(&s->learnts, c)<<1)|1: satset_handle(&s->clauses, c)<<1;  }
 static inline int     clause_check  (sat_solver2* s, satset* c)  { return c->learnt ? satset_check(&s->learnts, c)  : satset_check(&s->clauses, c);            }
-static inline int     clause_proofid(sat_solver2* s, satset* c, int partA)  { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | 1; }
+static inline int     clause_proofid(sat_solver2* s, satset* c, int partA)  { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (satset_handle(&s->clauses, c)<<2) | (partA<<1) | 1; }
 static inline int     clause_is_used(sat_solver2* s, cla h)      { return (h & 1) ? (h >> 1) < s->hLearntPivot : (h >> 1) < s->hClausePivot;                   }
 
-
-
 //static inline int     var_reason    (sat_solver2* s, int v)      { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1;                   } 
 //static inline int     lit_reason    (sat_solver2* s, int l)      { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; } 
 //static inline satset* var_unit_clause(sat_solver2* s, int v)           { return (s->reasons[v]&1) ? clause_read(s, s->reasons[v] >> 1) : NULL;  } 
@@ -163,9 +161,6 @@ int    clause_is_partA (sat_solver2* s, int h)                   { return clause
 void   clause_set_partA(sat_solver2* s, int h, int partA)        { clause_read(s, h)->partA = partA;        }
 int    clause_id(sat_solver2* s, int h)                          { return clause_read(s, h)->Id;            }
 
-#define sat_solver_foreach_clause( s, c, h )  satset_foreach_entry( &s->clauses, c, h, 1 )
-#define sat_solver_foreach_learnt( s, c, h )  satset_foreach_entry( &s->learnts, c, h, 1 )
-
 //=================================================================================================
 // Simple helpers:
 
@@ -1452,6 +1447,7 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end)
         if ( !solver2_enqueue(s,begin[0],0) )
             assert( 0 );
     }
+//satset_print( clause_read(s, Cid) );
     return Cid;
 }
 
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index 83dbb6cb..e5b85a43 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -184,6 +184,11 @@ static inline void    satset_print  (satset * c)          {
     for ( i = 0; (i < veci_size(pVec)) && ((c) = satset_read(p, veci_begin(pVec)[i])); i++ )
 #define satset_foreach_var( p, var, i, start )        \
     for ( i = start; (i < (int)(p)->nEnts) && ((var) = lit_var((p)->pEnts[i])); i++ )
+#define satset_foreach_lit( p, lit, i, start )        \
+    for ( i = start; (i < (int)(p)->nEnts) && ((lit) = (p)->pEnts[i]); i++ )
+
+#define sat_solver_foreach_clause( s, c, h )  satset_foreach_entry( &s->clauses, c, h, 1 )
+#define sat_solver_foreach_learnt( s, c, h )  satset_foreach_entry( &s->learnts, c, h, 1 )
 
 //=================================================================================================
 // Public APIs: