src/sat/bsat/satStore.h File Reference

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures
struct	Sto_Cls_t_
struct	Sto_Man_t_
Defines
#define	STO_MAX(a, b)   ((a) > (b) ? (a) : (b))
#define	Sto_ManForEachClause(p, pCls)   for( pCls = p->pHead; pCls; pCls = pCls->pNext )
#define	Sto_ManForEachClauseRoot(p, pCls)   for( pCls = p->pHead; pCls && pCls->fRoot; pCls = pCls->pNext )
Typedefs
typedef unsigned	lit
typedef struct Sto_Cls_t_	Sto_Cls_t
typedef struct Sto_Man_t_	Sto_Man_t
typedef struct Int_Man_t_	Int_Man_t
Functions
static lit	toLit (int v)
static lit	toLitCond (int v, int c)
static lit	lit_neg (lit l)
static int	lit_var (lit l)
static int	lit_sign (lit l)
static int	lit_print (lit l)
static lit	lit_read (int s)
static int	lit_check (lit l, int n)
Sto_Man_t *	Sto_ManAlloc ()
void	Sto_ManFree (Sto_Man_t *p)
int	Sto_ManAddClause (Sto_Man_t *p, lit *pBeg, lit *pEnd)
int	Sto_ManMemoryReport (Sto_Man_t *p)
void	Sto_ManMarkRoots (Sto_Man_t *p)
void	Sto_ManMarkClausesA (Sto_Man_t *p)
void	Sto_ManDumpClauses (Sto_Man_t *p, char *pFileName)
Sto_Man_t *	Sto_ManLoadClauses (char *pFileName)
Int_Man_t *	Int_ManAlloc (int nVarsAlloc)
void	Int_ManFree (Int_Man_t *p)
int	Int_ManInterpolate (Int_Man_t *p, Sto_Man_t *pCnf, int fVerbose, unsigned **ppResult)

---

Define Documentation

#define Sto_ManForEachClause	(	p,
		pCls		)	for( pCls = p->pHead; pCls; pCls = pCls->pNext )

Definition at line 101 of file satStore.h.

#define Sto_ManForEachClauseRoot	(	p,
		pCls		)	for( pCls = p->pHead; pCls && pCls->fRoot; pCls = pCls->pNext )

Definition at line 102 of file satStore.h.

#define STO_MAX	(	a,
		b		)	((a) > (b) ? (a) : (b))

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

]

Definition at line 43 of file satStore.h.

---

Typedef Documentation

typedef struct Int_Man_t_ Int_Man_t

Definition at line 123 of file satStore.h.

typedef unsigned lit

INCLUDES /// PARAMETERS /// BASIC TYPES ///

Definition at line 57 of file satStore.h.

typedef struct Sto_Cls_t_ Sto_Cls_t

Definition at line 59 of file satStore.h.

typedef struct Sto_Man_t_ Sto_Man_t

Definition at line 73 of file satStore.h.

---

Function Documentation

Int_Man_t* Int_ManAlloc

(

int

nVarsAlloc

)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Allocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file satInter.c.

{
    Int_Man_t * p;
    // allocate the manager
    p = (Int_Man_t *)malloc( sizeof(Int_Man_t) );
    memset( p, 0, sizeof(Int_Man_t) );
    // verification
    p->nResLitsAlloc = (1<<16);
    p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
    // parameters
    p->fProofWrite = 0;
    p->fProofVerif = 1;
    return p;    
}

void Int_ManFree

(

Int_Man_t *

p

)

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

