Version abc80130_2

3 files changed, 1394 insertions, 0 deletions

diff --git a/src/sat/proof/pr.c b/src/sat/proof/pr.c
new file mode 100644
index 00000000..2d1ab2d1
--- /dev/null
+++ b/src/sat/proof/pr.c
@@ -0,0 +1,1263 @@
+/**CFile****************************************************************
+
+  FileName    [pr.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Proof recording.]
+
+  Synopsis    [Core procedures of the package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: pr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+//#include "vec.h"
+#include "pr.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef unsigned lit;
+
+typedef struct Pr_Cls_t_ Pr_Cls_t;
+struct Pr_Cls_t_
+{
+    unsigned        uTruth;       // interpolant
+    void *          pProof;       // the proof node 
+//    void *          pAntis;       // the anticedents
+    Pr_Cls_t *      pNext;        // the next clause
+    Pr_Cls_t *      pNext0;       // the next 0-watch
+    Pr_Cls_t *      pNext1;       // the next 0-watch
+    int             Id;           // the clause ID
+    unsigned        fA     :  1;  // belongs to A
+    unsigned        fRoot  :  1;  // original clause
+    unsigned        fVisit :  1;  // visited clause
+    unsigned        nLits  : 24;  // the number of literals
+    lit             pLits[0];     // literals of this clause
+};
+
+struct Pr_Man_t_
+{
+    // general data
+    int             fProofWrite;  // writes the proof file
+    int             fProofVerif;  // verifies the proof
+    int             nVars;        // the number of variables
+    int             nVarsAB;      // the number of global variables
+    int             nRoots;       // the number of root clauses
+    int             nClauses;     // the number of all clauses
+    int             nClausesA;    // the number of clauses of A 
+    Pr_Cls_t *      pHead;        // the head clause
+    Pr_Cls_t *      pTail;        // the tail clause
+    Pr_Cls_t *      pLearnt;      // the tail clause
+    Pr_Cls_t *      pEmpty;       // the empty clause
+    // 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)
+    char *          pVarTypes;    // variable type (size nVars) [1=A, 0=B, <0=AB]
+    Pr_Cls_t **     pReasons;     // reasons for each assignment (size nVars)          
+    Pr_Cls_t **     pWatches;     // watched clauses for each literal (size 2*nVars)          
+    int             nVarsAlloc;   // the allocated size of arrays
+    // proof recording
+    void *          pManProof;    // proof manager
+    int             Counter;      // counter of resolved clauses
+    // memory management
+    int             nChunkSize;   // the number of bytes in a chunk
+    int             nChunkUsed;   // the number of bytes used in the last chunk
+    char *          pChunkLast;   // the last memory chunk
+    // 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;
+    int             timeTrace;
+    int             timeRead;
+    int             timeTotal;
+};
+
+#ifndef PRT
+#define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
+#endif
+
+// variable assignments 
+static const lit  LIT_UNDEF = 0xffffffff;
+
+// variable/literal conversions (taken from MiniSat)
+static inline lit   toLit    (int v)        { return v + v;  }
+static inline lit   toLitCond(int v, int c) { return v + v + (c != 0); }
+static inline lit   lit_neg  (lit l)        { return l ^ 1;  }
+static inline int   lit_var  (lit l)        { return l >> 1; }
+static inline int   lit_sign (lit l)        { return l & 1;  }
+static inline int   lit_print(lit l)        { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
+static inline lit   lit_read (int s)        { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
+static inline int   lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n;                  }
+
+// iterators through the clauses
+#define Pr_ManForEachClause( p, pCls )        for( pCls = p->pHead; pCls; pCls = pCls->pNext )
+#define Pr_ManForEachClauseRoot( p, pCls )    for( pCls = p->pHead; pCls != p->pLearnt; pCls = pCls->pNext )
+#define Pr_ManForEachClauseLearnt( p, pCls )  for( pCls = p->pLearnt; pCls; pCls = pCls->pNext )
+
+// static procedures
+static char *     Pr_ManMemoryFetch( Pr_Man_t * p, int nBytes );
+static void       Pr_ManMemoryStop( Pr_Man_t * p );
+static void       Pr_ManResize( Pr_Man_t * p, int nVarsNew );
+
+// exported procedures
+extern Pr_Man_t * Pr_ManAlloc( int nVarsAlloc );
+extern void       Pr_ManFree( Pr_Man_t * p );
+extern int        Pr_ManAddClause( Pr_Man_t * p, lit * pBeg, lit * pEnd, int fRoot, int fClauseA );
+extern int        Pr_ManProofWrite( Pr_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Pr_Man_t * Pr_ManAlloc( int nVarsAlloc )
+{
+    Pr_Man_t * p;
+    // allocate the manager
+    p = (Pr_Man_t *)malloc( sizeof(Pr_Man_t) );
+    memset( p, 0, sizeof(Pr_Man_t) );
+    // allocate internal arrays
+    Pr_ManResize( p, nVarsAlloc? nVarsAlloc : 256 );
+    // set the starting number of variables
+    p->nVars = 0;
+    // memory management
+    p->nChunkSize = (1<<16); // use 64K chunks
+    // verification
+    p->nResLitsAlloc = (1<<16);
+    p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
+    // parameters
+    p->fProofWrite = 0;
+    p->fProofVerif = 0;
+    return p;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resize proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pr_ManResize( Pr_Man_t * p, int nVarsNew )
+{
+    // check if resizing is needed
+    if ( p->nVarsAlloc < nVarsNew )
+    {
+        int nVarsAllocOld = p->nVarsAlloc;
+        // find the new size
+        if ( p->nVarsAlloc == 0 )
+            p->nVarsAlloc = 1;
+        while ( p->nVarsAlloc < nVarsNew ) 
+            p->nVarsAlloc *= 2;
+        // resize the arrays
+        p->pTrail    = (lit *)      realloc( p->pTrail,    sizeof(lit) * p->nVarsAlloc );
+        p->pAssigns  = (lit *)      realloc( p->pAssigns,  sizeof(lit) * p->nVarsAlloc );
+        p->pSeens    = (char *)     realloc( p->pSeens,    sizeof(char) * p->nVarsAlloc );
+        p->pVarTypes = (char *)     realloc( p->pVarTypes, sizeof(char) * p->nVarsAlloc );
+        p->pReasons  = (Pr_Cls_t **)realloc( p->pReasons,  sizeof(Pr_Cls_t *) * p->nVarsAlloc );
+        p->pWatches  = (Pr_Cls_t **)realloc( p->pWatches,  sizeof(Pr_Cls_t *) * p->nVarsAlloc*2 );
+        // clean the free space
+        memset( p->pAssigns  + nVarsAllocOld, 0xff, sizeof(lit) * (p->nVarsAlloc - nVarsAllocOld) );
+        memset( p->pSeens    + nVarsAllocOld, 0, sizeof(char) * (p->nVarsAlloc - nVarsAllocOld) );
+        memset( p->pVarTypes + nVarsAllocOld, 0, sizeof(char) * (p->nVarsAlloc - nVarsAllocOld) );
+        memset( p->pReasons  + nVarsAllocOld, 0, sizeof(Pr_Cls_t *) * (p->nVarsAlloc - nVarsAllocOld) );
+        memset( p->pWatches  + nVarsAllocOld, 0, sizeof(Pr_Cls_t *) * (p->nVarsAlloc - nVarsAllocOld)*2 );
+    }
+    // adjust the number of variables
+    if ( p->nVars < nVarsNew )
+        p->nVars = nVarsNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocate proof manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pr_ManFree( Pr_Man_t * p )
+{
+    printf( "Runtime stats:\n" );
+PRT( "Reading ", p->timeRead  );
+PRT( "BCP     ", p->timeBcp   );
+PRT( "Trace   ", p->timeTrace );
+PRT( "TOTAL   ", p->timeTotal );
+
+    Pr_ManMemoryStop( p );
+    free( p->pTrail );
+    free( p->pAssigns );
+    free( p->pSeens );
+    free( p->pVarTypes );
+    free( p->pReasons );
+    free( p->pWatches );
+    free( p->pResLits );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one clause to the watcher list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Pr_ManWatchClause( Pr_Man_t * p, Pr_Cls_t * pClause, lit Lit )
+{
+    assert( lit_check(Lit, p->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    [Adds one clause to the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pr_ManAddClause( Pr_Man_t * p, lit * pBeg, lit * pEnd, int fRoot, int fClauseA )
+{
+    Pr_Cls_t * pClause;
+    lit Lit, * i, * j;
+    int nSize, VarMax;
+
+    // process the literals
+    if ( pBeg < pEnd )
+    {
+        // insertion sort
+        VarMax = lit_var( *pBeg );
+        for ( i = pBeg + 1; i < pEnd; i++ )
+        {
+            Lit = *i;
+            VarMax = lit_var(Lit) > VarMax ? lit_var(Lit) : VarMax;
+            for ( j = i; j > pBeg && *(j-1) > Lit; j-- )
+                *j = *(j-1);
+            *j = Lit;
+        }
+        // make sure there is no duplicated variables
+        for ( i = pBeg + 1; i < pEnd; i++ )
+            assert( lit_var(*(i-1)) != lit_var(*i) );
+        // resize the manager
+        Pr_ManResize( p, VarMax+1 );
+    }
+
+    // get memory for the clause
+    nSize = sizeof(Pr_Cls_t) + sizeof(lit) * (pEnd - pBeg);
+    pClause = (Pr_Cls_t *)Pr_ManMemoryFetch( p, nSize );
+    memset( pClause, 0, sizeof(Pr_Cls_t) );
+
+    // assign the clause
+    assert( !fClauseA || fRoot ); // clause of A is always a root clause
+    p->nRoots += fRoot;
+    p->nClausesA += fClauseA;
+    pClause->Id = p->nClauses++;
+    pClause->fA = fClauseA;
+    pClause->fRoot = fRoot;
+    pClause->nLits = pEnd - pBeg;
+    memcpy( pClause->pLits, pBeg, sizeof(lit) * (pEnd - pBeg) );
+
+    // add the clause to the list
+    if ( p->pHead == NULL )
+        p->pHead = pClause;
+    if ( p->pTail == NULL )
+        p->pTail = pClause;
+    else
+    {
+        p->pTail->pNext = pClause;
+        p->pTail = pClause;
+    }
+
+    // mark the first learnt clause
+    if ( p->pLearnt == NULL && !pClause->fRoot )
+        p->pLearnt = pClause;
+
+    // add the empty clause
+    if ( pClause->nLits == 0 )
+    {
+        if ( p->pEmpty )
+            printf( "More than one empty clause!\n" );
+        p->pEmpty = pClause;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fetches memory.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Pr_ManMemoryFetch( Pr_Man_t * p, int nBytes )
+{
+    char * pMem;
+    if ( p->pChunkLast == NULL || nBytes > p->nChunkSize - p->nChunkUsed )
+    {
+        pMem = (char *)malloc( p->nChunkSize );
+        *(char **)pMem = p->pChunkLast;
+        p->pChunkLast = pMem;
+        p->nChunkUsed = sizeof(char *);
+    }
+    pMem = p->pChunkLast + p->nChunkUsed;
+    p->nChunkUsed += nBytes;
+    return pMem;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pr_ManMemoryStop( Pr_Man_t * p )
+{
+    char * pMem, * pNext;
+    if ( p->pChunkLast == NULL )
+        return;
+    for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext )
+        free( pMem );
+    free( pMem );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reports memory usage in bytes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pr_ManMemoryReport( Pr_Man_t * p )
+{
+    int Total;
+    char * pMem, * pNext;
+    if ( p->pChunkLast == NULL )
+        return 0;
+    Total = p->nChunkUsed; 
+    for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext )
+        Total += p->nChunkSize;
+    return Total;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_PrintBinary_( FILE * pFile, unsigned Sign[], int nBits )
+{
+    int Remainder, nWords;
+    int w, i;
+
+    Remainder = (nBits%(sizeof(unsigned)*8));
+    nWords    = (nBits/(sizeof(unsigned)*8)) + (Remainder>0);
+
+    for ( w = nWords-1; w >= 0; w-- )
+        for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- )
+            fprintf( pFile, "%c", '0' + (int)((Sign[w] & (1<<i)) > 0) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the interpolant for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pr_ManPrintInterOne( Pr_Man_t * p, Pr_Cls_t * pClause )
+{
+    printf( "Clause %2d :  ", pClause->Id );
+    Extra_PrintBinary_( stdout, &pClause->uTruth, (1 << p->nVarsAB) );
+    printf( "\n" );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Records implication.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Pr_ManEnqueue( Pr_Man_t * p, lit Lit, Pr_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 Pr_ManCancelUntil( Pr_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 Pr_Cls_t * Pr_ManPropagateOne( Pr_Man_t * p, lit Lit )
+{
+    Pr_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])
+            Pr_ManWatchClause( p, pCur, pCur->pLits[1] );
+            break;
+        }
+        if ( i < (int)pCur->nLits ) // found new watch
+            continue;
+
+        // clause is unit - enqueue new implication
+        if ( Pr_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     []
+
+***********************************************************************/
+Pr_Cls_t * Pr_ManPropagate( Pr_Man_t * p, int Start )
+{
+    Pr_Cls_t * pClause;
+    int i;
+    int clk = clock();
+    for ( i = Start; i < p->nTrailSize; i++ )
+    {
+        pClause = Pr_ManPropagateOne( p, p->pTrail[i] );
+        if ( pClause )
+        {
+p->timeBcp += clock() - clk;
+            return pClause;
+        }
+    }
+p->timeBcp += clock() - clk;
+    return NULL;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pr_ManPrintClause( Pr_Cls_t * pClause )
+{
+    int i;
+    printf( "Clause ID = %d. Proof = %d. {", pClause->Id, (int)pClause->pProof );
+    for ( i = 0; i < (int)pClause->nLits; i++ )
+        printf( " %d", pClause->pLits[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the resolvent.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pr_ManPrintResolvent( lit * pResLits, int nResLits )
+{
+    int i;
+    printf( "Resolvent: {" );
+    for ( i = 0; i < nResLits; i++ )
+        printf( " %d", pResLits[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes one root clause into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pr_ManProofWriteOne( Pr_Man_t * p, Pr_Cls_t * pClause )
+{
+    pClause->pProof = (void *)++p->Counter;
+
+    if ( p->fProofWrite )
+    {
+        int v;
+        fprintf( p->pManProof, "%d", (int)pClause->pProof );
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+            fprintf( p->pManProof, " %d", lit_print(pClause->pLits[v]) );
+        fprintf( p->pManProof, " 0 0\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Traces the proof for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pr_ManProofTraceOne( Pr_Man_t * p, Pr_Cls_t * pConflict, Pr_Cls_t * pFinal )
+{
+    Pr_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->nClausesA )
+        pFinal->uTruth = pConflict->uTruth;
+   
+    // follow the trail backwards
+    PrevId = (int)pConflict->pProof;
+    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( pReason->pProof > 0 );
+        p->Counter++;
+        if ( p->fProofWrite )
+            fprintf( p->pManProof, "%d * %d %d 0\n", p->Counter, PrevId, (int)pReason->pProof );
+        PrevId = p->Counter;
+
+        if ( p->nClausesA )
+        {
+            if ( p->pVarTypes[Var] == 1 ) // var of A
+                pFinal->uTruth |= pReason->uTruth;
+            else
+                pFinal->uTruth &= pReason->uTruth;
+        }
+ 
+        // resolve the temporary resolvent with the reason clause
+        if ( p->fProofVerif )
+        {
+            int v1, v2; 
+            if ( fPrint )
+                Pr_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 )
+            Pr_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 );
+            Pr_ManPrintClause( pConflict );
+            Pr_ManPrintResolvent( p->pResLits, p->nResLits );
+            Pr_ManPrintClause( pFinal );
+        }
+    }
+p->timeTrace += clock() - clk;
+
+    // return the proof pointer 
+    if ( p->nClausesA )
+    {
+        Pr_ManPrintInterOne( p, pFinal );
+    }
+    return p->Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof for one clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pr_ManProofRecordOne( Pr_Man_t * p, Pr_Cls_t * pClause )
+{
+    Pr_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 ( !Pr_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
+        {
+            assert( 0 ); // impossible
+            return 0;
+        }
+
+    // propagate the assumptions
+    pConflict = Pr_ManPropagate( p, p->nRootSize );
+    if ( pConflict == NULL )
+    {
+        assert( 0 ); // cannot prove
+        return 0;
+    }
+
+    // construct the proof
+    pClause->pProof = (void *)Pr_ManProofTraceOne( p, pConflict, pClause );
+
+    // undo to the root level
+    Pr_ManCancelUntil( p, p->nRootSize );
+
+    // add large clauses to the watched lists
+    if ( pClause->nLits > 1 )
+    {
+        Pr_ManWatchClause( p, pClause, pClause->pLits[0] );
+        Pr_ManWatchClause( p, pClause, pClause->pLits[1] );
+        return 1;
+    }
+    assert( pClause->nLits == 1 );
+
+    // if the clause proved is unit, add it and propagate
+    if ( !Pr_ManEnqueue( p, pClause->pLits[0], pClause ) )
+    {
+        assert( 0 ); // impossible
+        return 0;
+    }
+
+    // propagate the assumption
+    pConflict = Pr_ManPropagate( p, p->nRootSize );
+    if ( pConflict )
+    {
+        // construct the proof
+        p->pEmpty->pProof = (void *)Pr_ManProofTraceOne( p, pConflict, p->pEmpty );
+        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 Pr_ManProcessRoots( Pr_Man_t * p )
+{
+    Pr_Cls_t * pClause;
+    int Counter;
+
+    // make sure the root clauses are preceeding the learnt clauses
+    Counter = 0;
+    Pr_ManForEachClause( p, pClause )
+    {
+        assert( (int)pClause->fA    == (Counter < (int)p->nClausesA) );
+        assert( (int)pClause->fRoot == (Counter < (int)p->nRoots)    );
+        Counter++;
+    }
+    assert( p->nClauses == Counter );
+
+    // make sure the last clause if empty
+    assert( p->pTail->nLits == 0 );
+
+    // go through the root unit clauses
+    p->nTrailSize = 0;
+    Pr_ManForEachClauseRoot( p, pClause )
+    {
+        // create watcher lists for the root clauses
+        if ( pClause->nLits > 1 )
+        {
+            Pr_ManWatchClause( p, pClause, pClause->pLits[0] );
+            Pr_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->nVars) );
+        if ( !Pr_ManEnqueue( p, pClause->pLits[0], pClause ) )
+        {
+            // detected root level conflict
+            printf( "Pr_ManProcessRoots(): Detected a root-level conflict\n" );
+            assert( 0 );
+            return 0;
+        }
+    }
+
+    // propagate the root unit clauses
+    pClause = Pr_ManPropagate( p, 0 );
+    if ( pClause )
+    {
+        // detected root level conflict
+        printf( "Pr_ManProcessRoots(): Detected a root-level conflict\n" );
+        assert( 0 );
+        return 0;
+    }
+
+    // set the root level
+    p->nRootSize = p->nTrailSize;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Pr_ManPrepareInter( Pr_Man_t * p )
+{
+    unsigned uTruths[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    Pr_Cls_t * pClause;
+    int Var, v;
+
+    // mark the variable encountered in the clauses of A
+    Pr_ManForEachClauseRoot( p, 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
+    p->nVarsAB = 0;
+    Pr_ManForEachClauseRoot( p, 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
+                p->nVarsAB++;
+                p->pVarTypes[Var] = -1;
+            }
+        }
+    }
+
+    // order global variables
+    p->nVarsAB = 0;
+    for ( v = 0; v < p->nVars; v++ )
+        if ( p->pVarTypes[v] == -1 )
+            p->pVarTypes[v] -= p->nVarsAB++;
+printf( "There are %d global variables.\n", p->nVarsAB );
+
+    // set interpolants for root clauses
+    Pr_ManForEachClauseRoot( p, pClause )
+    {
+        if ( !pClause->fA ) // clause of B
+        {
+            pClause->uTruth = ~0;
+            Pr_ManPrintInterOne( p, pClause );
+            continue;
+        }
+        // clause of A
+        pClause->uTruth = 0;
+        for ( v = 0; v < (int)pClause->nLits; v++ )
+        {
+            Var = lit_var(pClause->pLits[v]);
+            if ( p->pVarTypes[Var] < 0 ) // global var
+            {
+                if ( lit_sign(pClause->pLits[v]) ) // negative var
+                    pClause->uTruth |= ~uTruths[ -p->pVarTypes[Var]-1 ];
+                else
+                    pClause->uTruth |= uTruths[ -p->pVarTypes[Var]-1 ];
+            }
+        }
+        Pr_ManPrintInterOne( p, pClause );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pr_ManProofWrite( Pr_Man_t * p )
+{
+    Pr_Cls_t * pClause;
+    int RetValue = 1;
+
+    // propagate root level assignments
+    Pr_ManProcessRoots( p );
+
+    // prepare the interpolant computation
+    if ( p->nClausesA )
+        Pr_ManPrepareInter( p );
+
+    // construct proof for each clause
+    // start the proof
+    if ( p->fProofWrite )
+        p->pManProof = fopen( "proof.cnf_", "w" );
+    p->Counter = 0;
+
+    // write the root clauses
+    Pr_ManForEachClauseRoot( p, pClause )
+        Pr_ManProofWriteOne( p, pClause );
+
+    // consider each learned clause
+    Pr_ManForEachClauseLearnt( p, pClause )
+    {
+        if ( !Pr_ManProofRecordOne( p, pClause ) )
+        {
+            RetValue = 0;
+            break;
+        }
+    }
+
+    if ( p->nClausesA )
+    {
+        printf( "Interpolant:  " );
+    }
+
+
+    // stop the proof
+    if ( p->fProofWrite )
+    {
+        fclose( p->pManProof );
+        p->pManProof = NULL;    
+    }
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads clauses from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Pr_Man_t * Pr_ManProofRead( char * pFileName )
+{
+    Pr_Man_t * p = NULL;
+    char * pCur, * pBuffer = NULL;
+    int * pArray = NULL;
+    FILE * pFile;
+    int RetValue, Counter, nNumbers, Temp;
+    int nClauses, nClausesA, nRoots, nVars;
+
+    // open the file
+    pFile = fopen( pFileName, "r" );
+    if ( pFile == NULL )
+    {
+        printf( "Count not open input file \"%s\".\n", pFileName );
+        return NULL;
+    }
+
+    // read the file
+    pBuffer = (char *)malloc( (1<<16) );
+    for ( Counter = 0; fgets( pBuffer, (1<<16), pFile ); )
+    {
+        if ( pBuffer[0] == 'c' )
+            continue;
+        if ( pBuffer[0] == 'p' )
+        {
+            assert( p == NULL );
+            nClausesA = 0;
+            RetValue = sscanf( pBuffer + 1, "%d %d %d %d", &nVars, &nClauses, &nRoots, &nClausesA );
+            if ( RetValue != 3 && RetValue != 4 )
+            {
+                printf( "Wrong input file format.\n" );
+            }
+            p = Pr_ManAlloc( nVars );
+            pArray = (int *)malloc( sizeof(int) * (nVars + 10) );
+            continue;
+        }
+        // skip empty lines
+        for ( pCur = pBuffer; *pCur; pCur++ )
+            if ( !(*pCur == ' ' || *pCur == '\t' || *pCur == '\r' || *pCur == '\n') )
+                break;
+        if ( *pCur == 0 )
+            continue;
+        // scan the numbers from file
+        nNumbers = 0;
+        pCur = pBuffer;
+        while ( *pCur )
+        {
+            // skip spaces
+            for ( ; *pCur && *pCur == ' '; pCur++ );
+            // read next number
+            Temp = 0;
+            sscanf( pCur, "%d", &Temp );
+            if ( Temp == 0 )
+                break;
+            pArray[ nNumbers++ ] = lit_read( Temp );
+            // skip non-spaces
+            for ( ; *pCur && *pCur != ' '; pCur++ );
+        }
+        // add the clause
+        if ( !Pr_ManAddClause( p, pArray, pArray + nNumbers, Counter < nRoots, Counter < nClausesA ) )
+        {
+            printf( "Bad clause number %d.\n", Counter );
+            return NULL;
+        }
+        // count the clauses
+        Counter++;
+    }
+    // check the number of clauses
+    if ( Counter != nClauses )
+        printf( "Expected %d clauses but read %d.\n", nClauses, Counter );
+
+    // finish
+    if ( pArray ) free( pArray );
+    if ( pBuffer ) free( pBuffer );
+    fclose( pFile );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+int Pr_ManProofCount_rec( Pr_Cls_t * pClause )
+{
+    Pr_Cls_t * pNext;
+    int i, Counter;    
+    if ( pClause->fRoot )
+        return 0;
+    if ( pClause->fVisit )
+        return 0;
+    pClause->fVisit = 1;
+    // count the number of visited clauses
+    Counter = 1;
+    Vec_PtrForEachEntry( pClause->pAntis, pNext, i )
+        Counter += Pr_ManProofCount_rec( pNext );
+    return Counter;
+}
+*/
+
+/**Function*************************************************************
+
+  Synopsis    [Records the proof.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Pr_ManProofTest( char * pFileName )
+{
+    Pr_Man_t * p;
+    int clk, clkTotal = clock();
+
+clk = clock();
+    p = Pr_ManProofRead( pFileName );
+p->timeRead = clock() - clk;
+    if ( p == NULL )
+        return 0;
+
+    Pr_ManProofWrite( p );
+
+    // print stats
+/*
+    nUsed = Pr_ManProofCount_rec( p->pEmpty );
+    printf( "Roots = %d. Learned = %d. Total = %d. Steps = %d.  Ave = %.2f.  Used = %d. Ratio = %.2f. \n", 
+        p->nRoots, p->nClauses-p->nRoots, p->nClauses, p->Counter,  
+        1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots),
+        nUsed, 1.0*nUsed/(p->nClauses-p->nRoots)  );
+*/
+    printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f Mb\n", 
+        p->nVars, p->nRoots, p->nClauses-p->nRoots, p->Counter,  
+        1.0*(p->Counter-p->nRoots)/(p->nClauses-p->nRoots), 
+        1.0*Pr_ManMemoryReport(p)/(1<<20) );
+
+p->timeTotal = clock() - clkTotal;
+    Pr_ManFree( p );
+    return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/proof/pr.h b/src/sat/proof/pr.h
new file mode 100644
index 00000000..1e71a2d3
--- /dev/null
+++ b/src/sat/proof/pr.h
@@ -0,0 +1,65 @@
+/**CFile****************************************************************
+
+  FileName    [pr.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Proof recording.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: pr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __PR_H__
+#define __PR_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Pr_Man_t_ Pr_Man_t;
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== pr.c ==========================================================*/
+ 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/sat/proof/stats.txt b/src/sat/proof/stats.txt
new file mode 100644
index 00000000..470b1630
--- /dev/null
+++ b/src/sat/proof/stats.txt
@@ -0,0 +1,66 @@
+UC Berkeley, ABC 1.01 (compiled Jan 20 2007 16:47:34)
+abc.rc: No such file or directory
+Loaded "abc.rc" from the parent directory.
+abc 01> test
+Found last conflict after adding unit clause number 10229!
+Roots = 7184. Learned = 3047. Total = 10231. Steps = 196361.  Ave = 62.09.  Used = 2224. Ratio = 0.73.
+Runtime stats:
+Reading  =   0.03 sec
+BCP      =   0.32 sec
+Trace    =   0.06 sec
+TOTAL    =   0.43 sec
+abc 01> test
+Found last conflict after adding unit clause number 7676!
+Roots = 6605. Learned = 1073. Total = 7678. Steps = 52402.  Ave = 42.68.  Used = 1011. Ratio = 0.94.
+Runtime stats:
+Reading  =   0.01 sec
+BCP      =   0.02 sec
+Trace    =   0.02 sec
+TOTAL    =   0.06 sec
+abc 01> test
+Found last conflict after adding unit clause number 37868!
+Roots = 15443. Learned = 22427. Total = 37870. Steps = 2365472.  Ave = 104.79.  Used = 19763. Ratio = 0.88.
+Runtime stats:
+Reading  =   0.20 sec
+BCP      =  14.67 sec
+Trace    =   0.56 sec
+TOTAL    =  15.74 sec
+abc 01>
+
+
+abc 05> wb ibm_bmc/len25u_renc.blif
+abc 05> ps
+(no name)    : i/o =  348/   1  lat =    0  nd =  3648  bdd  = 15522  lev = 246
+abc 05> sat -v
+==================================[MINISAT]===================================
+| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
+|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
+==============================================================================
+|         0 |   17413    54996 |    5804       0        0     0.0 |  0.000 % |
+|       100 |   17413    54996 |    6384     100      606     6.1 |  0.417 % |
+|       250 |   17413    54996 |    7023     250     1586     6.3 |  0.417 % |
+|       476 |   17413    54996 |    7725     476     3288     6.9 |  0.417 % |
+|       813 |   17413    54996 |    8498     813     7586     9.3 |  0.417 % |
+|      1319 |   17403    54970 |    9347    1318    14848    11.3 |  0.442 % |
+|      2078 |   17403    54970 |   10282    2076    40186    19.4 |  0.466 % |
+|      3217 |   17397    54948 |   11310    3208    99402    31.0 |  0.466 % |
+|      4926 |   17392    54930 |   12441    4911   131848    26.8 |  0.491 % |
+|      7489 |   17392    54930 |   13686    7474   204217    27.3 |  0.491 % |
+|     11336 |   17357    54829 |   15054   11310   332863    29.4 |  0.638 % |
+|     17103 |   17346    54794 |   16559    9130   203029    22.2 |  0.687 % |
+|     25752 |   17288    54606 |   18215    9083   176982    19.5 |  0.834 % |
+|     38727 |   17266    54536 |   20037   12674   278949    22.0 |  0.883 % |
+|     58188 |   17240    54453 |   22041   11905   255255    21.4 |  0.957 % |
+==============================================================================
+Start =   15. Conf =  79435. Dec = 130967. Prop = 24083434. Insp = 136774586.
+Total runtime =   18.66 sec.  Var select =    0.00 sec.  Var update =    0.00 sec.
+UNSATISFIABLE  Time =  18.69 sec
+abc 05>
+abc 05> test
+Found last conflict after adding unit clause number 96902!
+Roots = 17469. Learned = 79435. Total = 96904. Steps = 9700042.  Ave = 121.89.  Used = 57072. Ratio = 0.72.
+Runtime stats:
+Reading  =   1.26 sec
+BCP      = 204.99 sec
+Trace    =   2.85 sec
+TOTAL    = 209.85 sec
\ No newline at end of file