Added learned clause recycling to the SAT solver (may impact bmc2, bmc3, dsat, etc).

1 files changed, 401 insertions, 0 deletions

diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h
new file mode 100644
index 00000000..8b1a1294
--- /dev/null
+++ b/src/sat/bsat/satClause.h
@@ -0,0 +1,401 @@
+/**CFile****************************************************************
+
+  FileName    [satMem.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT solver.]
+
+  Synopsis    [Memory management.]
+
+  Author      [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 1, 2004.]
+
+  Revision    [$Id: satMem.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__sat__bsat__satMem_h
+#define ABC__sat__bsat__satMem_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "misc/util/abc_global.h"
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+ 
+//=================================================================================================
+// Clause datatype + minor functions:
+
+typedef int    lit;
+typedef int    cla;
+
+typedef struct clause_t clause;
+struct clause_t
+{
+    unsigned   lrn   :   1;
+    unsigned   mark  :   1;
+    unsigned   partA :   1;
+    unsigned   lbd   :   8;
+    unsigned   size  :  21;
+    lit        lits[0];
+};
+
+// learned clauses have "hidden" literal (c->lits[c->size]) to store clause ID
+
+// data-structure for logging entries
+// memory is allocated in 2^nPageSize word-sized pages
+// the first 'word' of each page are stores the word limit
+
+// although clause memory pieces are aligned to 64-bit words
+// the integer clause handles are in terms of 32-bit unsigneds
+// allowing for the first bit to be used for labeling 2-lit clauses
+
+
+typedef struct Sat_Mem_t_ Sat_Mem_t;
+struct Sat_Mem_t_
+{
+    int                 nEntries[2];  // entry count
+    int                 BookMarkH[2]; // bookmarks for handles
+    int                 BookMarkE[2]; // bookmarks for entries
+    int                 iPage[2];     // current memory page
+    int                 nPageSize;    // page log size in terms of ints
+    unsigned            uPageMask;    // page mask
+    unsigned            uLearnedMask; // learned mask
+    int                 nPagesAlloc;  // page count allocated
+    int **              pPages;       // page pointers
+}; 
+
+static inline int       Sat_MemLimit( int * p )                      { return p[0];                                 }
+static inline int       Sat_MemIncLimit( int * p, int nInts )        { return p[0] += nInts;                        }
+static inline void      Sat_MemWriteLimit( int * p, int nInts )      { p[0] = nInts;                                }
+
+static inline int       Sat_MemHandPage( Sat_Mem_t * p, cla h )      { return h >> p->nPageSize;                    }
+static inline int       Sat_MemHandShift( Sat_Mem_t * p, cla h )     { return h & p->uPageMask;                     }
+
+static inline int       Sat_MemIntSize( int size, int lrn )          { return (size + 2 + lrn) & ~01;               }
+static inline int       Sat_MemClauseSize( clause * p )              { return Sat_MemIntSize(p->size, p->lrn);      }
+
+//static inline clause *  Sat_MemClause( Sat_Mem_t * p, int i, int k ) { assert(i <= p->iPage[i&1] && k <= Sat_MemLimit(p->pPages[i]));  return (clause *)(p->pPages[i] + k ); }
+static inline clause *  Sat_MemClause( Sat_Mem_t * p, int i, int k ) { return (clause *)(p->pPages[i] + k);         }
+//static inline clause *  Sat_MemClauseHand( Sat_Mem_t * p, cla h )    { assert(Sat_MemHandPage(p, h) <= p->iPage[(h & p->uLearnedMask) > 0]); assert(Sat_MemHandShift(p, h) >= 2 && Sat_MemHandShift(p, h) < (int)p->uLearnedMask); return Sat_MemClause( p, Sat_MemHandPage(p, h), Sat_MemHandShift(p, h) );     }
+static inline clause *  Sat_MemClauseHand( Sat_Mem_t * p, cla h )    { return Sat_MemClause( p, Sat_MemHandPage(p, h), Sat_MemHandShift(p, h) );                             }
+static inline int       Sat_MemEntryNum( Sat_Mem_t * p, int lrn )    { return p->nEntries[lrn];                                                                              }
+
+static inline cla       Sat_MemHand( Sat_Mem_t * p, int i, int k )   { return (i << p->nPageSize) | k;                                                                       }
+static inline cla       Sat_MemHandCurrent( Sat_Mem_t * p, int lrn ) { return (p->iPage[lrn] << p->nPageSize) | Sat_MemLimit( p->pPages[p->iPage[lrn]] );                    }
+
+static inline double    Sat_MemMemoryHand( Sat_Mem_t * p, cla h )    { return 1.0 * ((Sat_MemHandPage(p, h) + 2)/2 * (1 << (p->nPageSize+2)) + Sat_MemHandShift(p, h) * 4);  }
+static inline double    Sat_MemMemoryUsed( Sat_Mem_t * p, int lrn )  { return Sat_MemMemoryHand( p, Sat_MemHandCurrent(p, lrn) );                                            }
+static inline double    Sat_MemMemoryAllUsed( Sat_Mem_t * p )        { return Sat_MemMemoryUsed( p, 0 ) + Sat_MemMemoryUsed( p, 1 );                                         }
+static inline double    Sat_MemMemoryAll( Sat_Mem_t * p )            { return 1.0 * (p->iPage[0] + p->iPage[1] + 2) * (1 << (p->nPageSize+2));                               }
+
+// p is memory storage
+// c is clause pointer
+// i is page number
+// k is page offset
+
+#define Sat_MemForEachClause( p, c, i, k )      \
+    for ( i = 0; i <= p->iPage[0]; i += 2 )     \
+        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )
+
+#define Sat_MemForEachLearned( p, c, i, k )     \
+    for ( i = 1; i <= p->iPage[1]; i += 2 )     \
+        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )
+
+////////////////////////////////////////////////////////////////////////
+///                       GLOBAL VARIABLES                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFINITIONS                          ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int      clause_from_lit( lit l )                     { return l + l + 1;                            }
+static inline int      clause_is_lit( cla h )                       { return (h & 1);                              }
+static inline lit      clause_read_lit( cla h )                     { return (lit)(h >> 1);                        }
+
+static inline int      clause_learnt_h( Sat_Mem_t * p, cla h )      { return (h & p->uLearnedMask) > 0;            }
+static inline int      clause_learnt( clause * c )                  { return c->lrn;                               }
+static inline int      clause_id( clause * c )                      { assert(c->lrn); return c->lits[c->size];     }
+static inline int      clause_size( clause * c )                    { return c->size;                              }
+static inline lit *    clause_begin( clause * c )                   { return c->lits;                              }
+static inline lit *    clause_end( clause * c )                     { return c->lits + c->size;                    }
+static inline void     clause_print( clause * c )               
+{ 
+    int i;
+    printf( "{ " );
+    for ( i = 0; i < clause_size(c); i++ )
+        printf( "%d ", (clause_begin(c)[i] & 1)? -(clause_begin(c)[i] >> 1) : clause_begin(c)[i] >> 1 );
+    printf( "}\n" );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DECLARATIONS                        ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocating vector.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Sat_MemAlloc_( Sat_Mem_t * p, int nPageSize )
+{
+    assert( nPageSize > 8 && nPageSize < 32 );
+    memset( p, 0, sizeof(Sat_Mem_t) );
+    p->nPageSize    = nPageSize;
+    p->uLearnedMask = (unsigned)(1 << nPageSize);
+    p->uPageMask    = (unsigned)((1 << nPageSize) - 1);
+    p->nPagesAlloc  = 256;
+    p->pPages       = ABC_CALLOC( int *, p->nPagesAlloc );
+    p->pPages[0]    = ABC_ALLOC( int, (1 << p->nPageSize) );
+    p->pPages[1]    = ABC_ALLOC( int, (1 << p->nPageSize) );
+    p->iPage[0]     = 0;
+    p->iPage[1]     = 1;
+    Sat_MemWriteLimit( p->pPages[0], 2 );
+    Sat_MemWriteLimit( p->pPages[1], 2 );
+}
+static inline Sat_Mem_t * Sat_MemAlloc( int nPageSize )
+{
+    Sat_Mem_t * p;
+    p = ABC_CALLOC( Sat_Mem_t, 1 );
+    Sat_MemAlloc_( p, nPageSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resetting vector.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Sat_MemRestart( Sat_Mem_t * p )
+{
+    p->nEntries[0]  = 0;
+    p->nEntries[1]  = 0;
+    p->iPage[0]     = 0;
+    p->iPage[1]     = 1;
+    Sat_MemWriteLimit( p->pPages[0], 2 );
+    Sat_MemWriteLimit( p->pPages[1], 2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the bookmark.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Sat_MemBookMark( Sat_Mem_t * p )
+{
+    p->BookMarkH[0] = Sat_MemHandCurrent( p, 0 );
+    p->BookMarkH[1] = Sat_MemHandCurrent( p, 1 );
+    p->BookMarkE[0] = p->nEntries[0];
+    p->BookMarkE[1] = p->nEntries[1];
+}
+static inline void Sat_MemRollBack( Sat_Mem_t * p )
+{
+    p->nEntries[0]  = p->BookMarkE[0];
+    p->nEntries[1]  = p->BookMarkE[1];
+    p->iPage[0]     = Sat_MemHandPage( p, p->BookMarkH[0] );
+    p->iPage[1]     = Sat_MemHandPage( p, p->BookMarkH[1] );
+    Sat_MemWriteLimit( p->pPages[0], Sat_MemHandShift( p, p->BookMarkH[0] ) );
+    Sat_MemWriteLimit( p->pPages[1], Sat_MemHandShift( p, p->BookMarkH[1] ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Freeing vector.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Sat_MemFree_( Sat_Mem_t * p )
+{
+    int i;
+    for ( i = 0; i < p->nPagesAlloc; i++ )
+        ABC_FREE( p->pPages[i] );
+    ABC_FREE( p->pPages );
+}
+static inline void Sat_MemFree( Sat_Mem_t * p )
+{
+    Sat_MemFree_( p );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates new clause.]
+
+  Description [The resulting clause is fully initialized.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Sat_MemAppend( Sat_Mem_t * p, int * pArray, int nSize, int lrn )
+{
+    clause * c;
+    int * pPage = p->pPages[p->iPage[lrn]];
+    int nInts = Sat_MemIntSize( nSize, lrn );
+    assert( nInts + 3 < (1 << p->nPageSize) );
+    // need two extra at the begining of the page and one extra in the end
+    if ( Sat_MemLimit(pPage) + nInts >= (1 << p->nPageSize) )
+    {
+        p->iPage[lrn] += 2;
+        if ( p->iPage[lrn] >= p->nPagesAlloc )
+        {
+            p->pPages = ABC_REALLOC( int *, p->pPages, p->nPagesAlloc * 2 );
+            memset( p->pPages + p->nPagesAlloc, 0, sizeof(int *) * p->nPagesAlloc );
+            p->nPagesAlloc *= 2;
+        }
+        if ( p->pPages[p->iPage[lrn]] == NULL )
+            p->pPages[p->iPage[lrn]] = ABC_ALLOC( int, (1 << p->nPageSize) );
+        pPage = p->pPages[p->iPage[lrn]];
+        Sat_MemWriteLimit( pPage, 2 );
+    }
+    pPage[Sat_MemLimit(pPage)] = 0;
+    c = (clause *)(pPage + Sat_MemLimit(pPage));
+    c->size = nSize;
+    c->lrn = lrn;
+    if ( pArray )
+        memcpy( c->lits, pArray, sizeof(int) * nSize );
+    if ( lrn )
+        c->lits[c->size] = p->nEntries[1];
+    p->nEntries[lrn]++;
+    Sat_MemIncLimit( pPage, nInts );
+    return Sat_MemHandCurrent(p, lrn) - nInts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Shrinking vector size.]
+
+  Description []
+
+  SideEffects [This procedure does not update the number of entries.]
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Sat_MemShrink( Sat_Mem_t * p, int h, int lrn )
+{
+    assert( clause_learnt_h(p, h) == lrn );
+    assert( h && h <= Sat_MemHandCurrent(p, lrn) );
+    p->iPage[lrn] = Sat_MemHandPage(p, h);
+    Sat_MemWriteLimit( p->pPages[p->iPage[lrn]], Sat_MemHandShift(p, h) );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Compacts learned clauses by removing marked entries.]
+
+  Description [Returns the number of remaining entries.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Sat_MemCompactLearned( Sat_Mem_t * p, int fDoMove )
+{
+    clause * c;
+    int i, k, iNew = 1, kNew = 2, nInts, Counter = 0;
+    // iterate through the learned clauses
+    Sat_MemForEachLearned( p, c, i, k )
+    {
+        assert( c->lrn );
+        // skip marked entry
+        if ( c->mark )
+            continue;
+        // compute entry size
+        nInts = Sat_MemClauseSize(c);
+        assert( !(nInts & 1) );
+        // check if we need to scroll to the next page
+        if ( kNew + nInts >= (1 << p->nPageSize) )
+        {
+            // set the limit of the current page
+            if ( fDoMove )
+                Sat_MemWriteLimit( p->pPages[iNew], kNew );
+            // move writing position to the new page
+            iNew += 2;
+            kNew = 2;
+        }
+        if ( fDoMove )
+        {
+            // make sure the result is the same as previous dry run
+            assert( c->lits[c->size] == Sat_MemHand(p, iNew, kNew) );
+            // only copy the clause if it has changed
+            if ( i != iNew || k != kNew )
+            {
+                memmove( p->pPages[iNew] + kNew, c, sizeof(int) * nInts );
+//                c = Sat_MemClause( p, iNew, kNew ); // assersions do not hold during dry run
+                c = (clause *)(p->pPages[iNew] + kNew);
+                assert( nInts == Sat_MemClauseSize(c) );
+            }
+            // set the new ID value
+            c->lits[c->size] = Counter;
+        }
+        else // remember the address of the clause in the new location
+            c->lits[c->size] = Sat_MemHand(p, iNew, kNew);
+        // update writing position
+        kNew += nInts;
+        assert( iNew <= i && kNew < (1 << p->nPageSize) );
+        // update counter
+        Counter++;
+    }
+    if ( fDoMove )
+    {
+        // update the page count
+        p->iPage[1] = iNew;
+        // set the limit of the last page
+        Sat_MemWriteLimit( p->pPages[iNew], kNew );
+        // update the counter
+        p->nEntries[1] = Counter;
+    }
+    return Counter;
+}
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+