ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cecSplit.c
Go to the documentation of this file.
1
20
21#include <math.h>
22#include "aig/gia/gia.h"
23#include "aig/gia/giaAig.h"
24#include "sat/cnf/cnf.h"
25#include "sat/bsat/satSolver.h"
26#include "misc/util/utilTruth.h"
27//#include "bdd/cudd/cuddInt.h"
28
29#ifdef ABC_USE_PTHREADS
30
31#ifdef _WIN32
32#include "../lib/pthread.h"
33#else
34#include <pthread.h>
35#include <unistd.h>
36#endif
37
38#endif
39
40ABC_NAMESPACE_IMPL_START
41
42
46
47#ifndef ABC_USE_PTHREADS
48
49int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; }
50
51#else // pthreads are used
52
56
57#if 0 // BDD code
58
70DdManager * Gia_ManBuildBdd( Gia_Man_t * p, Vec_Ptr_t ** pvNodes, int nSkip )
71{
72 abctime clk = Abc_Clock();
73 DdManager * dd;
74 DdNode * bBdd, * bBdd0, * bBdd1;
75 Vec_Ptr_t * vNodes;
76 Gia_Obj_t * pObj;
77 int i;
78 vNodes = Vec_PtrStart( Gia_ManObjNum(p) );
79 dd = Cudd_Init( Gia_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
80// Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
81 bBdd = Cudd_ReadLogicZero(dd); Cudd_Ref( bBdd );
82 Vec_PtrWriteEntry( vNodes, 0, bBdd );
83 Gia_ManForEachPi( p, pObj, i )
84 {
85 bBdd = i > nSkip ? Cudd_bddIthVar(dd, i) : Cudd_ReadLogicZero(dd); Cudd_Ref( bBdd );
86 Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd );
87 }
88 Gia_ManForEachAnd( p, pObj, i )
89 {
90 bBdd0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj) );
91 bBdd1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj) );
92 bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( bBdd );
93 Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd );
94 if ( i % 10 == 0 )
95 printf( "%d ", i );
96// if ( i == 3000 )
97// break;
98 }
99 printf( "\n" );
100 Gia_ManForEachPo( p, pObj, i )
101 {
102 bBdd = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vNodes, Gia_ObjFaninId0(pObj, Gia_ObjId(p, pObj))), Gia_ObjFaninC0(pObj) ); Cudd_Ref( bBdd );
103 Vec_PtrWriteEntry( vNodes, Gia_ObjId(p, pObj), bBdd );
104 }
105 if ( bBdd == Cudd_ReadLogicZero(dd) )
106 printf( "Equivalent!\n" );
107 else
108 printf( "Not tquivalent!\n" );
109 if ( pvNodes )
110 *pvNodes = vNodes;
111 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
112 return dd;
113}
114void Gia_ManDerefBdd( DdManager * dd, Vec_Ptr_t * vNodes )
115{
116 DdNode * bBdd;
117 int i;
118 Vec_PtrForEachEntry( DdNode *, vNodes, bBdd, i )
119 if ( bBdd )
120 Cudd_RecursiveDeref( dd, bBdd );
121 if ( Cudd_CheckZeroRef(dd) > 0 )
122 printf( "The number of referenced nodes = %d\n", Cudd_CheckZeroRef(dd) );
123 Cudd_PrintInfo( dd, stdout );
124 Cudd_Quit( dd );
125}
126void Gia_ManBuildBddTest( Gia_Man_t * p )
127{
128 Vec_Ptr_t * vNodes;
129 DdManager * dd = Gia_ManBuildBdd( p, &vNodes, 50 );
130 Gia_ManDerefBdd( dd, vNodes );
131}
132
133#endif // BDD code
134
146void Cec_GiaSplitExplore( Gia_Man_t * p )
147{
148 Gia_Obj_t * pObj, * pFan0, * pFan1;
149 int i, Counter = 0;
150 assert( p->pMuxes == NULL );
151 ABC_FREE( p->pRefs );
152 Gia_ManCreateRefs( p );
153 Gia_ManForEachAnd( p, pObj, i )
154 {
155 if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
156 continue;
157 if ( Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)) > 1 &&
158 Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) > 1 )
159 continue;
160 printf( "%5d : ", Counter++ );
161 printf( "%2d %2d ", Gia_ObjRefNum(p, Gia_Regular(pFan0)), Gia_ObjRefNum(p, Gia_Regular(pFan1)) );
162 printf( "%2d %2d \n", Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)), Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) );
163 }
164}
165
177int * Gia_PermuteSpecialOrder( Gia_Man_t * p )
178{
179 Vec_Int_t * vPerm;
180 Gia_Obj_t * pObj;
181 int i, * pOrder;
182 Gia_ManCreateRefs( p );
183 vPerm = Vec_IntAlloc( Gia_ManPiNum(p) );
184 Gia_ManForEachPi( p, pObj, i )
185 Vec_IntPush( vPerm, Gia_ObjRefNum(p, pObj) );
186 pOrder = Abc_QuickSortCost( Vec_IntArray(vPerm), Vec_IntSize(vPerm), 1 );
187 Vec_IntFree( vPerm );
188 return pOrder;
189}
190Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p )
191{
192 Gia_Man_t * pNew;
193 Vec_Int_t * vPerm;
194 int * pOrder = Gia_PermuteSpecialOrder( p );
195 vPerm = Vec_IntAllocArray( pOrder, Gia_ManPiNum(p) );
196 pNew = Gia_ManDupPerm( p, vPerm );
197 Vec_IntFree( vPerm );
198 return pNew;
199}
200
212int Gia_SplitCofVar2( Gia_Man_t * p, int * pnFanouts, int * pnCost )
213{
214 Gia_Obj_t * pObj;
215 int i, iBest = -1, CostBest = -1;
216 if ( p->pRefs == NULL )
217 Gia_ManCreateRefs( p );
218 Gia_ManForEachPi( p, pObj, i )
219 if ( CostBest < Gia_ObjRefNum(p, pObj) )
220 iBest = i, CostBest = Gia_ObjRefNum(p, pObj);
221 assert( iBest >= 0 );
222 *pnFanouts = Gia_ObjRefNum(p, Gia_ManPi(p, iBest));
223 *pnCost = -1;
224 return iBest;
225}
226int Gia_SplitCofVar( Gia_Man_t * p, int LookAhead, int * pnFanouts, int * pnCost )
227{
228 Gia_Man_t * pPart;
229 int Cost0, Cost1, CostBest = ABC_INFINITY;
230 int * pOrder, i, iBest = -1;
231 if ( LookAhead == 1 )
232 return Gia_SplitCofVar2( p, pnFanouts, pnCost );
233 pOrder = Gia_PermuteSpecialOrder( p );
234 LookAhead = Abc_MinInt( LookAhead, Gia_ManPiNum(p) );
235 for ( i = 0; i < LookAhead; i++ )
236 {
237 pPart = Gia_ManDupCofactorVar( p, pOrder[i], 0 );
238 Cost0 = Gia_ManAndNum(pPart);
239 Gia_ManStop( pPart );
240
241 pPart = Gia_ManDupCofactorVar( p, pOrder[i], 1 );
242 Cost1 = Gia_ManAndNum(pPart);
243 Gia_ManStop( pPart );
244
245 if ( CostBest > Cost0 + Cost1 )
246 CostBest = Cost0 + Cost1, iBest = pOrder[i];
247
248/*
249 pPart = Gia_ManDupExist( p, pOrder[i] );
250 printf( "%2d : Var = %4d Refs = %3d %6d %6d -> %6d %6d -> %6d\n",
251 i, pOrder[i], Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])),
252 Cost0, Cost1, Cost0+Cost1, Gia_ManAndNum(p), Gia_ManAndNum(pPart) );
253 Gia_ManStop( pPart );
254
255 printf( "%2d : Var = %4d Refs = %3d %6d %6d -> %6d\n",
256 i, pOrder[i], Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])),
257 Cost0, Cost1, Cost0+Cost1 );
258*/
259 }
260 ABC_FREE( pOrder );
261 assert( iBest >= 0 );
262 *pnFanouts = Gia_ObjRefNum(p, Gia_ManPi(p, iBest));
263 *pnCost = CostBest;
264 return iBest;
265}
266
278Abc_Cex_t * Cec_SplitDeriveModel( Gia_Man_t * p, Cnf_Dat_t * pCnf, sat_solver * pSat )
279{
280 Abc_Cex_t * pCex;
281 Gia_Obj_t * pObj;
282 int i, iLit, * pModel;
283 pModel = ABC_CALLOC( int, Gia_ManPiNum(p) );
284 Gia_ManForEachPi( p, pObj, i )
285 pModel[i] = sat_solver_var_value(pSat, pCnf->pVarNums[Gia_ObjId(p, pObj)]);
286 if ( p->vCofVars )
287 Vec_IntForEachEntry( p->vCofVars, iLit, i )
288 pModel[Abc_Lit2Var(iLit)] = !Abc_LitIsCompl(iLit);
289 pCex = Abc_CexCreate( 0, Gia_ManPiNum(p), pModel, 0, 0, 0 );
290 ABC_FREE( pModel );
291 return pCex;
292}
293
305static inline Cnf_Dat_t * Cec_GiaDeriveGiaRemapped( Gia_Man_t * p )
306{
307 Cnf_Dat_t * pCnf;
308 Aig_Man_t * pAig = Gia_ManToAigSimple( p );
309 pAig->nRegs = 0;
310 pCnf = Cnf_Derive( pAig, 0 );//Aig_ManCoNum(pAig) );
311 Aig_ManStop( pAig );
312 return pCnf;
313}
314static inline sat_solver * Cec_GiaDeriveSolver( Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut )
315{
316 sat_solver * pSat;
317 int i;
318 pSat = sat_solver_new();
319 sat_solver_setnvars( pSat, pCnf->nVars );
320 for ( i = 0; i < pCnf->nClauses; i++ )
321 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
322 {
323 // the problem is UNSAT
324 sat_solver_delete( pSat );
325 return NULL;
326 }
327 sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
328 return pSat;
329}
330static inline int Cnf_GiaSolveOne( Gia_Man_t * p, Cnf_Dat_t * pCnf, int nTimeOut, int * pnVars, int * pnConfs )
331{
332 int status;
333 sat_solver * pSat = Cec_GiaDeriveSolver( p, pCnf, nTimeOut );
334 if ( pSat == NULL )
335 {
336 *pnVars = 0;
337 *pnConfs = 0;
338 return 1;
339 }
340 status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
341 *pnVars = sat_solver_nvars( pSat );
342 *pnConfs = sat_solver_nconflicts( pSat );
343 if ( status == l_True )
344 p->pCexComb = Cec_SplitDeriveModel( p, pCnf, pSat );
345 sat_solver_delete( pSat );
346 if ( status == l_Undef )
347 return -1;
348 if ( status == l_False )
349 return 1;
350 return 0;
351}
352static inline void Cec_GiaSplitClean( Vec_Ptr_t * vStack )
353{
354 Gia_Man_t * pNew;
355 int i;
356 Vec_PtrForEachEntry( Gia_Man_t *, vStack, pNew, i )
357 Gia_ManStop( pNew );
358 Vec_PtrFree( vStack );
359}
360
372void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fStatus, double Prog, abctime clk )
373{
374 printf( "%4d : ", nIter );
375 printf( "Depth =%3d ", Depth );
376 printf( "SatVar =%7d ", nVars );
377 printf( "SatConf =%7d ", nConfs );
378 printf( "%s ", fStatus ? (fStatus == 1 ? "UNSAT " : "UNDECIDED") : "SAT " );
379 printf( "Solved %8.4f %% ", 100*Prog );
380 Abc_PrintTime( 1, "Time", clk );
381 //ABC_PRTr( "Time", Abc_Clock()-clk );
382 fflush( stdout );
383}
384void Cec_GiaSplitPrintRefs( Gia_Man_t * p )
385{
386 Gia_Obj_t * pObj;
387 int i;
388 if ( p->pRefs == NULL )
389 Gia_ManCreateRefs( p );
390 Gia_ManForEachPi( p, pObj, i )
391 printf( "%d ", Gia_ObjRefNum(p, pObj) );
392 printf( "\n" );
393}
394
406int Cec_GiaSplitTest2( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent )
407{
408 abctime clkTotal = Abc_Clock();
409 Vec_Ptr_t * vStack;
410 Cnf_Dat_t * pCnf;
411 int nSatVars, nSatConfs;
412 int nIter, status, RetValue = -1;
413 double Progress = 0;
414 // check the problem
415 pCnf = Cec_GiaDeriveGiaRemapped( p );
416 status = Cnf_GiaSolveOne( p, pCnf, nTimeOut, &nSatVars, &nSatConfs );
417 Cnf_DataFree( pCnf );
418 if ( fVerbose )
419 Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
420 if ( status == 0 )
421 {
422 if ( !fSilent )
423 printf( "The problem is SAT without cofactoring.\n" );
424 return 0;
425 }
426 if ( status == 1 )
427 {
428 if ( !fSilent )
429 printf( "The problem is UNSAT without cofactoring.\n" );
430 return 1;
431 }
432 assert( status == -1 );
433 // create local copy
434 vStack = Vec_PtrAlloc( 1000 );
435 Vec_PtrPush( vStack, Gia_ManDup(p) );
436 // start with the current problem
437 for ( nIter = 1; Vec_PtrSize(vStack) > 0; nIter++ )
438 {
439 // get the last AIG
440 Gia_Man_t * pLast = (Gia_Man_t *)Vec_PtrPop( vStack );
441 // determine cofactoring variable
442 int Depth = 1 + (pLast->vCofVars ? Vec_IntSize(pLast->vCofVars) : 0);
443 int nFanouts, Cost, iVar = Gia_SplitCofVar( pLast, LookAhead, &nFanouts, &Cost );
444 // cofactor
445 Gia_Man_t * pPart = Gia_ManDupCofactorVar( pLast, iVar, 0 );
446 if ( pLast->vCofVars == NULL )
447 pLast->vCofVars = Vec_IntAlloc( 100 );
448 // print results
449 if ( fVeryVerbose )
450 {
451// Cec_GiaSplitPrintRefs( pLast );
452 printf( "Var = %5d. Fanouts = %5d. Cost = %8d. AndBefore = %6d. AndAfter = %6d.\n",
453 iVar, nFanouts, Cost, Gia_ManAndNum(pLast), Gia_ManAndNum(pPart) );
454// Cec_GiaSplitPrintRefs( pPart );
455 }
456 // create variable
457 pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
458 Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
459 Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) );
460 // solve the problem
461 pCnf = Cec_GiaDeriveGiaRemapped( pPart );
462 status = Cnf_GiaSolveOne( pPart, pCnf, nTimeOut, &nSatVars, &nSatConfs );
463 Cnf_DataFree( pCnf );
464 if ( status == 1 )
465 Progress += 1.0 / pow((double)2, (double)Depth);
466 if ( fVerbose )
467 Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
468 if ( status == 0 ) // SAT
469 {
470 p->pCexComb = pPart->pCexComb; pPart->pCexComb = NULL;
471 Gia_ManStop( pLast );
472 Gia_ManStop( pPart );
473 RetValue = 0;
474 break;
475 }
476 if ( status == 1 ) // UNSAT
477 Gia_ManStop( pPart );
478 else // UNDEC
479 Vec_PtrPush( vStack, pPart );
480 // cofactor
481 pPart = Gia_ManDupCofactorVar( pLast, iVar, 1 );
482 // create variable
483 pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
484 Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
485 Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 0) );
486 Gia_ManStop( pLast );
487 // solve the problem
488 pCnf = Cec_GiaDeriveGiaRemapped( pPart );
489 status = Cnf_GiaSolveOne( pPart, pCnf, nTimeOut, &nSatVars, &nSatConfs );
490 Cnf_DataFree( pCnf );
491 if ( status == 1 )
492 Progress += 1.0 / pow((double)2, (double)Depth);
493 if ( fVerbose )
494 Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
495 if ( status == 0 ) // SAT
496 {
497 p->pCexComb = pPart->pCexComb; pPart->pCexComb = NULL;
498 Gia_ManStop( pPart );
499 RetValue = 0;
500 break;
501 }
502 if ( status == 1 ) // UNSAT
503 Gia_ManStop( pPart );
504 else // UNDEC
505 Vec_PtrPush( vStack, pPart );
506 if ( nIterMax && nIter >= nIterMax )
507 break;
508 }
509 if ( Vec_PtrSize(vStack) == 0 )
510 RetValue = 1;
511 // finish
512 Cec_GiaSplitClean( vStack );
513 if ( !fSilent )
514 {
515 if ( RetValue == 0 )
516 printf( "Problem is SAT " );
517 else if ( RetValue == 1 )
518 printf( "Problem is UNSAT " );
519 else if ( RetValue == -1 )
520 printf( "Problem is UNDECIDED " );
521 else assert( 0 );
522 printf( "after %d case-splits. ", nIter );
523 Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
524 fflush( stdout );
525 }
526 return RetValue;
527}
528
540#define PAR_THR_MAX 100
541typedef struct Par_ThData_t_
542{
543 Gia_Man_t * p;
544 Cnf_Dat_t * pCnf;
545 int iThread;
546 int nTimeOut;
547 int fWorking;
548 int Result;
549 int nVars;
550 int nConfs;
551} Par_ThData_t;
552void * Cec_GiaSplitWorkerThread( void * pArg )
553{
554 Par_ThData_t * pThData = (Par_ThData_t *)pArg;
555 volatile int * pPlace = &pThData->fWorking;
556 while ( 1 )
557 {
558 while ( *pPlace == 0 );
559 assert( pThData->fWorking );
560 if ( pThData->p == NULL )
561 {
562 pthread_exit( NULL );
563 assert( 0 );
564 return NULL;
565 }
566 pThData->Result = Cnf_GiaSolveOne( pThData->p, pThData->pCnf, pThData->nTimeOut, &pThData->nVars, &pThData->nConfs );
567 pThData->fWorking = 0;
568 }
569 assert( 0 );
570 return NULL;
571}
572int Cec_GiaSplitTestInt( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent )
573{
574 abctime clkTotal = Abc_Clock();
575 Par_ThData_t ThData[PAR_THR_MAX];
576 pthread_t WorkerThread[PAR_THR_MAX];
577 Vec_Ptr_t * vStack;
578 Cnf_Dat_t * pCnf;
579 double Progress = 0;
580 int i, status, nSatVars, nSatConfs;
581 int nIter = 0, RetValue = -1, fWorkToDo = 1;
582 Abc_CexFreeP( &p->pCexComb );
583 if ( fVerbose )
584 printf( "Solving CEC problem by cofactoring with the following parameters:\n" );
585 if ( fVerbose )
586 printf( "Processes = %d TimeOut = %d sec MaxIter = %d LookAhead = %d Verbose = %d.\n", nProcs, nTimeOut, nIterMax, LookAhead, fVerbose );
587 fflush( stdout );
588 if ( nProcs == 1 )
589 return Cec_GiaSplitTest2( p, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose, fSilent );
590 // subtract manager thread
591 nProcs--;
592 assert( nProcs >= 1 && nProcs <= PAR_THR_MAX );
593 // check the problem
594 pCnf = Cec_GiaDeriveGiaRemapped( p );
595 status = Cnf_GiaSolveOne( p, pCnf, nTimeOut, &nSatVars, &nSatConfs );
596 Cnf_DataFree( pCnf );
597 if ( fVerbose && status != -1 )
598 Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, status, Progress, Abc_Clock() - clkTotal );
599 if ( status == 0 )
600 {
601 if ( !fSilent )
602 printf( "The problem is SAT without cofactoring.\n" );
603 return 0;
604 }
605 if ( status == 1 )
606 {
607 if ( !fSilent )
608 printf( "The problem is UNSAT without cofactoring.\n" );
609 return 1;
610 }
611 assert( status == -1 );
612 // create local copy
613 vStack = Vec_PtrAlloc( 1000 );
614 Vec_PtrPush( vStack, Gia_ManDup(p) );
615 // start threads
616 for ( i = 0; i < nProcs; i++ )
617 {
618 ThData[i].p = NULL;
619 ThData[i].pCnf = NULL;
620 ThData[i].iThread = i;
621 ThData[i].nTimeOut = nTimeOut;
622 ThData[i].fWorking = 0;
623 ThData[i].Result = -1;
624 ThData[i].nVars = -1;
625 ThData[i].nConfs = -1;
626 status = pthread_create( WorkerThread + i, NULL,Cec_GiaSplitWorkerThread, (void *)(ThData + i) ); assert( status == 0 );
627 }
628 // look at the threads
629 while ( fWorkToDo )
630 {
631 fWorkToDo = (int)(Vec_PtrSize(vStack) > 0);
632 for ( i = 0; i < nProcs; i++ )
633 {
634 // check if this thread is working
635 if ( ThData[i].fWorking )
636 {
637 fWorkToDo = 1;
638 continue;
639 }
640 // check if this thread has recently finished
641 if ( ThData[i].p != NULL )
642 {
643 Gia_Man_t * pLast = ThData[i].p;
644 int Depth = pLast->vCofVars ? Vec_IntSize(pLast->vCofVars) : 0;
645 if ( pLast->vCofVars == NULL )
646 pLast->vCofVars = Vec_IntAlloc( 100 );
647 if ( fVerbose )
648 Cec_GiaSplitPrint( i+1, Depth, ThData[i].nVars, ThData[i].nConfs, ThData[i].Result, Progress, Abc_Clock() - clkTotal );
649 if ( ThData[i].Result == 0 ) // SAT
650 {
651 p->pCexComb = pLast->pCexComb; pLast->pCexComb = NULL;
652 RetValue = 0;
653 goto finish;
654 }
655 if ( ThData[i].Result == -1 ) // UNDEC
656 {
657 // determine cofactoring variable
658 int nFanouts, Cost, iVar = Gia_SplitCofVar( pLast, LookAhead, &nFanouts, &Cost );
659 // cofactor
660 Gia_Man_t * pPart = Gia_ManDupCofactorVar( pLast, iVar, 0 );
661 pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
662 Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
663 Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) );
664 Vec_PtrPush( vStack, pPart );
665 // print results
666 if ( fVeryVerbose )
667 {
668// Cec_GiaSplitPrintRefs( pLast );
669 printf( "Var = %5d. Fanouts = %5d. Cost = %8d. AndBefore = %6d. AndAfter = %6d.\n",
670 iVar, nFanouts, Cost, Gia_ManAndNum(pLast), Gia_ManAndNum(pPart) );
671// Cec_GiaSplitPrintRefs( pPart );
672 }
673 // cofactor
674 pPart = Gia_ManDupCofactorVar( pLast, iVar, 1 );
675 pPart->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
676 Vec_IntAppend( pPart->vCofVars, pLast->vCofVars );
677 Vec_IntPush( pPart->vCofVars, Abc_Var2Lit(iVar, 1) );
678 Vec_PtrPush( vStack, pPart );
679 // keep working
680 fWorkToDo = 1;
681 nIter++;
682 }
683 else
684 Progress += 1.0 / pow((double)2, (double)Depth);
685 Gia_ManStopP( &ThData[i].p );
686 if ( ThData[i].pCnf == NULL )
687 continue;
688 Cnf_DataFree( ThData[i].pCnf );
689 ThData[i].pCnf = NULL;
690 }
691 if ( Vec_PtrSize(vStack) == 0 )
692 continue;
693 // start a new thread
694 assert( ThData[i].p == NULL );
695 ThData[i].p = (Gia_Man_t*)Vec_PtrPop( vStack );
696 ThData[i].pCnf = Cec_GiaDeriveGiaRemapped( ThData[i].p );
697 ThData[i].fWorking = 1;
698 }
699 if ( nIterMax && nIter >= nIterMax )
700 break;
701 }
702 if ( !fWorkToDo )
703 RetValue = 1;
704finish:
705 // wait till threads finish
706 for ( i = 0; i < nProcs; i++ )
707 if ( ThData[i].fWorking )
708 i = -1;
709 // stop threads
710 for ( i = 0; i < nProcs; i++ )
711 {
712 assert( !ThData[i].fWorking );
713 // cleanup
714 Gia_ManStopP( &ThData[i].p );
715 if ( ThData[i].pCnf == NULL )
716 continue;
717 Cnf_DataFree( ThData[i].pCnf );
718 ThData[i].pCnf = NULL;
719 // stop
720 ThData[i].p = NULL;
721 ThData[i].fWorking = 1;
722 }
723 // finish
724 Cec_GiaSplitClean( vStack );
725 if ( !fSilent )
726 {
727 if ( RetValue == 0 )
728 printf( "Problem is SAT " );
729 else if ( RetValue == 1 )
730 printf( "Problem is UNSAT " );
731 else if ( RetValue == -1 )
732 printf( "Problem is UNDECIDED " );
733 else assert( 0 );
734 printf( "after %d case-splits. ", nIter );
735 Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
736 fflush( stdout );
737 }
738 return RetValue;
739}
740int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent )
741{
742 Abc_Cex_t * pCex = NULL;
743 Gia_Man_t * pOne;
744 Gia_Obj_t * pObj;
745 int i, RetValue1, fOneUndef = 0, RetValue = -1;
746 Abc_CexFreeP( &p->pCexComb );
747 Gia_ManForEachPo( p, pObj, i )
748 {
749 pOne = Gia_ManDupOutputGroup( p, i, i+1 );
750 if ( fVerbose )
751 printf( "\nSolving output %d:\n", i );
752 RetValue1 = Cec_GiaSplitTestInt( pOne, nProcs, nTimeOut, nIterMax, LookAhead, fVerbose, fVeryVerbose, fSilent );
753 Gia_ManStop( pOne );
754 // collect the result
755 if ( RetValue1 == 0 && RetValue == -1 )
756 {
757 pCex = pOne->pCexComb; pOne->pCexComb = NULL;
758 pCex->iPo = i;
759 RetValue = 0;
760 }
761 if ( RetValue1 == -1 )
762 fOneUndef = 1;
763 }
764 if ( RetValue == -1 )
765 RetValue = fOneUndef ? -1 : 1;
766 else
767 p->pCexComb = pCex;
768 return RetValue;
769}
770
782void Cec_GiaPrintCofStats( Gia_Man_t * p )
783{
784 Gia_Man_t * pCof0, * pCof1;
785 Gia_Obj_t * pObj, * pFan0, * pFan1, * pCtrl;
786 Vec_Int_t * vMarks;
787 int i, Count = 0;
788 vMarks = Vec_IntStart( Gia_ManObjNum(p) );
789 Gia_ManForEachAnd( p, pObj, i )
790 {
791 if ( !Gia_ObjIsMuxType(pObj) )
792 continue;
793 if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
794 continue;
795 pCtrl = Gia_ObjRecognizeMux( pObj, &pFan1, &pFan0 );
796 pCtrl = Gia_Regular(pCtrl);
797 Vec_IntAddToEntry( vMarks, Gia_ObjId(p, pCtrl), 1 );
798 }
799 printf( "The AIG with %d candidate nodes (PI+AND) has %d unique MUX control drivers:\n",
800 Gia_ManCandNum(p), Vec_IntCountPositive(vMarks) );
801 Gia_ManLevelNum( p );
802 Gia_ManForEachCand( p, pObj, i )
803 {
804 if ( !Vec_IntEntry(vMarks, i) )
805 continue;
806 pCof0 = Gia_ManDupCofactorObj( p, i, 0 );
807 pCof1 = Gia_ManDupCofactorObj( p, i, 1 );
808 printf( "%6d : ", Count++ );
809 printf( "Obj = %6d ", i );
810 printf( "MUX refs = %5d ", Vec_IntEntry(vMarks, i) );
811 printf( "Level = %5d ", Gia_ObjLevelId(p, i) );
812 printf( "Cof0 = %7d ", Gia_ManAndNum(pCof0) );
813 printf( "Cof1 = %7d ", Gia_ManAndNum(pCof1) );
814 printf( "\n" );
815 Gia_ManStop( pCof0 );
816 Gia_ManStop( pCof1 );
817 }
818 Vec_IntFree( vMarks );
819}
820void Cec_GiaPrintCofStats2( Gia_Man_t * p )
821{
822 Gia_Man_t * pCof0, * pCof1;
823 Gia_Obj_t * pObj;
824 int i;
825 Gia_ManLevelNum( p );
826 Gia_ManCreateRefs( p );
827 Gia_ManForEachPi( p, pObj, i )
828 {
829 pCof0 = Gia_ManDupCofactorVar( p, i, 0 );
830 pCof1 = Gia_ManDupCofactorVar( p, i, 1 );
831 printf( "PI %5d : ", i );
832 printf( "Refs = %5d ", Gia_ObjRefNum(p, pObj) );
833 printf( "Cof0 = %7d ", Gia_ManAndNum(pCof0) );
834 printf( "Cof1 = %7d ", Gia_ManAndNum(pCof1) );
835 printf( "\n" );
836 Gia_ManStop( pCof0 );
837 Gia_ManStop( pCof1 );
838 }
839}
840
841#endif // pthreads are used
842
846
847
848ABC_NAMESPACE_IMPL_END
849
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
Abc_QuickSortCost
int * Abc_QuickSortCost(int *pCosts, int nSize, int fDecrease)
Definition utilSort.c:923
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
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
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
PAR_THR_MAX
#define PAR_THR_MAX
DECLARATIONS ///.
Definition bmcBmcG.c:31
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
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
Cec_GiaSplitTest
ABC_NAMESPACE_IMPL_START int Cec_GiaSplitTest(Gia_Man_t *p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose, int fSilent)
DECLARATIONS ///.
Definition cecSplit.c:49
Cnf_Derive
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition cnfCore.c:165
Cnf_Dat_t
struct Cnf_Dat_t_ Cnf_Dat_t
Definition cnf.h:52
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition cnfMan.c:207
p
Cube * p
Definition exorList.c:222
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition giaAig.c:408
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition giaDup.c:720
Gia_ObjRecognizeMux
Gia_Obj_t * Gia_ObjRecognizeMux(Gia_Obj_t *pNode, Gia_Obj_t **ppNodeT, Gia_Obj_t **ppNodeE)
Definition giaUtil.c:1056
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition gia.h:1250
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManDupOutputGroup
Gia_Man_t * Gia_ManDupOutputGroup(Gia_Man_t *p, int iOutStart, int iOutStop)
Definition giaDup.c:313
Gia_ManForEachCand
#define Gia_ManForEachCand(p, pObj, i)
Definition gia.h:1220
Gia_ManStopP
void Gia_ManStopP(Gia_Man_t **p)
Definition giaMan.c:224
Gia_ManDupCofactorVar
Gia_Man_t * Gia_ManDupCofactorVar(Gia_Man_t *p, int iVar, int Value)
Definition giaDup.c:1861
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition gia.h:1248
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManDupPerm
Gia_Man_t * Gia_ManDupPerm(Gia_Man_t *p, Vec_Int_t *vPiPerm)
Definition giaDup.c:929
Gia_ManDupCofactorObj
Gia_Man_t * Gia_ManDupCofactorObj(Gia_Man_t *p, int iObj, int Value)
Definition giaDup.c:1935
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_ObjRecognizeExor
int Gia_ObjRecognizeExor(Gia_Obj_t *pObj, Gia_Obj_t **ppFan0, Gia_Obj_t **ppFan1)
Definition giaUtil.c:1018
Gia_ManCreateRefs
void Gia_ManCreateRefs(Gia_Man_t *p)
Definition giaUtil.c:779
Gia_ManLevelNum
int Gia_ManLevelNum(Gia_Man_t *p)
Definition giaUtil.c:546
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137
sat_solver_nconflicts
int sat_solver_nconflicts(sat_solver *s)
Definition satSolver.c:2381
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition satSolver.c:1272
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition satSolver.c:2369
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Cnf_Dat_t_::nVars
int nVars
Definition cnf.h:59
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition cnf.h:63
Cnf_Dat_t_::pClauses
int ** pClauses
Definition cnf.h:62
Cnf_Dat_t_::nClauses
int nClauses
Definition cnf.h:61
Gia_Man_t_::vCofVars
Vec_Int_t * vCofVars
Definition gia.h:191
Gia_Man_t_::pCexComb
Abc_Cex_t * pCexComb
Definition gia.h:149
Abc_CexFreeP
void Abc_CexFreeP(Abc_Cex_t **p)
Definition utilCex.c:361
Abc_CexCreate
Abc_Cex_t * Abc_CexCreate(int nRegs, int nPis, int *pArray, int iFrame, int iPo, int fSkipRegs)
Definition utilCex.c:110
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
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
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