ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
absGla.c
Go to the documentation of this file.
1
20
21#include "base/main/main.h"
22#include "sat/cnf/cnf.h"
23#include "sat/bsat/satSolver2.h"
24#include "bool/kit/kit.h"
25#include "abs.h"
26#include "absRef.h"
27//#include "absRef2.h"
28
29ABC_NAMESPACE_IMPL_START
30
34
35#define GA2_BIG_NUM 0x3FFFFFF0
36
37typedef struct Ga2_Man_t_ Ga2_Man_t; // manager
38struct Ga2_Man_t_
39{
40 // user data
41 Gia_Man_t * pGia; // working AIG manager
42 Abs_Par_t * pPars; // parameters
43 // markings
44 Vec_Ptr_t * vCnfs; // for each object: CNF0, CNF1
45 // abstraction
46 Vec_Int_t * vIds; // abstraction ID for each GIA object
47 Vec_Int_t * vProofIds; // mapping of GIA objects into their proof IDs
48 Vec_Int_t * vAbs; // array of abstracted objects
49 Vec_Int_t * vValues; // array of objects with abstraction ID assigned
50 int nProofIds; // the counter of proof IDs
51 int LimAbs; // limit value for starting abstraction objects
52 int LimPpi; // limit value for starting PPI objects
53 int nMarked; // total number of marked nodes and flops
54 int fUseNewLine; // remember that you used new line
55 // refinement
56 Rnm_Man_t * pRnm; // refinement manager
57// Rf2_Man_t * pRf2; // refinement manager
58 // SAT solver and variables
59 Vec_Ptr_t * vId2Lit; // mapping, for each timeframe, of object ID into SAT literal
60 sat_solver2 * pSat; // incremental SAT solver
61 int nSatVars; // the number of SAT variables
62 int nCexes; // the number of counter-examples
63 int nObjAdded; // objs added during refinement
64 int nPdrCalls; // count the number of concurrent calls
65 // hash table
66 int * pTable;
67 int nTable;
68 int nHashHit;
69 int nHashMiss;
70 int nHashOver;
71 // temporaries
72 Vec_Int_t * vLits;
73 Vec_Int_t * vIsopMem;
74 char * pSopSizes, ** pSops; // CNF representation
75 // statistics
76 abctime timeStart;
77 abctime timeInit;
78 abctime timeSat;
79 abctime timeUnsat;
80 abctime timeCex;
81 abctime timeOther;
82};
83
84static inline int Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj)); }
85static inline void Ga2_ObjSetId( Ga2_Man_t * p, Gia_Obj_t * pObj, int i ) { Vec_IntWriteEntry(p->vIds, Gia_ObjId(p->pGia, pObj), i); }
86
87static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return (Vec_Int_t *)Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj) ); }
88static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return (Vec_Int_t *)Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)+1 ); }
89
90static inline int Ga2_ObjIsAbs0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return Ga2_ObjId(p,pObj) >= 0 && Ga2_ObjId(p,pObj) < p->LimAbs; }
91static inline int Ga2_ObjIsLeaf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return Ga2_ObjId(p,pObj) >= p->LimAbs && Ga2_ObjId(p,pObj) < p->LimPpi; }
92static inline int Ga2_ObjIsAbs( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Ga2_ObjId(p,pObj) >= 0 && Ga2_ObjCnf0(p,pObj); }
93static inline int Ga2_ObjIsLeaf( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Ga2_ObjId(p,pObj) >= 0 && !Ga2_ObjCnf0(p,pObj); }
94
95static inline Vec_Int_t * Ga2_MapFrameMap( Ga2_Man_t * p, int f ) { return (Vec_Int_t *)Vec_PtrEntry( p->vId2Lit, f ); }
96
97// returns literal of this object, or -1 if SAT variable of the object is not assigned
98static inline int Ga2_ObjFindLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
99{
100// int Id = Ga2_ObjId(p,pObj);
101 assert( Ga2_ObjId(p,pObj) >= 0 && Ga2_ObjId(p,pObj) < Vec_IntSize(p->vValues) );
102 return Vec_IntEntry( Ga2_MapFrameMap(p, f), Ga2_ObjId(p,pObj) );
103}
104// inserts literal of this object
105static inline void Ga2_ObjAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int Lit )
106{
107// assert( Lit > 1 );
108 assert( Ga2_ObjFindLit(p, pObj, f) == -1 );
109 Vec_IntSetEntry( Ga2_MapFrameMap(p, f), Ga2_ObjId(p,pObj), Lit );
110}
111// returns or inserts-and-returns literal of this object
112static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
113{
114 int Lit = Ga2_ObjFindLit( p, pObj, f );
115 if ( Lit == -1 )
116 {
117 Lit = toLitCond( p->nSatVars++, 0 );
118 Ga2_ObjAddLit( p, pObj, f, Lit );
119 }
120// assert( Lit > 1 );
121 return Lit;
122}
123
124
128
140unsigned Ga2_ObjComputeTruth_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fFirst )
141{
142 unsigned Val0, Val1;
143 if ( pObj->fPhase && !fFirst )
144 return pObj->Value;
145 assert( Gia_ObjIsAnd(pObj) );
146 Val0 = Ga2_ObjComputeTruth_rec( p, Gia_ObjFanin0(pObj), 0 );
147 Val1 = Ga2_ObjComputeTruth_rec( p, Gia_ObjFanin1(pObj), 0 );
148 return (Gia_ObjFaninC0(pObj) ? ~Val0 : Val0) & (Gia_ObjFaninC1(pObj) ? ~Val1 : Val1);
149}
150unsigned Ga2_ManComputeTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves )
151{
152 static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
153 Gia_Obj_t * pObj;
154 unsigned Res;
155 int i;
156 Gia_ManForEachObjVec( vLeaves, p, pObj, i )
157 pObj->Value = uTruth5[i];
158 Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
159 Gia_ManForEachObjVec( vLeaves, p, pObj, i )
160 pObj->Value = 0;
161 return Res;
162}
163
176int Ga2_ManBreakTree_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fFirst, int N )
177{ // breaks a tree rooted at the node into N-feasible subtrees
178 int Val0, Val1;
179 if ( pObj->fPhase && !fFirst )
180 return 1;
181 Val0 = Ga2_ManBreakTree_rec( p, Gia_ObjFanin0(pObj), 0, N );
182 Val1 = Ga2_ManBreakTree_rec( p, Gia_ObjFanin1(pObj), 0, N );
183 if ( Val0 + Val1 < N )
184 return Val0 + Val1;
185 if ( Val0 + Val1 == N )
186 {
187 pObj->fPhase = 1;
188 return 1;
189 }
190 assert( Val0 + Val1 > N );
191 assert( Val0 < N && Val1 < N );
192 if ( Val0 >= Val1 )
193 {
194 Gia_ObjFanin0(pObj)->fPhase = 1;
195 Val0 = 1;
196 }
197 else
198 {
199 Gia_ObjFanin1(pObj)->fPhase = 1;
200 Val1 = 1;
201 }
202 if ( Val0 + Val1 < N )
203 return Val0 + Val1;
204 if ( Val0 + Val1 == N )
205 {
206 pObj->fPhase = 1;
207 return 1;
208 }
209 assert( 0 );
210 return -1;
211}
212int Ga2_ManCheckNodesAnd( Gia_Man_t * p, Vec_Int_t * vNodes )
213{
214 Gia_Obj_t * pObj;
215 int i;
216 Gia_ManForEachObjVec( vNodes, p, pObj, i )
217 if ( (!Gia_ObjFanin0(pObj)->fPhase && Gia_ObjFaninC0(pObj)) ||
218 (!Gia_ObjFanin1(pObj)->fPhase && Gia_ObjFaninC1(pObj)) )
219 return 0;
220 return 1;
221}
222void Ga2_ManCollectNodes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes, int fFirst )
223{
224 if ( pObj->fPhase && !fFirst )
225 return;
226 assert( Gia_ObjIsAnd(pObj) );
227 Ga2_ManCollectNodes_rec( p, Gia_ObjFanin0(pObj), vNodes, 0 );
228 Ga2_ManCollectNodes_rec( p, Gia_ObjFanin1(pObj), vNodes, 0 );
229 Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
230
231}
232void Ga2_ManCollectLeaves_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLeaves, int fFirst )
233{
234 if ( pObj->fPhase && !fFirst )
235 {
236 Vec_IntPushUnique( vLeaves, Gia_ObjId(p, pObj) );
237 return;
238 }
239 assert( Gia_ObjIsAnd(pObj) );
240 Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin0(pObj), vLeaves, 0 );
241 Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin1(pObj), vLeaves, 0 );
242}
243int Ga2_ManMarkup( Gia_Man_t * p, int N, int fSimple )
244{
245 static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
246// abctime clk = Abc_Clock();
247 Vec_Int_t * vLeaves;
248 Gia_Obj_t * pObj;
249 int i, k, Leaf, CountMarks;
250
251 vLeaves = Vec_IntAlloc( 100 );
252
253 if ( fSimple )
254 {
255 Gia_ManForEachObj( p, pObj, i )
256 pObj->fPhase = !Gia_ObjIsCo(pObj);
257 }
258 else
259 {
260 // label nodes with multiple fanouts and inputs MUXes
261 Gia_ManForEachObj( p, pObj, i )
262 {
263 pObj->Value = 0;
264 if ( !Gia_ObjIsAnd(pObj) )
265 continue;
266 Gia_ObjFanin0(pObj)->Value++;
267 Gia_ObjFanin1(pObj)->Value++;
268 if ( !Gia_ObjIsMuxType(pObj) )
269 continue;
270 Gia_ObjFanin0(Gia_ObjFanin0(pObj))->Value++;
271 Gia_ObjFanin1(Gia_ObjFanin0(pObj))->Value++;
272 Gia_ObjFanin0(Gia_ObjFanin1(pObj))->Value++;
273 Gia_ObjFanin1(Gia_ObjFanin1(pObj))->Value++;
274 }
275 Gia_ManForEachObj( p, pObj, i )
276 {
277 pObj->fPhase = 0;
278 if ( Gia_ObjIsAnd(pObj) )
279 pObj->fPhase = (pObj->Value > 1);
280 else if ( Gia_ObjIsCo(pObj) )
281 Gia_ObjFanin0(pObj)->fPhase = 1;
282 else
283 pObj->fPhase = 1;
284 }
285 // add marks when needed
286 Gia_ManForEachAnd( p, pObj, i )
287 {
288 if ( !pObj->fPhase )
289 continue;
290 Vec_IntClear( vLeaves );
291 Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 );
292 if ( Vec_IntSize(vLeaves) > N )
293 Ga2_ManBreakTree_rec( p, pObj, 1, N );
294 }
295 }
296
297 // verify that the tree is split correctly
298 Vec_IntFreeP( &p->vMapping );
299 p->vMapping = Vec_IntStart( Gia_ManObjNum(p) );
300 Gia_ManForEachRo( p, pObj, i )
301 {
302 Gia_Obj_t * pObjRi = Gia_ObjRoToRi(p, pObj);
303 assert( pObj->fPhase );
304 assert( Gia_ObjFanin0(pObjRi)->fPhase );
305 // create map
306 Vec_IntWriteEntry( p->vMapping, Gia_ObjId(p, pObj), Vec_IntSize(p->vMapping) );
307 Vec_IntPush( p->vMapping, 1 );
308 Vec_IntPush( p->vMapping, Gia_ObjFaninId0p(p, pObjRi) );
309 Vec_IntPush( p->vMapping, Gia_ObjFaninC0(pObjRi) ? 0x55555555 : 0xAAAAAAAA );
310 Vec_IntPush( p->vMapping, -1 ); // placeholder for ref counter
311 }
312 CountMarks = Gia_ManRegNum(p);
313 Gia_ManForEachAnd( p, pObj, i )
314 {
315 if ( !pObj->fPhase )
316 continue;
317 Vec_IntClear( vLeaves );
318 Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 );
319 assert( Vec_IntSize(vLeaves) <= N );
320 // create map
321 Vec_IntWriteEntry( p->vMapping, i, Vec_IntSize(p->vMapping) );
322 Vec_IntPush( p->vMapping, Vec_IntSize(vLeaves) );
323 Vec_IntForEachEntry( vLeaves, Leaf, k )
324 {
325 Vec_IntPush( p->vMapping, Leaf );
326 Gia_ManObj(p, Leaf)->Value = uTruth5[k];
327 assert( Gia_ManObj(p, Leaf)->fPhase );
328 }
329 Vec_IntPush( p->vMapping, (int)Ga2_ObjComputeTruth_rec( p, pObj, 1 ) );
330 Vec_IntPush( p->vMapping, -1 ); // placeholder for ref counter
331 CountMarks++;
332 }
333// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
334 Vec_IntFree( vLeaves );
335 Gia_ManCleanValue( p );
336 return CountMarks;
337}
338void Ga2_ManComputeTest( Gia_Man_t * p )
339{
340 abctime clk;
341// unsigned uTruth;
342 Gia_Obj_t * pObj;
343 int i, Counter = 0;
344 clk = Abc_Clock();
345 Ga2_ManMarkup( p, 5, 0 );
346 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
347 Gia_ManForEachAnd( p, pObj, i )
348 {
349 if ( !pObj->fPhase )
350 continue;
351// uTruth = Ga2_ObjTruth( p, pObj );
352// printf( "%6d : ", Counter );
353// Kit_DsdPrintFromTruth( &uTruth, Ga2_ObjLeaveNum(p, pObj) );
354// printf( "\n" );
355 Counter++;
356 }
357 Abc_Print( 1, "Marked AND nodes = %6d. ", Counter );
358 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
359}
360
372Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Abs_Par_t * pPars )
373{
374 Ga2_Man_t * p;
375 p = ABC_CALLOC( Ga2_Man_t, 1 );
376 p->timeStart = Abc_Clock();
377 p->fUseNewLine = 1;
378 // user data
379 p->pGia = pGia;
380 p->pPars = pPars;
381 // markings
382 p->nMarked = Ga2_ManMarkup( pGia, 5, pPars->fUseSimple );
383 p->vCnfs = Vec_PtrAlloc( 1000 );
384 Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) );
385 Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) );
386 // abstraction
387 p->vIds = Vec_IntStartFull( Gia_ManObjNum(pGia) );
388 p->vProofIds = Vec_IntAlloc( 0 );
389 p->vAbs = Vec_IntAlloc( 1000 );
390 p->vValues = Vec_IntAlloc( 1000 );
391 // add constant node to abstraction
392 Ga2_ObjSetId( p, Gia_ManConst0(pGia), 0 );
393 Vec_IntPush( p->vValues, 0 );
394 Vec_IntPush( p->vAbs, 0 );
395 // refinement
396 p->pRnm = Rnm_ManStart( pGia );
397// p->pRf2 = Rf2_ManStart( pGia );
398 // SAT solver and variables
399 p->vId2Lit = Vec_PtrAlloc( 1000 );
400 // temporaries
401 p->vLits = Vec_IntAlloc( 100 );
402 p->vIsopMem = Vec_IntAlloc( 100 );
403 Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
404 // hash table
405 p->nTable = Abc_PrimeCudd(1<<18);
406 p->pTable = ABC_CALLOC( int, 6 * p->nTable );
407 return p;
408}
409
410void Ga2_ManDumpStats( Gia_Man_t * pGia, Abs_Par_t * pPars, sat_solver2 * pSat, int iFrame, int fUseN )
411{
412 FILE * pFile;
413 char pFileName[32];
414 sprintf( pFileName, "stats_gla%s%s.txt", fUseN ? "n":"", pPars->fUseFullProof ? "p":"" );
415
416 pFile = fopen( pFileName, "a+" );
417
418 fprintf( pFile, "%s pi=%d ff=%d and=%d mem=%d bmc=%d",
419 pGia->pName,
420 Gia_ManPiNum(pGia), Gia_ManRegNum(pGia), Gia_ManAndNum(pGia),
421 (int)(1 + sat_solver2_memory_proof(pSat)/(1<<20)),
422 iFrame );
423
424 if ( pGia->vGateClasses )
425 fprintf( pFile, " ff=%d and=%d",
426 Gia_GlaCountFlops( pGia, pGia->vGateClasses ),
427 Gia_GlaCountNodes( pGia, pGia->vGateClasses ) );
428
429 fprintf( pFile, "\n" );
430 fclose( pFile );
431}
432void Ga2_ManReportMemory( Ga2_Man_t * p )
433{
434 double memTot = 0;
435 double memAig = 1.0 * p->pGia->nObjsAlloc * sizeof(Gia_Obj_t) + Vec_IntMemory(p->pGia->vMapping);
436 double memSat = sat_solver2_memory( p->pSat, 1 );
437 double memPro = sat_solver2_memory_proof( p->pSat );
438 double memMap = Vec_VecMemoryInt( (Vec_Vec_t *)p->vId2Lit );
439 double memRef = Rnm_ManMemoryUsage( p->pRnm );
440 double memHash= sizeof(int) * 6 * p->nTable;
441 double memOth = sizeof(Ga2_Man_t);
442 memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCnfs );
443 memOth += Vec_IntMemory( p->vIds );
444 memOth += Vec_IntMemory( p->vProofIds );
445 memOth += Vec_IntMemory( p->vAbs );
446 memOth += Vec_IntMemory( p->vValues );
447 memOth += Vec_IntMemory( p->vLits );
448 memOth += Vec_IntMemory( p->vIsopMem );
449 memOth += 336450 + (sizeof(char) + sizeof(char*)) * 65536;
450 memTot = memAig + memSat + memPro + memMap + memRef + memHash + memOth;
451 ABC_PRMP( "Memory: AIG ", memAig, memTot );
452 ABC_PRMP( "Memory: SAT ", memSat, memTot );
453 ABC_PRMP( "Memory: Proof ", memPro, memTot );
454 ABC_PRMP( "Memory: Map ", memMap, memTot );
455 ABC_PRMP( "Memory: Refine ", memRef, memTot );
456 ABC_PRMP( "Memory: Hash ", memHash,memTot );
457 ABC_PRMP( "Memory: Other ", memOth, memTot );
458 ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
459}
460void Ga2_ManStop( Ga2_Man_t * p )
461{
462 Vec_IntFreeP( &p->pGia->vMapping );
463 Gia_ManSetPhase( p->pGia );
464 if ( p->pPars->fVerbose )
465 Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Lrn = %d Reduce = %d Cex = %d ObjsAdded = %d\n",
466 sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat),
467 sat_solver2_nconflicts(p->pSat), sat_solver2_nlearnts(p->pSat),
468 p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
469 if ( p->pPars->fVerbose )
470 Abc_Print( 1, "Hash hits = %d. Hash misses = %d. Hash overs = %d. Concurrent calls = %d.\n",
471 p->nHashHit, p->nHashMiss, p->nHashOver, p->nPdrCalls );
472
473 if( p->pSat ) sat_solver2_delete( p->pSat );
474 Vec_VecFree( (Vec_Vec_t *)p->vCnfs );
475 Vec_VecFree( (Vec_Vec_t *)p->vId2Lit );
476 Vec_IntFree( p->vIds );
477 Vec_IntFree( p->vProofIds );
478 Vec_IntFree( p->vAbs );
479 Vec_IntFree( p->vValues );
480 Vec_IntFree( p->vLits );
481 Vec_IntFree( p->vIsopMem );
482 Rnm_ManStop( p->pRnm, 0 );
483// Rf2_ManStop( p->pRf2, p->pPars->fVerbose );
484 ABC_FREE( p->pTable );
485 ABC_FREE( p->pSopSizes );
486 ABC_FREE( p->pSops[1] );
487 ABC_FREE( p->pSops );
488 ABC_FREE( p );
489}
490
491
506static inline unsigned Ga2_ObjTruthDepends( unsigned t, int v )
507{
508 static unsigned uInvTruth5[5] = { 0x55555555, 0x33333333, 0x0F0F0F0F, 0x00FF00FF, 0x0000FFFF };
509 assert( v >= 0 && v <= 4 );
510 return ((t ^ (t >> (1 << v))) & uInvTruth5[v]);
511}
512unsigned Ga2_ObjComputeTruthSpecial( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vLits )
513{
514 int fVerbose = 0;
515 static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
516 unsigned Res;
517 Gia_Obj_t * pObj;
518 int i, Entry;
519// int Id = Gia_ObjId(p, pRoot);
520 assert( Gia_ObjIsAnd(pRoot) );
521
522 if ( fVerbose )
523 printf( "Object %d.\n", Gia_ObjId(p, pRoot) );
524
525 // assign elementary truth tables
526 Gia_ManForEachObjVec( vLeaves, p, pObj, i )
527 {
528 Entry = Vec_IntEntry( vLits, i );
529 assert( Entry >= 0 );
530 if ( Entry == 0 )
531 pObj->Value = 0;
532 else if ( Entry == 1 )
533 pObj->Value = ~0;
534 else // non-trivial literal
535 pObj->Value = uTruth5[i];
536 if ( fVerbose )
537 printf( "%d ", Entry );
538 }
539
540 if ( fVerbose )
541 {
542 Res = Ga2_ObjTruth( p, pRoot );
543// Kit_DsdPrintFromTruth( &Res, Vec_IntSize(vLeaves) );
544 printf( "\n" );
545 }
546
547 // compute truth table
548 Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
549 if ( Res != 0 && Res != ~0 )
550 {
551 // find essential variables
552 int nUsed = 0, pUsed[5];
553 for ( i = 0; i < Vec_IntSize(vLeaves); i++ )
554 if ( Ga2_ObjTruthDepends( Res, i ) )
555 pUsed[nUsed++] = i;
556 assert( nUsed > 0 );
557 // order positions by literal value
558 Vec_IntSelectSortCost( pUsed, nUsed, vLits );
559 assert( Vec_IntEntry(vLits, pUsed[0]) <= Vec_IntEntry(vLits, pUsed[nUsed-1]) );
560 // assign elementary truth tables to the leaves
561 Gia_ManForEachObjVec( vLeaves, p, pObj, i )
562 {
563 Entry = Vec_IntEntry( vLits, i );
564 assert( Entry >= 0 );
565 if ( Entry == 0 )
566 pObj->Value = 0;
567 else if ( Entry == 1 )
568 pObj->Value = ~0;
569 else // non-trivial literal
570 pObj->Value = 0xDEADCAFE; // not important
571 }
572 for ( i = 0; i < nUsed; i++ )
573 {
574 Entry = Vec_IntEntry( vLits, pUsed[i] );
575 assert( Entry > 1 );
576 pObj = Gia_ManObj( p, Vec_IntEntry(vLeaves, pUsed[i]) );
577 pObj->Value = Abc_LitIsCompl(Entry) ? ~uTruth5[i] : uTruth5[i];
578// pObj->Value = uTruth5[i];
579 // remember this literal
580 pUsed[i] = Abc_LitRegular(Entry);
581// pUsed[i] = Entry;
582 }
583 // compute truth table
584 Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
585 // reload the literals
586 Vec_IntClear( vLits );
587 for ( i = 0; i < nUsed; i++ )
588 {
589 Vec_IntPush( vLits, pUsed[i] );
590 assert( Ga2_ObjTruthDepends(Res, i) );
591 if ( fVerbose )
592 printf( "%d ", pUsed[i] );
593 }
594 for ( ; i < 5; i++ )
595 assert( !Ga2_ObjTruthDepends(Res, i) );
596
597if ( fVerbose )
598{
599// Kit_DsdPrintFromTruth( &Res, nUsed );
600 printf( "\n" );
601}
602
603 }
604 else
605 {
606
607if ( fVerbose )
608{
609 Vec_IntClear( vLits );
610 printf( "Const %d\n", Res > 0 );
611}
612
613 }
614 Gia_ManForEachObjVec( vLeaves, p, pObj, i )
615 pObj->Value = 0;
616 return Res;
617}
618
630Vec_Int_t * Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCover )
631{
632 int RetValue;
633 assert( nVars <= 5 );
634 // transform truth table into the SOP
635 RetValue = Kit_TruthIsop( &uTruth, nVars, vCover, 0 );
636 assert( RetValue == 0 );
637 // check the case of constant cover
638 return Vec_IntDup( vCover );
639}
640
652static inline void Ga2_ManCnfAddDynamic( Ga2_Man_t * p, int uTruth, int Lits[], int iLitOut, int ProofId )
653{
654 int i, k, b, Cube, nClaLits, ClaLits[6];
655// assert( uTruth > 0 && uTruth < 0xffff );
656 for ( i = 0; i < 2; i++ )
657 {
658 if ( i )
659 uTruth = 0xffff & ~uTruth;
660// Extra_PrintBinary( stdout, &uTruth, 16 ); printf( "\n" );
661 for ( k = 0; k < p->pSopSizes[uTruth]; k++ )
662 {
663 nClaLits = 0;
664 ClaLits[nClaLits++] = i ? lit_neg(iLitOut) : iLitOut;
665 Cube = p->pSops[uTruth][k];
666 for ( b = 3; b >= 0; b-- )
667 {
668 if ( Cube % 3 == 0 ) // value 0 --> add positive literal
669 {
670 assert( Lits[b] > 1 );
671 ClaLits[nClaLits++] = Lits[b];
672 }
673 else if ( Cube % 3 == 1 ) // value 1 --> add negative literal
674 {
675 assert( Lits[b] > 1 );
676 ClaLits[nClaLits++] = lit_neg(Lits[b]);
677 }
678 Cube = Cube / 3;
679 }
680 sat_solver2_addclause( p->pSat, ClaLits, ClaLits+nClaLits, ProofId );
681 }
682 }
683}
684void Ga2_ManCnfAddStatic( sat_solver2 * pSat, Vec_Int_t * vCnf0, Vec_Int_t * vCnf1, int Lits[], int iLitOut, int ProofId )
685{
686 Vec_Int_t * vCnf;
687 int i, k, b, Cube, Literal, nClaLits, ClaLits[6];
688 for ( i = 0; i < 2; i++ )
689 {
690 vCnf = i ? vCnf1 : vCnf0;
691 Vec_IntForEachEntry( vCnf, Cube, k )
692 {
693 nClaLits = 0;
694 ClaLits[nClaLits++] = i ? lit_neg(iLitOut) : iLitOut;
695 for ( b = 0; b < 5; b++ )
696 {
697 Literal = 3 & (Cube >> (b << 1));
698 if ( Literal == 1 ) // value 0 --> add positive literal
699 {
700// assert( Lits[b] > 1 );
701 ClaLits[nClaLits++] = Lits[b];
702 }
703 else if ( Literal == 2 ) // value 1 --> add negative literal
704 {
705// assert( Lits[b] > 1 );
706 ClaLits[nClaLits++] = lit_neg(Lits[b]);
707 }
708 else if ( Literal != 0 )
709 assert( 0 );
710 }
711 sat_solver2_addclause( pSat, ClaLits, ClaLits+nClaLits, ProofId );
712 }
713 }
714}
715
727static inline unsigned Saig_ManBmcHashKey( int * pArray )
728{
729 static int s_Primes[5] = { 12582917, 25165843, 50331653, 100663319, 201326611 };
730 unsigned i, Key = 0;
731 for ( i = 0; i < 5; i++ )
732 Key += pArray[i] * s_Primes[i];
733 return Key;
734}
735static inline int * Saig_ManBmcLookup( Ga2_Man_t * p, int * pArray )
736{
737 int * pTable = p->pTable + 6 * (Saig_ManBmcHashKey(pArray) % p->nTable);
738 if ( memcmp( pTable, pArray, 20 ) )
739 {
740 if ( pTable[0] == 0 )
741 p->nHashMiss++;
742 else
743 p->nHashOver++;
744 memcpy( pTable, pArray, 20 );
745 pTable[5] = 0;
746 }
747 else
748 p->nHashHit++;
749 assert( pTable + 5 < pTable + 6 * p->nTable );
750 return pTable + 5;
751}
752
764static inline void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs )
765{
766 unsigned uTruth;
767 int nLeaves;
768// int Id = Gia_ObjId(p->pGia, pObj);
769 assert( pObj->fPhase );
770 assert( Vec_PtrSize(p->vCnfs) == 2 * Vec_IntSize(p->vValues) );
771 // assign abstraction ID to the node
772 if ( Ga2_ObjId(p,pObj) == -1 )
773 {
774 Ga2_ObjSetId( p, pObj, Vec_IntSize(p->vValues) );
775 Vec_IntPush( p->vValues, Gia_ObjId(p->pGia, pObj) );
776 Vec_PtrPush( p->vCnfs, NULL );
777 Vec_PtrPush( p->vCnfs, NULL );
778 }
779 assert( Ga2_ObjCnf0(p, pObj) == NULL );
780 if ( !fAbs )
781 return;
782 Vec_IntPush( p->vAbs, Gia_ObjId(p->pGia, pObj) );
783 assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
784 // compute parameters
785 nLeaves = Ga2_ObjLeaveNum(p->pGia, pObj);
786 uTruth = Ga2_ObjTruth( p->pGia, pObj );
787 // create CNF for pos/neg phases
788 Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj), Ga2_ManCnfCompute( uTruth, nLeaves, p->vIsopMem) );
789 Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, Ga2_ManCnfCompute(~uTruth, nLeaves, p->vIsopMem) );
790}
791
792static inline void Ga2_ManAddToAbsOneStatic( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int fUseId )
793{
794 Vec_Int_t * vLeaves;
795 Gia_Obj_t * pLeaf;
796 int k, Lit, iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f );
797 assert( iLitOut > 1 );
798 assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) );
799 if ( Gia_ObjIsConst0(pObj) || (f == 0 && Gia_ObjIsRo(p->pGia, pObj)) )
800 {
801 iLitOut = Abc_LitNot( iLitOut );
802 sat_solver2_addclause( p->pSat, &iLitOut, &iLitOut + 1, fUseId ? Gia_ObjId(p->pGia, pObj) : -1 );
803 }
804 else
805 {
806 int fUseStatic = 1;
807 Vec_IntClear( p->vLits );
808 vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
809 Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, k )
810 {
811 Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f - Gia_ObjIsRo(p->pGia, pObj) );
812 Vec_IntPush( p->vLits, Lit );
813 if ( Lit < 2 )
814 fUseStatic = 0;
815 }
816 if ( fUseStatic || Gia_ObjIsRo(p->pGia, pObj) )
817 Ga2_ManCnfAddStatic( p->pSat, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, fUseId ? Gia_ObjId(p->pGia, pObj) : -1 );
818 else
819 {
820 unsigned uTruth = Ga2_ObjComputeTruthSpecial( p->pGia, pObj, vLeaves, p->vLits );
821 Ga2_ManCnfAddDynamic( p, uTruth & 0xFFFF, Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) );
822 }
823 }
824}
825static inline void Ga2_ManAddToAbsOneDynamic( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
826{
827// int Id = Gia_ObjId(p->pGia, pObj);
828 Vec_Int_t * vLeaves;
829 Gia_Obj_t * pLeaf;
830 unsigned uTruth;
831 int i, Lit = 0;
832
833 assert( Ga2_ObjIsAbs0(p, pObj) );
834 assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) );
835 if ( Gia_ObjIsConst0(pObj) || (f == 0 && Gia_ObjIsRo(p->pGia, pObj)) )
836 {
837 Ga2_ObjAddLit( p, pObj, f, 0 );
838 }
839 else if ( Gia_ObjIsRo(p->pGia, pObj) )
840 {
841 // if flop is included in the abstraction, but its driver is not
842 // flop input driver has no variable assigned -- we assign it here
843 pLeaf = Gia_ObjRoToRi( p->pGia, pObj );
844 Lit = Ga2_ObjFindOrAddLit( p, Gia_ObjFanin0(pLeaf), f-1 );
845 assert( Lit >= 0 );
846 Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(pLeaf) );
847 Ga2_ObjAddLit( p, pObj, f, Lit );
848 }
849 else
850 {
851 assert( Gia_ObjIsAnd(pObj) );
852 Vec_IntClear( p->vLits );
853 vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
854 Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, i )
855 {
856 if ( Ga2_ObjIsAbs0(p, pLeaf) ) // belongs to original abstraction
857 {
858 Lit = Ga2_ObjFindLit( p, pLeaf, f );
859 assert( Lit >= 0 );
860 }
861 else if ( Ga2_ObjIsLeaf0(p, pLeaf) ) // belongs to original PPIs
862 {
863 Lit = Ga2_ObjFindLit( p, pLeaf, f );
864// Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f );
865 if ( Lit == -1 )
866 {
867 Lit = GA2_BIG_NUM + 2*i;
868// assert( 0 );
869 }
870 }
871 else assert( 0 );
872 Vec_IntPush( p->vLits, Lit );
873 }
874
875 // minimize truth table
876 uTruth = Ga2_ObjComputeTruthSpecial( p->pGia, pObj, vLeaves, p->vLits );
877 if ( uTruth == 0 || uTruth == ~0 ) // const 0 / 1
878 {
879 Lit = (uTruth > 0);
880 Ga2_ObjAddLit( p, pObj, f, Lit );
881 }
882 else if ( uTruth == 0xAAAAAAAA || uTruth == 0x55555555 ) // buffer / inverter
883 {
884 Lit = Vec_IntEntry( p->vLits, 0 );
885 if ( Lit >= GA2_BIG_NUM )
886 {
887 pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, (Lit-GA2_BIG_NUM)/2) );
888 Lit = Ga2_ObjFindLit( p, pLeaf, f );
889 assert( Lit == -1 );
890 Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f );
891 }
892 assert( Lit >= 0 );
893 Lit = Abc_LitNotCond( Lit, uTruth == 0x55555555 );
894 Ga2_ObjAddLit( p, pObj, f, Lit );
895 assert( Lit < 10000000 );
896 }
897 else
898 {
899 assert( Vec_IntSize(p->vLits) > 1 && Vec_IntSize(p->vLits) < 6 );
900 // replace literals
901 Vec_IntForEachEntry( p->vLits, Lit, i )
902 {
903 if ( Lit >= GA2_BIG_NUM )
904 {
905 pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, (Lit-GA2_BIG_NUM)/2) );
906 Lit = Ga2_ObjFindLit( p, pLeaf, f );
907 assert( Lit == -1 );
908 Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f );
909 Vec_IntWriteEntry( p->vLits, i, Lit );
910 }
911 assert( Lit < 10000000 );
912 }
913
914 // add new nodes
915 if ( Vec_IntSize(p->vLits) == 5 )
916 {
917 Vec_IntClear( p->vLits );
918 Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, i )
919 Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pLeaf, f ) );
920 Lit = Ga2_ObjFindOrAddLit(p, pObj, f);
921 Ga2_ManCnfAddStatic( p->pSat, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), Lit, -1 );
922 }
923 else
924 {
925// int fUseHash = 1;
926 if ( !p->pPars->fSkipHash )
927 {
928 int * pLookup, nSize = Vec_IntSize(p->vLits);
929 assert( Vec_IntSize(p->vLits) < 5 );
930 assert( Vec_IntEntry(p->vLits, 0) <= Vec_IntEntryLast(p->vLits) );
931 assert( Ga2_ObjFindLit(p, pObj, f) == -1 );
932 for ( i = Vec_IntSize(p->vLits); i < 4; i++ )
933 Vec_IntPush( p->vLits, GA2_BIG_NUM );
934 Vec_IntPush( p->vLits, (int)uTruth );
935 assert( Vec_IntSize(p->vLits) == 5 );
936
937 // perform structural hashing here!!!
938 pLookup = Saig_ManBmcLookup( p, Vec_IntArray(p->vLits) );
939 if ( *pLookup == 0 )
940 {
941 *pLookup = Ga2_ObjFindOrAddLit(p, pObj, f);
942 Vec_IntShrink( p->vLits, nSize );
943 Ga2_ManCnfAddDynamic( p, uTruth & 0xFFFF, Vec_IntArray(p->vLits), *pLookup, -1 );
944 }
945 else
946 Ga2_ObjAddLit( p, pObj, f, *pLookup );
947
948 }
949 else
950 {
951 Lit = Ga2_ObjFindOrAddLit(p, pObj, f);
952 Ga2_ManCnfAddDynamic( p, uTruth & 0xFFFF, Vec_IntArray(p->vLits), Lit, -1 );
953 }
954 }
955 }
956 }
957}
958
959void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
960{
961 int fSimple = 0;
962 Gia_Obj_t * pObj;
963 int i;
964 Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
965 {
966 if ( i == p->LimAbs )
967 break;
968 if ( fSimple )
969 Ga2_ManAddToAbsOneStatic( p, pObj, f, 0 );
970 else
971 Ga2_ManAddToAbsOneDynamic( p, pObj, f );
972 }
973 Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
974 if ( i >= p->LimAbs )
975 Ga2_ManAddToAbsOneStatic( p, pObj, f, 1 );
976// sat_solver2_simplify( p->pSat );
977}
978
979void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
980{
981 Vec_Int_t * vLeaves;
982 Gia_Obj_t * pObj, * pFanin;
983 int f, i, k;
984 // add abstraction objects
985 Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
986 {
987 Ga2_ManSetupNode( p, pObj, 1 );
988 if ( p->pSat->pPrf2 )
989 Vec_IntWriteEntry( p->vProofIds, Gia_ObjId(p->pGia, pObj), p->nProofIds++ );
990 }
991 // add PPI objects
992 Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
993 {
994 vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
995 Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
996 if ( Ga2_ObjId( p, pFanin ) == -1 )
997 Ga2_ManSetupNode( p, pFanin, 0 );
998 }
999 // add new clauses to the timeframes
1000 for ( f = 0; f <= p->pPars->iFrame; f++ )
1001 {
1002 Vec_IntFillExtra( Ga2_MapFrameMap(p, f), Vec_IntSize(p->vValues), -1 );
1003 Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
1004 Ga2_ManAddToAbsOneStatic( p, pObj, f, 1 );
1005 }
1006// sat_solver2_simplify( p->pSat );
1007}
1008
1009void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues, int nSatVars )
1010{
1011 Vec_Int_t * vMap;
1012 Gia_Obj_t * pObj;
1013 int i, k, Entry;
1014 assert( nAbs > 0 );
1015 assert( nValues > 0 );
1016 assert( nSatVars > 0 );
1017 // shrink abstraction
1018 Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
1019 {
1020 if ( !i ) continue;
1021 assert( Ga2_ObjCnf0(p, pObj) != NULL );
1022 assert( Ga2_ObjCnf1(p, pObj) != NULL );
1023 if ( i < nAbs )
1024 continue;
1025 Vec_IntFree( Ga2_ObjCnf0(p, pObj) );
1026 Vec_IntFree( Ga2_ObjCnf1(p, pObj) );
1027 Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj), NULL );
1028 Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, NULL );
1029 }
1030 Vec_IntShrink( p->vAbs, nAbs );
1031 // shrink values
1032 Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
1033 {
1034 assert( Ga2_ObjId(p,pObj) >= 0 );
1035 if ( i < nValues )
1036 continue;
1037 Ga2_ObjSetId( p, pObj, -1 );
1038 }
1039 Vec_IntShrink( p->vValues, nValues );
1040 Vec_PtrShrink( p->vCnfs, 2 * nValues );
1041 // hack to clear constant
1042 if ( nValues == 1 )
1043 nValues = 0;
1044 // clean mapping for each timeframe
1045 Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i )
1046 {
1047 Vec_IntShrink( vMap, nValues );
1048 Vec_IntForEachEntryStart( vMap, Entry, k, p->LimAbs )
1049 if ( Entry >= 2*nSatVars )
1050 Vec_IntWriteEntry( vMap, k, -1 );
1051 }
1052 // shrink SAT variables
1053 p->nSatVars = nSatVars;
1054}
1055
1067void Ga2_ManAbsTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vClasses, int fFirst )
1068{
1069 if ( pObj->fPhase && !fFirst )
1070 return;
1071 assert( Gia_ObjIsAnd(pObj) );
1072 Ga2_ManAbsTranslate_rec( p, Gia_ObjFanin0(pObj), vClasses, 0 );
1073 Ga2_ManAbsTranslate_rec( p, Gia_ObjFanin1(pObj), vClasses, 0 );
1074 Vec_IntWriteEntry( vClasses, Gia_ObjId(p, pObj), 1 );
1075}
1076
1077Vec_Int_t * Ga2_ManAbsTranslate( Ga2_Man_t * p )
1078{
1079 Vec_Int_t * vGateClasses;
1080 Gia_Obj_t * pObj;
1081 int i;
1082 vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
1083 Vec_IntWriteEntry( vGateClasses, 0, 1 );
1084 Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
1085 {
1086 if ( Gia_ObjIsAnd(pObj) )
1087 Ga2_ManAbsTranslate_rec( p->pGia, pObj, vGateClasses, 1 );
1088 else if ( Gia_ObjIsRo(p->pGia, pObj) )
1089 Vec_IntWriteEntry( vGateClasses, Gia_ObjId(p->pGia, pObj), 1 );
1090 else if ( !Gia_ObjIsConst0(pObj) )
1091 assert( 0 );
1092// Gia_ObjPrint( p->pGia, pObj );
1093 }
1094 return vGateClasses;
1095}
1096
1097Vec_Int_t * Ga2_ManAbsDerive( Gia_Man_t * p )
1098{
1099 Vec_Int_t * vToAdd;
1100 Gia_Obj_t * pObj;
1101 int i;
1102 vToAdd = Vec_IntAlloc( 1000 );
1103 Gia_ManForEachRo( p, pObj, i )
1104 if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, Gia_ObjId(p, pObj)) )
1105 Vec_IntPush( vToAdd, Gia_ObjId(p, pObj) );
1106 Gia_ManForEachAnd( p, pObj, i )
1107 if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, i) )
1108 Vec_IntPush( vToAdd, i );
1109 return vToAdd;
1110}
1111
1112void Ga2_ManRestart( Ga2_Man_t * p )
1113{
1114 Vec_Int_t * vToAdd;
1115 int Lit = 1;
1116 assert( p->pGia != NULL && p->pGia->vGateClasses != NULL );
1117 assert( Gia_ManPi(p->pGia, 0)->fPhase ); // marks are set
1118 // clear SAT variable numbers (begin with 1)
1119 if ( p->pSat ) sat_solver2_delete( p->pSat );
1120 p->pSat = sat_solver2_new();
1121 p->pSat->nLearntStart = p->pPars->nLearnedStart;
1122 p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
1123 p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
1124 p->pSat->nLearntMax = p->pSat->nLearntStart;
1125 // add clause x0 = 0 (lit0 = 1; lit1 = 0)
1126 sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, -1 );
1127 // remove previous abstraction
1128 Ga2_ManShrinkAbs( p, 1, 1, 1 );
1129 // start new abstraction
1130 vToAdd = Ga2_ManAbsDerive( p->pGia );
1131 assert( p->pSat->pPrf2 == NULL );
1132 assert( p->pPars->iFrame < 0 );
1133 Ga2_ManAddToAbs( p, vToAdd );
1134 Vec_IntFree( vToAdd );
1135 p->LimAbs = Vec_IntSize(p->vAbs);
1136 p->LimPpi = Vec_IntSize(p->vValues);
1137 // set runtime limit
1138 if ( p->pPars->nTimeOut )
1139 sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + p->timeStart );
1140 // clean the hash table
1141 memset( p->pTable, 0, 6 * sizeof(int) * p->nTable );
1142}
1143
1144
1156static inline int Ga2_ObjSatValue( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
1157{
1158 int Lit = Ga2_ObjFindLit( p, pObj, f );
1159 assert( !Gia_ObjIsConst0(pObj) );
1160 if ( Lit == -1 )
1161 return 0;
1162 if ( Abc_Lit2Var(Lit) >= p->pSat->size )
1163 return 0;
1164 return Abc_LitIsCompl(Lit) ^ sat_solver2_var_value( p->pSat, Abc_Lit2Var(Lit) );
1165}
1166Abc_Cex_t * Ga2_ManDeriveCex( Ga2_Man_t * p, Vec_Int_t * vPis )
1167{
1168 Abc_Cex_t * pCex;
1169 Gia_Obj_t * pObj;
1170 int i, f;
1171 pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
1172 pCex->iPo = 0;
1173 pCex->iFrame = p->pPars->iFrame;
1174 Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
1175 {
1176 if ( !Gia_ObjIsPi(p->pGia, pObj) )
1177 continue;
1178 assert( Gia_ObjIsPi(p->pGia, pObj) );
1179 for ( f = 0; f <= pCex->iFrame; f++ )
1180 if ( Ga2_ObjSatValue( p, pObj, f ) )
1181 Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Gia_ObjCioId(pObj) );
1182 }
1183 return pCex;
1184}
1185void Ga2_ManRefinePrint( Ga2_Man_t * p, Vec_Int_t * vVec )
1186{
1187 Gia_Obj_t * pObj, * pFanin;
1188 int i, k;
1189 printf( "\n Unsat core: \n" );
1190 Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
1191 {
1192 Vec_Int_t * vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
1193 printf( "%12d : ", i );
1194 printf( "Obj =%6d ", Gia_ObjId(p->pGia, pObj) );
1195 if ( Gia_ObjIsRo(p->pGia, pObj) )
1196 printf( "ff " );
1197 else
1198 printf( " " );
1199 if ( Ga2_ObjIsAbs0(p, pObj) )
1200 printf( "a " );
1201 else if ( Ga2_ObjIsLeaf0(p, pObj) )
1202 printf( "l " );
1203 else
1204 printf( " " );
1205 printf( "Fanins: " );
1206 Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
1207 {
1208 printf( "%6d ", Gia_ObjId(p->pGia, pFanin) );
1209 if ( Gia_ObjIsRo(p->pGia, pFanin) )
1210 printf( "ff " );
1211 else
1212 printf( " " );
1213 if ( Ga2_ObjIsAbs0(p, pFanin) )
1214 printf( "a " );
1215 else if ( Ga2_ObjIsLeaf0(p, pFanin) )
1216 printf( "l " );
1217 else
1218 printf( " " );
1219 }
1220 printf( "\n" );
1221 }
1222}
1223void Ga2_ManRefinePrintPPis( Ga2_Man_t * p )
1224{
1225 Vec_Int_t * vVec = Vec_IntAlloc( 100 );
1226 Gia_Obj_t * pObj;
1227 int i;
1228 Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
1229 {
1230 if ( !i ) continue;
1231 if ( Ga2_ObjIsAbs(p, pObj) )
1232 continue;
1233 assert( pObj->fPhase );
1234 assert( Ga2_ObjIsLeaf(p, pObj) );
1235 assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj) );
1236 Vec_IntPush( vVec, Gia_ObjId(p->pGia, pObj) );
1237 }
1238 printf( " Current PPIs (%d): ", Vec_IntSize(vVec) );
1239 Vec_IntSort( vVec, 1 );
1240 Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
1241 printf( "%d ", Gia_ObjId(p->pGia, pObj) );
1242 printf( "\n" );
1243 Vec_IntFree( vVec );
1244}
1245
1246
1247void Ga2_GlaPrepareCexAndMap( Ga2_Man_t * p, Abc_Cex_t ** ppCex, Vec_Int_t ** pvMaps )
1248{
1249 Abc_Cex_t * pCex;
1250 Vec_Int_t * vMap;
1251 Gia_Obj_t * pObj;
1252 int f, i, k;
1253/*
1254 Gia_ManForEachObj( p->pGia, pObj, i )
1255 if ( Ga2_ObjId(p, pObj) >= 0 )
1256 assert( Vec_IntEntry(p->vValues, Ga2_ObjId(p, pObj)) == i );
1257*/
1258 // find PIs and PPIs
1259 vMap = Vec_IntAlloc( 1000 );
1260 Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
1261 {
1262 if ( !i ) continue;
1263 if ( Ga2_ObjIsAbs(p, pObj) )
1264 continue;
1265 assert( pObj->fPhase );
1266 assert( Ga2_ObjIsLeaf(p, pObj) );
1267 assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj) );
1268 Vec_IntPush( vMap, Gia_ObjId(p->pGia, pObj) );
1269 }
1270 // derive counter-example
1271 pCex = Abc_CexAlloc( 0, Vec_IntSize(vMap), p->pPars->iFrame+1 );
1272 pCex->iFrame = p->pPars->iFrame;
1273 for ( f = 0; f <= p->pPars->iFrame; f++ )
1274 Gia_ManForEachObjVec( vMap, p->pGia, pObj, k )
1275 if ( Ga2_ObjSatValue( p, pObj, f ) )
1276 Abc_InfoSetBit( pCex->pData, f * Vec_IntSize(vMap) + k );
1277 *pvMaps = vMap;
1278 *ppCex = pCex;
1279}
1280Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p )
1281{
1282 Abc_Cex_t * pCex;
1283 Vec_Int_t * vMap, * vVec;
1284 Gia_Obj_t * pObj;
1285 int i, k;
1286 if ( p->pPars->fAddLayer )
1287 {
1288 // use simplified refinement strategy, which adds logic near at PPI without finding important ones
1289 vVec = Vec_IntAlloc( 100 );
1290 Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
1291 {
1292 if ( !i ) continue;
1293 if ( Ga2_ObjIsAbs(p, pObj) )
1294 continue;
1295 assert( pObj->fPhase );
1296 assert( Ga2_ObjIsLeaf(p, pObj) );
1297 assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj) );
1298 if ( Gia_ObjIsPi(p->pGia, pObj) )
1299 continue;
1300 Vec_IntPush( vVec, Gia_ObjId(p->pGia, pObj) );
1301 }
1302 p->nObjAdded += Vec_IntSize(vVec);
1303 return vVec;
1304 }
1305 Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap );
1306 // Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 );
1307 vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, p->pPars->fNewRefine, 1 );
1308// printf( "Refinement %d\n", Vec_IntSize(vVec) );
1309 Abc_CexFree( pCex );
1310 if ( Vec_IntSize(vVec) == 0 )
1311 {
1312 Vec_IntFree( vVec );
1313 Abc_CexFreeP( &p->pGia->pCexSeq );
1314 p->pGia->pCexSeq = Ga2_ManDeriveCex( p, vMap );
1315 Vec_IntFree( vMap );
1316 return NULL;
1317 }
1318 Vec_IntFree( vMap );
1319 // remove those already added
1320 k = 0;
1321 Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
1322 if ( !Ga2_ObjIsAbs(p, pObj) )
1323 Vec_IntWriteEntry( vVec, k++, Gia_ObjId(p->pGia, pObj) );
1324 Vec_IntShrink( vVec, k );
1325
1326 // these objects should be PPIs that are not abstracted yet
1327 Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
1328 assert( pObj->fPhase );//&& Ga2_ObjIsLeaf(p, pObj) );
1329 p->nObjAdded += Vec_IntSize(vVec);
1330 return vVec;
1331}
1332
1344int Ga2_GlaAbsCount( Ga2_Man_t * p, int fRo, int fAnd )
1345{
1346 Gia_Obj_t * pObj;
1347 int i, Counter = 0;
1348 if ( fRo )
1349 Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
1350 Counter += Gia_ObjIsRo(p->pGia, pObj);
1351 else if ( fAnd )
1352 Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
1353 Counter += Gia_ObjIsAnd(pObj);
1354 else assert( 0 );
1355 return Counter;
1356}
1357
1369void Ga2_ManAbsPrintFrame( Ga2_Man_t * p, int nFrames, int nConfls, int nCexes, abctime Time, int fFinal )
1370{
1371 int fUseNewLine = ((fFinal && nCexes) || p->pPars->fVeryVerbose);
1372 if ( Abc_FrameIsBatchMode() && !fUseNewLine )
1373 return;
1374 p->fUseNewLine = fUseNewLine;
1375 Abc_Print( 1, "%4d :", nFrames );
1376 Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * Vec_IntSize(p->vAbs) / p->nMarked) );
1377 Abc_Print( 1, "%6d", Vec_IntSize(p->vAbs) );
1378 Abc_Print( 1, "%5d", Vec_IntSize(p->vValues)-Vec_IntSize(p->vAbs)-1 );
1379 Abc_Print( 1, "%5d", Ga2_GlaAbsCount(p, 1, 0) );
1380 Abc_Print( 1, "%6d", Ga2_GlaAbsCount(p, 0, 1) );
1381 Abc_Print( 1, "%8d", nConfls );
1382 if ( nCexes == 0 )
1383 Abc_Print( 1, "%5c", '-' );
1384 else
1385 Abc_Print( 1, "%5d", nCexes );
1386 Abc_PrintInt( sat_solver2_nvars(p->pSat) );
1387 Abc_PrintInt( sat_solver2_nclauses(p->pSat) );
1388 Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
1389 Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
1390 Abc_Print( 1, "%5.0f MB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<20) );
1391 Abc_Print( 1, "%s", fUseNewLine ? "\n" : "\r" );
1392 fflush( stdout );
1393}
1394
1406char * Ga2_GlaGetFileName( Ga2_Man_t * p, int fAbs )
1407{
1408 static char * pFileNameDef = "glabs.aig";
1409 if ( p->pPars->pFileVabs )
1410 return p->pPars->pFileVabs;
1411 if ( p->pGia->pSpec )
1412 {
1413 if ( fAbs )
1414 return Extra_FileNameGenericAppend( p->pGia->pSpec, "_abs.aig");
1415 else
1416 return Extra_FileNameGenericAppend( p->pGia->pSpec, "_gla.aig");
1417 }
1418 return pFileNameDef;
1419}
1420
1421void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
1422{
1423 char * pFileName;
1424 assert( p->pPars->fDumpMabs || p->pPars->fDumpVabs );
1425 if ( p->pPars->fDumpMabs )
1426 {
1427 pFileName = Ga2_GlaGetFileName(p, 0);
1428 if ( fVerbose )
1429 Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
1430 // dump abstraction map
1431 Vec_IntFreeP( &p->pGia->vGateClasses );
1432 p->pGia->vGateClasses = Ga2_ManAbsTranslate( p );
1433 Gia_AigerWrite( p->pGia, pFileName, 0, 0, 0 );
1434 }
1435 else if ( p->pPars->fDumpVabs )
1436 {
1437 Vec_Int_t * vGateClasses;
1438 Gia_Man_t * pAbs;
1439 pFileName = Ga2_GlaGetFileName(p, 1);
1440 if ( fVerbose )
1441 Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
1442 // dump absracted model
1443 vGateClasses = Ga2_ManAbsTranslate( p );
1444 pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
1445 Gia_ManCleanValue( p->pGia );
1446 Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
1447 Gia_ManStop( pAbs );
1448 Vec_IntFreeP( &vGateClasses );
1449 }
1450 else assert( 0 );
1451}
1452
1464void Gia_Ga2SendAbsracted( Ga2_Man_t * p, int fVerbose )
1465{
1466 Gia_Man_t * pAbs;
1467 Vec_Int_t * vGateClasses;
1468 assert( Abc_FrameIsBridgeMode() );
1469// if ( fVerbose )
1470// Abc_Print( 1, "Sending abstracted model...\n" );
1471 // create abstraction (value of p->pGia is not used here)
1472 vGateClasses = Ga2_ManAbsTranslate( p );
1473 pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
1474 Vec_IntFreeP( &vGateClasses );
1475 Gia_ManCleanValue( p->pGia );
1476 // send it out
1477 Gia_ManToBridgeAbsNetlist( stdout, pAbs, BRIDGE_ABS_NETLIST );
1478 Gia_ManStop( pAbs );
1479}
1480void Gia_Ga2SendCancel( Ga2_Man_t * p, int fVerbose )
1481{
1482 extern int Gia_ManToBridgeBadAbs( FILE * pFile );
1483 assert( Abc_FrameIsBridgeMode() );
1484// if ( fVerbose )
1485// Abc_Print( 1, "Cancelling previously sent model...\n" );
1486 Gia_ManToBridgeBadAbs( stdout );
1487}
1488
1500int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
1501{
1502 int fUseSecondCore = 1;
1503 Ga2_Man_t * p;
1504 Vec_Int_t * vCore, * vPPis;
1505 abctime clk2, clk = Abc_Clock();
1506 int Status = l_Undef, RetValue = -1, iFrameTryToProve = -1, fOneIsSent = 0;
1507 int i, c, f, Lit;
1508 pPars->iFrame = -1;
1509 // check trivial case
1510 assert( Gia_ManPoNum(pAig) == 1 );
1511 ABC_FREE( pAig->pCexSeq );
1512 if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) )
1513 {
1514 if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) )
1515 {
1516 Abc_Print( 1, "Sequential miter is trivially UNSAT.\n" );
1517 return 1;
1518 }
1519 pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 );
1520 Abc_Print( 1, "Sequential miter is trivially SAT.\n" );
1521 return 0;
1522 }
1523 // create gate classes if not given
1524 if ( pAig->vGateClasses == NULL )
1525 {
1526 pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
1527 Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
1528 Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)), 1 );
1529 }
1530 // start the manager
1531 p = Ga2_ManStart( pAig, pPars );
1532 p->timeInit = Abc_Clock() - clk;
1533 // perform initial abstraction
1534 if ( p->pPars->fVerbose )
1535 {
1536 Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" );
1537 Abc_Print( 1, "FrameMax = %d ConfMax = %d Timeout = %d Limit = %d %% Limit2 = %d %% RatioMax = %d %%\n",
1538 pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin, pPars->nRatioMin2, pPars->nRatioMax );
1539 Abc_Print( 1, "LrnStart = %d LrnDelta = %d LrnRatio = %d %% Skip = %d SimpleCNF = %d Dump = %d\n",
1540 pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs );
1541 if ( pPars->fDumpVabs || pPars->fDumpMabs )
1542 Abc_Print( 1, "%s will be continuously dumped into file \"%s\".\n",
1543 pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map",
1544 Ga2_GlaGetFileName(p, pPars->fDumpVabs) );
1545 if ( pPars->fDumpMabs )
1546 {
1547 {
1548 char Command[1000];
1549 Abc_FrameSetStatus( -1 );
1550 Abc_FrameSetCex( NULL );
1551 Abc_FrameSetNFrames( -1 );
1552 sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status"));
1553 Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
1554 }
1555 {
1556 // create trivial abstraction map
1557 Gia_Obj_t * pObj;
1558 char * pFileName = Ga2_GlaGetFileName(p, 0);
1559 Vec_Int_t * vMap = pAig->vGateClasses; pAig->vGateClasses = NULL;
1560 pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
1561 Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
1562 Gia_ManForEachAnd( pAig, pObj, i )
1563 Vec_IntWriteEntry( pAig->vGateClasses, i, 1 );
1564 Gia_ManForEachRo( pAig, pObj, i )
1565 Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjId(pAig, pObj), 1 );
1566 Gia_AigerWrite( pAig, pFileName, 0, 0, 0 );
1567 Vec_IntFree( pAig->vGateClasses );
1568 pAig->vGateClasses = vMap;
1569 if ( p->pPars->fVerbose )
1570 Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
1571 }
1572 }
1573 Abc_Print( 1, " Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" );
1574 }
1575 // iterate unrolling
1576 for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ )
1577 {
1578 int nAbsOld;
1579 // remember the timeframe
1580 p->pPars->iFrame = -1;
1581 // create new SAT solver
1582 Ga2_ManRestart( p );
1583 // remember abstraction size after the last restart
1584 nAbsOld = Vec_IntSize(p->vAbs);
1585 // unroll the circuit
1586 for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
1587 {
1588 // remember current limits
1589 int nConflsBeg = sat_solver2_nconflicts(p->pSat);
1590 int nAbs = Vec_IntSize(p->vAbs);
1591 int nValues = Vec_IntSize(p->vValues);
1592 int nVarsOld;
1593 // remember the timeframe
1594 p->pPars->iFrame = f;
1595 // extend and clear storage
1596 if ( f == Vec_PtrSize(p->vId2Lit) )
1597 Vec_PtrPush( p->vId2Lit, Vec_IntAlloc(0) );
1598 Vec_IntFillExtra( Ga2_MapFrameMap(p, f), Vec_IntSize(p->vValues), -1 );
1599 // add static clauses to this timeframe
1600 Ga2_ManAddAbsClauses( p, f );
1601 // skip checking if skipcheck is enabled (&gla -s)
1602 if ( p->pPars->fUseSkip && f <= p->pPars->iFrameProved )
1603 continue;
1604 // skip checking if we need to skip several starting frames (&gla -S <num>)
1605 if ( p->pPars->nFramesStart && f <= p->pPars->nFramesStart )
1606 continue;
1607 // get the output literal
1608// Lit = Ga2_ManUnroll_rec( p, Gia_ManPo(pAig,0), f );
1609 Lit = Ga2_ObjFindLit( p, Gia_ObjFanin0(Gia_ManPo(pAig,0)), f );
1610 assert( Lit >= 0 );
1611 Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(Gia_ManPo(pAig,0)) );
1612 if ( Lit == 0 )
1613 continue;
1614 assert( Lit > 1 );
1615 // check for counter-examples
1616 if ( p->nSatVars > sat_solver2_nvars(p->pSat) )
1617 sat_solver2_setnvars( p->pSat, p->nSatVars );
1618 nVarsOld = p->nSatVars;
1619 for ( c = 0; ; c++ )
1620 {
1621 // consider the special case when the target literal is implied false
1622 // by implications which happened as a result of previous refinements
1623 // note that incremental UNSAT core cannot be computed because there is no learned clauses
1624 // in this case, we will assume that UNSAT core cannot reduce the problem
1625 if ( var_is_assigned(p->pSat, Abc_Lit2Var(Lit)) )
1626 {
1627 Prf_ManStopP( &p->pSat->pPrf2 );
1628 break;
1629 }
1630 // perform SAT solving
1631 clk2 = Abc_Clock();
1632 Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1633 if ( Status == l_True ) // perform refinement
1634 {
1635 p->nCexes++;
1636 p->timeSat += Abc_Clock() - clk2;
1637
1638 // cancel old one if it was sent
1639 if ( Abc_FrameIsBridgeMode() && fOneIsSent )
1640 {
1641 Gia_Ga2SendCancel( p, pPars->fVerbose );
1642 fOneIsSent = 0;
1643 }
1644 if ( iFrameTryToProve >= 0 )
1645 {
1646 Gia_GlaProveCancel( pPars->fVerbose );
1647 iFrameTryToProve = -1;
1648 }
1649
1650 // perform refinement
1651 clk2 = Abc_Clock();
1652 Rnm_ManSetRefId( p->pRnm, c );
1653 vPPis = Ga2_ManRefine( p );
1654 p->timeCex += Abc_Clock() - clk2;
1655 if ( vPPis == NULL )
1656 {
1657 if ( pPars->fVerbose )
1658 Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, Abc_Clock() - clk, 1 );
1659 goto finish;
1660 }
1661
1662 if ( c == 0 )
1663 {
1664// Ga2_ManRefinePrintPPis( p );
1665 // create bookmark to be used for rollback
1666 assert( nVarsOld == p->pSat->size );
1667 sat_solver2_bookmark( p->pSat );
1668 // start incremental proof manager
1669 assert( p->pSat->pPrf2 == NULL );
1670 p->pSat->pPrf2 = Prf_ManAlloc();
1671 if ( p->pSat->pPrf2 )
1672 {
1673 p->nProofIds = 0;
1674 Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
1675 Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vPPis) );
1676 }
1677 }
1678 else
1679 {
1680 // resize the proof logger
1681 if ( p->pSat->pPrf2 )
1682 Prf_ManGrow( p->pSat->pPrf2, p->nProofIds + Vec_IntSize(vPPis) );
1683 }
1684
1685 Ga2_ManAddToAbs( p, vPPis );
1686 Vec_IntFree( vPPis );
1687 if ( pPars->fVerbose )
1688 Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c+1, Abc_Clock() - clk, 0 );
1689 // check if the number of objects is below limit
1690 if ( pPars->nRatioMin2 && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin2 / 100 )
1691 {
1692 Status = l_Undef;
1693 goto finish;
1694 }
1695 continue;
1696 }
1697 p->timeUnsat += Abc_Clock() - clk2;
1698 if ( Status == l_Undef ) // ran out of resources
1699 goto finish;
1700 if ( p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit ) // timeout
1701 goto finish;
1702 if ( c == 0 )
1703 {
1704 if ( f > p->pPars->iFrameProved )
1705 p->pPars->nFramesNoChange++;
1706 break;
1707 }
1708 if ( f > p->pPars->iFrameProved )
1709 p->pPars->nFramesNoChange = 0;
1710
1711 // derive the core
1712 assert( p->pSat->pPrf2 != NULL );
1713 vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat );
1714 Prf_ManStopP( &p->pSat->pPrf2 );
1715 // update the SAT solver
1716 sat_solver2_rollback( p->pSat );
1717 // reduce abstraction
1718 Ga2_ManShrinkAbs( p, nAbs, nValues, nVarsOld );
1719
1720 // purify UNSAT core
1721 if ( fUseSecondCore )
1722 {
1723// int nOldCore = Vec_IntSize(vCore);
1724 // reverse the order of objects in the core
1725// Vec_IntSort( vCore, 0 );
1726// Vec_IntPrint( vCore );
1727 // create bookmark to be used for rollback
1728 assert( nVarsOld == p->pSat->size );
1729 sat_solver2_bookmark( p->pSat );
1730 // start incremental proof manager
1731 assert( p->pSat->pPrf2 == NULL );
1732 p->pSat->pPrf2 = Prf_ManAlloc();
1733 if ( p->pSat->pPrf2 )
1734 {
1735 p->nProofIds = 0;
1736 Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
1737 Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vCore) );
1738
1739 Ga2_ManAddToAbs( p, vCore );
1740 Vec_IntFree( vCore );
1741 }
1742 // run SAT solver
1743 clk2 = Abc_Clock();
1744 Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1745 if ( Status == l_Undef )
1746 goto finish;
1747 assert( Status == l_False );
1748 p->timeUnsat += Abc_Clock() - clk2;
1749
1750 // derive the core
1751 assert( p->pSat->pPrf2 != NULL );
1752 vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat );
1753 Prf_ManStopP( &p->pSat->pPrf2 );
1754 // update the SAT solver
1755 sat_solver2_rollback( p->pSat );
1756 // reduce abstraction
1757 Ga2_ManShrinkAbs( p, nAbs, nValues, nVarsOld );
1758// printf( "\n%4d -> %4d\n", nOldCore, Vec_IntSize(vCore) );
1759 }
1760
1761 Ga2_ManAddToAbs( p, vCore );
1762// Ga2_ManRefinePrint( p, vCore );
1763 Vec_IntFree( vCore );
1764 break;
1765 }
1766 // remember the last proved frame
1767 if ( p->pPars->iFrameProved < f )
1768 p->pPars->iFrameProved = f;
1769 // print statistics
1770 if ( pPars->fVerbose )
1771 Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, Abc_Clock() - clk, 1 );
1772 // check if abstraction was proved
1773 if ( Gia_GlaProveCheck( pPars->fVerbose ) )
1774 {
1775 RetValue = 1;
1776 goto finish;
1777 }
1778 if ( c > 0 )
1779 {
1780 if ( p->pPars->fVeryVerbose )
1781 Abc_Print( 1, "\n" );
1782 // recompute the abstraction
1783 Vec_IntFreeP( &pAig->vGateClasses );
1784 pAig->vGateClasses = Ga2_ManAbsTranslate( p );
1785 // check if the number of objects is below limit
1786 if ( pPars->nRatioMin && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin / 100 )
1787 {
1788 Status = l_Undef;
1789 goto finish;
1790 }
1791 }
1792 // check the number of stable frames
1793 if ( p->pPars->nFramesNoChange == p->pPars->nFramesNoChangeLim )
1794 {
1795 // dump the model into file
1796 if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs )
1797 {
1798 char Command[1000];
1799 Abc_FrameSetStatus( -1 );
1800 Abc_FrameSetCex( NULL );
1801 Abc_FrameSetNFrames( f );
1802 sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status"));
1803 Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
1804 Ga2_GlaDumpAbsracted( p, pPars->fVerbose );
1805 }
1806 // call the prover
1807 if ( p->pPars->fCallProver )
1808 {
1809 // cancel old one if it is proving
1810 if ( iFrameTryToProve >= 0 )
1811 Gia_GlaProveCancel( pPars->fVerbose );
1812 // prove new one
1813 Gia_GlaProveAbsracted( pAig, pPars->fSimpProver, pPars->fVeryVerbose );
1814 iFrameTryToProve = f;
1815 p->nPdrCalls++;
1816 }
1817 // speak to the bridge
1818 if ( Abc_FrameIsBridgeMode() )
1819 {
1820 // cancel old one if it was sent
1821 if ( fOneIsSent )
1822 Gia_Ga2SendCancel( p, pPars->fVerbose );
1823 // send new one
1824 Gia_Ga2SendAbsracted( p, pPars->fVerbose );
1825 fOneIsSent = 1;
1826 }
1827 }
1828 // if abstraction grew more than a certain percentage, force a restart
1829 if ( pPars->nRatioMax == 0 )
1830 continue;
1831 if ( c > 0 && (f > 20 || Vec_IntSize(p->vAbs) > 100) && Vec_IntSize(p->vAbs) - nAbsOld >= nAbsOld * pPars->nRatioMax / 100 )
1832 {
1833 if ( p->pPars->fVerbose )
1834 Abc_Print( 1, "Forcing restart because abstraction grew from %d to %d (more than %d %%).\n",
1835 nAbsOld, Vec_IntSize(p->vAbs), pPars->nRatioMax );
1836 break;
1837 }
1838 }
1839 }
1840finish:
1841 Prf_ManStopP( &p->pSat->pPrf2 );
1842 // cancel old one if it is proving
1843 if ( iFrameTryToProve >= 0 )
1844 Gia_GlaProveCancel( pPars->fVerbose );
1845 // analize the results
1846 if ( !p->fUseNewLine )
1847 Abc_Print( 1, "\n" );
1848 if ( RetValue == 1 )
1849 Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d ", p->pPars->iFrameProved+1, iFrameTryToProve );
1850 else if ( pAig->pCexSeq == NULL )
1851 {
1852 Vec_IntFreeP( &pAig->vGateClasses );
1853 pAig->vGateClasses = Ga2_ManAbsTranslate( p );
1854 if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit )
1855 Abc_Print( 1, "GLA reached timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
1856 else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
1857 Abc_Print( 1, "GLA exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
1858 else if ( pPars->nRatioMin2 && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin2 / 100 )
1859 Abc_Print( 1, "GLA found that the size of abstraction exceeds %d %% in frame %d during refinement. ", pPars->nRatioMin2, p->pPars->iFrameProved+1 );
1860 else if ( pPars->nRatioMin && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin / 100 )
1861 Abc_Print( 1, "GLA found that the size of abstraction exceeds %d %% in frame %d. ", pPars->nRatioMin, p->pPars->iFrameProved+1 );
1862 else
1863 Abc_Print( 1, "GLA finished %d frames and produced a %d-stable abstraction. ", p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
1864 p->pPars->iFrame = p->pPars->iFrameProved;
1865 }
1866 else
1867 {
1868 if ( p->pPars->fVerbose )
1869 Abc_Print( 1, "\n" );
1870 if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
1871 Abc_Print( 1, " Gia_ManPerformGlaOld(): CEX verification has failed!\n" );
1872 Abc_Print( 1, "True counter-example detected in frame %d. ", f );
1873 p->pPars->iFrame = f - 1;
1874 Vec_IntFreeP( &pAig->vGateClasses );
1875 RetValue = 0;
1876 }
1877 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1878 if ( p->pPars->fVerbose )
1879 {
1880 p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
1881 ABC_PRTP( "Runtime: Initializing", p->timeInit, Abc_Clock() - clk );
1882 ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, Abc_Clock() - clk );
1883 ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, Abc_Clock() - clk );
1884 ABC_PRTP( "Runtime: Refinement ", p->timeCex, Abc_Clock() - clk );
1885 ABC_PRTP( "Runtime: Other ", p->timeOther, Abc_Clock() - clk );
1886 ABC_PRTP( "Runtime: TOTAL ", Abc_Clock() - clk, Abc_Clock() - clk );
1887 Ga2_ManReportMemory( p );
1888 }
1889// Ga2_ManDumpStats( p->pGia, p->pPars, p->pSat, p->pPars->iFrameProved, 0 );
1890 Ga2_ManStop( p );
1891 fflush( stdout );
1892 return RetValue;
1893}
1894
1898
1899
1900ABC_NAMESPACE_IMPL_END
1901
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition abc_global.h:258
Gia_ManToBridgeAbsNetlist
int Gia_ManToBridgeAbsNetlist(FILE *pFile, void *p, int pkg_type)
Definition utilBridge.c:192
ABC_PRMP
#define ABC_PRMP(a, f, F)
Definition abc_global.h:262
BRIDGE_ABS_NETLIST
#define BRIDGE_ABS_NETLIST
Definition abc_global.h:387
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Abc_FrameGetGlobalFrame
ABC_DLL Abc_Frame_t * Abc_FrameGetGlobalFrame()
Definition mainFrame.c:643
Ga2_GlaAbsCount
int Ga2_GlaAbsCount(Ga2_Man_t *p, int fRo, int fAnd)
Definition absGla.c:1344
Ga2_ManReportMemory
void Ga2_ManReportMemory(Ga2_Man_t *p)
Definition absGla.c:432
Ga2_ManDumpStats
void Ga2_ManDumpStats(Gia_Man_t *pGia, Abs_Par_t *pPars, sat_solver2 *pSat, int iFrame, int fUseN)
Definition absGla.c:410
Ga2_ManMarkup
int Ga2_ManMarkup(Gia_Man_t *p, int N, int fSimple)
Definition absGla.c:243
Ga2_ManRestart
void Ga2_ManRestart(Ga2_Man_t *p)
Definition absGla.c:1112
Ga2_ManAbsTranslate_rec
void Ga2_ManAbsTranslate_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vClasses, int fFirst)
Definition absGla.c:1067
Ga2_ManComputeTest
void Ga2_ManComputeTest(Gia_Man_t *p)
Definition absGla.c:338
Ga2_GlaPrepareCexAndMap
void Ga2_GlaPrepareCexAndMap(Ga2_Man_t *p, Abc_Cex_t **ppCex, Vec_Int_t **pvMaps)
Definition absGla.c:1247
Ga2_ManAbsDerive
Vec_Int_t * Ga2_ManAbsDerive(Gia_Man_t *p)
Definition absGla.c:1097
Ga2_Man_t
struct Ga2_Man_t_ Ga2_Man_t
Definition absGla.c:37
Ga2_ManAddToAbs
void Ga2_ManAddToAbs(Ga2_Man_t *p, Vec_Int_t *vToAdd)
Definition absGla.c:979
Ga2_GlaDumpAbsracted
void Ga2_GlaDumpAbsracted(Ga2_Man_t *p, int fVerbose)
Definition absGla.c:1421
Ga2_ManRefinePrint
void Ga2_ManRefinePrint(Ga2_Man_t *p, Vec_Int_t *vVec)
Definition absGla.c:1185
Ga2_ManAbsTranslate
Vec_Int_t * Ga2_ManAbsTranslate(Ga2_Man_t *p)
Definition absGla.c:1077
Ga2_ManCollectNodes_rec
void Ga2_ManCollectNodes_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vNodes, int fFirst)
Definition absGla.c:222
Gia_Ga2SendAbsracted
void Gia_Ga2SendAbsracted(Ga2_Man_t *p, int fVerbose)
Definition absGla.c:1464
Ga2_ManAddAbsClauses
void Ga2_ManAddAbsClauses(Ga2_Man_t *p, int f)
Definition absGla.c:959
Ga2_ManShrinkAbs
void Ga2_ManShrinkAbs(Ga2_Man_t *p, int nAbs, int nValues, int nSatVars)
Definition absGla.c:1009
Ga2_ManCollectLeaves_rec
void Ga2_ManCollectLeaves_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vLeaves, int fFirst)
Definition absGla.c:232
Gia_ManPerformGla
int Gia_ManPerformGla(Gia_Man_t *pAig, Abs_Par_t *pPars)
Definition absGla.c:1500
Ga2_ManBreakTree_rec
int Ga2_ManBreakTree_rec(Gia_Man_t *p, Gia_Obj_t *pObj, int fFirst, int N)
Definition absGla.c:176
Ga2_GlaGetFileName
char * Ga2_GlaGetFileName(Ga2_Man_t *p, int fAbs)
Definition absGla.c:1406
Ga2_ManRefinePrintPPis
void Ga2_ManRefinePrintPPis(Ga2_Man_t *p)
Definition absGla.c:1223
Ga2_ManStart
Ga2_Man_t * Ga2_ManStart(Gia_Man_t *pGia, Abs_Par_t *pPars)
Definition absGla.c:372
Ga2_ManCnfCompute
Vec_Int_t * Ga2_ManCnfCompute(unsigned uTruth, int nVars, Vec_Int_t *vCover)
Definition absGla.c:630
Ga2_ManCheckNodesAnd
int Ga2_ManCheckNodesAnd(Gia_Man_t *p, Vec_Int_t *vNodes)
Definition absGla.c:212
GA2_BIG_NUM
#define GA2_BIG_NUM
DECLARATIONS ///.
Definition absGla.c:35
Ga2_ManStop
void Ga2_ManStop(Ga2_Man_t *p)
Definition absGla.c:460
Gia_Ga2SendCancel
void Gia_Ga2SendCancel(Ga2_Man_t *p, int fVerbose)
Definition absGla.c:1480
Ga2_ObjComputeTruthSpecial
unsigned Ga2_ObjComputeTruthSpecial(Gia_Man_t *p, Gia_Obj_t *pRoot, Vec_Int_t *vLeaves, Vec_Int_t *vLits)
Definition absGla.c:512
Ga2_ManComputeTruth
unsigned Ga2_ManComputeTruth(Gia_Man_t *p, Gia_Obj_t *pRoot, Vec_Int_t *vLeaves)
Definition absGla.c:150
Ga2_ManCnfAddStatic
void Ga2_ManCnfAddStatic(sat_solver2 *pSat, Vec_Int_t *vCnf0, Vec_Int_t *vCnf1, int Lits[], int iLitOut, int ProofId)
Definition absGla.c:684
Ga2_ManAbsPrintFrame
void Ga2_ManAbsPrintFrame(Ga2_Man_t *p, int nFrames, int nConfls, int nCexes, abctime Time, int fFinal)
Definition absGla.c:1369
Ga2_ManDeriveCex
Abc_Cex_t * Ga2_ManDeriveCex(Ga2_Man_t *p, Vec_Int_t *vPis)
Definition absGla.c:1166
Ga2_ManRefine
Vec_Int_t * Ga2_ManRefine(Ga2_Man_t *p)
Definition absGla.c:1280
Ga2_ObjComputeTruth_rec
unsigned Ga2_ObjComputeTruth_rec(Gia_Man_t *p, Gia_Obj_t *pObj, int fFirst)
FUNCTION DEFINITIONS ///.
Definition absGla.c:140
Rnm_ManStop
void Rnm_ManStop(Rnm_Man_t *p, int fProfile)
Definition absRef.c:285
Rnm_ManMemoryUsage
double Rnm_ManMemoryUsage(Rnm_Man_t *p)
Definition absRef.c:317
Rnm_ManRefine
Vec_Int_t * Rnm_ManRefine(Rnm_Man_t *p, Abc_Cex_t *pCex, Vec_Int_t *vMap, int fPropFanout, int fNewRefinement, int fVerbose)
Definition absRef.c:673
Rnm_ManStart
Rnm_Man_t * Rnm_ManStart(Gia_Man_t *pGia)
FUNCTION DEFINITIONS ///.
Definition absRef.c:264
Rnm_Man_t
struct Rnm_Man_t_ Rnm_Man_t
Definition absRef.h:55
Gia_GlaCountNodes
int Gia_GlaCountNodes(Gia_Man_t *p, Vec_Int_t *vGla)
Definition absUtil.c:240
Gia_ManDupAbsGates
Gia_Man_t * Gia_ManDupAbsGates(Gia_Man_t *p, Vec_Int_t *vGateClasses)
Definition absDup.c:220
Abs_Par_t
typedefABC_NAMESPACE_HEADER_START struct Abs_Par_t_ Abs_Par_t
INCLUDES ///.
Definition abs.h:46
Gia_GlaProveCancel
void Gia_GlaProveCancel(int fVerbose)
Definition absPth.c:46
Gia_GlaProveAbsracted
void Gia_GlaProveAbsracted(Gia_Man_t *p, int fSimpProver, int fVerbose)
DECLARATIONS ///.
Definition absPth.c:45
Gia_GlaProveCheck
int Gia_GlaProveCheck(int fVerbose)
Definition absPth.c:47
Gia_GlaCountFlops
int Gia_GlaCountFlops(Gia_Man_t *p, Vec_Int_t *vGla)
Definition absUtil.c:231
Abc_FrameSetNFrames
ABC_DLL void Abc_FrameSetNFrames(int nFrames)
Definition mainFrame.c:100
Abc_FrameSetStatus
ABC_DLL void Abc_FrameSetStatus(int Status)
Definition mainFrame.c:101
Abc_FrameSetCex
ABC_DLL void Abc_FrameSetCex(Abc_Cex_t *pCex)
Definition mainFrame.c:99
Abc_FrameIsBridgeMode
ABC_DLL int Abc_FrameIsBridgeMode()
Definition mainFrame.c:113
Abc_FrameIsBatchMode
ABC_DLL int Abc_FrameIsBatchMode()
Definition mainFrame.c:110
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
l_True
#define l_True
Definition bmcBmcS.c:35
l_Undef
#define l_Undef
Definition bmcBmcS.c:34
l_False
#define l_False
Definition bmcBmcS.c:36
Cmd_CommandExecute
ABC_DLL int Cmd_CommandExecute(Abc_Frame_t *pAbc, const char *sCommand)
Definition cmdApi.c:193
Cnf_ReadMsops
void Cnf_ReadMsops(char **ppSopSizes, char ***ppSops)
FUNCTION DEFINITIONS ///.
Definition cnfData.c:4537
p
Cube * p
Definition exorList.c:222
Cube
struct cube Cube
Extra_FileNameGenericAppend
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition extraUtilFile.c:192
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition gia.h:1252
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ObjIsMuxType
int Gia_ObjIsMuxType(Gia_Obj_t *pNode)
Definition giaUtil.c:982
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Gia_ManCleanValue
void Gia_ManCleanValue(Gia_Man_t *p)
Definition giaUtil.c:351
Gia_ManVerifyCex
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition giaCex.c:48
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
Gia_ManSetPhase
void Gia_ManSetPhase(Gia_Man_t *p)
Definition giaUtil.c:420
Gia_AigerWrite
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine)
Definition giaAiger.c:1595
Kit_TruthIsop
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
Definition kitIsop.c:134
sat_solver2_memory_proof
double sat_solver2_memory_proof(sat_solver2 *s)
Definition satSolver2.c:1733
sat_solver2_delete
void sat_solver2_delete(sat_solver2 *s)
Definition satSolver2.c:1225
sat_solver2_memory
double sat_solver2_memory(sat_solver2 *s, int fAll)
Definition satSolver2.c:1692
var_is_assigned
int var_is_assigned(sat_solver2 *s, int v)
Definition satSolver2.c:83
sat_solver2_new
sat_solver2 * sat_solver2_new(void)
Definition satSolver2.c:1109
sat_solver2_rollback
void sat_solver2_rollback(sat_solver2 *s)
Definition satSolver2.c:1586
sat_solver2_solve
int sat_solver2_solve(sat_solver2 *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition satSolver2.c:1835
sat_solver2_setnvars
void sat_solver2_setnvars(sat_solver2 *s, int n)
Definition satSolver2.c:1170
Sat_ProofCore
void * Sat_ProofCore(sat_solver2 *s)
Definition satSolver2.c:1985
sat_solver2_addclause
int sat_solver2_addclause(sat_solver2 *s, lit *begin, lit *end, int Id)
Definition satSolver2.c:1287
sat_solver2
struct sat_solver2_t sat_solver2
Definition satSolver2.h:44
Ga2_Man_t_
Definition absGla.c:39
Ga2_Man_t_::timeInit
abctime timeInit
Definition absGla.c:77
Ga2_Man_t_::pRnm
Rnm_Man_t * pRnm
Definition absGla.c:56
Ga2_Man_t_::nPdrCalls
int nPdrCalls
Definition absGla.c:64
Ga2_Man_t_::timeSat
abctime timeSat
Definition absGla.c:78
Ga2_Man_t_::vValues
Vec_Int_t * vValues
Definition absGla.c:49
Ga2_Man_t_::timeStart
abctime timeStart
Definition absGla.c:76
Ga2_Man_t_::timeOther
abctime timeOther
Definition absGla.c:81
Ga2_Man_t_::nTable
int nTable
Definition absGla.c:67
Ga2_Man_t_::vCnfs
Vec_Ptr_t * vCnfs
Definition absGla.c:44
Ga2_Man_t_::nHashOver
int nHashOver
Definition absGla.c:70
Ga2_Man_t_::vIsopMem
Vec_Int_t * vIsopMem
Definition absGla.c:73
Ga2_Man_t_::pSopSizes
char * pSopSizes
Definition absGla.c:74
Ga2_Man_t_::pSat
sat_solver2 * pSat
Definition absGla.c:60
Ga2_Man_t_::nHashHit
int nHashHit
Definition absGla.c:68
Ga2_Man_t_::nMarked
int nMarked
Definition absGla.c:53
Ga2_Man_t_::nProofIds
int nProofIds
Definition absGla.c:50
Ga2_Man_t_::vAbs
Vec_Int_t * vAbs
Definition absGla.c:48
Ga2_Man_t_::vId2Lit
Vec_Ptr_t * vId2Lit
Definition absGla.c:59
Ga2_Man_t_::vProofIds
Vec_Int_t * vProofIds
Definition absGla.c:47
Ga2_Man_t_::nCexes
int nCexes
Definition absGla.c:62
Ga2_Man_t_::LimPpi
int LimPpi
Definition absGla.c:52
Ga2_Man_t_::vIds
Vec_Int_t * vIds
Definition absGla.c:46
Ga2_Man_t_::LimAbs
int LimAbs
Definition absGla.c:51
Ga2_Man_t_::pSops
char ** pSops
Definition absGla.c:74
Ga2_Man_t_::nObjAdded
int nObjAdded
Definition absGla.c:63
Ga2_Man_t_::pTable
int * pTable
Definition absGla.c:66
Ga2_Man_t_::pGia
Gia_Man_t * pGia
Definition absGla.c:41
Ga2_Man_t_::timeUnsat
abctime timeUnsat
Definition absGla.c:79
Ga2_Man_t_::nSatVars
int nSatVars
Definition absGla.c:61
Ga2_Man_t_::timeCex
abctime timeCex
Definition absGla.c:80
Ga2_Man_t_::fUseNewLine
int fUseNewLine
Definition absGla.c:54
Ga2_Man_t_::pPars
Abs_Par_t * pPars
Definition absGla.c:42
Ga2_Man_t_::vLits
Vec_Int_t * vLits
Definition absGla.c:72
Ga2_Man_t_::nHashMiss
int nHashMiss
Definition absGla.c:69
Gia_Man_t_::vGateClasses
Vec_Int_t * vGateClasses
Definition gia.h:157
Gia_Man_t_::pCexSeq
Abc_Cex_t * pCexSeq
Definition gia.h:150
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Gia_Obj_t_::fPhase
unsigned fPhase
Definition gia.h:87
Gia_ManToBridgeBadAbs
int Gia_ManToBridgeBadAbs(FILE *pFile)
Definition utilBridge.c:202
Abc_CexFreeP
void Abc_CexFreeP(Abc_Cex_t **p)
Definition utilCex.c:361
Abc_CexMakeTriv
Abc_Cex_t * Abc_CexMakeTriv(int nRegs, int nTruePis, int nTruePos, int iFrameOut)
Definition utilCex.c:85
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition utilCex.c:382
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition utilCex.c:51
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
assert
#define assert(ex)
Definition util_old.h:213
memcpy
char * memcpy()
memset
char * memset()
memcmp
int memcmp()
sprintf
char * sprintf()
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42