1 /**CFile****************************************************************
2
3 FileName [satProof2.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [SAT solver.]
8
9 Synopsis [Proof logging.]
10
11 Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - January 1, 2004.]
16
17 Revision [$Id: satProof2.h,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC__sat__bsat__satProof2_h
22 #define ABC__sat__bsat__satProof2_h
23
24 ////////////////////////////////////////////////////////////////////////
25 /// INCLUDES ///
26 ////////////////////////////////////////////////////////////////////////
27
28 #include "misc/vec/vec.h"
29
30 ABC_NAMESPACE_HEADER_START
31
32 ////////////////////////////////////////////////////////////////////////
33 /// PARAMETERS ///
34 ////////////////////////////////////////////////////////////////////////
35
36 ////////////////////////////////////////////////////////////////////////
37 /// STRUCTURE DEFINITIONS ///
38 ////////////////////////////////////////////////////////////////////////
39
40 typedef struct Prf_Man_t_ Prf_Man_t;
41 struct Prf_Man_t_
42 {
43 int iFirst; // first learned clause with proof
44 int iFirst2; // first learned clause with proof
45 int nWords; // the number of proof words
46 word * pInfo; // pointer to the current proof
47 Vec_Wrd_t * vInfo; // proof information
48 Vec_Int_t * vSaved; // IDs of saved clauses
49 Vec_Int_t * vId2Pr; // mapping proof IDs of problem clauses into bitshifts (user's array)
50 };
51
52 ////////////////////////////////////////////////////////////////////////
53 /// GLOBAL VARIABLES ///
54 ////////////////////////////////////////////////////////////////////////
55
56 ////////////////////////////////////////////////////////////////////////
57 /// MACRO DEFINITIONS ///
58 ////////////////////////////////////////////////////////////////////////
59
Prf_BitWordNum(int nWidth)60 static inline int Prf_BitWordNum( int nWidth ) { return (nWidth >> 6) + ((nWidth & 63) > 0); }
Prf_ManSize(Prf_Man_t * p)61 static inline int Prf_ManSize( Prf_Man_t * p ) { return Vec_WrdSize( p->vInfo ) / p->nWords; }
Prf_ManClearNewInfo(Prf_Man_t * p)62 static inline void Prf_ManClearNewInfo( Prf_Man_t * p ) { int w; for ( w = 0; w < p->nWords; w++ ) Vec_WrdPush( p->vInfo, 0 ); }
Prf_ManClauseInfo(Prf_Man_t * p,int Id)63 static inline word * Prf_ManClauseInfo( Prf_Man_t * p, int Id ) { return Vec_WrdEntryP( p->vInfo, Id * p->nWords ); }
64
65 ////////////////////////////////////////////////////////////////////////
66 /// FUNCTION DECLARATIONS ///
67 ////////////////////////////////////////////////////////////////////////
68
69
70 /**Function*************************************************************
71
72 Synopsis []
73
74 Description []
75
76 SideEffects []
77
78 SeeAlso []
79
80 ***********************************************************************/
Prf_ManAlloc()81 static inline Prf_Man_t * Prf_ManAlloc()
82 {
83 Prf_Man_t * p;
84 p = ABC_CALLOC( Prf_Man_t, 1 );
85 p->iFirst = -1;
86 p->iFirst2 = -1;
87 p->vInfo = Vec_WrdAlloc( 1000 );
88 p->vSaved = Vec_IntAlloc( 1000 );
89 return p;
90 }
Prf_ManStop(Prf_Man_t * p)91 static inline void Prf_ManStop( Prf_Man_t * p )
92 {
93 if ( p == NULL )
94 return;
95 Vec_IntFree( p->vSaved );
96 Vec_WrdFree( p->vInfo );
97 ABC_FREE( p );
98 }
Prf_ManStopP(Prf_Man_t ** p)99 static inline void Prf_ManStopP( Prf_Man_t ** p )
100 {
101 Prf_ManStop( *p );
102 *p = NULL;
103 }
Prf_ManMemory(Prf_Man_t * p)104 static inline double Prf_ManMemory( Prf_Man_t * p )
105 {
106 return Vec_WrdMemory(p->vInfo) + Vec_IntMemory(p->vSaved) + sizeof(Prf_Man_t);
107 }
108
109 /**Function*************************************************************
110
111 Synopsis []
112
113 Description []
114
115 SideEffects []
116
117 SeeAlso []
118
119 ***********************************************************************/
Prf_ManRestart(Prf_Man_t * p,Vec_Int_t * vId2Pr,int iFirst,int nWidth)120 static inline void Prf_ManRestart( Prf_Man_t * p, Vec_Int_t * vId2Pr, int iFirst, int nWidth )
121 {
122 assert( p->iFirst == -1 );
123 p->iFirst = iFirst;
124 p->nWords = Prf_BitWordNum( nWidth );
125 p->vId2Pr = vId2Pr;
126 p->pInfo = NULL;
127 Vec_WrdClear( p->vInfo );
128 }
Prf_ManGrow(Prf_Man_t * p,int nWidth)129 static inline void Prf_ManGrow( Prf_Man_t * p, int nWidth )
130 {
131 Vec_Wrd_t * vInfoNew;
132 int i, w, nSize, nWordsNew;
133 assert( p->iFirst >= 0 );
134 assert( p->pInfo == NULL );
135 if ( nWidth < 64 * p->nWords )
136 return;
137 // get word count after resizing
138 nWordsNew = Abc_MaxInt( Prf_BitWordNum(nWidth), 2 * p->nWords );
139 // remap the entries
140 nSize = Prf_ManSize( p );
141 vInfoNew = Vec_WrdAlloc( (nSize + 1000) * nWordsNew );
142 for ( i = 0; i < nSize; i++ )
143 {
144 p->pInfo = Prf_ManClauseInfo( p, i );
145 for ( w = 0; w < p->nWords; w++ )
146 Vec_WrdPush( vInfoNew, p->pInfo[w] );
147 for ( ; w < nWordsNew; w++ )
148 Vec_WrdPush( vInfoNew, 0 );
149 }
150 Vec_WrdFree( p->vInfo );
151 p->vInfo = vInfoNew;
152 p->nWords = nWordsNew;
153 p->pInfo = NULL;
154
155 }
Prf_ManShrink(Prf_Man_t * p,int iClause)156 static inline void Prf_ManShrink( Prf_Man_t * p, int iClause )
157 {
158 assert( p->iFirst >= 0 );
159 assert( iClause - p->iFirst >= 0 );
160 assert( iClause - p->iFirst < Prf_ManSize(p) );
161 Vec_WrdShrink( p->vInfo, (iClause - p->iFirst) * p->nWords );
162 }
163
164 /**Function*************************************************************
165
166 Synopsis []
167
168 Description []
169
170 SideEffects []
171
172 SeeAlso []
173
174 ***********************************************************************/
Prf_ManAddSaved(Prf_Man_t * p,int i,int iNew)175 static inline void Prf_ManAddSaved( Prf_Man_t * p, int i, int iNew )
176 {
177 assert( p->iFirst >= 0 );
178 if ( i < p->iFirst )
179 return;
180 if ( Vec_IntSize(p->vSaved) == 0 )
181 {
182 assert( p->iFirst2 == -1 );
183 p->iFirst2 = iNew;
184 }
185 Vec_IntPush( p->vSaved, i );
186 }
Prf_ManCompact(Prf_Man_t * p,int iNew)187 static inline void Prf_ManCompact( Prf_Man_t * p, int iNew )
188 {
189 int i, w, k = 0, Entry, nSize;
190 assert( p->iFirst >= 0 );
191 assert( p->pInfo == NULL );
192 nSize = Prf_ManSize( p );
193 Vec_IntForEachEntry( p->vSaved, Entry, i )
194 {
195 assert( Entry - p->iFirst >= 0 && Entry - p->iFirst < nSize );
196 p->pInfo = Prf_ManClauseInfo( p, Entry - p->iFirst );
197 for ( w = 0; w < p->nWords; w++ )
198 Vec_WrdWriteEntry( p->vInfo, k++, p->pInfo[w] );
199 }
200 Vec_WrdShrink( p->vInfo, k );
201 Vec_IntClear( p->vSaved );
202 p->pInfo = NULL;
203 // update first
204 if ( p->iFirst2 == -1 )
205 p->iFirst = iNew;
206 else
207 p->iFirst = p->iFirst2;
208 p->iFirst2 = -1;
209 }
210
211 /**Function*************************************************************
212
213 Synopsis []
214
215 Description []
216
217 SideEffects []
218
219 SeeAlso []
220
221 ***********************************************************************/
Prf_ManChainResolve(Prf_Man_t * p,clause * c)222 static inline void Prf_ManChainResolve( Prf_Man_t * p, clause * c )
223 {
224 assert( p->iFirst >= 0 );
225 assert( p->pInfo != NULL );
226 // add to proof info
227 if ( c->lrn ) // learned clause
228 {
229 if ( clause_id(c) >= p->iFirst )
230 {
231 word * pProofStart;
232 int w;
233 assert( clause_id(c) - p->iFirst >= 0 );
234 assert( clause_id(c) - p->iFirst < Prf_ManSize(p) );
235 pProofStart = Prf_ManClauseInfo( p, clause_id(c) - p->iFirst );
236 for ( w = 0; w < p->nWords; w++ )
237 p->pInfo[w] |= pProofStart[w];
238 }
239 }
240 else // problem clause
241 {
242 if ( clause_id(c) >= 0 ) // has proof ID
243 {
244 int Entry;
245 if ( p->vId2Pr == NULL )
246 Entry = clause_id(c);
247 else
248 Entry = Vec_IntEntry( p->vId2Pr, clause_id(c) );
249 if ( Entry >= 0 )
250 {
251 assert( Entry < 64 * p->nWords );
252 Abc_InfoSetBit( (unsigned *)p->pInfo, Entry );
253 }
254 }
255 }
256 }
Prf_ManChainStart(Prf_Man_t * p,clause * c)257 static inline void Prf_ManChainStart( Prf_Man_t * p, clause * c )
258 {
259 assert( p->iFirst >= 0 );
260 // prepare info for new clause
261 Prf_ManClearNewInfo( p );
262 // get pointer to the proof
263 assert( p->pInfo == NULL );
264 p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 );
265 // add to proof info
266 Prf_ManChainResolve( p, c );
267 }
Prf_ManChainStop(Prf_Man_t * p)268 static inline int Prf_ManChainStop( Prf_Man_t * p )
269 {
270 assert( p->pInfo != NULL );
271 p->pInfo = NULL;
272 return 0;
273 }
274
275
276 /**Function*************************************************************
277
278 Synopsis []
279
280 Description []
281
282 SideEffects []
283
284 SeeAlso []
285
286 ***********************************************************************/
Prf_ManUnsatCore(Prf_Man_t * p)287 static inline Vec_Int_t * Prf_ManUnsatCore( Prf_Man_t * p )
288 {
289 Vec_Int_t * vCore;
290 int i, Entry;
291 assert( p->iFirst >= 0 );
292 assert( p->pInfo == NULL );
293 assert( Prf_ManSize(p) > 0 );
294 vCore = Vec_IntAlloc( 64 * p->nWords );
295 p->pInfo = Prf_ManClauseInfo( p, Prf_ManSize(p)-1 );
296 if ( p->vId2Pr == NULL )
297 {
298 for ( i = 0; i < 64 * p->nWords; i++ )
299 if ( Abc_InfoHasBit( (unsigned *)p->pInfo, i ) )
300 Vec_IntPush( vCore, i );
301 }
302 else
303 {
304 Vec_IntForEachEntry( p->vId2Pr, Entry, i )
305 {
306 if ( Entry < 0 )
307 continue;
308 assert( Entry < 64 * p->nWords );
309 if ( Abc_InfoHasBit( (unsigned *)p->pInfo, Entry ) )
310 Vec_IntPush( vCore, i );
311 }
312 }
313 p->pInfo = NULL;
314 Vec_IntSort( vCore, 1 );
315 return vCore;
316 }
317
318
319
320 ABC_NAMESPACE_HEADER_END
321
322 #endif
323
324 ////////////////////////////////////////////////////////////////////////
325 /// END OF FILE ///
326 ////////////////////////////////////////////////////////////////////////
327
328