satClause.h File Reference

#include "misc/util/abc_global.h"

Go to the source code of this file.

Data Structures
struct	clause_t
struct	Sat_Mem_t_

Macros
#define	LEARNT_MAX_START_DEFAULT   10000
	INCLUDES ///. More...
#define	LEARNT_MAX_INCRE_DEFAULT   1000
#define	LEARNT_MAX_RATIO_DEFAULT   50
#define	Sat_MemForEachClause(p, c, i, k)
#define	Sat_MemForEachClause2(p, c, i, k)
#define	Sat_MemForEachLearned(p, c, i, k)

Typedefs
typedef struct clause_t	clause
	STRUCTURE DEFINITIONS ///. More...
typedef struct Sat_Mem_t_	Sat_Mem_t

Functions
static int	Sat_MemLimit (int *p)
static int	Sat_MemIncLimit (int *p, int nInts)
static void	Sat_MemWriteLimit (int *p, int nInts)
static int	Sat_MemHandPage (Sat_Mem_t *p, cla h)
static int	Sat_MemHandShift (Sat_Mem_t *p, cla h)
static int	Sat_MemIntSize (int size, int lrn)
static int	Sat_MemClauseSize (clause *p)
static int	Sat_MemClauseSize2 (clause *p)
static clause *	Sat_MemClause (Sat_Mem_t *p, int i, int k)
static clause *	Sat_MemClauseHand (Sat_Mem_t *p, cla h)
static int	Sat_MemEntryNum (Sat_Mem_t *p, int lrn)
static cla	Sat_MemHand (Sat_Mem_t *p, int i, int k)
static cla	Sat_MemHandCurrent (Sat_Mem_t *p, int lrn)
static int	Sat_MemClauseUsed (Sat_Mem_t *p, cla h)
static double	Sat_MemMemoryHand (Sat_Mem_t *p, cla h)
static double	Sat_MemMemoryUsed (Sat_Mem_t *p, int lrn)
static double	Sat_MemMemoryAllUsed (Sat_Mem_t *p)
static double	Sat_MemMemoryAll (Sat_Mem_t *p)
static int	clause_from_lit (lit l)
	GLOBAL VARIABLES ///. More...
static int	clause_is_lit (cla h)
static lit	clause_read_lit (cla h)
static int	clause_learnt_h (Sat_Mem_t *p, cla h)
static int	clause_learnt (clause *c)
static int	clause_id (clause *c)
static void	clause_set_id (clause *c, int id)
static int	clause_size (clause *c)
static lit *	clause_begin (clause *c)
static lit *	clause_end (clause *c)
static void	clause_print (clause *c)
static int	Sat_MemCountL (Sat_Mem_t *p)
	FUNCTION DECLARATIONS ///. More...
static void	Sat_MemAlloc_ (Sat_Mem_t *p, int nPageSize)
static Sat_Mem_t *	Sat_MemAlloc (int nPageSize)
static void	Sat_MemRestart (Sat_Mem_t *p)
static void	Sat_MemBookMark (Sat_Mem_t *p)
static void	Sat_MemRollBack (Sat_Mem_t *p)
static void	Sat_MemFree_ (Sat_Mem_t *p)
static void	Sat_MemFree (Sat_Mem_t *p)
static int	Sat_MemAppend (Sat_Mem_t *p, int *pArray, int nSize, int lrn, int fPlus1)
static void	Sat_MemShrink (Sat_Mem_t *p, int h, int lrn)
static int	Sat_MemCompactLearned (Sat_Mem_t *p, int fDoMove)

Macro Definition Documentation

#define LEARNT_MAX_INCRE_DEFAULT   1000

Definition at line 38 of file satClause.h.

#define LEARNT_MAX_RATIO_DEFAULT   50

Definition at line 39 of file satClause.h.

#define LEARNT_MAX_START_DEFAULT   10000

INCLUDES ///.

CFile****************************************************************

FileName [satMem.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT solver.]

Synopsis [Memory management.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

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

]PARAMETERS ///

Definition at line 37 of file satClause.h.

#define Sat_MemForEachClause	(		p,
			c,
			i,
			k
	)

Value:

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) ) if ( i == 0 && k == 2 ) {} else