Synopsis [Deallocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 244 of file satInter.c.

{
/*
    printf( "Runtime stats:\n" );
PRT( "BCP     ", p->timeBcp   );
PRT( "Trace   ", p->timeTrace );
PRT( "TOTAL   ", p->timeTotal );
*/
    free( p->pInters );
    free( p->pProofNums );
    free( p->pTrail );
    free( p->pAssigns );
    free( p->pSeens );
    free( p->pVarTypes );
    free( p->pReasons );
    free( p->pWatches );
    free( p->pResLits );
    free( p );
}

int Int_ManInterpolate	(	Int_Man_t *	p,
		Sto_Man_t *	pCnf,
		int	fVerbose,
		unsigned **	ppResult
	)

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

Synopsis [Computes interpolant for the given CNF.]

Description [Returns the number of common variable found and interpolant. Returns 0, if something did not work.]

SideEffects []

SeeAlso []

Definition at line 921 of file satInter.c.

{
    Sto_Cls_t * pClause;
    int RetValue = 1;
    int clkTotal = clock();

    // check that the CNF makes sense
    assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
    p->pCnf = pCnf;
    p->fVerbose = fVerbose;
    *ppResult = NULL;

    // adjust the manager
    Int_ManResize( p );

    // prepare the interpolant computation
    Int_ManPrepareInter( p );

    // construct proof for each clause
    // start the proof
    if ( p->fProofWrite )
    {
        p->pFile = fopen( "proof.cnf_", "w" );
        p->Counter = 0;
    }

    // write the root clauses
    Sto_ManForEachClauseRoot( p->pCnf, pClause )
        Int_ManProofWriteOne( p, pClause );

    // propagate root level assignments
    if ( Int_ManProcessRoots( p ) )
    {
        // if there is no conflict, consider learned clauses
        Sto_ManForEachClause( p->pCnf, pClause )
        {
            if ( pClause->fRoot )
                continue;
            if ( !Int_ManProofRecordOne( p, pClause ) )
            {
                RetValue = 0;
                break;
            }
        }
    }

    // stop the proof
    if ( p->fProofWrite )
    {
        fclose( p->pFile );
        p->pFile = NULL;    
    }

    if ( fVerbose )
    {
    printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f Mb\n", 
        p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
        1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 
        1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
p->timeTotal += clock() - clkTotal;
    }

    *ppResult = Int_ManTruthRead( p, p->pCnf->pTail );
    return p->nVarsAB;
}

static int lit_check	(	lit	l,
		int	n
	)			[inline, static]

Definition at line 98 of file satStore.h.

{ return l >= 0 && lit_var(l) < n;                  }

static lit lit_neg

(

lit

l

)

[inline, static]

Definition at line 93 of file satStore.h.

{ return l ^ 1;  }

static int lit_print

(

lit

l

)

[inline, static]

Definition at line 96 of file satStore.h.

{ return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }

static lit lit_read

(

int

s

)

[inline, static]

Definition at line 97 of file satStore.h.

{ return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }

static int lit_sign

(

lit

l

)

[inline, static]

Definition at line 95 of file satStore.h.

{ return l & 1;  }

static int lit_var

(

lit

l

)

[inline, static]

Definition at line 94 of file satStore.h.

{ return l >> 1; }

int Sto_ManAddClause	(	Sto_Man_t *	p,
		lit *	pBeg,
		lit *	pEnd
	)

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

Synopsis [Adds one clause to the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 157 of file satStore.c.

{
    Sto_Cls_t * pClause;
    lit Lit, * i, * j;
    int nSize;

    // process the literals
    if ( pBeg < pEnd )
    {
        // insertion sort
        for ( i = pBeg + 1; i < pEnd; i++ )
        {
            Lit = *i;
            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++ )
            if ( lit_var(*(i-1)) == lit_var(*i) )
            {
                printf( "The clause contains two literals of the same variable: %d and %d.\n", *(i-1), *i );
                return 0;
            }
        // check the largest var size
        p->nVars = STO_MAX( p->nVars, lit_var(*(pEnd-1)) + 1 );
    }

    // get memory for the clause
    nSize = sizeof(Sto_Cls_t) + sizeof(lit) * (pEnd - pBeg);
    pClause = (Sto_Cls_t *)Sto_ManMemoryFetch( p, nSize );
    memset( pClause, 0, sizeof(Sto_Cls_t) );

    // assign the clause
    pClause->Id = p->nClauses++;
    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;
    }

    // add the empty clause
    if ( pClause->nLits == 0 )
    {
        if ( p->pEmpty )
        {
            printf( "More than one empty clause!\n" );
            return 0;
        }
        p->pEmpty = pClause;
    }
    return 1;
}

Sto_Man_t* Sto_ManAlloc

(

)

MACRO DEFINITIONS /// FUNCTION DECLARATIONS ///

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

Synopsis [Allocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 118 of file satStore.c.

{
    Sto_Man_t * p;
    // allocate the manager
    p = (Sto_Man_t *)malloc( sizeof(Sto_Man_t) );
    memset( p, 0, sizeof(Sto_Man_t) );
    // memory management
    p->nChunkSize = (1<<16); // use 64K chunks
    return p;    
}

void Sto_ManDumpClauses	(	Sto_Man_t *	p,
		char *	pFileName
	)

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

Synopsis [Writes the stored clauses into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 275 of file satStore.c.

{
    FILE * pFile;
    Sto_Cls_t * pClause;
    int i;
    // start the file
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        printf( "Error: Cannot open output file (%s).\n", pFileName );
        return;
    }
    // write the data
    fprintf( pFile, "p %d %d %d %d\n", p->nVars, p->nClauses, p->nRoots, p->nClausesA );
    Sto_ManForEachClause( p, pClause )
    {
        for ( i = 0; i < (int)pClause->nLits; i++ )
            fprintf( pFile, " %d", lit_print(pClause->pLits[i]) );
        fprintf( pFile, "\n" );
    }
    fprintf( pFile, " 0\n" );
    fclose( pFile );
}

void Sto_ManFree

(

Sto_Man_t *

p

)

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

Synopsis [Deallocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file satStore.c.

{
    Sto_ManMemoryStop( p );
    free( p );
}

Sto_Man_t* Sto_ManLoadClauses

(

char *

pFileName

)

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

Synopsis [Reads CNF from file.]

Description []

SideEffects []

SeeAlso []

Definition at line 354 of file satStore.c.

{
    FILE * pFile;
    Sto_Man_t * p;
    Sto_Cls_t * pClause;
    char pBuffer[1024];
    int nLits, nLitsAlloc, Counter, Number;
    lit * pLits;

    // start the file
    pFile = fopen( pFileName, "r" );
    if ( pFile == NULL )
    {
        printf( "Error: Cannot open input file (%s).\n", pFileName );
        return NULL;
    }

    // create the manager
    p = Sto_ManAlloc();

    // alloc the array of literals
    nLitsAlloc = 1024;
    pLits = (lit *)malloc( sizeof(lit) * nLitsAlloc );

    // read file header
    p->nVars = p->nClauses = p->nRoots = p->nClausesA = 0;
    while ( fgets( pBuffer, 1024, pFile ) )
    {
        if ( pBuffer[0] == 'c' )
            continue;
        if ( pBuffer[0] == 'p' )
        {
            sscanf( pBuffer + 1, "%d %d %d %d", p->nVars, p->nClauses, p->nRoots, p->nClausesA );
            break;
        }
        printf( "Warning: Skipping line: \"%s\"\n", pBuffer );
    }

    // read the clauses
    nLits = 0;
    while ( Sto_ManLoadNumber(pFile, &Number) )
    {
        if ( Number == 0 )
        {
            int RetValue;
            RetValue = Sto_ManAddClause( p, pLits, pLits + nLits );
            assert( RetValue );
            nLits = 0;
            continue;
        }
        if ( nLits == nLitsAlloc )
        {
            nLitsAlloc *= 2;
            pLits = (lit *)realloc( pLits, sizeof(lit) * nLitsAlloc );
        }
        pLits[ nLits++ ] = lit_read(Number);
    }
    if ( nLits > 0 )
        printf( "Error: The last clause was not saved.\n" );

    // count clauses
    Counter = 0;
    Sto_ManForEachClause( p, pClause )
        Counter++;

    // check the number of clauses
    if ( p->nClauses != Counter )
    {
        printf( "Error: The actual number of clauses (%d) is different than declared (%d).\n", Counter, p->nClauses );
        Sto_ManFree( p );
        return NULL;
    }

    free( pLits );
    fclose( pFile );
    return p;
}

void Sto_ManMarkClausesA

(

Sto_Man_t *

p

)

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

Synopsis [Mark all clauses added so far as clause of A.]

Description []

SideEffects []

SeeAlso []

Definition at line 252 of file satStore.c.

{
    Sto_Cls_t * pClause;
    p->nClausesA = 0;
    Sto_ManForEachClause( p, pClause )
    {
        pClause->fA = 1;
        p->nClausesA++;
    }
}

void Sto_ManMarkRoots

(

Sto_Man_t *

p

)

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

Synopsis [Mark all clauses added so far as root clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 230 of file satStore.c.

{
    Sto_Cls_t * pClause;
    p->nRoots = 0;
    Sto_ManForEachClause( p, pClause )
    {
        pClause->fRoot = 1;
        p->nRoots++;
    }
}

int Sto_ManMemoryReport

(

Sto_Man_t *

p

)

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

Synopsis [Reports memory usage in bytes.]

Description []

SideEffects []

SeeAlso []

Definition at line 94 of file satStore.c.

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

static lit toLit

(

int

v

)

[inline, static]

Definition at line 91 of file satStore.h.

{ return v + v;  }

static lit toLitCond	(	int	v,
		int	c
	)			[inline, static]

Definition at line 92 of file satStore.h.

{ return v + v + (c != 0); }