/**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 <num_vars> <num_all_clauses> <num_root_clauses> */ #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 /// ////////////////////////////////////////////////////////////////////////