src/sat/bsat/satStore.c File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "satStore.h"
Include dependency graph for satStore.c:

Go to the source code of this file.

Functions

char * Sto_ManMemoryFetch (Sto_Man_t *p, int nBytes)
void Sto_ManMemoryStop (Sto_Man_t *p)
int Sto_ManMemoryReport (Sto_Man_t *p)
Sto_Man_t * Sto_ManAlloc ()
void Sto_ManFree (Sto_Man_t *p)
int Sto_ManAddClause (Sto_Man_t *p, lit *pBeg, lit *pEnd)
void Sto_ManMarkRoots (Sto_Man_t *p)
void Sto_ManMarkClausesA (Sto_Man_t *p)
void Sto_ManDumpClauses (Sto_Man_t *p, char *pFileName)
int Sto_ManLoadNumber (FILE *pFile, int *pNumber)
Sto_Man_t * Sto_ManLoadClauses (char *pFileName)

Function Documentation

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.

00158 {
00159     Sto_Cls_t * pClause;
00160     lit Lit, * i, * j;
00161     int nSize;
00162 
00163     // process the literals
00164     if ( pBeg < pEnd )
00165     {
00166         // insertion sort
00167         for ( i = pBeg + 1; i < pEnd; i++ )
00168         {
00169             Lit = *i;
00170             for ( j = i; j > pBeg && *(j-1) > Lit; j-- )
00171                 *j = *(j-1);
00172             *j = Lit;
00173         }
00174         // make sure there is no duplicated variables
00175         for ( i = pBeg + 1; i < pEnd; i++ )
00176             if ( lit_var(*(i-1)) == lit_var(*i) )
00177             {
00178                 printf( "The clause contains two literals of the same variable: %d and %d.\n", *(i-1), *i );
00179                 return 0;
00180             }
00181         // check the largest var size
00182         p->nVars = STO_MAX( p->nVars, lit_var(*(pEnd-1)) + 1 );
00183     }
00184 
00185     // get memory for the clause
00186     nSize = sizeof(Sto_Cls_t) + sizeof(lit) * (pEnd - pBeg);
00187     pClause = (Sto_Cls_t *)Sto_ManMemoryFetch( p, nSize );
00188     memset( pClause, 0, sizeof(Sto_Cls_t) );
00189 
00190     // assign the clause
00191     pClause->Id = p->nClauses++;
00192     pClause->nLits = pEnd - pBeg;
00193     memcpy( pClause->pLits, pBeg, sizeof(lit) * (pEnd - pBeg) );
00194 
00195     // add the clause to the list
00196     if ( p->pHead == NULL )
00197         p->pHead = pClause;
00198     if ( p->pTail == NULL )
00199         p->pTail = pClause;
00200     else
00201     {
00202         p->pTail->pNext = pClause;
00203         p->pTail = pClause;
00204     }
00205 
00206     // add the empty clause
00207     if ( pClause->nLits == 0 )
00208     {
00209         if ( p->pEmpty )
00210         {
00211             printf( "More than one empty clause!\n" );
00212             return 0;
00213         }
00214         p->pEmpty = pClause;
00215     }
00216     return 1;
00217 }

Sto_Man_t* Sto_ManAlloc (  ) 

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