Definition at line 117 of file satClause.h.

#define Sat_MemForEachClause2	(		p,
			c,
			i,
			k
	)

Value:

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_MemClauseSize2(c) ) if ( i == 0 && k == 2 ) {} else

Definition at line 122 of file satClause.h.

#define Sat_MemForEachLearned	(		p,
			c,
			i,
			k
	)

Value:

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) )

Definition at line 126 of file satClause.h.

Typedef Documentation

typedef struct clause_t clause

STRUCTURE DEFINITIONS ///.

Definition at line 48 of file satClause.h.

typedef struct Sat_Mem_t_ Sat_Mem_t

Definition at line 70 of file satClause.h.

Function Documentation

static lit* clause_begin ( clause *  c )

inlinestatic

Definition at line 147 of file satClause.h.

{ return c->lits;                              }

static lit* clause_end ( clause *  c )

inlinestatic

Definition at line 148 of file satClause.h.

{ return c->lits + c->size;                    }

static int clause_from_lit ( lit  l )

inlinestatic

GLOBAL VARIABLES ///.

MACRO DEFINITIONS ///

Definition at line 138 of file satClause.h.

{ return l + l + 1;                            }

static int clause_id ( clause *  c )

inlinestatic

Definition at line 144 of file satClause.h.

{ return c->lits[c->size];                     }

static int clause_is_lit ( cla  h )

inlinestatic

Definition at line 139 of file satClause.h.

{ return (h & 1);                              }

static int clause_learnt ( clause *  c )

inlinestatic

Definition at line 143 of file satClause.h.

{ return c->lrn;                               }

static int clause_learnt_h ( Sat_Mem_t *  p, cla  h  )

inlinestatic

Definition at line 142 of file satClause.h.

{ return (h & p->uLearnedMask) > 0;            }

static void clause_print ( clause *  c )

inlinestatic

Definition at line 149 of file satClause.h.

{ 
    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" );
}

static lit clause_read_lit ( cla  h )

inlinestatic

Definition at line 140 of file satClause.h.

{ return (lit)(h >> 1);                        }

static void clause_set_id ( clause *  c, int  id  )

inlinestatic

Definition at line 145 of file satClause.h.

{ c->lits[c->size] = id;                       }

static int clause_size ( clause *  c )

inlinestatic

Definition at line 146 of file satClause.h.

{ return c->size;                              }

static Sat_Mem_t* Sat_MemAlloc ( int  nPageSize )

inlinestatic

Definition at line 209 of file satClause.h.

{
    Sat_Mem_t * p;
    p = ABC_CALLOC( Sat_Mem_t, 1 );
    Sat_MemAlloc_( p, nPageSize );
    return p;
}

static void Sat_MemAlloc_ ( Sat_Mem_t *  p, int  nPageSize  )

inlinestatic

Function*************************************************************

