1 /**CFile****************************************************************
2
3 FileName [giaCSat.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [A simple circuit-based solver.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: giaCSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "gia.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 //#define gia_assert(exp) ((void)0)
27 //#define gia_assert(exp) (assert(exp))
28
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
33 typedef struct Cbs2_Par_t_ Cbs2_Par_t;
34 struct Cbs2_Par_t_
35 {
36 // conflict limits
37 int nBTLimit; // limit on the number of conflicts
38 int nJustLimit; // limit on the size of justification queue
39 // current parameters
40 int nBTThis; // number of conflicts
41 int nBTThisNc; // number of conflicts
42 int nJustThis; // max size of the frontier
43 int nBTTotal; // total number of conflicts
44 int nJustTotal; // total size of the frontier
45 // decision heuristics
46 int fUseHighest; // use node with the highest ID
47 int fUseLowest; // use node with the highest ID
48 int fUseMaxFF; // use node with the largest fanin fanout
49 int fUseFanout; // use node with the largest fanin fanout
50 // other
51 int fVerbose;
52 };
53
54 typedef struct Cbs2_Que_t_ Cbs2_Que_t;
55 struct Cbs2_Que_t_
56 {
57 int iHead; // beginning of the queue
58 int iTail; // end of the queue
59 int nSize; // allocated size
60 int * pData; // nodes stored in the queue
61 };
62
63 typedef struct Cbs2_Man_t_ Cbs2_Man_t;
64 struct Cbs2_Man_t_
65 {
66 Cbs2_Par_t Pars; // parameters
67 Gia_Man_t * pAig; // AIG manager
68 Cbs2_Que_t pProp; // propagation queue
69 Cbs2_Que_t pJust; // justification queue
70 Cbs2_Que_t pClauses; // clause queue
71 Vec_Int_t * vModel; // satisfying assignment
72 Vec_Int_t * vTemp; // temporary storage
73 // internal data
74 Vec_Str_t vAssign;
75 Vec_Str_t vMark;
76 Vec_Int_t vLevReason;
77 Vec_Int_t vWatches;
78 Vec_Int_t vWatchUpds;
79 Vec_Int_t vFanoutN;
80 Vec_Int_t vFanout0;
81 Vec_Int_t vActivity;
82 Vec_Int_t vActStore;
83 Vec_Int_t vJStore;
84 // SAT calls statistics
85 int nSatUnsat; // the number of proofs
86 int nSatSat; // the number of failure
87 int nSatUndec; // the number of timeouts
88 int nSatTotal; // the number of calls
89 // conflicts
90 int nConfUnsat; // conflicts in unsat problems
91 int nConfSat; // conflicts in sat problems
92 int nConfUndec; // conflicts in undec problems
93 // runtime stats
94 abctime timeJFront;
95 abctime timeSatUnsat; // unsat
96 abctime timeSatSat; // sat
97 abctime timeSatUndec; // undecided
98 abctime timeTotal; // total runtime
99 // other statistics
100 int nPropCalls[3];
101 int nFails[2];
102 int nClauseConf;
103 };
104
Cbs2_VarUnused(Cbs2_Man_t * p,int iVar)105 static inline int Cbs2_VarUnused( Cbs2_Man_t * p, int iVar ) { return Vec_IntEntry(&p->vLevReason, 3*iVar) == -1; }
Cbs2_VarSetUnused(Cbs2_Man_t * p,int iVar)106 static inline void Cbs2_VarSetUnused( Cbs2_Man_t * p, int iVar ) { Vec_IntWriteEntry(&p->vLevReason, 3*iVar, -1); }
107
108 /*
109 static inline int Cbs2_VarMark0( Cbs2_Man_t * p, int iVar ) { return Vec_StrEntry(&p->vAssign, iVar); }
110 static inline void Cbs2_VarSetMark0( Cbs2_Man_t * p, int iVar, int Value ) { Vec_StrWriteEntry(&p->vAssign, iVar, (char)Value); }
111
112 static inline int Cbs2_VarMark1( Cbs2_Man_t * p, int iVar ) { return Vec_StrEntry(&p->vValue, iVar); }
113 static inline void Cbs2_VarSetMark1( Cbs2_Man_t * p, int iVar, int Value ) { Vec_StrWriteEntry(&p->vValue, iVar, (char)Value); }
114
115 static inline int Cbs2_VarIsAssigned( Cbs2_Man_t * p, int iVar ) { return Cbs2_VarMark0(p, iVar); }
116 static inline void Cbs2_VarAssign( Cbs2_Man_t * p, int iVar ) { assert(!Cbs2_VarIsAssigned(p, iVar)); Cbs2_VarSetMark0(p, iVar, 1); }
117 static inline void Cbs2_VarUnassign( Cbs2_Man_t * p, int iVar ) { assert( Cbs2_VarIsAssigned(p, iVar)); Cbs2_VarSetMark0(p, iVar, 0); Cbs2_VarSetUnused(p, iVar); }
118 static inline int Cbs2_VarValue( Cbs2_Man_t * p, int iVar ) { assert( Cbs2_VarIsAssigned(p, iVar)); return Cbs2_VarMark1(p, iVar); }
119 static inline void Cbs2_VarSetValue( Cbs2_Man_t * p, int iVar, int v ) { assert( Cbs2_VarIsAssigned(p, iVar)); Cbs2_VarSetMark1(p, iVar, v); }
120
121 static inline int Cbs2_VarIsJust( Cbs2_Man_t * p, Gia_Obj_t * pVar, int iVar ) { return Gia_ObjIsAnd(pVar) && !Cbs2_VarIsAssigned(p, Gia_ObjFaninId0(pVar, iVar)) && !Cbs2_VarIsAssigned(p, Gia_ObjFaninId1(pVar, iVar)); }
122 static inline int Cbs2_VarFanin0Value( Cbs2_Man_t * p, Gia_Obj_t * pVar, int iVar ) { return Cbs2_VarIsAssigned(p, Gia_ObjFaninId0(pVar, iVar)) ? (Cbs2_VarValue(p, Gia_ObjFaninId0(pVar, iVar)) ^ Gia_ObjFaninC0(pVar)) : 2; }
123 static inline int Cbs2_VarFanin1Value( Cbs2_Man_t * p, Gia_Obj_t * pVar, int iVar ) { return Cbs2_VarIsAssigned(p, Gia_ObjFaninId1(pVar, iVar)) ? (Cbs2_VarValue(p, Gia_ObjFaninId1(pVar, iVar)) ^ Gia_ObjFaninC1(pVar)) : 2; }
124 */
125
Cbs2_VarMark0(Cbs2_Man_t * p,int iVar)126 static inline int Cbs2_VarMark0( Cbs2_Man_t * p, int iVar ) { return Vec_StrEntry(&p->vMark, iVar); }
Cbs2_VarSetMark0(Cbs2_Man_t * p,int iVar,int Value)127 static inline void Cbs2_VarSetMark0( Cbs2_Man_t * p, int iVar, int Value ) { Vec_StrWriteEntry(&p->vMark, iVar, (char)Value); }
128
129 //static inline int Cbs2_VarMark0( Cbs2_Man_t * p, int iVar ) { return Vec_StrEntry(&p->vAssign, iVar) >= 2; }
130 //static inline void Cbs2_VarSetMark0( Cbs2_Man_t * p, int iVar, int Value ) { Vec_StrWriteEntry(&p->vAssign, iVar, (char)(2^Vec_StrEntry(&p->vAssign, iVar))); }
131
Cbs2_VarIsAssigned(Cbs2_Man_t * p,int iVar)132 static inline int Cbs2_VarIsAssigned( Cbs2_Man_t * p, int iVar ) { return Vec_StrEntry(&p->vAssign, iVar) < 2; }
Cbs2_VarUnassign(Cbs2_Man_t * p,int iVar)133 static inline void Cbs2_VarUnassign( Cbs2_Man_t * p, int iVar ) { assert( Cbs2_VarIsAssigned(p, iVar)); Vec_StrWriteEntry(&p->vAssign, iVar, (char)(2+Vec_StrEntry(&p->vAssign, iVar))); Cbs2_VarSetUnused(p, iVar); }
134
Cbs2_VarValue(Cbs2_Man_t * p,int iVar)135 static inline int Cbs2_VarValue( Cbs2_Man_t * p, int iVar ) { return Vec_StrEntry(&p->vAssign, iVar); }
Cbs2_VarSetValue(Cbs2_Man_t * p,int iVar,int v)136 static inline void Cbs2_VarSetValue( Cbs2_Man_t * p, int iVar, int v ) { assert( !Cbs2_VarIsAssigned(p, iVar)); Vec_StrWriteEntry(&p->vAssign, iVar, (char)v); }
137
Cbs2_VarIsJust(Cbs2_Man_t * p,Gia_Obj_t * pVar,int iVar)138 static inline int Cbs2_VarIsJust( Cbs2_Man_t * p, Gia_Obj_t * pVar, int iVar ) { return Gia_ObjIsAnd(pVar) && !Cbs2_VarIsAssigned(p, Gia_ObjFaninId0(pVar, iVar)) && !Cbs2_VarIsAssigned(p, Gia_ObjFaninId1(pVar, iVar)); }
Cbs2_VarFanin0Value(Cbs2_Man_t * p,Gia_Obj_t * pVar,int iVar)139 static inline int Cbs2_VarFanin0Value( Cbs2_Man_t * p, Gia_Obj_t * pVar, int iVar ) { return Cbs2_VarValue(p, Gia_ObjFaninId0(pVar, iVar)) ^ Gia_ObjFaninC0(pVar); }
Cbs2_VarFanin1Value(Cbs2_Man_t * p,Gia_Obj_t * pVar,int iVar)140 static inline int Cbs2_VarFanin1Value( Cbs2_Man_t * p, Gia_Obj_t * pVar, int iVar ) { return Cbs2_VarValue(p, Gia_ObjFaninId1(pVar, iVar)) ^ Gia_ObjFaninC1(pVar); }
141
142
Cbs2_VarDecLevel(Cbs2_Man_t * p,int iVar)143 static inline int Cbs2_VarDecLevel( Cbs2_Man_t * p, int iVar ) { assert( !Cbs2_VarUnused(p, iVar) ); return Vec_IntEntry(&p->vLevReason, 3*iVar); }
Cbs2_VarReason0(Cbs2_Man_t * p,int iVar)144 static inline int Cbs2_VarReason0( Cbs2_Man_t * p, int iVar ) { assert( !Cbs2_VarUnused(p, iVar) ); return Vec_IntEntry(&p->vLevReason, 3*iVar+1); }
Cbs2_VarReason1(Cbs2_Man_t * p,int iVar)145 static inline int Cbs2_VarReason1( Cbs2_Man_t * p, int iVar ) { assert( !Cbs2_VarUnused(p, iVar) ); return Vec_IntEntry(&p->vLevReason, 3*iVar+2); }
Cbs2_VarReasonP(Cbs2_Man_t * p,int iVar)146 static inline int * Cbs2_VarReasonP( Cbs2_Man_t * p, int iVar ) { assert( !Cbs2_VarUnused(p, iVar) ); return Vec_IntEntryP(&p->vLevReason, 3*iVar+1); }
147 //static inline int Cbs2_ClauseDecLevel( Cbs2_Man_t * p, int hClause ) { return Cbs2_VarDecLevel( p, p->pClauses.pData[hClause] ); }
148
Cbs2_ClauseSize(Cbs2_Man_t * p,int hClause)149 static inline int Cbs2_ClauseSize( Cbs2_Man_t * p, int hClause ) { return p->pClauses.pData[hClause]; }
Cbs2_ClauseLits(Cbs2_Man_t * p,int hClause)150 static inline int * Cbs2_ClauseLits( Cbs2_Man_t * p, int hClause ) { return p->pClauses.pData+hClause+1; }
Cbs2_ClauseLit(Cbs2_Man_t * p,int hClause,int i)151 static inline int Cbs2_ClauseLit( Cbs2_Man_t * p, int hClause, int i ) { return p->pClauses.pData[hClause+1+i]; }
Cbs2_ClauseNext1p(Cbs2_Man_t * p,int hClause)152 static inline int * Cbs2_ClauseNext1p( Cbs2_Man_t * p, int hClause ) { return p->pClauses.pData+hClause+Cbs2_ClauseSize(p, hClause)+2; }
153
Cbs2_ClauseSetSize(Cbs2_Man_t * p,int hClause,int x)154 static inline void Cbs2_ClauseSetSize( Cbs2_Man_t * p, int hClause, int x ) { p->pClauses.pData[hClause] = x; }
Cbs2_ClauseSetLit(Cbs2_Man_t * p,int hClause,int i,int x)155 static inline void Cbs2_ClauseSetLit( Cbs2_Man_t * p, int hClause, int i, int x ) { p->pClauses.pData[hClause+i+1] = x; }
Cbs2_ClauseSetNext(Cbs2_Man_t * p,int hClause,int n,int x)156 static inline void Cbs2_ClauseSetNext( Cbs2_Man_t * p, int hClause, int n, int x ){ p->pClauses.pData[hClause+Cbs2_ClauseSize(p, hClause)+1+n] = x; }
157
158
159 #define Cbs2_QueForEachEntry( Que, iObj, i ) \
160 for ( i = (Que).iHead; (i < (Que).iTail) && ((iObj) = (Que).pData[i]); i++ )
161
162 #define Cbs2_ClauseForEachEntry( p, hClause, iObj, i ) \
163 for ( i = 1; i <= Cbs2_ClauseSize(p, hClause) && (iObj = (p)->pClauses.pData[hClause+i]); i++ )
164 #define Cbs2_ClauseForEachEntry1( p, hClause, iObj, i ) \
165 for ( i = 2; i <= Cbs2_ClauseSize(p, hClause) && (iObj = (p)->pClauses.pData[hClause+i]); i++ )
166
167 #define Cbs2_ObjForEachFanout( p, iObj, iFanLit ) \
168 for ( iFanLit = Vec_IntEntry(&p->vFanout0, iObj); iFanLit; iFanLit = Vec_IntEntry(&p->vFanoutN, iFanLit) )
169
170 ////////////////////////////////////////////////////////////////////////
171 /// FUNCTION DEFINITIONS ///
172 ////////////////////////////////////////////////////////////////////////
173
174 /**Function*************************************************************
175
176 Synopsis [Sets default values of the parameters.]
177
178 Description []
179
180 SideEffects []
181
182 SeeAlso []
183
184 ***********************************************************************/
Cbs2_SetDefaultParams(Cbs2_Par_t * pPars)185 void Cbs2_SetDefaultParams( Cbs2_Par_t * pPars )
186 {
187 memset( pPars, 0, sizeof(Cbs2_Par_t) );
188 pPars->nBTLimit = 1000; // limit on the number of conflicts
189 pPars->nJustLimit = 500; // limit on the size of justification queue
190 pPars->fUseHighest = 1; // use node with the highest ID
191 pPars->fUseLowest = 0; // use node with the highest ID
192 pPars->fUseMaxFF = 0; // use node with the largest fanin fanout
193 pPars->fUseFanout = 1;
194 pPars->fVerbose = 1; // print detailed statistics
195 }
Cbs2_ManSetConflictNum(Cbs2_Man_t * p,int Num)196 void Cbs2_ManSetConflictNum( Cbs2_Man_t * p, int Num )
197 {
198 p->Pars.nBTLimit = Num;
199 }
200
201 /**Function*************************************************************
202
203 Synopsis []
204
205 Description []
206
207 SideEffects []
208
209 SeeAlso []
210
211 ***********************************************************************/
Cbs2_ManAlloc(Gia_Man_t * pGia)212 Cbs2_Man_t * Cbs2_ManAlloc( Gia_Man_t * pGia )
213 {
214 Cbs2_Man_t * p;
215 p = ABC_CALLOC( Cbs2_Man_t, 1 );
216 p->pProp.nSize = p->pJust.nSize = p->pClauses.nSize = 10000;
217 p->pProp.pData = ABC_ALLOC( int, p->pProp.nSize );
218 p->pJust.pData = ABC_ALLOC( int, p->pJust.nSize );
219 p->pClauses.pData = ABC_ALLOC( int, p->pClauses.nSize );
220 p->pClauses.iHead = p->pClauses.iTail = 1;
221 p->vModel = Vec_IntAlloc( 1000 );
222 p->vTemp = Vec_IntAlloc( 1000 );
223 p->pAig = pGia;
224 Cbs2_SetDefaultParams( &p->Pars );
225 Vec_StrFill( &p->vAssign, Gia_ManObjNum(pGia), 2 );
226 Vec_StrFill( &p->vMark, Gia_ManObjNum(pGia), 0 );
227 Vec_IntFill( &p->vLevReason, 3*Gia_ManObjNum(pGia), -1 );
228 Vec_IntFill( &p->vWatches, 2*Gia_ManObjNum(pGia), 0 );
229 Vec_IntFill( &p->vFanout0, Gia_ManObjNum(pGia), 0 );
230 Vec_IntFill( &p->vFanoutN, 2*Gia_ManObjNum(pGia), 0 );
231 Vec_IntFill( &p->vActivity, Gia_ManObjNum(pGia), 0 );
232 Vec_IntGrow( &p->vActStore, 1000 );
233 Vec_IntGrow( &p->vJStore, 1000 );
234 Vec_IntGrow( &p->vWatchUpds, 1000 );
235 return p;
236 }
237
238 /**Function*************************************************************
239
240 Synopsis []
241
242 Description []
243
244 SideEffects []
245
246 SeeAlso []
247
248 ***********************************************************************/
Cbs2_ManStop(Cbs2_Man_t * p)249 void Cbs2_ManStop( Cbs2_Man_t * p )
250 {
251 Vec_StrErase( &p->vAssign );
252 Vec_StrErase( &p->vMark );
253 Vec_IntErase( &p->vLevReason );
254 Vec_IntErase( &p->vWatches );
255 Vec_IntErase( &p->vFanout0 );
256 Vec_IntErase( &p->vFanoutN );
257 Vec_IntErase( &p->vActivity );
258 Vec_IntErase( &p->vActStore );
259 Vec_IntErase( &p->vJStore );
260 Vec_IntErase( &p->vWatchUpds );
261 Vec_IntFree( p->vModel );
262 Vec_IntFree( p->vTemp );
263 ABC_FREE( p->pClauses.pData );
264 ABC_FREE( p->pProp.pData );
265 ABC_FREE( p->pJust.pData );
266 ABC_FREE( p );
267 }
268
269 /**Function*************************************************************
270
271 Synopsis [Returns satisfying assignment.]
272
273 Description []
274
275 SideEffects []
276
277 SeeAlso []
278
279 ***********************************************************************/
Cbs2_ReadModel(Cbs2_Man_t * p)280 Vec_Int_t * Cbs2_ReadModel( Cbs2_Man_t * p )
281 {
282 return p->vModel;
283 }
284
285
286
287
288 /**Function*************************************************************
289
290 Synopsis [Returns 1 if the solver is out of limits.]
291
292 Description []
293
294 SideEffects []
295
296 SeeAlso []
297
298 ***********************************************************************/
Cbs2_ManCheckLimits(Cbs2_Man_t * p)299 static inline int Cbs2_ManCheckLimits( Cbs2_Man_t * p )
300 {
301 p->nFails[0] += p->Pars.nJustThis > p->Pars.nJustLimit;
302 p->nFails[1] += p->Pars.nBTThis > p->Pars.nBTLimit;
303 return p->Pars.nJustThis > p->Pars.nJustLimit || p->Pars.nBTThis > p->Pars.nBTLimit;
304 }
305
306 /**Function*************************************************************
307
308 Synopsis [Saves the satisfying assignment as an array of literals.]
309
310 Description []
311
312 SideEffects []
313
314 SeeAlso []
315
316 ***********************************************************************/
Cbs2_ManSaveModel(Cbs2_Man_t * p,Vec_Int_t * vCex)317 static inline void Cbs2_ManSaveModel( Cbs2_Man_t * p, Vec_Int_t * vCex )
318 {
319 int i, iLit;
320 Vec_IntClear( vCex );
321 p->pProp.iHead = 0;
322 Cbs2_QueForEachEntry( p->pProp, iLit, i )
323 {
324 int iVar = Abc_Lit2Var(iLit);
325 if ( Gia_ObjIsCi(Gia_ManObj(p->pAig, iVar)) )
326 Vec_IntPush( vCex, Abc_Var2Lit(Gia_ManIdToCioId(p->pAig, iVar), !Cbs2_VarValue(p, iVar)) );
327 }
328 }
Cbs2_ManSaveModelAll(Cbs2_Man_t * p,Vec_Int_t * vCex)329 static inline void Cbs2_ManSaveModelAll( Cbs2_Man_t * p, Vec_Int_t * vCex )
330 {
331 int i, iLit;
332 Vec_IntClear( vCex );
333 p->pProp.iHead = 0;
334 Cbs2_QueForEachEntry( p->pProp, iLit, i )
335 {
336 int iVar = Abc_Lit2Var(iLit);
337 Vec_IntPush( vCex, Abc_Var2Lit(iVar, !Cbs2_VarValue(p, iVar)) );
338 }
339 }
340
341 /**Function*************************************************************
342
343 Synopsis []
344
345 Description []
346
347 SideEffects []
348
349 SeeAlso []
350
351 ***********************************************************************/
Cbs2_QueIsEmpty(Cbs2_Que_t * p)352 static inline int Cbs2_QueIsEmpty( Cbs2_Que_t * p )
353 {
354 return p->iHead == p->iTail;
355 }
356
357 /**Function*************************************************************
358
359 Synopsis []
360
361 Description []
362
363 SideEffects []
364
365 SeeAlso []
366
367 ***********************************************************************/
Cbs2_QuePush(Cbs2_Que_t * p,int iObj)368 static inline void Cbs2_QuePush( Cbs2_Que_t * p, int iObj )
369 {
370 if ( p->iTail == p->nSize )
371 {
372 p->nSize *= 2;
373 p->pData = ABC_REALLOC( int, p->pData, p->nSize );
374 }
375 p->pData[p->iTail++] = iObj;
376 }
Cbs2_QueGrow(Cbs2_Que_t * p,int Plus)377 static inline void Cbs2_QueGrow( Cbs2_Que_t * p, int Plus )
378 {
379 if ( p->iTail + Plus > p->nSize )
380 {
381 p->nSize *= 2;
382 p->pData = ABC_REALLOC( int, p->pData, p->nSize );
383 }
384 assert( p->iTail + Plus <= p->nSize );
385 }
386
387 /**Function*************************************************************
388
389 Synopsis [Returns 1 if the object in the queue.]
390
391 Description []
392
393 SideEffects []
394
395 SeeAlso []
396
397 ***********************************************************************/
Cbs2_QueHasNode(Cbs2_Que_t * p,int iObj)398 static inline int Cbs2_QueHasNode( Cbs2_Que_t * p, int iObj )
399 {
400 int i, iTemp;
401 Cbs2_QueForEachEntry( *p, iTemp, i )
402 if ( iTemp == iObj )
403 return 1;
404 return 0;
405 }
406
407 /**Function*************************************************************
408
409 Synopsis []
410
411 Description []
412
413 SideEffects []
414
415 SeeAlso []
416
417 ***********************************************************************/
Cbs2_QueStore(Cbs2_Que_t * p,int * piHeadOld,int * piTailOld)418 static inline void Cbs2_QueStore( Cbs2_Que_t * p, int * piHeadOld, int * piTailOld )
419 {
420 int i;
421 *piHeadOld = p->iHead;
422 *piTailOld = p->iTail;
423 for ( i = *piHeadOld; i < *piTailOld; i++ )
424 Cbs2_QuePush( p, p->pData[i] );
425 p->iHead = *piTailOld;
426 }
427
428 /**Function*************************************************************
429
430 Synopsis []
431
432 Description []
433
434 SideEffects []
435
436 SeeAlso []
437
438 ***********************************************************************/
Cbs2_QueRestore(Cbs2_Que_t * p,int iHeadOld,int iTailOld)439 static inline void Cbs2_QueRestore( Cbs2_Que_t * p, int iHeadOld, int iTailOld )
440 {
441 p->iHead = iHeadOld;
442 p->iTail = iTailOld;
443 }
444
445
446 /**Function*************************************************************
447
448 Synopsis [Max number of fanins fanouts.]
449
450 Description []
451
452 SideEffects []
453
454 SeeAlso []
455
456 ***********************************************************************/
Cbs2_VarFaninFanoutMax(Cbs2_Man_t * p,Gia_Obj_t * pObj)457 static inline int Cbs2_VarFaninFanoutMax( Cbs2_Man_t * p, Gia_Obj_t * pObj )
458 {
459 int Count0, Count1;
460 assert( !Gia_IsComplement(pObj) );
461 assert( Gia_ObjIsAnd(pObj) );
462 Count0 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin0(pObj) );
463 Count1 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin1(pObj) );
464 return Abc_MaxInt( Count0, Count1 );
465 }
466
467 /**Function*************************************************************
468
469 Synopsis [Find variable with the highest ID.]
470
471 Description []
472
473 SideEffects []
474
475 SeeAlso []
476
477 ***********************************************************************/
Cbs2_ManDecideHighest(Cbs2_Man_t * p)478 static inline int Cbs2_ManDecideHighest( Cbs2_Man_t * p )
479 {
480 int i, iObj, iObjMax = 0;
481 Cbs2_QueForEachEntry( p->pJust, iObj, i )
482 if ( iObjMax == 0 || iObjMax < iObj )
483 iObjMax = iObj;
484 return iObjMax;
485 }
486
487 /**Function*************************************************************
488
489 Synopsis [Find variable with the lowest ID.]
490
491 Description []
492
493 SideEffects []
494
495 SeeAlso []
496
497 ***********************************************************************/
Cbs2_ManDecideLowest(Cbs2_Man_t * p)498 static inline Gia_Obj_t * Cbs2_ManDecideLowest( Cbs2_Man_t * p )
499 {
500 int i, iObj, iObjMin = 0;
501 Cbs2_QueForEachEntry( p->pJust, iObj, i )
502 if ( iObjMin == 0 || iObjMin > iObj )
503 iObjMin = iObj;
504 return Gia_ManObj(p->pAig, iObjMin);
505 }
506
507 /**Function*************************************************************
508
509 Synopsis [Find variable with the maximum number of fanin fanouts.]
510
511 Description []
512
513 SideEffects []
514
515 SeeAlso []
516
517 ***********************************************************************/
Cbs2_ManDecideMaxFF(Cbs2_Man_t * p)518 static inline Gia_Obj_t * Cbs2_ManDecideMaxFF( Cbs2_Man_t * p )
519 {
520 Gia_Obj_t * pObj, * pObjMax = NULL;
521 int i, iMaxFF = 0, iCurFF, iObj;
522 assert( p->pAig->pRefs != NULL );
523 Cbs2_QueForEachEntry( p->pJust, iObj, i )
524 {
525 pObj = Gia_ManObj(p->pAig, iObj);
526 iCurFF = Cbs2_VarFaninFanoutMax( p, pObj );
527 assert( iCurFF > 0 );
528 if ( iMaxFF < iCurFF )
529 {
530 iMaxFF = iCurFF;
531 pObjMax = pObj;
532 }
533 }
534 return pObjMax;
535 }
536
537
538 /**Function*************************************************************
539
540 Synopsis []
541
542 Description []
543
544 SideEffects []
545
546 SeeAlso []
547
548 ***********************************************************************/
Cbs2_ManCancelUntil(Cbs2_Man_t * p,int iBound)549 static inline void Cbs2_ManCancelUntil( Cbs2_Man_t * p, int iBound )
550 {
551 int i, iLit;
552 assert( iBound <= p->pProp.iTail );
553 p->pProp.iHead = iBound;
554 Cbs2_QueForEachEntry( p->pProp, iLit, i )
555 Cbs2_VarUnassign( p, Abc_Lit2Var(iLit) );
556 p->pProp.iTail = iBound;
557 }
558
559 /**Function*************************************************************
560
561 Synopsis [Assigns the variables a value.]
562
563 Description [Returns 1 if conflict; 0 if no conflict.]
564
565 SideEffects []
566
567 SeeAlso []
568
569 ***********************************************************************/
Cbs2_ManAssign(Cbs2_Man_t * p,int iLit,int Level,int iRes0,int iRes1)570 static inline void Cbs2_ManAssign( Cbs2_Man_t * p, int iLit, int Level, int iRes0, int iRes1 )
571 {
572 int iObj = Abc_Lit2Var(iLit);
573 assert( Cbs2_VarUnused(p, iObj) );
574 assert( !Cbs2_VarIsAssigned(p, iObj) );
575 //Cbs2_VarAssign( p, iObj );
576 Cbs2_VarSetValue( p, iObj, !Abc_LitIsCompl(iLit) );
577 Cbs2_QuePush( &p->pProp, iLit );
578 Vec_IntWriteEntry( &p->vLevReason, 3*iObj, Level );
579 Vec_IntWriteEntry( &p->vLevReason, 3*iObj+1, iRes0 );
580 Vec_IntWriteEntry( &p->vLevReason, 3*iObj+2, iRes1 );
581 }
582
583
584
585
586
587
588
589
590
591 /**Function*************************************************************
592
593 Synopsis [Prints conflict clause.]
594
595 Description []
596
597 SideEffects []
598
599 SeeAlso []
600
601 ***********************************************************************/
Cbs2_ManPrintClause(Cbs2_Man_t * p,int Level,int hClause)602 static inline void Cbs2_ManPrintClause( Cbs2_Man_t * p, int Level, int hClause )
603 {
604 int i, iLit;
605 assert( Cbs2_QueIsEmpty( &p->pClauses ) );
606 printf( "Level %2d : ", Level );
607 Cbs2_ClauseForEachEntry( p, hClause, iLit, i )
608 printf( "%c%d ", Abc_LitIsCompl(iLit) ? '-':'+', Abc_Lit2Var(iLit) );
609 // printf( "%d=%d(%d) ", iObj, Cbs2_VarValue(p, Abc_Lit2Var(iLit)), Cbs2_VarDecLevel(p, Abc_Lit2Var(iLit)) );
610 printf( "\n" );
611 }
Cbs2_ManPrintCube(Cbs2_Man_t * p,int Level,int hClause)612 static inline void Cbs2_ManPrintCube( Cbs2_Man_t * p, int Level, int hClause )
613 {
614 int i, iObj;
615 assert( Cbs2_QueIsEmpty( &p->pClauses ) );
616 printf( "Level %2d : ", Level );
617 Cbs2_ClauseForEachEntry( p, hClause, iObj, i )
618 printf( "%c%d ", Cbs2_VarValue(p, iObj)? '+':'-', iObj );
619 printf( "\n" );
620 }
Cbs2_ManBumpClause(Cbs2_Man_t * p,int hClause)621 static inline void Cbs2_ManBumpClause( Cbs2_Man_t * p, int hClause )
622 {
623 int i, iObj;
624 assert( Cbs2_QueIsEmpty( &p->pClauses ) );
625 Cbs2_ClauseForEachEntry( p, hClause, iObj, i )
626 {
627 //if ( Vec_IntEntry(&p->vActivity, iObj) == 0 )
628 // Vec_IntPush( &p->vActStore, iObj );
629 //Vec_IntAddToEntry( &p->vActivity, iObj, 1 );
630 }
631 }
Cbs2_ManBumpClean(Cbs2_Man_t * p)632 static inline void Cbs2_ManBumpClean( Cbs2_Man_t * p )
633 {
634 int i, iObj;
635 Vec_IntForEachEntry( &p->vActStore, iObj, i )
636 Vec_IntWriteEntry( &p->vActivity, iObj, 0 );
637 }
638
639 /**Function*************************************************************
640
641 Synopsis [Finalized the clause.]
642
643 Description []
644
645 SideEffects []
646
647 SeeAlso []
648
649 ***********************************************************************/
Cbs2_ManCleanWatch(Cbs2_Man_t * p)650 static inline void Cbs2_ManCleanWatch( Cbs2_Man_t * p )
651 {
652 int i, iLit;
653 Vec_IntForEachEntry( &p->vWatchUpds, iLit, i )
654 Vec_IntWriteEntry( &p->vWatches, iLit, 0 );
655 Vec_IntClear( &p->vWatchUpds );
656 //Vec_IntForEachEntry( &p->vWatches, iLit, i )
657 // assert( iLit == 0 );
658 }
Cbs2_ManWatchClause(Cbs2_Man_t * p,int hClause,int Lit)659 static inline void Cbs2_ManWatchClause( Cbs2_Man_t * p, int hClause, int Lit )
660 {
661 int * pLits = Cbs2_ClauseLits( p, hClause );
662 int * pPlace = Vec_IntEntryP( &p->vWatches, Abc_LitNot(Lit) );
663 if ( *pPlace == 0 )
664 Vec_IntPush( &p->vWatchUpds, Abc_LitNot(Lit) );
665 /*
666 if ( pClause->pLits[0] == Lit )
667 pClause->pNext0 = p->pWatches[lit_neg(Lit)];
668 else
669 {
670 assert( pClause->pLits[1] == Lit );
671 pClause->pNext1 = p->pWatches[lit_neg(Lit)];
672 }
673 p->pWatches[lit_neg(Lit)] = pClause;
674 */
675 assert( Lit == pLits[0] || Lit == pLits[1] );
676 Cbs2_ClauseSetNext( p, hClause, Lit == pLits[1], *pPlace );
677 *pPlace = hClause;
678 }
Cbs2_QueFinish(Cbs2_Man_t * p,int Level)679 static inline int Cbs2_QueFinish( Cbs2_Man_t * p, int Level )
680 {
681 Cbs2_Que_t * pQue = &(p->pClauses);
682 int i, iObj, hClauseC, hClause = pQue->iHead, Size = pQue->iTail - pQue->iHead - 1;
683 assert( pQue->iHead+1 < pQue->iTail );
684 Cbs2_ClauseSetSize( p, pQue->iHead, Size );
685 hClauseC = pQue->iHead = pQue->iTail;
686 //printf( "Adding cube: " ); Cbs2_ManPrintCube(p, Level, hClause);
687 if ( Size == 1 )
688 return hClause;
689 // create watched clause
690 pQue->iHead = hClause;
691 Cbs2_QueForEachEntry( p->pClauses, iObj, i )
692 {
693 if ( i == hClauseC )
694 break;
695 else if ( i == hClause ) // nlits
696 Cbs2_QuePush( pQue, iObj );
697 else // literals
698 Cbs2_QuePush( pQue, Abc_Var2Lit(iObj, Cbs2_VarValue(p, iObj)) ); // complement
699 }
700 Cbs2_QuePush( pQue, 0 ); // next0
701 Cbs2_QuePush( pQue, 0 ); // next1
702 pQue->iHead = pQue->iTail;
703 Cbs2_ManWatchClause( p, hClauseC, Cbs2_ClauseLit(p, hClauseC, 0) );
704 Cbs2_ManWatchClause( p, hClauseC, Cbs2_ClauseLit(p, hClauseC, 1) );
705 //printf( "Adding clause %d: ", hClauseC ); Cbs2_ManPrintClause(p, Level, hClauseC);
706 return hClause;
707 }
708
709 /**Function*************************************************************
710
711 Synopsis [Returns conflict clause.]
712
713 Description [Performs conflict analysis.]
714
715 SideEffects []
716
717 SeeAlso []
718
719 ***********************************************************************/
Cbs2_ManDeriveReason(Cbs2_Man_t * p,int Level)720 static inline int Cbs2_ManDeriveReason( Cbs2_Man_t * p, int Level )
721 {
722 Cbs2_Que_t * pQue = &(p->pClauses);
723 int i, k, iObj, iLitLevel, * pReason;
724 assert( pQue->pData[pQue->iHead] == 0 );
725 assert( pQue->pData[pQue->iHead+1] == 0 );
726 assert( pQue->iHead + 2 < pQue->iTail );
727 //for ( i = pQue->iHead + 2; i < pQue->iTail; i++ )
728 // assert( !Cbs2_VarMark0(p, pQue->pData[i]) );
729 // compact literals
730 Vec_IntClear( p->vTemp );
731 for ( i = k = pQue->iHead + 2; i < pQue->iTail; i++ )
732 {
733 iObj = pQue->pData[i];
734 if ( Cbs2_VarMark0(p, iObj) ) // unassigned - seen again
735 continue;
736 //if ( Vec_IntEntry(&p->vActivity, iObj) == 0 )
737 // Vec_IntPush( &p->vActStore, iObj );
738 //Vec_IntAddToEntry( &p->vActivity, iObj, 1 );
739 // assigned - seen first time
740 Cbs2_VarSetMark0(p, iObj, 1);
741 Vec_IntPush( p->vTemp, iObj );
742 // check decision level
743 iLitLevel = Cbs2_VarDecLevel( p, iObj );
744 if ( iLitLevel < Level )
745 {
746 pQue->pData[k++] = iObj;
747 continue;
748 }
749 assert( iLitLevel == Level );
750 pReason = Cbs2_VarReasonP( p, iObj );
751 if ( pReason[0] == 0 && pReason[1] == 0 ) // no reason
752 {
753 assert( pQue->pData[pQue->iHead+1] == 0 );
754 pQue->pData[pQue->iHead+1] = iObj;
755 }
756 else if ( pReason[0] != 0 ) // circuit reason
757 {
758 Cbs2_QuePush( pQue, pReason[0] );
759 if ( pReason[1] )
760 Cbs2_QuePush( pQue, pReason[1] );
761 }
762 else // clause reason
763 {
764 int i, * pLits, nLits = Cbs2_ClauseSize( p, pReason[1] );
765 assert( pReason[1] );
766 Cbs2_QueGrow( pQue, nLits );
767 pLits = Cbs2_ClauseLits( p, pReason[1] );
768 assert( iObj == Abc_Lit2Var(pLits[0]) );
769 for ( i = 1; i < nLits; i++ )
770 Cbs2_QuePush( pQue, Abc_Lit2Var(pLits[i]) );
771 }
772 }
773 assert( pQue->pData[pQue->iHead] == 0 );
774 assert( pQue->pData[pQue->iHead+1] != 0 );
775 pQue->iTail = k;
776 // clear the marks
777 Vec_IntForEachEntry( p->vTemp, iObj, i )
778 Cbs2_VarSetMark0(p, iObj, 0);
779 return Cbs2_QueFinish( p, Level );
780 }
Cbs2_ManAnalyze(Cbs2_Man_t * p,int Level,int iVar,int iFan0,int iFan1)781 static inline int Cbs2_ManAnalyze( Cbs2_Man_t * p, int Level, int iVar, int iFan0, int iFan1 )
782 {
783 Cbs2_Que_t * pQue = &(p->pClauses);
784 assert( Cbs2_VarIsAssigned(p, iVar) );
785 assert( Cbs2_QueIsEmpty( pQue ) );
786 Cbs2_QuePush( pQue, 0 );
787 Cbs2_QuePush( pQue, 0 );
788 if ( iFan0 ) // circuit conflict
789 {
790 assert( Cbs2_VarIsAssigned(p, iFan0) );
791 assert( iFan1 == 0 || Cbs2_VarIsAssigned(p, iFan1) );
792 Cbs2_QuePush( pQue, iVar );
793 Cbs2_QuePush( pQue, iFan0 );
794 if ( iFan1 )
795 Cbs2_QuePush( pQue, iFan1 );
796 }
797 else // clause conflict
798 {
799 int i, * pLits, nLits = Cbs2_ClauseSize( p, iFan1 );
800 assert( iFan1 );
801 Cbs2_QueGrow( pQue, nLits );
802 pLits = Cbs2_ClauseLits( p, iFan1 );
803 assert( iVar == Abc_Lit2Var(pLits[0]) );
804 assert( Cbs2_VarValue(p, iVar) == Abc_LitIsCompl(pLits[0]) );
805 for ( i = 0; i < nLits; i++ )
806 Cbs2_QuePush( pQue, Abc_Lit2Var(pLits[i]) );
807 }
808 return Cbs2_ManDeriveReason( p, Level );
809 }
810
811
812 /**Function*************************************************************
813
814 Synopsis [Propagate one assignment.]
815
816 Description [Returns handle of the conflict clause, if conflict occurs.]
817
818 SideEffects []
819
820 SeeAlso []
821
822 ***********************************************************************/
Cbs2_ManPropagateClauses(Cbs2_Man_t * p,int Level,int Lit)823 static inline int Cbs2_ManPropagateClauses( Cbs2_Man_t * p, int Level, int Lit )
824 {
825 int i, Value, Cur, LitF = Abc_LitNot(Lit);
826 int * pPrev = Vec_IntEntryP( &p->vWatches, Lit );
827 //for ( pCur = p->pWatches[Lit]; pCur; pCur = *ppPrev )
828 for ( Cur = *pPrev; Cur; Cur = *pPrev )
829 {
830 int nLits = Cbs2_ClauseSize( p, Cur );
831 int * pLits = Cbs2_ClauseLits( p, Cur );
832 p->nPropCalls[1]++;
833 //printf( " Watching literal %c%d on level %d.\n", Abc_LitIsCompl(Lit) ? '-':'+', Abc_Lit2Var(Lit), Level );
834 // make sure the false literal is in the second literal of the clause
835 //if ( pCur->pLits[0] == LitF )
836 if ( pLits[0] == LitF )
837 {
838 //pCur->pLits[0] = pCur->pLits[1];
839 pLits[0] = pLits[1];
840 //pCur->pLits[1] = LitF;
841 pLits[1] = LitF;
842 //pTemp = pCur->pNext0;
843 //pCur->pNext0 = pCur->pNext1;
844 //pCur->pNext1 = pTemp;
845 ABC_SWAP( int, pLits[nLits], pLits[nLits+1] );
846 }
847 //assert( pCur->pLits[1] == LitF );
848 assert( pLits[1] == LitF );
849
850 // if the first literal is true, the clause is satisfied
851 //if ( pCur->pLits[0] == p->pAssigns[lit_var(pCur->pLits[0])] )
852 if ( Cbs2_VarValue(p, Abc_Lit2Var(pLits[0])) == !Abc_LitIsCompl(pLits[0]) )
853 {
854 //ppPrev = &pCur->pNext1;
855 pPrev = Cbs2_ClauseNext1p(p, Cur);
856 continue;
857 }
858
859 // look for a new literal to watch
860 for ( i = 2; i < nLits; i++ )
861 {
862 // skip the case when the literal is false
863 //if ( lit_neg(pCur->pLits[i]) == p->pAssigns[lit_var(pCur->pLits[i])] )
864 if ( Cbs2_VarValue(p, Abc_Lit2Var(pLits[i])) == Abc_LitIsCompl(pLits[i]) )
865 continue;
866 // the literal is either true or unassigned - watch it
867 //pCur->pLits[1] = pCur->pLits[i];
868 //pCur->pLits[i] = LitF;
869 pLits[1] = pLits[i];
870 pLits[i] = LitF;
871 // remove this clause from the watch list of Lit
872 //*ppPrev = pCur->pNext1;
873 *pPrev = *Cbs2_ClauseNext1p(p, Cur);
874 // add this clause to the watch list of pCur->pLits[i] (now it is pCur->pLits[1])
875 //Intb_ManWatchClause( p, pCur, pCur->pLits[1] );
876 Cbs2_ManWatchClause( p, Cur, Cbs2_ClauseLit(p, Cur, 1) );
877 break;
878 }
879 if ( i < nLits ) // found new watch
880 continue;
881
882 // clause is unit - enqueue new implication
883 //if ( Inta_ManEnqueue(p, pCur->pLits[0], pCur) )
884 //{
885 // ppPrev = &pCur->pNext1;
886 // continue;
887 //}
888
889 // clause is unit - enqueue new implication
890 Value = Cbs2_VarValue(p, Abc_Lit2Var(pLits[0]));
891 if ( Value >= 2 ) // unassigned
892 {
893 Cbs2_ManAssign( p, pLits[0], Level, 0, Cur );
894 pPrev = Cbs2_ClauseNext1p(p, Cur);
895 continue;
896 }
897
898 // conflict detected - return the conflict clause
899 //return pCur;
900 if ( Value == Abc_LitIsCompl(pLits[0]) )
901 {
902 p->nClauseConf++;
903 return Cbs2_ManAnalyze( p, Level, Abc_Lit2Var(pLits[0]), 0, Cur );
904 }
905 }
906 return 0;
907 }
908
909
910 /**Function*************************************************************
911
912 Synopsis [Performs resolution of two clauses.]
913
914 Description []
915
916 SideEffects []
917
918 SeeAlso []
919
920 ***********************************************************************/
Cbs2_ManResolve(Cbs2_Man_t * p,int Level,int hClause0,int hClause1)921 static inline int Cbs2_ManResolve( Cbs2_Man_t * p, int Level, int hClause0, int hClause1 )
922 {
923 Cbs2_Que_t * pQue = &(p->pClauses);
924 int i, iObj, LevelMax = -1, LevelCur;
925 assert( pQue->pData[hClause0+1] != 0 );
926 assert( pQue->pData[hClause0+1] == pQue->pData[hClause1+1] );
927 //Cbs2_ClauseForEachEntry1( p, hClause0, iObj, i )
928 // assert( !Cbs2_VarMark0(p, iObj) );
929 //Cbs2_ClauseForEachEntry1( p, hClause1, iObj, i )
930 // assert( !Cbs2_VarMark0(p, iObj) );
931 assert( Cbs2_QueIsEmpty( pQue ) );
932 Cbs2_QuePush( pQue, 0 );
933 Cbs2_QuePush( pQue, 0 );
934 // for ( i = hClause0 + 1; (iObj = pQue->pData[i]); i++ )
935 Cbs2_ClauseForEachEntry1( p, hClause0, iObj, i )
936 {
937 if ( Cbs2_VarMark0(p, iObj) ) // unassigned - seen again
938 continue;
939 //if ( Vec_IntEntry(&p->vActivity, iObj) == 0 )
940 // Vec_IntPush( &p->vActStore, iObj );
941 //Vec_IntAddToEntry( &p->vActivity, iObj, 1 );
942 // assigned - seen first time
943 Cbs2_VarSetMark0(p, iObj, 1);
944 Cbs2_QuePush( pQue, iObj );
945 LevelCur = Cbs2_VarDecLevel( p, iObj );
946 if ( LevelMax < LevelCur )
947 LevelMax = LevelCur;
948 }
949 // for ( i = hClause1 + 1; (iObj = pQue->pData[i]); i++ )
950 Cbs2_ClauseForEachEntry1( p, hClause1, iObj, i )
951 {
952 if ( Cbs2_VarMark0(p, iObj) ) // unassigned - seen again
953 continue;
954 //if ( Vec_IntEntry(&p->vActivity, iObj) == 0 )
955 // Vec_IntPush( &p->vActStore, iObj );
956 //Vec_IntAddToEntry( &p->vActivity, iObj, 1 );
957 // assigned - seen first time
958 Cbs2_VarSetMark0(p, iObj, 1);
959 Cbs2_QuePush( pQue, iObj );
960 LevelCur = Cbs2_VarDecLevel( p, iObj );
961 if ( LevelMax < LevelCur )
962 LevelMax = LevelCur;
963 }
964 for ( i = pQue->iHead + 2; i < pQue->iTail; i++ )
965 Cbs2_VarSetMark0(p, pQue->pData[i], 0);
966 return Cbs2_ManDeriveReason( p, LevelMax );
967 }
968
969 /**Function*************************************************************
970
971 Synopsis [Propagates a variable.]
972
973 Description [Returns clause handle if conflict; 0 if no conflict.]
974
975 SideEffects []
976
977 SeeAlso []
978
979 ***********************************************************************/
Cbs2_ManPropagateOne(Cbs2_Man_t * p,int iVar,int Level)980 static inline int Cbs2_ManPropagateOne( Cbs2_Man_t * p, int iVar, int Level )
981 {
982 Gia_Obj_t * pVar = Gia_ManObj( p->pAig, iVar ); int Value0, Value1;
983 assert( !Gia_IsComplement(pVar) );
984 assert( Cbs2_VarIsAssigned(p, iVar) );
985 if ( Gia_ObjIsCi(pVar) )
986 return 0;
987 p->nPropCalls[0]++;
988 assert( Gia_ObjIsAnd(pVar) );
989 Value0 = Cbs2_VarFanin0Value(p, pVar, iVar);
990 Value1 = Cbs2_VarFanin1Value(p, pVar, iVar);
991 if ( Cbs2_VarValue(p, iVar) == 1 )
992 { // value is 1
993 if ( Value0 == 0 || Value1 == 0 ) // one is 0
994 {
995 if ( Value0 == 0 && Value1 != 0 )
996 return Cbs2_ManAnalyze( p, Level, iVar, Gia_ObjFaninId0(pVar, iVar), 0 );
997 if ( Value0 != 0 && Value1 == 0 )
998 return Cbs2_ManAnalyze( p, Level, iVar, Gia_ObjFaninId1(pVar, iVar), 0 );
999 assert( Value0 == 0 && Value1 == 0 );
1000 return Cbs2_ManAnalyze( p, Level, iVar, Gia_ObjFaninId0(pVar, iVar), Gia_ObjFaninId1(pVar, iVar) );
1001 }
1002 if ( Value0 >= 2 ) // first is unassigned
1003 Cbs2_ManAssign( p, Gia_ObjFaninLit0(pVar, iVar), Level, iVar, 0 );
1004 if ( Value1 >= 2 ) // first is unassigned
1005 Cbs2_ManAssign( p, Gia_ObjFaninLit1(pVar, iVar), Level, iVar, 0 );
1006 return 0;
1007 }
1008 // value is 0
1009 if ( Value0 == 0 || Value1 == 0 ) // one is 0
1010 return 0;
1011 if ( Value0 == 1 && Value1 == 1 ) // both are 1
1012 return Cbs2_ManAnalyze( p, Level, iVar, Gia_ObjFaninId0(pVar, iVar), Gia_ObjFaninId1(pVar, iVar) );
1013 if ( Value0 == 1 || Value1 == 1 ) // one is 1
1014 {
1015 if ( Value0 >= 2 ) // first is unassigned
1016 Cbs2_ManAssign( p, Abc_LitNot(Gia_ObjFaninLit0(pVar, iVar)), Level, iVar, Gia_ObjFaninId1(pVar, iVar) );
1017 if ( Value1 >= 2 ) // second is unassigned
1018 Cbs2_ManAssign( p, Abc_LitNot(Gia_ObjFaninLit1(pVar, iVar)), Level, iVar, Gia_ObjFaninId0(pVar, iVar) );
1019 return 0;
1020 }
1021 assert( Cbs2_VarIsJust(p, pVar, iVar) );
1022 //assert( !Cbs2_QueHasNode( &p->pJust, iVar ) );
1023 if ( !p->Pars.fUseFanout )
1024 Cbs2_QuePush( &p->pJust, iVar );
1025 return 0;
1026 }
1027
1028 /**Function*************************************************************
1029
1030 Synopsis [Propagates a variable.]
1031
1032 Description [Returns 1 if conflict; 0 if no conflict.]
1033
1034 SideEffects []
1035
1036 SeeAlso []
1037
1038 ***********************************************************************/
Cbs2_ManPropagateTwo(Cbs2_Man_t * p,int iVar,int Level)1039 static inline int Cbs2_ManPropagateTwo( Cbs2_Man_t * p, int iVar, int Level )
1040 {
1041 Gia_Obj_t * pVar = Gia_ManObj( p->pAig, iVar ); int Value0, Value1;
1042 assert( !Gia_IsComplement(pVar) );
1043 assert( Gia_ObjIsAnd(pVar) );
1044 assert( Cbs2_VarIsAssigned(p, iVar) );
1045 assert( Cbs2_VarValue(p, iVar) == 0 );
1046 Value0 = Cbs2_VarFanin0Value(p, pVar, iVar);
1047 Value1 = Cbs2_VarFanin1Value(p, pVar, iVar);
1048 p->nPropCalls[1]++;
1049 // value is 0
1050 if ( Value0 == 0 || Value1 == 0 ) // one is 0
1051 return 0;
1052 if ( Value0 == 1 && Value1 == 1 ) // both are 1
1053 return Cbs2_ManAnalyze( p, Level, iVar, Gia_ObjFaninId0(pVar, iVar), Gia_ObjFaninId1(pVar, iVar) );
1054 assert( Value0 == 1 || Value1 == 1 );
1055 if ( Value0 >= 2 ) // first is unassigned
1056 Cbs2_ManAssign( p, Abc_LitNot(Gia_ObjFaninLit0(pVar, iVar)), Level, iVar, Gia_ObjFaninId1(pVar, iVar) );
1057 if ( Value1 >= 2 ) // first is unassigned
1058 Cbs2_ManAssign( p, Abc_LitNot(Gia_ObjFaninLit1(pVar, iVar)), Level, iVar, Gia_ObjFaninId0(pVar, iVar) );
1059 return 0;
1060 }
1061
1062 /**Function*************************************************************
1063
1064 Synopsis [Propagates a variable.]
1065
1066 Description [Returns 1 if conflict; 0 if no conflict.]
1067
1068 SideEffects []
1069
1070 SeeAlso []
1071
1072 ***********************************************************************/
Cbs2_ManPropagateUnassigned(Cbs2_Man_t * p,int iVar,int Level)1073 static inline void Cbs2_ManPropagateUnassigned( Cbs2_Man_t * p, int iVar, int Level )
1074 {
1075 Gia_Obj_t * pVar = Gia_ManObj( p->pAig, iVar ); int Value0, Value1;
1076 assert( !Gia_IsComplement(pVar) );
1077 assert( Gia_ObjIsAnd(pVar) );
1078 assert( !Cbs2_VarIsAssigned(p, iVar) );
1079 Value0 = Cbs2_VarFanin0Value(p, pVar, iVar);
1080 Value1 = Cbs2_VarFanin1Value(p, pVar, iVar);
1081 p->nPropCalls[2]++;
1082 if ( Value0 == 0 && Value1 == 0 ) // the output becomes 1
1083 Cbs2_ManAssign( p, Abc_Var2Lit(iVar, 1), Level, Gia_ObjFaninId0(pVar, iVar), Gia_ObjFaninId1(pVar, iVar) );
1084 else if ( Value0 == 0 ) // the output becomes 0
1085 Cbs2_ManAssign( p, Abc_Var2Lit(iVar, 1), Level, Gia_ObjFaninId0(pVar, iVar), 0 );
1086 else if ( Value1 == 0 ) // the output becomes 0
1087 Cbs2_ManAssign( p, Abc_Var2Lit(iVar, 1), Level, Gia_ObjFaninId1(pVar, iVar), 0 );
1088 else if ( Value0 == 1 && Value1 == 1 ) // the output becomes 1
1089 Cbs2_ManAssign( p, Abc_Var2Lit(iVar, 0), Level, Gia_ObjFaninId0(pVar, iVar), Gia_ObjFaninId1(pVar, iVar) );
1090 }
1091
1092 /**Function*************************************************************
1093
1094 Synopsis [Propagates all variables.]
1095
1096 Description [Returns 1 if conflict; 0 if no conflict.]
1097
1098 SideEffects []
1099
1100 SeeAlso []
1101
1102 ***********************************************************************/
Cbs2_ManPropagate(Cbs2_Man_t * p,int Level)1103 int Cbs2_ManPropagate( Cbs2_Man_t * p, int Level )
1104 {
1105 while ( 1 )
1106 {
1107 int i, k, iVar, iLit, hClause;
1108 Cbs2_QueForEachEntry( p->pProp, iLit, i )
1109 {
1110 if ( (hClause = Cbs2_ManPropagateOne( p, Abc_Lit2Var(iLit), Level )) )
1111 return hClause;
1112 }
1113 p->pProp.iHead = p->pProp.iTail;
1114 k = p->pJust.iHead;
1115 Cbs2_QueForEachEntry( p->pJust, iVar, i )
1116 {
1117 if ( Cbs2_VarIsJust(p, Gia_ManObj(p->pAig, iVar), iVar) )
1118 p->pJust.pData[k++] = iVar;
1119 else if ( (hClause = Cbs2_ManPropagateTwo( p, iVar, Level )) )
1120 return hClause;
1121 }
1122 if ( k == p->pJust.iTail )
1123 break;
1124 p->pJust.iTail = k;
1125 }
1126 return 0;
1127 }
1128
1129
Cbs2_ManPropagate2(Cbs2_Man_t * p,int Level)1130 int Cbs2_ManPropagate2( Cbs2_Man_t * p, int Level )
1131 {
1132 int i, iLit, iFan, hClause;
1133 Cbs2_QueForEachEntry( p->pProp, iLit, i )
1134 {
1135 if ( (hClause = Cbs2_ManPropagateClauses(p, Level, iLit)) )
1136 return hClause;
1137 Cbs2_ObjForEachFanout( p, Abc_Lit2Var(iLit), iFan )
1138 {
1139 int iFanout = Abc_Lit2Var(iFan);
1140 if ( !Cbs2_VarIsAssigned(p, iFanout) )
1141 Cbs2_ManPropagateUnassigned( p, iFanout, Level );
1142 else if ( (hClause = Cbs2_ManPropagateOne(p, iFanout, Level)) )
1143 return hClause;
1144 }
1145 if ( (hClause = Cbs2_ManPropagateOne( p, Abc_Lit2Var(iLit), Level )) )
1146 return hClause;
1147 }
1148 p->pProp.iHead = p->pProp.iTail;
1149 return 0;
1150 }
1151
1152
1153 /**Function*************************************************************
1154
1155 Synopsis [Updates J-frontier.]
1156
1157 Description [Returns 1 if found SAT; 0 if continues solving.]
1158
1159 SideEffects []
1160
1161 SeeAlso []
1162
1163 ***********************************************************************/
Cbs2_ManUpdateDecVar2(Cbs2_Man_t * p,int iObj,int iDecLit)1164 static inline int Cbs2_ManUpdateDecVar2( Cbs2_Man_t * p, int iObj, int iDecLit )
1165 {
1166 Gia_Obj_t * pObj = Gia_ManObj(p->pAig, iObj); int iFan;
1167
1168 iFan = Gia_ObjFaninId0(pObj, iObj);
1169 if ( iDecLit == -1 || Gia_ObjLevelId(p->pAig, Abc_Lit2Var(iDecLit)) < Gia_ObjLevelId(p->pAig, iFan) )
1170 iDecLit = Abc_LitNot(Gia_ObjFaninLit0(pObj, iObj));
1171
1172 iFan = Gia_ObjFaninId1(pObj, iObj);
1173 if ( iDecLit == -1 || Gia_ObjLevelId(p->pAig, Abc_Lit2Var(iDecLit)) < Gia_ObjLevelId(p->pAig, iFan) )
1174 iDecLit = Abc_LitNot(Gia_ObjFaninLit1(pObj, iObj));
1175
1176 return iDecLit;
1177 }
Cbs2_ManUpdateDecVar3(Cbs2_Man_t * p,int iObj,int iDecLit)1178 static inline int Cbs2_ManUpdateDecVar3( Cbs2_Man_t * p, int iObj, int iDecLit )
1179 {
1180 Gia_Obj_t * pObj = Gia_ManObj(p->pAig, iObj); int iFan;
1181
1182 iFan = Gia_ObjFaninId0(pObj, iObj);
1183 if ( iDecLit == -1 || Vec_IntEntry(&p->vActivity, Abc_Lit2Var(iDecLit)) < Vec_IntEntry(&p->vActivity, iFan) )
1184 iDecLit = Abc_LitNot(Gia_ObjFaninLit0(pObj, iObj));
1185
1186 iFan = Gia_ObjFaninId1(pObj, iObj);
1187 if ( iDecLit == -1 || Vec_IntEntry(&p->vActivity, Abc_Lit2Var(iDecLit)) < Vec_IntEntry(&p->vActivity, iFan) )
1188 iDecLit = Abc_LitNot(Gia_ObjFaninLit1(pObj, iObj));
1189
1190 return iDecLit;
1191 }
Cbs2_ManUpdateDecVar(Cbs2_Man_t * p,int iObj,int iDecLit)1192 static inline int Cbs2_ManUpdateDecVar( Cbs2_Man_t * p, int iObj, int iDecLit )
1193 {
1194 Gia_Obj_t * pObj = Gia_ManObj(p->pAig, iObj); int iFan;
1195
1196 iFan = Gia_ObjFaninId0(pObj, iObj);
1197 if ( iDecLit == -1 || Gia_ObjRefNumId(p->pAig, Abc_Lit2Var(iDecLit)) < Gia_ObjRefNumId(p->pAig, iFan) )
1198 iDecLit = Abc_LitNot(Gia_ObjFaninLit0(pObj, iObj));
1199
1200 iFan = Gia_ObjFaninId1(pObj, iObj);
1201 if ( iDecLit == -1 || Gia_ObjRefNumId(p->pAig, Abc_Lit2Var(iDecLit)) < Gia_ObjRefNumId(p->pAig, iFan) )
1202 iDecLit = Abc_LitNot(Gia_ObjFaninLit1(pObj, iObj));
1203
1204 return iDecLit;
1205 }
Cbs2_ManUpdateFrontier(Cbs2_Man_t * p,int iPropHeadOld,int * piDecLit)1206 int Cbs2_ManUpdateFrontier( Cbs2_Man_t * p, int iPropHeadOld, int * piDecLit )
1207 {
1208 abctime clk = Abc_Clock();
1209 int i, iVar, iLit, iJustTailOld = p->pJust.iTail;
1210 *piDecLit = -1;
1211 assert( Cbs2_QueIsEmpty(&p->pProp) );
1212 // visit old frontier nodes
1213 Cbs2_QueForEachEntry( p->pJust, iVar, i )
1214 if ( i == iJustTailOld )
1215 break;
1216 else if ( Cbs2_VarIsJust(p, Gia_ManObj(p->pAig, iVar), iVar) )
1217 {
1218 Cbs2_QuePush( &p->pJust, iVar );
1219 //*piDecLit = Cbs2_ManUpdateDecVar( p, iVar, *piDecLit );
1220 }
1221 // append new nodes
1222 p->pProp.iHead = iPropHeadOld;
1223 Cbs2_QueForEachEntry( p->pProp, iLit, i )
1224 {
1225 iVar = Abc_Lit2Var(iLit);
1226 if ( Cbs2_VarIsJust(p, Gia_ManObj(p->pAig, iVar), iVar) )
1227 {
1228 Cbs2_QuePush( &p->pJust, iVar );
1229 //*piDecLit = Cbs2_ManUpdateDecVar( p, iVar, *piDecLit );
1230 }
1231 }
1232 p->pProp.iHead = p->pProp.iTail;
1233 // update the head of the frontier
1234 p->pJust.iHead = iJustTailOld;
1235 // return 1 if the queue is empty
1236 p->timeJFront += Abc_Clock() - clk;
1237 //printf( "%d ", p->pJust.iTail - p->pJust.iHead );
1238 return Cbs2_QueIsEmpty(&p->pJust);
1239 }
1240
1241 /**Function*************************************************************
1242
1243 Synopsis [Solve the problem recursively.]
1244
1245 Description [Returns learnt clause if unsat, NULL if sat or undecided.]
1246
1247 SideEffects []
1248
1249 SeeAlso []
1250
1251 ***********************************************************************/
1252
Cbs2_ManSolve1_rec(Cbs2_Man_t * p,int Level)1253 int Cbs2_ManSolve1_rec( Cbs2_Man_t * p, int Level )
1254 {
1255 Gia_Obj_t * pVar;
1256 Cbs2_Que_t * pQue = &(p->pClauses);
1257 int iPropHead, iJustHead, iJustTail;
1258 int hClause, hLearn0, hLearn1, iVar, iDecLit;
1259 // propagate assignments
1260 assert( !Cbs2_QueIsEmpty(&p->pProp) );
1261 if ( (hClause = Cbs2_ManPropagate( p, Level )) )
1262 return hClause;
1263 // check for satisfying assignment
1264 assert( Cbs2_QueIsEmpty(&p->pProp) );
1265 if ( Cbs2_QueIsEmpty(&p->pJust) )
1266 return 0;
1267 // quit using resource limits
1268 p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
1269 if ( Cbs2_ManCheckLimits( p ) )
1270 return 0;
1271 // remember the state before branching
1272 iPropHead = p->pProp.iHead;
1273 Cbs2_QueStore( &p->pJust, &iJustHead, &iJustTail );
1274 // find the decision variable
1275 assert( p->Pars.fUseHighest );
1276 iVar = Cbs2_ManDecideHighest( p );
1277 pVar = Gia_ManObj( p->pAig, iVar );
1278 assert( Cbs2_VarIsJust(p, pVar, iVar) );
1279 // chose decision variable using fanout count
1280 if ( Gia_ObjRefNum(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefNum(p->pAig, Gia_ObjFanin1(pVar)) )
1281 iDecLit = Abc_LitNot(Gia_ObjFaninLit0(pVar, iVar));
1282 else
1283 iDecLit = Abc_LitNot(Gia_ObjFaninLit1(pVar, iVar));
1284 // decide on first fanin
1285 Cbs2_ManAssign( p, iDecLit, Level+1, 0, 0 );
1286 if ( !(hLearn0 = Cbs2_ManSolve1_rec( p, Level+1 )) )
1287 return 0;
1288 if ( pQue->pData[hLearn0+1] != Abc_Lit2Var(iDecLit) )
1289 return hLearn0;
1290 Cbs2_ManCancelUntil( p, iPropHead );
1291 Cbs2_QueRestore( &p->pJust, iJustHead, iJustTail );
1292 // decide on second fanin
1293 Cbs2_ManAssign( p, Abc_LitNot(iDecLit), Level+1, 0, 0 );
1294 if ( !(hLearn1 = Cbs2_ManSolve1_rec( p, Level+1 )) )
1295 return 0;
1296 if ( pQue->pData[hLearn1+1] != Abc_Lit2Var(iDecLit) )
1297 return hLearn1;
1298 hClause = Cbs2_ManResolve( p, Level, hLearn0, hLearn1 );
1299 Cbs2_ManBumpClause( p, hClause );
1300 // Cbs2_ManPrintCube( p, Level, hClause );
1301 // if ( Level > Cbs2_ClauseDecLevel(p, hClause) )
1302 // p->Pars.nBTThisNc++;
1303 p->Pars.nBTThis++;
1304 return hClause;
1305 }
1306
Cbs2_ManSolve2_rec(Cbs2_Man_t * p,int Level)1307 int Cbs2_ManSolve2_rec( Cbs2_Man_t * p, int Level )
1308 {
1309 Gia_Obj_t * pVar;
1310 Cbs2_Que_t * pQue = &(p->pClauses);
1311 int iPropHead, iJustHead, iJustTail;
1312 int hClause, hLearn0, hLearn1, iVar, iDecLit, iDecLit2;
1313 int iPropHeadOld = p->pProp.iHead;
1314 // propagate assignments
1315 assert( !Cbs2_QueIsEmpty(&p->pProp) );
1316 if ( (hClause = Cbs2_ManPropagate2( p, Level )) )
1317 return hClause;
1318 // check for satisfying assignment
1319 assert( Cbs2_QueIsEmpty(&p->pProp) );
1320 // if ( Cbs2_QueIsEmpty(&p->pJust) )
1321 // return 0;
1322 if ( Cbs2_ManUpdateFrontier(p, iPropHeadOld, &iDecLit2) )
1323 return 0;
1324 // quit using resource limits
1325 p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
1326 if ( Cbs2_ManCheckLimits( p ) )
1327 return 0;
1328 // remember the state before branching
1329 iPropHead = p->pProp.iHead;
1330 // Cbs2_QueStore( &p->pJust, &iJustHead, &iJustTail );
1331 iJustHead = p->pJust.iHead;
1332 iJustTail = p->pJust.iTail;
1333 // find the decision variable
1334
1335 assert( p->Pars.fUseHighest );
1336 iVar = Cbs2_ManDecideHighest( p );
1337 pVar = Gia_ManObj( p->pAig, iVar );
1338 assert( Cbs2_VarIsJust(p, pVar, iVar) );
1339 // chose decision variable using fanout count
1340 if ( Gia_ObjRefNum(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefNum(p->pAig, Gia_ObjFanin1(pVar)) )
1341 // if ( Vec_IntEntry(&p->vActivity, Gia_ObjFaninId0(pVar, iVar)) > Vec_IntEntry(&p->vActivity, Gia_ObjFaninId1(pVar, iVar)) )
1342 iDecLit = Abc_LitNot(Gia_ObjFaninLit0(pVar, iVar));
1343 else
1344 iDecLit = Abc_LitNot(Gia_ObjFaninLit1(pVar, iVar));
1345
1346 //iDecLit = iDecLit2;
1347
1348 // decide on first fanin
1349 Cbs2_ManAssign( p, iDecLit, Level+1, 0, 0 );
1350 if ( !(hLearn0 = Cbs2_ManSolve2_rec( p, Level+1 )) )
1351 return 0;
1352 if ( pQue->pData[hLearn0+1] != Abc_Lit2Var(iDecLit) )
1353 return hLearn0;
1354 Cbs2_ManCancelUntil( p, iPropHead );
1355 Cbs2_QueRestore( &p->pJust, iJustHead, iJustTail );
1356 // decide on second fanin
1357 Cbs2_ManAssign( p, Abc_LitNot(iDecLit), Level+1, 0, 0 );
1358 if ( !(hLearn1 = Cbs2_ManSolve2_rec( p, Level+1 )) )
1359 return 0;
1360 if ( pQue->pData[hLearn1+1] != Abc_Lit2Var(iDecLit) )
1361 return hLearn1;
1362 hClause = Cbs2_ManResolve( p, Level, hLearn0, hLearn1 );
1363 Cbs2_ManBumpClause( p, hClause );
1364 //Cbs2_ManPrintCube( p, Level, hClause );
1365 // if ( Level > Cbs2_ClauseDecLevel(p, hClause) )
1366 // p->Pars.nBTThisNc++;
1367 p->Pars.nBTThis++;
1368 return hClause;
1369 }
1370
Cbs2_ManSolve_rec(Cbs2_Man_t * p,int Level)1371 int Cbs2_ManSolve_rec( Cbs2_Man_t * p, int Level )
1372 {
1373 return p->Pars.fUseFanout ? Cbs2_ManSolve2_rec(p, Level) : Cbs2_ManSolve1_rec(p, Level);
1374 }
1375
1376 /**Function*************************************************************
1377
1378 Synopsis [Looking for a satisfying assignment of the node.]
1379
1380 Description [Assumes that each node has flag pObj->fMark0 set to 0.
1381 Returns 1 if unsatisfiable, 0 if satisfiable, and -1 if undecided.
1382 The node may be complemented. ]
1383
1384 SideEffects [The two procedures differ in the CEX format.]
1385
1386 SeeAlso []
1387
1388 ***********************************************************************/
Cbs2_ManSolve(Cbs2_Man_t * p,int iLit)1389 int Cbs2_ManSolve( Cbs2_Man_t * p, int iLit )
1390 {
1391 int RetValue = 0;
1392 assert( !p->pProp.iHead && !p->pProp.iTail );
1393 assert( !p->pJust.iHead && !p->pJust.iTail );
1394 assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
1395 p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
1396 Cbs2_ManAssign( p, iLit, 0, 0, 0 );
1397 if ( !Cbs2_ManSolve_rec(p, 0) && !Cbs2_ManCheckLimits(p) )
1398 Cbs2_ManSaveModel( p, p->vModel );
1399 else
1400 RetValue = 1;
1401 Cbs2_ManCancelUntil( p, 0 );
1402 Cbs2_ManCleanWatch( p );
1403 Cbs2_ManBumpClean( p );
1404 p->pJust.iHead = p->pJust.iTail = 0;
1405 p->pClauses.iHead = p->pClauses.iTail = 1;
1406 p->Pars.nBTTotal += p->Pars.nBTThis;
1407 p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
1408 if ( Cbs2_ManCheckLimits( p ) )
1409 RetValue = -1;
1410 return RetValue;
1411 }
Cbs2_ManSolve2(Cbs2_Man_t * p,int iLit,int iLit2)1412 int Cbs2_ManSolve2( Cbs2_Man_t * p, int iLit, int iLit2 )
1413 {
1414 int RetValue = 0;
1415 assert( !p->pProp.iHead && !p->pProp.iTail );
1416 assert( !p->pJust.iHead && !p->pJust.iTail );
1417 assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 );
1418 p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0;
1419 Cbs2_ManAssign( p, iLit, 0, 0, 0 );
1420 if ( iLit2 )
1421 Cbs2_ManAssign( p, iLit2, 0, 0, 0 );
1422 if ( !Cbs2_ManSolve_rec(p, 0) && !Cbs2_ManCheckLimits(p) )
1423 Cbs2_ManSaveModelAll( p, p->vModel );
1424 else
1425 RetValue = 1;
1426 Cbs2_ManCancelUntil( p, 0 );
1427 Cbs2_ManCleanWatch( p );
1428 Cbs2_ManBumpClean( p );
1429 p->pJust.iHead = p->pJust.iTail = 0;
1430 p->pClauses.iHead = p->pClauses.iTail = 1;
1431 p->Pars.nBTTotal += p->Pars.nBTThis;
1432 p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
1433 if ( Cbs2_ManCheckLimits( p ) )
1434 RetValue = -1;
1435 return RetValue;
1436 }
1437
1438 /**Function*************************************************************
1439
1440 Synopsis [Prints statistics of the manager.]
1441
1442 Description []
1443
1444 SideEffects []
1445
1446 SeeAlso []
1447
1448 ***********************************************************************/
Cbs2_ManSatPrintStats(Cbs2_Man_t * p)1449 void Cbs2_ManSatPrintStats( Cbs2_Man_t * p )
1450 {
1451 printf( "CO = %8d ", Gia_ManCoNum(p->pAig) );
1452 printf( "AND = %8d ", Gia_ManAndNum(p->pAig) );
1453 printf( "Conf = %6d ", p->Pars.nBTLimit );
1454 printf( "JustMax = %5d ", p->Pars.nJustLimit );
1455 printf( "\n" );
1456 printf( "Unsat calls %6d (%6.2f %%) Ave conf = %8.1f ",
1457 p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
1458 ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
1459 printf( "Sat calls %6d (%6.2f %%) Ave conf = %8.1f ",
1460 p->nSatSat, p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
1461 ABC_PRTP( "Time", p->timeSatSat, p->timeTotal );
1462 printf( "Undef calls %6d (%6.2f %%) Ave conf = %8.1f ",
1463 p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
1464 ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
1465 ABC_PRT( "Total time", p->timeTotal );
1466 }
1467
1468 /**Function*************************************************************
1469
1470 Synopsis [Create fanout.]
1471
1472 Description []
1473
1474 SideEffects []
1475
1476 SeeAlso []
1477
1478 ***********************************************************************/
Cbs2_ObjPrintFanouts(Cbs2_Man_t * p,int iObj)1479 void Cbs2_ObjPrintFanouts( Cbs2_Man_t * p, int iObj )
1480 {
1481 int iFanLit;
1482 printf( "Fanouts of node %d: ", iObj );
1483 Cbs2_ObjForEachFanout( p, iObj, iFanLit )
1484 printf( "%d ", Abc_Lit2Var(iFanLit) );
1485 printf( "\n" );
1486 }
1487
Cbs2_ManPrintFanouts(Cbs2_Man_t * p)1488 void Cbs2_ManPrintFanouts( Cbs2_Man_t * p )
1489 {
1490 Gia_Obj_t * pObj; int iObj;
1491 Gia_ManForEachObj( p->pAig, pObj, iObj )
1492 if ( Vec_IntEntry(&p->vFanout0, iObj) )
1493 Cbs2_ObjPrintFanouts( p, iObj );
1494 }
Cbs2_ObjCreateFanout(Cbs2_Man_t * p,int iObj,int iFan0,int iFan1)1495 void Cbs2_ObjCreateFanout( Cbs2_Man_t * p, int iObj, int iFan0, int iFan1 )
1496 {
1497 Vec_IntWriteEntry( &p->vFanoutN, Abc_Var2Lit(iObj, 0), Vec_IntEntry(&p->vFanout0, iFan0) );
1498 Vec_IntWriteEntry( &p->vFanoutN, Abc_Var2Lit(iObj, 1), Vec_IntEntry(&p->vFanout0, iFan1) );
1499 Vec_IntWriteEntry( &p->vFanout0, iFan0, Abc_Var2Lit(iObj, 0) );
1500 Vec_IntWriteEntry( &p->vFanout0, iFan1, Abc_Var2Lit(iObj, 1) );
1501 }
Cbs2_ObjDeleteFanout(Cbs2_Man_t * p,int iObj)1502 void Cbs2_ObjDeleteFanout( Cbs2_Man_t * p, int iObj )
1503 {
1504 Vec_IntWriteEntry( &p->vFanoutN, Abc_Var2Lit(iObj, 0), 0 );
1505 Vec_IntWriteEntry( &p->vFanoutN, Abc_Var2Lit(iObj, 1), 0 );
1506 Vec_IntWriteEntry( &p->vFanout0, iObj, 0 );
1507 }
Cbs2_ManCreateFanout_rec(Cbs2_Man_t * p,int iObj)1508 void Cbs2_ManCreateFanout_rec( Cbs2_Man_t * p, int iObj )
1509 {
1510 Gia_Obj_t * pObj; int iFan0, iFan1;
1511 if ( !iObj || Gia_ObjIsTravIdCurrentId(p->pAig, iObj) )
1512 return;
1513 Gia_ObjSetTravIdCurrentId(p->pAig, iObj);
1514 pObj = Gia_ManObj(p->pAig, iObj);
1515 if ( Gia_ObjIsCi(pObj) )
1516 return;
1517 assert( Gia_ObjIsAnd(pObj) );
1518 iFan0 = Gia_ObjFaninId0(pObj, iObj);
1519 iFan1 = Gia_ObjFaninId1(pObj, iObj);
1520 Cbs2_ManCreateFanout_rec( p, iFan0 );
1521 Cbs2_ManCreateFanout_rec( p, iFan1 );
1522 Cbs2_ObjCreateFanout( p, iObj, iFan0, iFan1 );
1523 }
Cbs2_ManDeleteFanout_rec(Cbs2_Man_t * p,int iObj)1524 void Cbs2_ManDeleteFanout_rec( Cbs2_Man_t * p, int iObj )
1525 {
1526 Gia_Obj_t * pObj = Gia_ManObj(p->pAig, iObj); int iFan0, iFan1;
1527 Cbs2_ObjDeleteFanout( p, iObj );
1528 if ( Gia_ObjIsCi(pObj) )
1529 return;
1530 assert( Gia_ObjIsAnd(pObj) );
1531 iFan0 = Gia_ObjFaninId0(pObj, iObj);
1532 iFan1 = Gia_ObjFaninId1(pObj, iObj);
1533 if ( Vec_IntEntry(&p->vFanout0, iFan0) ) Cbs2_ManDeleteFanout_rec( p, iFan0 );
1534 if ( Vec_IntEntry(&p->vFanout0, iFan1) ) Cbs2_ManDeleteFanout_rec( p, iFan1 );
1535 }
Cbs2_ManCheckFanouts(Cbs2_Man_t * p)1536 void Cbs2_ManCheckFanouts( Cbs2_Man_t * p )
1537 {
1538 Gia_Obj_t * pObj;
1539 int iObj;
1540 Gia_ManForEachObj( p->pAig, pObj, iObj )
1541 {
1542 assert( Vec_IntEntry(&p->vFanout0, iObj) == 0 );
1543 assert( Vec_IntEntry(&p->vFanoutN, Abc_Var2Lit(iObj, 0)) == 0 );
1544 assert( Vec_IntEntry(&p->vFanoutN, Abc_Var2Lit(iObj, 1)) == 0 );
1545 }
1546 }
1547
1548 /**Function*************************************************************
1549
1550 Synopsis [Procedure to test the new SAT solver.]
1551
1552 Description []
1553
1554 SideEffects []
1555
1556 SeeAlso []
1557
1558 ***********************************************************************/
Cbs2_ManSolveMiterNc(Gia_Man_t * pAig,int nConfs,Vec_Str_t ** pvStatus,int fVerbose)1559 Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
1560 {
1561 extern void Gia_ManCollectTest( Gia_Man_t * pAig );
1562 extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
1563 Cbs2_Man_t * p;
1564 Vec_Int_t * vCex, * vVisit, * vCexStore;
1565 Vec_Str_t * vStatus;
1566 Gia_Obj_t * pRoot;
1567 int i, status;
1568 abctime clk, clkTotal = Abc_Clock();
1569 assert( Gia_ManRegNum(pAig) == 0 );
1570 // Gia_ManCollectTest( pAig );
1571 // prepare AIG
1572 Gia_ManCreateRefs( pAig );
1573 //Gia_ManLevelNum( pAig );
1574 //Gia_ManCleanMark0( pAig );
1575 //Gia_ManCleanMark1( pAig );
1576 //Gia_ManFillValue( pAig ); // maps nodes into trail ids
1577 //Gia_ManSetPhase( pAig ); // maps nodes into trail ids
1578 // create logic network
1579 p = Cbs2_ManAlloc( pAig );
1580 p->Pars.nBTLimit = nConfs;
1581 // create resulting data-structures
1582 vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
1583 vCexStore = Vec_IntAlloc( 10000 );
1584 vVisit = Vec_IntAlloc( 100 );
1585 vCex = Cbs2_ReadModel( p );
1586 // solve for each output
1587 Gia_ManForEachCo( pAig, pRoot, i )
1588 {
1589 //printf( "\nOutput %d\n", i );
1590
1591 Vec_IntClear( vCex );
1592 if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
1593 {
1594 if ( Gia_ObjFaninC0(pRoot) )
1595 {
1596 // printf( "Constant 1 output of SRM!!!\n" );
1597 Cec_ManSatAddToStore( vCexStore, vCex, i ); // trivial counter-example
1598 Vec_StrPush( vStatus, 0 );
1599 }
1600 else
1601 {
1602 // printf( "Constant 0 output of SRM!!!\n" );
1603 Vec_StrPush( vStatus, 1 );
1604 }
1605 continue;
1606 }
1607 clk = Abc_Clock();
1608 p->Pars.fUseHighest = 1;
1609 p->Pars.fUseLowest = 0;
1610
1611 Gia_ManIncrementTravId( pAig );
1612 Cbs2_ManCreateFanout_rec( p, Gia_ObjFaninId0p(pAig, pRoot) );
1613 //Cbs2_ManPrintFanouts( p );
1614
1615 status = Cbs2_ManSolve( p, Gia_ObjFaninLit0p(pAig, pRoot) );
1616 //printf( "\n" );
1617
1618 Cbs2_ManDeleteFanout_rec( p, Gia_ObjFaninId0p(pAig, pRoot) );
1619 //Cbs2_ManCheckFanouts( p );
1620
1621 /*
1622 if ( status == -1 )
1623 {
1624 p->Pars.fUseHighest = 0;
1625 p->Pars.fUseLowest = 1;
1626 status = Cbs2_ManSolve( p, Gia_ObjChild0(pRoot) );
1627 }
1628 */
1629 Vec_StrPush( vStatus, (char)status );
1630 if ( status == -1 )
1631 {
1632 p->nSatUndec++;
1633 p->nConfUndec += p->Pars.nBTThis;
1634 Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
1635 p->timeSatUndec += Abc_Clock() - clk;
1636 continue;
1637 }
1638 if ( status == 1 )
1639 {
1640 p->nSatUnsat++;
1641 p->nConfUnsat += p->Pars.nBTThis;
1642 p->timeSatUnsat += Abc_Clock() - clk;
1643 continue;
1644 }
1645 p->nSatSat++;
1646 p->nConfSat += p->Pars.nBTThis;
1647 // Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
1648 Cec_ManSatAddToStore( vCexStore, vCex, i );
1649 p->timeSatSat += Abc_Clock() - clk;
1650 }
1651 Vec_IntFree( vVisit );
1652 p->nSatTotal = Gia_ManPoNum(pAig);
1653 p->timeTotal = Abc_Clock() - clkTotal;
1654 if ( fVerbose )
1655 Cbs2_ManSatPrintStats( p );
1656 // printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
1657 printf( "Prop1 = %d. Prop2 = %d. Prop3 = %d. ClaConf = %d. FailJ = %d. FailC = %d. ", p->nPropCalls[0], p->nPropCalls[1], p->nPropCalls[2], p->nClauseConf, p->nFails[0], p->nFails[1] );
1658 Abc_PrintTime( 1, "JFront", p->timeJFront );
1659
1660 Cbs2_ManStop( p );
1661 *pvStatus = vStatus;
1662
1663 // printf( "Total number of cex literals = %d. (Ave = %d)\n",
1664 // Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat,
1665 // (Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat)/p->nSatSat );
1666 return vCexStore;
1667 }
1668
1669
1670 ////////////////////////////////////////////////////////////////////////
1671 /// END OF FILE ///
1672 ////////////////////////////////////////////////////////////////////////
1673
1674
1675 ABC_NAMESPACE_IMPL_END
1676
1677