Synopsis [Allocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 118 of file satStore.c.

00119 {
00120     Sto_Man_t * p;
00121     // allocate the manager
00122     p = (Sto_Man_t *)malloc( sizeof(Sto_Man_t) );
00123     memset( p, 0, sizeof(Sto_Man_t) );
00124     // memory management
00125     p->nChunkSize = (1<<16); // use 64K chunks
00126     return p;    
00127 }

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.

00276 {
00277     FILE * pFile;
00278     Sto_Cls_t * pClause;
00279     int i;
00280     // start the file
00281     pFile = fopen( pFileName, "w" );
00282     if ( pFile == NULL )
00283     {
00284         printf( "Error: Cannot open output file (%s).\n", pFileName );
00285         return;
00286     }
00287     // write the data
00288     fprintf( pFile, "p %d %d %d %d\n", p->nVars, p->nClauses, p->nRoots, p->nClausesA );
00289     Sto_ManForEachClause( p, pClause )
00290     {
00291         for ( i = 0; i < (int)pClause->nLits; i++ )
00292             fprintf( pFile, " %d", lit_print(pClause->pLits[i]) );
00293         fprintf( pFile, "\n" );
00294     }
00295     fprintf( pFile, " 0\n" );
00296     fclose( pFile );
00297 }

void Sto_ManFree ( Sto_Man_t *  p  ) 

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

Synopsis [Deallocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file satStore.c.

00141 {
00142     Sto_ManMemoryStop( p );
00143     free( p );
00144 }

Sto_Man_t* Sto_ManLoadClauses ( char *  pFileName  ) 

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

Synopsis [Reads CNF from file.]

Description []

SideEffects []

SeeAlso []

Definition at line 354 of file satStore.c.

00355 {
00356     FILE * pFile;
00357     Sto_Man_t * p;
00358     Sto_Cls_t * pClause;
00359     char pBuffer[1024];
00360     int nLits, nLitsAlloc, Counter, Number;
00361     lit * pLits;
00362 
00363     // start the file
00364     pFile = fopen( pFileName, "r" );
00365     if ( pFile == NULL )
00366     {
00367         printf( "Error: Cannot open input file (%s).\n", pFileName );
00368         return NULL;
00369     }
00370 
00371     // create the manager
00372     p = Sto_ManAlloc();
00373 
00374     // alloc the array of literals
00375     nLitsAlloc = 1024;
00376     pLits = (lit *)malloc( sizeof(lit) * nLitsAlloc );
00377 
00378     // read file header
00379     p->nVars = p->nClauses = p->nRoots = p->nClausesA = 0;
00380     while ( fgets( pBuffer, 1024, pFile ) )
00381     {
00382         if ( pBuffer[0] == 'c' )
00383             continue;
00384         if ( pBuffer[0] == 'p' )
00385         {
00386             sscanf( pBuffer + 1, "%d %d %d %d", p->nVars, p->nClauses, p->nRoots, p->nClausesA );
00387             break;
00388         }
00389         printf( "Warning: Skipping line: \"%s\"\n", pBuffer );
00390     }
00391 
00392     // read the clauses
00393     nLits = 0;
00394     while ( Sto_ManLoadNumber(pFile, &Number) )
00395     {
00396         if ( Number == 0 )
00397         {
00398             int RetValue;
00399             RetValue = Sto_ManAddClause( p, pLits, pLits + nLits );
00400             assert( RetValue );
00401             nLits = 0;
00402             continue;
00403         }
00404         if ( nLits == nLitsAlloc )
00405         {
00406             nLitsAlloc *= 2;
00407             pLits = (lit *)realloc( pLits, sizeof(lit) * nLitsAlloc );
00408         }
00409         pLits[ nLits++ ] = lit_read(Number);
00410     }
00411     if ( nLits > 0 )
00412         printf( "Error: The last clause was not saved.\n" );
00413 
00414     // count clauses
00415     Counter = 0;
00416     Sto_ManForEachClause( p, pClause )
00417         Counter++;
00418 
00419     // check the number of clauses
00420     if ( p->nClauses != Counter )
00421     {
00422         printf( "Error: The actual number of clauses (%d) is different than declared (%d).\n", Counter, p->nClauses );
00423         Sto_ManFree( p );
00424         return NULL;
00425     }
00426 
00427     free( pLits );
00428     fclose( pFile );
00429     return p;
00430 }

int Sto_ManLoadNumber ( FILE *  pFile,
int *  pNumber 
)

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

Synopsis [Reads one literal from file.]

Description []

SideEffects []

SeeAlso []

Definition at line 310 of file satStore.c.

00311 {
00312     int Char, Number = 0, Sign = 0;
00313     // skip space-like chars
00314     do {
00315         Char = fgetc( pFile );
00316         if ( Char == EOF )
00317             return 0;
00318     } while ( Char == ' ' || Char == '\t' || Char == '\r' || Char == '\n' );
00319     // read the literal
00320     while ( 1 )
00321     {
00322         // get the next character
00323         Char = fgetc( pFile );
00324         if ( Char == ' ' || Char == '\t' || Char == '\r' || Char == '\n' )
00325             break;
00326         // check that the char is a digit
00327         if ( (Char < '0' || Char > '9') && Char != '-' )
00328         {
00329             printf( "Error: Wrong char (%c) in the input file.\n", Char );
00330             return 0;
00331         }
00332         // check if this is a minus
00333         if ( Char == '-' )
00334             Sign = 1;
00335         else
00336             Number = 10 * Number + Char;
00337     }
00338     // return the number
00339     *pNumber = Sign? -Number : Number;
00340     return 1;
00341 }

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.

00253 {
00254     Sto_Cls_t * pClause;
00255     p->nClausesA = 0;
00256     Sto_ManForEachClause( p, pClause )
00257     {
00258         pClause->fA = 1;
00259         p->nClausesA++;
00260     }
00261 }

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.

00231 {
00232     Sto_Cls_t * pClause;
00233     p->nRoots = 0;
00234     Sto_ManForEachClause( p, pClause )
00235     {
00236         pClause->fRoot = 1;
00237         p->nRoots++;
00238     }
00239 }

char* Sto_ManMemoryFetch ( Sto_Man_t *  p,
int  nBytes 
)

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

FileName [satStore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT solver.]

Synopsis [Records the trace of SAT solving in the CNF form.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
satStore.c,v 1.4 2005/09/16 22:55:03 casem Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Fetches memory.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file satStore.c.

00048 {
00049     char * pMem;
00050     if ( p->pChunkLast == NULL || nBytes > p->nChunkSize - p->nChunkUsed )
00051     {
00052         pMem = (char *)malloc( p->nChunkSize );
00053         *(char **)pMem = p->pChunkLast;
00054         p->pChunkLast = pMem;
00055         p->nChunkUsed = sizeof(char *);
00056     }
00057     pMem = p->pChunkLast + p->nChunkUsed;
00058     p->nChunkUsed += nBytes;
00059     return pMem;
00060 }

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.

00095 {
00096     int Total;
00097     char * pMem, * pNext;
00098     if ( p->pChunkLast == NULL )
00099         return 0;
00100     Total = p->nChunkUsed; 
00101     for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext )
00102         Total += p->nChunkSize;
00103     return Total;
00104 }

void Sto_ManMemoryStop ( Sto_Man_t *  p  ) 

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

Synopsis [Frees memory manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 73 of file satStore.c.

00074 {
00075     char * pMem, * pNext;
00076     if ( p->pChunkLast == NULL )
00077         return;
00078     for ( pMem = p->pChunkLast; pNext = *(char **)pMem; pMem = pNext )
00079         free( pMem );
00080     free( pMem );
00081 }

Generated on Tue Jan 5 12:19:37 2010 for abc70930 by  doxygen 1.6.1