Synopsis [Allocating vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 193 of file satClause.h.

{
    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 int Sat_MemAppend ( Sat_Mem_t *  p, int *  pArray, int  nSize, int  lrn, int  fPlus1  )

inlinestatic

Function*************************************************************

Synopsis [Creates new clause.]

Description [The resulting clause is fully initialized.]

SideEffects []

SeeAlso []

Definition at line 301 of file satClause.h.

{
    clause * c;
    int * pPage = p->pPages[p->iPage[lrn]];
    int nInts = Sat_MemIntSize( nSize, lrn | fPlus1 );
    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 + 2 >= (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 | fPlus1 )
        c->lits[c->size] = p->nEntries[lrn];
    p->nEntries[lrn]++;
    Sat_MemIncLimit( pPage, nInts );
    return Sat_MemHandCurrent(p, lrn) - nInts;
}

static void Sat_MemBookMark ( Sat_Mem_t *  p )

inlinestatic

Function*************************************************************

Synopsis [Sets the bookmark.]

Description []

SideEffects []

SeeAlso []

Definition at line 249 of file satClause.h.

{
    p->BookMarkE[0] = p->nEntries[0];
    p->BookMarkE[1] = p->nEntries[1];
    p->BookMarkH[0] = Sat_MemHandCurrent( p, 0 );
    p->BookMarkH[1] = Sat_MemHandCurrent( p, 1 );
}

static clause* Sat_MemClause ( Sat_Mem_t *  p, int  i, int  k  )

inlinestatic

Definition at line 96 of file satClause.h.

{ assert( k ); return (clause *)(p->pPages[i] + k);         }

static clause* Sat_MemClauseHand ( Sat_Mem_t *  p, cla  h  )

inlinestatic

Definition at line 98 of file satClause.h.

{ return h ? Sat_MemClause( p, Sat_MemHandPage(p, h), Sat_MemHandShift(p, h) ) : NULL;                  }

static int Sat_MemClauseSize ( clause *  p )

inlinestatic

Definition at line 92 of file satClause.h.

{ return Sat_MemIntSize(p->size, p->lrn);      }

static int Sat_MemClauseSize2 ( clause *  p )

inlinestatic

Definition at line 93 of file satClause.h.

{ return Sat_MemIntSize(p->size, 1);           }

static int Sat_MemClauseUsed ( Sat_Mem_t *  p, cla  h  )

inlinestatic

Definition at line 104 of file satClause.h.

{ return h < p->BookMarkH[(h & p->uLearnedMask) > 0];                                                   }

static int Sat_MemCompactLearned ( Sat_Mem_t *  p, int  fDoMove  )

inlinestatic

Function*************************************************************

Synopsis [Compacts learned clauses by removing marked entries.]

Description [Returns the number of remaining entries.]

SideEffects []

SeeAlso []

Definition at line 366 of file satClause.h.

{
    clause * c, * cPivot = NULL;
    int i, k, iNew = 1, kNew = 2, nInts, fStartLooking, Counter = 0;
    int hLimit = Sat_MemHandCurrent(p, 1);
    if ( hLimit == Sat_MemHand(p, 1, 2) )
        return 0;
    if ( fDoMove && p->BookMarkH[1] )
    {
        // move the pivot
        assert( p->BookMarkH[1] >= Sat_MemHand(p, 1, 2) && p->BookMarkH[1] <= hLimit );
        // get the pivot and remember it may be pointed offlimit
        cPivot = Sat_MemClauseHand( p, p->BookMarkH[1] );
        if ( p->BookMarkH[1] < hLimit && !cPivot->mark )
        {
            p->BookMarkH[1] = cPivot->lits[cPivot->size];
            cPivot = NULL;
        }
        // else find the next used clause after cPivot
    }
    // iterate through the learned clauses
    fStartLooking = 0;
    Sat_MemForEachLearned( p, c, i, k )
    {
        assert( c->lrn );
        // skip marked entry
        if ( c->mark )
        {
            // if pivot is a marked clause, start looking for the next non-marked one
            if ( cPivot && cPivot == c )
            {
                fStartLooking = 1;
                cPivot = NULL;
            }
            continue;
        }
        // if we started looking before, we found it!
        if ( fStartLooking )
        {
            fStartLooking = 0;
            p->BookMarkH[1] = c->lits[c->size];
        }
        // 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 counter
        p->nEntries[1] = Counter;
        // update the page count
        p->iPage[1] = iNew;
        // set the limit of the last page
        Sat_MemWriteLimit( p->pPages[iNew], kNew );
        // check if the pivot need to be updated
        if ( p->BookMarkH[1] )
        {
            if ( cPivot )
            {
                p->BookMarkH[1] = Sat_MemHandCurrent(p, 1);
                p->BookMarkE[1] = p->nEntries[1];
            }
            else
                p->BookMarkE[1] = clause_id(Sat_MemClauseHand( p, p->BookMarkH[1] ));
        }

    }
    return Counter;
}

static int Sat_MemCountL ( Sat_Mem_t *  p )

inlinestatic

FUNCTION DECLARATIONS ///.

Function*************************************************************

Synopsis [Allocating vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file satClause.h.

{
    clause * c;
    int i, k, Count = 0;
    Sat_MemForEachLearned( p, c, i, k )
        Count++;
    return Count;
}

static int Sat_MemEntryNum ( Sat_Mem_t *  p, int  lrn  )

inlinestatic

Definition at line 99 of file satClause.h.

{ return p->nEntries[lrn];                                                                              }

static void Sat_MemFree ( Sat_Mem_t *  p )

inlinestatic

Definition at line 284 of file satClause.h.

{
    Sat_MemFree_( p );
    ABC_FREE( p );
}

static void Sat_MemFree_ ( Sat_Mem_t *  p )

inlinestatic

Function*************************************************************

Synopsis [Freeing vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 277 of file satClause.h.

{
    int i;
    for ( i = 0; i < p->nPagesAlloc; i++ )
        ABC_FREE( p->pPages[i] );
    ABC_FREE( p->pPages );
}

static cla Sat_MemHand ( Sat_Mem_t *  p, int  i, int  k  )

inlinestatic

Definition at line 101 of file satClause.h.

{ return (i << p->nPageSize) | k;                                                                       }

static cla Sat_MemHandCurrent ( Sat_Mem_t *  p, int  lrn  )

inlinestatic

Definition at line 102 of file satClause.h.

{ return (p->iPage[lrn] << p->nPageSize) | Sat_MemLimit( p->pPages[p->iPage[lrn]] );                    }

static int Sat_MemHandPage ( Sat_Mem_t *  p, cla  h  )

inlinestatic

Definition at line 88 of file satClause.h.

{ return h >> p->nPageSize;                    }

static int Sat_MemHandShift ( Sat_Mem_t *  p, cla  h  )

inlinestatic

Definition at line 89 of file satClause.h.

{ return h & p->uPageMask;                     }

static int Sat_MemIncLimit ( int *  p, int  nInts  )

inlinestatic

Definition at line 85 of file satClause.h.

{ return p[0] += nInts;                        }

static int Sat_MemIntSize ( int  size, int  lrn  )

inlinestatic

Definition at line 91 of file satClause.h.

{ return (size + 2 + lrn) & ~01;               }

static int Sat_MemLimit ( int *  p )

inlinestatic

Definition at line 84 of file satClause.h.

{ return p[0];                                 }

static double Sat_MemMemoryAll ( Sat_Mem_t *  p )

inlinestatic

Definition at line 109 of file satClause.h.

{ return 1.0 * (p->iPage[0] + p->iPage[1] + 2) * (1 << (p->nPageSize+2));                               }

static double Sat_MemMemoryAllUsed ( Sat_Mem_t *  p )

inlinestatic

Definition at line 108 of file satClause.h.

{ return Sat_MemMemoryUsed( p, 0 ) + Sat_MemMemoryUsed( p, 1 );                                         }

static double Sat_MemMemoryHand ( Sat_Mem_t *  p, cla  h  )

inlinestatic

Definition at line 106 of file satClause.h.

{ return 1.0 * ((Sat_MemHandPage(p, h) + 2)/2 * (1 << (p->nPageSize+2)) + Sat_MemHandShift(p, h) * 4);  }

static double Sat_MemMemoryUsed ( Sat_Mem_t *  p, int  lrn  )

inlinestatic

Definition at line 107 of file satClause.h.

{ return Sat_MemMemoryHand( p, Sat_MemHandCurrent(p, lrn) );                                            }

static void Sat_MemRestart ( Sat_Mem_t *  p )

inlinestatic

Function*************************************************************

Synopsis [Resetting vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 228 of file satClause.h.

{
    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 );
}

static void Sat_MemRollBack ( Sat_Mem_t *  p )

inlinestatic

Definition at line 256 of file satClause.h.

{
    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[p->iPage[0]], Sat_MemHandShift( p, p->BookMarkH[0] ) );
    Sat_MemWriteLimit( p->pPages[p->iPage[1]], Sat_MemHandShift( p, p->BookMarkH[1] ) );
}

static void Sat_MemShrink ( Sat_Mem_t *  p, int  h, int  lrn  )

inlinestatic

Function*************************************************************

Synopsis [Shrinking vector size.]

Description []

SideEffects [This procedure does not update the number of entries.]

SeeAlso []

Definition at line 346 of file satClause.h.

{
    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) );
}

static void Sat_MemWriteLimit ( int *  p, int  nInts  )

inlinestatic

Definition at line 86 of file satClause.h.

{ p[0] = nInts;                                }