/**CFile**************************************************************** FileName [satStore.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 ABC__sat__bsat__satStore_h #define ABC__sat__bsat__satStore_h /* The trace of SAT solving contains the original clauses 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 <num_vars> <num_all_clauses> <num_root_clauses> */ //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// #include "satSolver.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_HEADER_START #ifdef _WIN32 #define inline __inline // compatible with MS VS 6.0 #endif #define STO_MAX(a,b) ((a) > (b) ? (a) : (b)) //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// /* typedef unsigned lit; // 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; } */ 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 1-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 }; // 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 int Sto_ManChangeLastClause( Sto_Man_t * p ); extern Sto_Man_t * Sto_ManLoadClauses( char * pFileName ); /*=== satInter.c ==========================================================*/ typedef struct Int_Man_t_ Int_Man_t; extern Int_Man_t * Int_ManAlloc(); extern int * Int_ManSetGlobalVars( Int_Man_t * p, int nGloVars ); extern void Int_ManFree( Int_Man_t * p ); extern int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult ); /*=== satInterA.c ==========================================================*/ typedef struct Inta_Man_t_ Inta_Man_t; extern Inta_Man_t * Inta_ManAlloc(); extern void Inta_ManFree( Inta_Man_t * p ); extern void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, abctime TimeToStop, void * vVarsAB, int fVerbose ); /*=== satInterB.c ==========================================================*/ typedef struct Intb_Man_t_ Intb_Man_t; extern Intb_Man_t * Intb_ManAlloc(); extern void Intb_ManFree( Intb_Man_t * p ); extern void * Intb_ManInterpolate( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose ); /*=== satInterP.c ==========================================================*/ typedef struct Intp_Man_t_ Intp_Man_t; extern Intp_Man_t * Intp_ManAlloc(); extern void Intp_ManFree( Intp_Man_t * p ); extern void * Intp_ManUnsatCore( Intp_Man_t * p, Sto_Man_t * pCnf, int fLearned, int fVerbose ); extern void Intp_ManUnsatCorePrintForBmc( FILE * pFile, Sto_Man_t * pCnf, void * vCore, void * vVarMap ); ABC_NAMESPACE_HEADER_END #endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////