mirror of https://github.com/YosysHQ/abc.git
159 lines
6.5 KiB
C
159 lines
6.5 KiB
C
/**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 ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|