From 4812c90424dfc40d26725244723887a2d16ddfd9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 1 Oct 2007 08:01:00 -0700 Subject: Version abc71001 --- src/sat/bsat/satStore.h | 137 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 137 insertions(+) create mode 100644 src/sat/bsat/satStore.h (limited to 'src/sat/bsat/satStore.h') diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h new file mode 100644 index 00000000..346b59df --- /dev/null +++ b/src/sat/bsat/satStore.h @@ -0,0 +1,137 @@ +/**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__ + +/* + The trace of SAT solving contains the original clause of the problem + along with the learned clauses derived during SAT solving. + The first line of the resulting file contains 3 numbers instead of 2: + c +*/ + +#ifdef __cplusplus +extern "C" { +#endif + +#ifdef _WIN32 +#define inline __inline // compatible with MS VS 6.0 +#endif + +#ifndef PRT +#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)) +#endif + +#define STO_MAX(a,b) ((a) > (b) ? (a) : (b)) + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef unsigned lit; + +typedef struct Sto_Cls_t_ Sto_Cls_t; +struct Sto_Cls_t_ +{ + Sto_Cls_t * pNext; // the next clause + Sto_Cls_t * pNext0; // the next 0-watch + Sto_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 +}; + +typedef struct Sto_Man_t_ Sto_Man_t; +struct Sto_Man_t_ +{ + // general data + int nVars; // the number of variables + int nRoots; // the number of root clauses + int nClauses; // the number of all clauses + int nClausesA; // the number of clauses of A + Sto_Cls_t * pHead; // the head clause + Sto_Cls_t * pTail; // the tail clause + Sto_Cls_t * pEmpty; // the empty clause + // 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 +}; + +// 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 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 ) + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== satStore.c ==========================================================*/ +extern Sto_Man_t * Sto_ManAlloc(); +extern void Sto_ManFree( Sto_Man_t * p ); +extern int Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd ); +extern int Sto_ManMemoryReport( Sto_Man_t * p ); +extern void Sto_ManMarkRoots( Sto_Man_t * p ); +extern void Sto_ManMarkClausesA( Sto_Man_t * p ); +extern void Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName ); +extern Sto_Man_t * Sto_ManLoadClauses( char * pFileName ); + +/*=== satInter.c ==========================================================*/ +typedef struct Int_Man_t_ Int_Man_t; +extern Int_Man_t * Int_ManAlloc( int nVarsAlloc ); +extern void Int_ManFree( Int_Man_t * p ); +extern int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + -- cgit v1.2.3