1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
/**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, 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 fVerbose );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
