ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
giaSatLut.c
Go to the documentation of this file.
1
20
21#include "gia.h"
22#include "misc/tim/tim.h"
23#include "misc/util/utilTruth.h"
24#include "sat/bsat/satStore.h"
25#include "misc/util/utilNam.h"
26#include "map/scl/sclCon.h"
27#include "misc/vec/vecHsh.h"
28
29#ifdef _MSC_VER
30#define unlink _unlink
31#else
32#include <unistd.h>
33#endif
34
35ABC_NAMESPACE_IMPL_START
36
37
41
42typedef struct Sbl_Man_t_ Sbl_Man_t;
43struct Sbl_Man_t_
44{
45 sat_solver * pSat; // SAT solver
46 Vec_Int_t * vCardVars; // candinality variables
47 int nVars; // max vars
48 int LogN; // base-2 log of max vars
49 int Power2; // power-2 of LogN
50 int FirstVar; // first variable to be used
51 // statistics
52 int nTried; // nodes tried
53 int nImproved; // nodes improved
54 int nRuns; // the number of runs
55 int nHashWins; // the number of hashed windows
56 int nSmallWins; // the number of small windows
57 int nLargeWins; // the number of large windows
58 int nIterOuts; // the number of iters exceeded
59 // parameters
60 int LutSize; // LUT size
61 int nBTLimit; // conflicts
62 int DelayMax; // external delay
63 int nEdges; // the number of edges
64 int fDelay; // delay mode
65 int fReverse; // reverse windowing
66 int fVerbose; // verbose
67 int fVeryVerbose; // verbose
68 int fVeryVeryVerbose; // verbose
69 // window
70 Gia_Man_t * pGia;
71 Vec_Int_t * vLeaves; // leaf nodes
72 Vec_Int_t * vAnds; // AND-gates
73 Vec_Int_t * vNodes; // internal LUTs
74 Vec_Int_t * vRoots; // driver nodes (a subset of vAnds)
75 Vec_Int_t * vRootVars; // driver nodes (as SAT variables)
76 Hsh_VecMan_t * pHash; // hash table for windows
77 // timing
78 Vec_Int_t * vArrs; // arrival times
79 Vec_Int_t * vReqs; // required times
80 Vec_Wec_t * vWindow; // fanins of each node in the window
81 Vec_Int_t * vPath; // critical path (as SAT variables)
82 Vec_Int_t * vEdges; // fanin edges
83 // cuts
84 Vec_Wrd_t * vCutsI1; // input bit patterns
85 Vec_Wrd_t * vCutsI2; // input bit patterns
86 Vec_Wrd_t * vCutsN1; // node bit patterns
87 Vec_Wrd_t * vCutsN2; // node bit patterns
88 Vec_Int_t * vCutsNum; // cut counts for each obj
89 Vec_Int_t * vCutsStart; // starting cuts for each obj
90 Vec_Int_t * vCutsObj; // object to which this cut belongs
91 Vec_Wrd_t * vTempI1; // temporary cuts
92 Vec_Wrd_t * vTempI2; // temporary cuts
93 Vec_Wrd_t * vTempN1; // temporary cuts
94 Vec_Wrd_t * vTempN2; // temporary cuts
95 Vec_Int_t * vSolInit; // initial solution
96 Vec_Int_t * vSolCur; // current solution
97 Vec_Int_t * vSolBest; // best solution
98 // temporary
99 Vec_Int_t * vLits; // literals
100 Vec_Int_t * vAssump; // literals
101 Vec_Int_t * vPolar; // variables polarity
102 // statistics
103 abctime timeWin; // windowing
104 abctime timeCut; // cut computation
105 abctime timeSat; // SAT runtime
106 abctime timeSatSat; // satisfiable time
107 abctime timeSatUns; // unsatisfiable time
108 abctime timeSatUnd; // undecided time
109 abctime timeTime; // timing time
110 abctime timeStart; // starting time
111 abctime timeTotal; // all runtime
112 abctime timeOther; // other time
113};
114
115extern sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars );
116
120
132Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int Number )
133{
134 Sbl_Man_t * p = ABC_CALLOC( Sbl_Man_t, 1 );
135 p->nVars = Number;
136 p->LogN = Abc_Base2Log(Number);
137 p->Power2 = 1 << p->LogN;
138 p->pSat = Sbm_AddCardinSolver( p->LogN, &p->vCardVars );
139 p->FirstVar = sat_solver_nvars( p->pSat );
140 sat_solver_bookmark( p->pSat );
141 // window
142 p->pGia = pGia;
143 p->vLeaves = Vec_IntAlloc( p->nVars );
144 p->vAnds = Vec_IntAlloc( p->nVars );
145 p->vNodes = Vec_IntAlloc( p->nVars );
146 p->vRoots = Vec_IntAlloc( p->nVars );
147 p->vRootVars = Vec_IntAlloc( p->nVars );
148 p->pHash = Hsh_VecManStart( 1000 );
149 // timing
150 p->vArrs = Vec_IntAlloc( 0 );
151 p->vReqs = Vec_IntAlloc( 0 );
152 p->vWindow = Vec_WecAlloc( 128 );
153 p->vPath = Vec_IntAlloc( 32 );
154 p->vEdges = Vec_IntAlloc( 32 );
155 // cuts
156 p->vCutsI1 = Vec_WrdAlloc( 1000 ); // input bit patterns
157 p->vCutsI2 = Vec_WrdAlloc( 1000 ); // input bit patterns
158 p->vCutsN1 = Vec_WrdAlloc( 1000 ); // node bit patterns
159 p->vCutsN2 = Vec_WrdAlloc( 1000 ); // node bit patterns
160 p->vCutsNum = Vec_IntAlloc( 64 ); // cut counts for each obj
161 p->vCutsStart = Vec_IntAlloc( 64 ); // starting cuts for each obj
162 p->vCutsObj = Vec_IntAlloc( 1000 );
163 p->vSolInit = Vec_IntAlloc( 64 );
164 p->vSolCur = Vec_IntAlloc( 64 );
165 p->vSolBest = Vec_IntAlloc( 64 );
166 p->vTempI1 = Vec_WrdAlloc( 32 );
167 p->vTempI2 = Vec_WrdAlloc( 32 );
168 p->vTempN1 = Vec_WrdAlloc( 32 );
169 p->vTempN2 = Vec_WrdAlloc( 32 );
170 // internal
171 p->vLits = Vec_IntAlloc( 64 );
172 p->vAssump = Vec_IntAlloc( 64 );
173 p->vPolar = Vec_IntAlloc( 1000 );
174 // other
175 Gia_ManFillValue( pGia );
176 return p;
177}
178void Sbl_ManClean( Sbl_Man_t * p )
179{
180 p->timeStart = Abc_Clock();
181 sat_solver_rollback( p->pSat );
182 sat_solver_bookmark( p->pSat );
183 // internal
184 Vec_IntClear( p->vLeaves );
185 Vec_IntClear( p->vAnds );
186 Vec_IntClear( p->vNodes );
187 Vec_IntClear( p->vRoots );
188 Vec_IntClear( p->vRootVars );
189 // timing
190 Vec_IntClear( p->vArrs );
191 Vec_IntClear( p->vReqs );
192 Vec_WecClear( p->vWindow );
193 Vec_IntClear( p->vPath );
194 Vec_IntClear( p->vEdges );
195 // cuts
196 Vec_WrdClear( p->vCutsI1 );
197 Vec_WrdClear( p->vCutsI2 );
198 Vec_WrdClear( p->vCutsN1 );
199 Vec_WrdClear( p->vCutsN2 );
200 Vec_IntClear( p->vCutsNum );
201 Vec_IntClear( p->vCutsStart );
202 Vec_IntClear( p->vCutsObj );
203 Vec_IntClear( p->vSolInit );
204 Vec_IntClear( p->vSolCur );
205 Vec_IntClear( p->vSolBest );
206 Vec_WrdClear( p->vTempI1 );
207 Vec_WrdClear( p->vTempI2 );
208 Vec_WrdClear( p->vTempN1 );
209 Vec_WrdClear( p->vTempN2 );
210 // temporary
211 Vec_IntClear( p->vLits );
212 Vec_IntClear( p->vAssump );
213 Vec_IntClear( p->vPolar );
214 // other
215 Gia_ManFillValue( p->pGia );
216}
217void Sbl_ManStop( Sbl_Man_t * p )
218{
219 sat_solver_delete( p->pSat );
220 Vec_IntFree( p->vCardVars );
221 // internal
222 Vec_IntFree( p->vLeaves );
223 Vec_IntFree( p->vAnds );
224 Vec_IntFree( p->vNodes );
225 Vec_IntFree( p->vRoots );
226 Vec_IntFree( p->vRootVars );
227 Hsh_VecManStop( p->pHash );
228 // timing
229 Vec_IntFree( p->vArrs );
230 Vec_IntFree( p->vReqs );
231 Vec_WecFree( p->vWindow );
232 Vec_IntFree( p->vPath );
233 Vec_IntFree( p->vEdges );
234 // cuts
235 Vec_WrdFree( p->vCutsI1 );
236 Vec_WrdFree( p->vCutsI2 );
237 Vec_WrdFree( p->vCutsN1 );
238 Vec_WrdFree( p->vCutsN2 );
239 Vec_IntFree( p->vCutsNum );
240 Vec_IntFree( p->vCutsStart );
241 Vec_IntFree( p->vCutsObj );
242 Vec_IntFree( p->vSolInit );
243 Vec_IntFree( p->vSolCur );
244 Vec_IntFree( p->vSolBest );
245 Vec_WrdFree( p->vTempI1 );
246 Vec_WrdFree( p->vTempI2 );
247 Vec_WrdFree( p->vTempN1 );
248 Vec_WrdFree( p->vTempN2 );
249 // temporary
250 Vec_IntFree( p->vLits );
251 Vec_IntFree( p->vAssump );
252 Vec_IntFree( p->vPolar );
253 // other
254 ABC_FREE( p );
255}
256
268void Sbl_ManGetCurrentMapping( Sbl_Man_t * p )
269{
270 Vec_Int_t * vObj;
271 word CutI1, CutI2, CutN1, CutN2;
272 int i, c, b, iObj;
273 Vec_WecClear( p->vWindow );
274 Vec_WecInit( p->vWindow, Vec_IntSize(p->vAnds) );
275 assert( Vec_IntSize(p->vSolCur) > 0 );
276 Vec_IntForEachEntry( p->vSolCur, c, i )
277 {
278 CutI1 = Vec_WrdEntry( p->vCutsI1, c );
279 CutI2 = Vec_WrdEntry( p->vCutsI2, c );
280 CutN1 = Vec_WrdEntry( p->vCutsN1, c );
281 CutN2 = Vec_WrdEntry( p->vCutsN2, c );
282 iObj = Vec_IntEntry( p->vCutsObj, c );
283 //iObj = Vec_IntEntry( p->vAnds, iObj );
284 vObj = Vec_WecEntry( p->vWindow, iObj );
285 Vec_IntClear( vObj );
286 assert( Vec_IntSize(vObj) == 0 );
287 for ( b = 0; b < 64; b++ )
288 if ( (CutI1 >> b) & 1 )
289 Vec_IntPush( vObj, Vec_IntEntry(p->vLeaves, b) );
290 for ( b = 0; b < 64; b++ )
291 if ( (CutI2 >> b) & 1 )
292 Vec_IntPush( vObj, Vec_IntEntry(p->vLeaves, 64+b) );
293 for ( b = 0; b < 64; b++ )
294 if ( (CutN1 >> b) & 1 )
295 Vec_IntPush( vObj, Vec_IntEntry(p->vAnds, b) );
296 for ( b = 0; b < 64; b++ )
297 if ( (CutN2 >> b) & 1 )
298 Vec_IntPush( vObj, Vec_IntEntry(p->vAnds, 64+b) );
299 }
300}
301
302
314int Sbl_ManComputeDelay( Sbl_Man_t * p, int iLut, Vec_Int_t * vFanins )
315{
316 int k, iFan, Delay = 0;
317 Vec_IntForEachEntry( vFanins, iFan, k )
318 Delay = Abc_MaxInt( Delay, Vec_IntEntry(p->vArrs, iFan) + 1 );
319 return Delay;
320}
321int Sbl_ManCreateTiming( Sbl_Man_t * p, int DelayStart )
322{
323 Vec_Int_t * vFanins;
324 int DelayMax = DelayStart, Delay, iLut, iFan, k;
325 // compute arrival times
326 Vec_IntFill( p->vArrs, Gia_ManObjNum(p->pGia), 0 );
327 if ( p->pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)p->pGia->pManTime) )
328 {
329 Gia_Obj_t * pObj;
330 Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( p->pGia );
331 Tim_ManIncrementTravId( (Tim_Man_t*)p->pGia->pManTime );
332 Gia_ManForEachObjVec( vNodes, p->pGia, pObj, k )
333 {
334 iLut = Gia_ObjId( p->pGia, pObj );
335 if ( Gia_ObjIsAnd(pObj) )
336 {
337 if ( Gia_ObjIsLut2(p->pGia, iLut) )
338 {
339 vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
340 Delay = Sbl_ManComputeDelay( p, iLut, vFanins );
341 Vec_IntWriteEntry( p->vArrs, iLut, Delay );
342 DelayMax = Abc_MaxInt( DelayMax, Delay );
343 }
344 }
345 else if ( Gia_ObjIsCi(pObj) )
346 {
347 int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)p->pGia->pManTime, Gia_ObjCioId(pObj) );
348 Vec_IntWriteEntry( p->vArrs, iLut, arrTime );
349 }
350 else if ( Gia_ObjIsCo(pObj) )
351 {
352 int arrTime = Vec_IntEntry( p->vArrs, Gia_ObjFaninId0(pObj, iLut) );
353 Tim_ManSetCoArrival( (Tim_Man_t*)p->pGia->pManTime, Gia_ObjCioId(pObj), arrTime );
354 }
355 else if ( !Gia_ObjIsConst0(pObj) )
356 assert( 0 );
357 }
358 Vec_IntFree( vNodes );
359 }
360 else
361 {
362 Gia_ManForEachLut2( p->pGia, iLut )
363 {
364 vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
365 Delay = Sbl_ManComputeDelay( p, iLut, vFanins );
366 Vec_IntWriteEntry( p->vArrs, iLut, Delay );
367 DelayMax = Abc_MaxInt( DelayMax, Delay );
368 }
369 }
370 // compute required times
371 Vec_IntFill( p->vReqs, Gia_ManObjNum(p->pGia), ABC_INFINITY );
372 Gia_ManForEachCoDriverId( p->pGia, iLut, k )
373 Vec_IntDowndateEntry( p->vReqs, iLut, DelayMax );
374 if ( p->pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)p->pGia->pManTime) )
375 {
376 Gia_Obj_t * pObj;
377 Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( p->pGia );
378 Tim_ManIncrementTravId( (Tim_Man_t*)p->pGia->pManTime );
379 Tim_ManInitPoRequiredAll( (Tim_Man_t*)p->pGia->pManTime, DelayMax );
380 Gia_ManForEachObjVecReverse( vNodes, p->pGia, pObj, k )
381 {
382 iLut = Gia_ObjId( p->pGia, pObj );
383 if ( Gia_ObjIsAnd(pObj) )
384 {
385 if ( Gia_ObjIsLut2(p->pGia, iLut) )
386 {
387 Delay = Vec_IntEntry(p->vReqs, iLut) - 1;
388 vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
389 Vec_IntForEachEntry( vFanins, iFan, k )
390 Vec_IntDowndateEntry( p->vReqs, iFan, Delay );
391 }
392 }
393 else if ( Gia_ObjIsCi(pObj) )
394 {
395 int reqTime = Vec_IntEntry( p->vReqs, iLut );
396 Tim_ManSetCiRequired( (Tim_Man_t*)p->pGia->pManTime, Gia_ObjCioId(pObj), reqTime );
397 }
398 else if ( Gia_ObjIsCo(pObj) )
399 {
400 int reqTime = Tim_ManGetCoRequired( (Tim_Man_t*)p->pGia->pManTime, Gia_ObjCioId(pObj) );
401 Vec_IntWriteEntry( p->vReqs, Gia_ObjFaninId0(pObj, iLut), reqTime );
402 }
403 else if ( !Gia_ObjIsConst0(pObj) )
404 assert( 0 );
405 }
406 Vec_IntFree( vNodes );
407 }
408 else
409 {
410 Gia_ManForEachLut2Reverse( p->pGia, iLut )
411 {
412 Delay = Vec_IntEntry(p->vReqs, iLut) - 1;
413 vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
414 Vec_IntForEachEntry( vFanins, iFan, k )
415 Vec_IntDowndateEntry( p->vReqs, iFan, Delay );
416 }
417 }
418 return DelayMax;
419}
420
421
433int Sbl_ManEvaluateMappingEdge( Sbl_Man_t * p, int DelayGlo )
434{
435 abctime clk = Abc_Clock();
436 Vec_Int_t * vArray;
437 int i, DelayMax;
438 Vec_IntClear( p->vPath );
439 // update new timing
440 Sbl_ManGetCurrentMapping( p );
441 // derive new timing
442 DelayMax = Gia_ManEvalWindow( p->pGia, p->vLeaves, p->vAnds, p->vWindow, p->vPolar, 1 );
443 p->timeTime += Abc_Clock() - clk;
444 if ( DelayMax <= DelayGlo )
445 return 1;
446 // create critical path composed of all nodes
447 Vec_WecForEachLevel( p->vWindow, vArray, i )
448 if ( Vec_IntSize(vArray) > 0 )
449 Vec_IntPush( p->vPath, Abc_Var2Lit(i, 1) );
450 return 0;
451}
452
465int Sbl_ManCriticalFanin( Sbl_Man_t * p, int iLut, Vec_Int_t * vFanins )
466{
467 int k, iFan, Delay = Vec_IntEntry(p->vArrs, iLut);
468 Vec_IntForEachEntry( vFanins, iFan, k )
469 if ( Vec_IntEntry(p->vArrs, iFan) + 1 == Delay )
470 return iFan;
471 return -1;
472}
473int Sbl_ManEvaluateMapping( Sbl_Man_t * p, int DelayGlo )
474{
475 abctime clk = Abc_Clock();
476 Vec_Int_t * vFanins;
477 int i, iLut = -1, iAnd, Delay, Required;
478 if ( p->pGia->vEdge1 )
479 return Sbl_ManEvaluateMappingEdge( p, DelayGlo );
480 Vec_IntClear( p->vPath );
481 // derive timing
482 Sbl_ManCreateTiming( p, DelayGlo );
483 // update new timing
484 Sbl_ManGetCurrentMapping( p );
485 Vec_IntForEachEntry( p->vAnds, iLut, i )
486 {
487 vFanins = Vec_WecEntry( p->vWindow, i );
488 Delay = Sbl_ManComputeDelay( p, iLut, vFanins );
489 Vec_IntWriteEntry( p->vArrs, iLut, Delay );
490 }
491 // compare timing at the root nodes
492 Vec_IntForEachEntry( p->vRoots, iLut, i )
493 {
494 Delay = Vec_IntEntry( p->vArrs, iLut );
495 Required = Vec_IntEntry( p->vReqs, iLut );
496 if ( Delay > Required ) // updated timing exceeded original timing
497 break;
498 }
499 p->timeTime += Abc_Clock() - clk;
500 if ( i == Vec_IntSize(p->vRoots) )
501 return 1;
502 // derive the critical path
503
504 // find SAT variable of the node whose GIA ID is "iLut"
505 iAnd = Vec_IntFind( p->vAnds, iLut );
506 assert( iAnd >= 0 );
507 // critical path begins in node "iLut", which is i-th root of the window
508 assert( iAnd == Vec_IntEntry(p->vRootVars, i) );
509 while ( 1 )
510 {
511 Vec_IntPush( p->vPath, Abc_Var2Lit(iAnd, 1) );
512 // find fanins of this node
513 vFanins = Vec_WecEntry( p->vWindow, iAnd );
514 // find critical fanin
515 iLut = Sbl_ManCriticalFanin( p, iLut, vFanins );
516 assert( iLut > 0 );
517 // find SAT variable of the node whose GIA ID is "iLut"
518 iAnd = Vec_IntFind( p->vAnds, iLut );
519 if ( iAnd == -1 )
520 break;
521 }
522 return 0;
523}
524
525
537void Sbl_ManUpdateMapping( Sbl_Man_t * p )
538{
539// Gia_Obj_t * pObj;
540 Vec_Int_t * vObj;
541 word CutI1, CutI2, CutN1, CutN2;
542 int i, c, b, iObj, iTemp;
543 assert( Vec_IntSize(p->vSolBest) < Vec_IntSize(p->vSolInit) );
544 Vec_IntForEachEntry( p->vAnds, iObj, i )
545 {
546 vObj = Vec_WecEntry(p->pGia->vMapping2, iObj);
547 Vec_IntForEachEntry( vObj, iTemp, b )
548 Gia_ObjLutRefDecId( p->pGia, iTemp );
549 Vec_IntClear( vObj );
550 }
551 Vec_IntForEachEntry( p->vSolBest, c, i )
552 {
553 CutI1 = Vec_WrdEntry( p->vCutsI1, c );
554 CutI2 = Vec_WrdEntry( p->vCutsI2, c );
555 CutN1 = Vec_WrdEntry( p->vCutsN1, c );
556 CutN2 = Vec_WrdEntry( p->vCutsN2, c );
557 iObj = Vec_IntEntry( p->vCutsObj, c );
558 iObj = Vec_IntEntry( p->vAnds, iObj );
559 vObj = Vec_WecEntry( p->pGia->vMapping2, iObj );
560 Vec_IntClear( vObj );
561 assert( Vec_IntSize(vObj) == 0 );
562 for ( b = 0; b < 64; b++ )
563 if ( (CutI1 >> b) & 1 )
564 Vec_IntPush( vObj, Vec_IntEntry(p->vLeaves, b) );
565 for ( b = 0; b < 64; b++ )
566 if ( (CutI2 >> b) & 1 )
567 Vec_IntPush( vObj, Vec_IntEntry(p->vLeaves, 64+b) );
568 for ( b = 0; b < 64; b++ )
569 if ( (CutN1 >> b) & 1 )
570 Vec_IntPush( vObj, Vec_IntEntry(p->vAnds, b) );
571 for ( b = 0; b < 64; b++ )
572 if ( (CutN2 >> b) & 1 )
573 Vec_IntPush( vObj, Vec_IntEntry(p->vAnds, 64+b) );
574 Vec_IntForEachEntry( vObj, iTemp, b )
575 Gia_ObjLutRefIncId( p->pGia, iTemp );
576 }
577/*
578 // verify
579 Gia_ManForEachLut2Vec( p->pGia, vObj, i )
580 Vec_IntForEachEntry( vObj, iTemp, b )
581 Gia_ObjLutRefDecId( p->pGia, iTemp );
582 Gia_ManForEachCo( p->pGia, pObj, i )
583 Gia_ObjLutRefDecId( p->pGia, Gia_ObjFaninId0p(p->pGia, pObj) );
584
585 for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
586 if ( p->pGia->pLutRefs[i] )
587 printf( "Object %d has %d refs\n", i, p->pGia->pLutRefs[i] );
588
589 Gia_ManForEachCo( p->pGia, pObj, i )
590 Gia_ObjLutRefIncId( p->pGia, Gia_ObjFaninId0p(p->pGia, pObj) );
591 Gia_ManForEachLut2Vec( p->pGia, vObj, i )
592 Vec_IntForEachEntry( vObj, iTemp, b )
593 Gia_ObjLutRefIncId( p->pGia, iTemp );
594*/
595}
596
608static int Sbl_ManPrintCut( word CutI1, word CutI2, word CutN1, word CutN2 )
609{
610 int b, Count = 0;
611 printf( "{ " );
612 for ( b = 0; b < 64; b++ )
613 if ( (CutI1 >> b) & 1 )
614 printf( "i%d ", b ), Count++;
615 for ( b = 0; b < 64; b++ )
616 if ( (CutI2 >> b) & 1 )
617 printf( "i%d ", 64+b ), Count++;
618 printf( " " );
619 for ( b = 0; b < 64; b++ )
620 if ( (CutN1 >> b) & 1 )
621 printf( "n%d ", b ), Count++;
622 for ( b = 0; b < 64; b++ )
623 if ( (CutN2 >> b) & 1 )
624 printf( "n%d ", 64+b ), Count++;
625 printf( "};\n" );
626 return Count;
627}
628static int Sbl_ManFindAndPrintCut( Sbl_Man_t * p, int c )
629{
630 return Sbl_ManPrintCut( Vec_WrdEntry(p->vCutsI1, c), Vec_WrdEntry(p->vCutsI2, c), Vec_WrdEntry(p->vCutsN1, c), Vec_WrdEntry(p->vCutsN2, c) );
631}
632static inline int Sbl_CutIsFeasible( word CutI1, word CutI2, word CutN1, word CutN2, int LutSize )
633{
634 int Count = (CutI1 != 0) + (CutI2 != 0) + (CutN1 != 0) + (CutN2 != 0);
635 assert( LutSize <= 6 );
636 CutI1 &= CutI1-1; CutI2 &= CutI2-1; CutN1 &= CutN1-1; CutN2 &= CutN2-1; Count += (CutI1 != 0) + (CutI2 != 0) + (CutN1 != 0) + (CutN2 != 0);
637 CutI1 &= CutI1-1; CutI2 &= CutI2-1; CutN1 &= CutN1-1; CutN2 &= CutN2-1; Count += (CutI1 != 0) + (CutI2 != 0) + (CutN1 != 0) + (CutN2 != 0);
638 CutI1 &= CutI1-1; CutI2 &= CutI2-1; CutN1 &= CutN1-1; CutN2 &= CutN2-1; Count += (CutI1 != 0) + (CutI2 != 0) + (CutN1 != 0) + (CutN2 != 0);
639 CutI1 &= CutI1-1; CutI2 &= CutI2-1; CutN1 &= CutN1-1; CutN2 &= CutN2-1; Count += (CutI1 != 0) + (CutI2 != 0) + (CutN1 != 0) + (CutN2 != 0);
640 if ( LutSize <= 4 )
641 return Count <= 4;
642 CutI1 &= CutI1-1; CutI2 &= CutI2-1; CutN1 &= CutN1-1; CutN2 &= CutN2-1; Count += (CutI1 != 0) + (CutI2 != 0) + (CutN1 != 0) + (CutN2 != 0);
643 CutI1 &= CutI1-1; CutI2 &= CutI2-1; CutN1 &= CutN1-1; CutN2 &= CutN2-1; Count += (CutI1 != 0) + (CutI2 != 0) + (CutN1 != 0) + (CutN2 != 0);
644 return Count <= 6;
645}
646static inline int Sbl_CutPushUncontained( Vec_Wrd_t * vCutsI1, Vec_Wrd_t * vCutsI2, Vec_Wrd_t * vCutsN1, Vec_Wrd_t * vCutsN2, word CutI1, word CutI2, word CutN1, word CutN2 )
647{
648 int i, k = 0;
649 assert( vCutsI1->nSize == vCutsN1->nSize );
650 assert( vCutsI2->nSize == vCutsN2->nSize );
651 for ( i = 0; i < vCutsI1->nSize; i++ )
652 if ( (vCutsI1->pArray[i] & CutI1) == vCutsI1->pArray[i] &&
653 (vCutsI2->pArray[i] & CutI2) == vCutsI2->pArray[i] &&
654 (vCutsN1->pArray[i] & CutN1) == vCutsN1->pArray[i] &&
655 (vCutsN2->pArray[i] & CutN2) == vCutsN2->pArray[i] )
656 return 1;
657 for ( i = 0; i < vCutsI1->nSize; i++ )
658 if ( (vCutsI1->pArray[i] & CutI1) != CutI1 ||
659 (vCutsI2->pArray[i] & CutI2) != CutI2 ||
660 (vCutsN1->pArray[i] & CutN1) != CutN1 ||
661 (vCutsN2->pArray[i] & CutN2) != CutN2 )
662 {
663 Vec_WrdWriteEntry( vCutsI1, k, vCutsI1->pArray[i] );
664 Vec_WrdWriteEntry( vCutsI2, k, vCutsI2->pArray[i] );
665 Vec_WrdWriteEntry( vCutsN1, k, vCutsN1->pArray[i] );
666 Vec_WrdWriteEntry( vCutsN2, k, vCutsN2->pArray[i] );
667 k++;
668 }
669 Vec_WrdShrink( vCutsI1, k );
670 Vec_WrdShrink( vCutsI2, k );
671 Vec_WrdShrink( vCutsN1, k );
672 Vec_WrdShrink( vCutsN2, k );
673 Vec_WrdPush( vCutsI1, CutI1 );
674 Vec_WrdPush( vCutsI2, CutI2 );
675 Vec_WrdPush( vCutsN1, CutN1 );
676 Vec_WrdPush( vCutsN2, CutN2 );
677 return 0;
678}
679static inline void Sbl_ManComputeCutsOne( Sbl_Man_t * p, int Fan0, int Fan1, int Obj )
680{
681 word * pCutsI1 = Vec_WrdArray(p->vCutsI1);
682 word * pCutsI2 = Vec_WrdArray(p->vCutsI2);
683 word * pCutsN1 = Vec_WrdArray(p->vCutsN1);
684 word * pCutsN2 = Vec_WrdArray(p->vCutsN2);
685 int Start0 = Vec_IntEntry( p->vCutsStart, Fan0 );
686 int Start1 = Vec_IntEntry( p->vCutsStart, Fan1 );
687 int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Fan0 );
688 int Limit1 = Start1 + Vec_IntEntry( p->vCutsNum, Fan1 );
689 int i, k;
690 assert( Obj >= 0 && Obj < 128 );
691 Vec_WrdClear( p->vTempI1 );
692 Vec_WrdClear( p->vTempI2 );
693 Vec_WrdClear( p->vTempN1 );
694 Vec_WrdClear( p->vTempN2 );
695 for ( i = Start0; i < Limit0; i++ )
696 for ( k = Start1; k < Limit1; k++ )
697 if ( Sbl_CutIsFeasible(pCutsI1[i] | pCutsI1[k], pCutsI2[i] | pCutsI2[k], pCutsN1[i] | pCutsN1[k], pCutsN2[i] | pCutsN2[k], p->LutSize) )
698 Sbl_CutPushUncontained( p->vTempI1, p->vTempI2, p->vTempN1, p->vTempN2, pCutsI1[i] | pCutsI1[k], pCutsI2[i] | pCutsI2[k], pCutsN1[i] | pCutsN1[k], pCutsN2[i] | pCutsN2[k] );
699 Vec_IntPush( p->vCutsStart, Vec_WrdSize(p->vCutsI1) );
700 Vec_IntPush( p->vCutsNum, Vec_WrdSize(p->vTempI1) + 1 );
701 Vec_WrdAppend( p->vCutsI1, p->vTempI1 );
702 Vec_WrdAppend( p->vCutsI2, p->vTempI2 );
703 Vec_WrdAppend( p->vCutsN1, p->vTempN1 );
704 Vec_WrdAppend( p->vCutsN2, p->vTempN2 );
705 Vec_WrdPush( p->vCutsI1, 0 );
706 Vec_WrdPush( p->vCutsI2, 0 );
707 if ( Obj < 64 )
708 {
709 Vec_WrdPush( p->vCutsN1, (((word)1) << Obj) );
710 Vec_WrdPush( p->vCutsN2, 0 );
711 }
712 else
713 {
714 Vec_WrdPush( p->vCutsN1, 0 );
715 Vec_WrdPush( p->vCutsN2, (((word)1) << (Obj-64)) );
716 }
717 for ( i = 0; i <= Vec_WrdSize(p->vTempI1); i++ )
718 Vec_IntPush( p->vCutsObj, Obj );
719}
720static inline int Sbl_ManFindCut( Sbl_Man_t * p, int Obj, word CutI1, word CutI2, word CutN1, word CutN2 )
721{
722 word * pCutsI1 = Vec_WrdArray(p->vCutsI1);
723 word * pCutsI2 = Vec_WrdArray(p->vCutsI2);
724 word * pCutsN1 = Vec_WrdArray(p->vCutsN1);
725 word * pCutsN2 = Vec_WrdArray(p->vCutsN2);
726 int Start0 = Vec_IntEntry( p->vCutsStart, Obj );
727 int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Obj );
728 int i;
729 //printf( "\nLooking for:\n" );
730 //Sbl_ManPrintCut( CutI, CutN );
731 //printf( "\n" );
732 for ( i = Start0; i < Limit0; i++ )
733 {
734 //Sbl_ManPrintCut( pCutsI[i], pCutsN[i] );
735 if ( pCutsI1[i] == CutI1 && pCutsI2[i] == CutI2 && pCutsN1[i] == CutN1 && pCutsN2[i] == CutN2 )
736 return i;
737 }
738 return -1;
739}
740int Sbl_ManComputeCuts( Sbl_Man_t * p )
741{
742 abctime clk = Abc_Clock();
743 Gia_Obj_t * pObj; Vec_Int_t * vFanins;
744 int i, k, Index, Fanin, nObjs = Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vAnds);
745 assert( Vec_IntSize(p->vLeaves) <= 128 && Vec_IntSize(p->vAnds) <= p->nVars );
746 // assign leaf cuts
747 Vec_IntClear( p->vCutsStart );
748 Vec_IntClear( p->vCutsObj );
749 Vec_IntClear( p->vCutsNum );
750 Vec_WrdClear( p->vCutsI1 );
751 Vec_WrdClear( p->vCutsI2 );
752 Vec_WrdClear( p->vCutsN1 );
753 Vec_WrdClear( p->vCutsN2 );
754 Gia_ManForEachObjVec( p->vLeaves, p->pGia, pObj, i )
755 {
756 Vec_IntPush( p->vCutsStart, Vec_WrdSize(p->vCutsI1) );
757 Vec_IntPush( p->vCutsObj, -1 );
758 Vec_IntPush( p->vCutsNum, 1 );
759 if ( i < 64 )
760 {
761 Vec_WrdPush( p->vCutsI1, (((word)1) << i) );
762 Vec_WrdPush( p->vCutsI2, 0 );
763 }
764 else
765 {
766 Vec_WrdPush( p->vCutsI1, 0 );
767 Vec_WrdPush( p->vCutsI2, (((word)1) << (i-64)) );
768 }
769 Vec_WrdPush( p->vCutsN1, 0 );
770 Vec_WrdPush( p->vCutsN2, 0 );
771 pObj->Value = i;
772 }
773 // assign internal cuts
774 Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i )
775 {
776 assert( Gia_ObjIsAnd(pObj) );
777 assert( ~Gia_ObjFanin0(pObj)->Value );
778 assert( ~Gia_ObjFanin1(pObj)->Value );
779 Sbl_ManComputeCutsOne( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value, i );
780 pObj->Value = Vec_IntSize(p->vLeaves) + i;
781 }
782 assert( Vec_IntSize(p->vCutsStart) == nObjs );
783 assert( Vec_IntSize(p->vCutsNum) == nObjs );
784 assert( Vec_WrdSize(p->vCutsI1) == Vec_WrdSize(p->vCutsN1) );
785 assert( Vec_WrdSize(p->vCutsI2) == Vec_WrdSize(p->vCutsN2) );
786 assert( Vec_WrdSize(p->vCutsI1) == Vec_IntSize(p->vCutsObj) );
787 // check that roots are mapped nodes
788 Vec_IntClear( p->vRootVars );
789 Gia_ManForEachObjVec( p->vRoots, p->pGia, pObj, i )
790 {
791 int Obj = Gia_ObjId(p->pGia, pObj);
792 if ( Gia_ObjIsCi(pObj) )
793 continue;
794 assert( Gia_ObjIsLut2(p->pGia, Obj) );
795 assert( ~pObj->Value );
796 Vec_IntPush( p->vRootVars, pObj->Value - Vec_IntSize(p->vLeaves) );
797 }
798 // create current solution
799 Vec_IntClear( p->vPolar );
800 Vec_IntClear( p->vSolInit );
801 Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i )
802 {
803 word CutI1 = 0, CutI2 = 0, CutN1 = 0, CutN2 = 0;
804 int Obj = Gia_ObjId(p->pGia, pObj);
805 if ( !Gia_ObjIsLut2(p->pGia, Obj) )
806 continue;
807 assert( (int)pObj->Value == Vec_IntSize(p->vLeaves) + i );
808 // add node
809 Vec_IntPush( p->vPolar, i );
810 Vec_IntPush( p->vSolInit, i );
811 // add its cut
812 //Gia_LutForEachFaninObj( p->pGia, Obj, pFanin, k )
813 vFanins = Gia_ObjLutFanins2( p->pGia, Obj );
814 Vec_IntForEachEntry( vFanins, Fanin, k )
815 {
816 Gia_Obj_t * pFanin = Gia_ManObj( p->pGia, Fanin );
817 assert( (int)pFanin->Value < Vec_IntSize(p->vLeaves) || Gia_ObjIsLut2(p->pGia, Fanin) );
818// if ( ~pFanin->Value == 0 )
819// Gia_ManPrintConeMulti( p->pGia, p->vAnds, p->vLeaves, p->vPath );
820 if ( ~pFanin->Value == 0 )
821 continue;
822 assert( ~pFanin->Value );
823 if ( (int)pFanin->Value < Vec_IntSize(p->vLeaves) )
824 {
825 if ( (int)pFanin->Value < 64 )
826 CutI1 |= ((word)1 << pFanin->Value);
827 else
828 CutI2 |= ((word)1 << (pFanin->Value - 64));
829 }
830 else
831 {
832 if ( pFanin->Value - Vec_IntSize(p->vLeaves) < 64 )
833 CutN1 |= ((word)1 << (pFanin->Value - Vec_IntSize(p->vLeaves)));
834 else
835 CutN2 |= ((word)1 << (pFanin->Value - Vec_IntSize(p->vLeaves) - 64));
836 }
837 }
838 // find the new cut
839 Index = Sbl_ManFindCut( p, Vec_IntSize(p->vLeaves) + i, CutI1, CutI2, CutN1, CutN2 );
840 if ( Index < 0 )
841 {
842 //printf( "Cannot find the available cut.\n" );
843 continue;
844 }
845 assert( Index >= 0 );
846 Vec_IntPush( p->vPolar, p->FirstVar+Index );
847 }
848 // clean value
849 Gia_ManForEachObjVec( p->vLeaves, p->pGia, pObj, i )
850 pObj->Value = ~0;
851 Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i )
852 pObj->Value = ~0;
853 p->timeCut += Abc_Clock() - clk;
854 return Vec_WrdSize(p->vCutsI1);
855}
856int Sbl_ManCreateCnf( Sbl_Man_t * p )
857{
858 int i, k, c, pLits[2], value;
859 word * pCutsN1 = Vec_WrdArray(p->vCutsN1);
860 word * pCutsN2 = Vec_WrdArray(p->vCutsN2);
861 assert( p->FirstVar == sat_solver_nvars(p->pSat) );
862 sat_solver_setnvars( p->pSat, sat_solver_nvars(p->pSat) + Vec_WrdSize(p->vCutsI1) );
863 //printf( "\n" );
864 for ( i = 0; i < Vec_IntSize(p->vAnds); i++ )
865 {
866 int Start0 = Vec_IntEntry( p->vCutsStart, Vec_IntSize(p->vLeaves) + i );
867 int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Vec_IntSize(p->vLeaves) + i ) - 1;
868 // add main clause
869 Vec_IntClear( p->vLits );
870 Vec_IntPush( p->vLits, Abc_Var2Lit(i, 1) );
871 //printf( "Node %d implies cuts: ", i );
872 for ( k = Start0; k < Limit0; k++ )
873 {
874 Vec_IntPush( p->vLits, Abc_Var2Lit(p->FirstVar+k, 0) );
875 //printf( "%d ", p->FirstVar+k );
876 }
877 //printf( "\n" );
878 value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) );
879 assert( value );
880 // binary clauses
881 for ( k = Start0; k < Limit0; k++ )
882 {
883 word Cut1 = pCutsN1[k];
884 word Cut2 = pCutsN2[k];
885 //printf( "Cut %d implies root node %d.\n", p->FirstVar+k, i );
886 // root clause
887 pLits[0] = Abc_Var2Lit( p->FirstVar+k, 1 );
888 pLits[1] = Abc_Var2Lit( i, 0 );
889 value = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
890 assert( value );
891 // fanin clauses
892 for ( c = 0; c < 64 && Cut1; c++, Cut1 >>= 1 )
893 {
894 if ( (Cut1 & 1) == 0 )
895 continue;
896 //printf( "Cut %d implies fanin %d.\n", p->FirstVar+k, c );
897 pLits[1] = Abc_Var2Lit( c, 0 );
898 value = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
899 assert( value );
900 }
901 for ( c = 0; c < 64 && Cut2; c++, Cut2 >>= 1 )
902 {
903 if ( (Cut2 & 1) == 0 )
904 continue;
905 //printf( "Cut %d implies fanin %d.\n", p->FirstVar+k, c );
906 pLits[1] = Abc_Var2Lit( c+64, 0 );
907 value = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
908 assert( value );
909 }
910 }
911 }
912 sat_solver_set_polarity( p->pSat, Vec_IntArray(p->vPolar), Vec_IntSize(p->vPolar) );
913 return 1;
914}
915
916
928
929void Sbl_ManWindow( Sbl_Man_t * p )
930{
931 int i, ObjId;
932 // collect leaves
933 Vec_IntClear( p->vLeaves );
934 Gia_ManForEachCiId( p->pGia, ObjId, i )
935 Vec_IntPush( p->vLeaves, ObjId );
936 // collect internal
937 Vec_IntClear( p->vAnds );
938 Gia_ManForEachAndId( p->pGia, ObjId )
939 Vec_IntPush( p->vAnds, ObjId );
940 // collect roots
941 Vec_IntClear( p->vRoots );
942 Gia_ManForEachCoDriverId( p->pGia, ObjId, i )
943 Vec_IntPush( p->vRoots, ObjId );
944}
945
946int Sbl_ManWindow2( Sbl_Man_t * p, int iPivot )
947{
948 abctime clk = Abc_Clock();
949 Vec_Int_t * vRoots, * vNodes, * vLeaves, * vAnds;
950 int Count = Gia_ManComputeOneWin( p->pGia, iPivot, &vRoots, &vNodes, &vLeaves, &vAnds );
951 p->timeWin += Abc_Clock() - clk;
952 if ( Count == 0 )
953 return 0;
954 Vec_IntClear( p->vRoots ); Vec_IntAppend( p->vRoots, vRoots );
955 Vec_IntClear( p->vNodes ); Vec_IntAppend( p->vNodes, vNodes );
956 Vec_IntClear( p->vLeaves ); Vec_IntAppend( p->vLeaves, vLeaves );
957 Vec_IntClear( p->vAnds ); Vec_IntAppend( p->vAnds, vAnds );
958//Vec_IntPrint( vRoots );
959//Vec_IntPrint( vAnds );
960//Vec_IntPrint( vLeaves );
961 // recompute internal nodes
962// Gia_ManIncrementTravId( p->pGia );
963// Gia_ManCollectAnds( p->pGia, Vec_IntArray(p->vRoots), Vec_IntSize(p->vRoots), p->vAnds, p->vLeaves );
964 return Count;
965}
966
967int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot )
968{
969 int fKeepTrying = 1;
970 abctime clk = Abc_Clock(), clk2;
971 int i, status, Root, Count, StartSol, nConfTotal = 0, nIters = 0;
972 int nEntries = Hsh_VecSize( p->pHash );
973 p->nTried++;
974
975 Sbl_ManClean( p );
976
977 // compute one window
978 Count = Sbl_ManWindow2( p, iPivot );
979 if ( Count == 0 )
980 {
981 if ( p->fVeryVerbose )
982 printf( "Obj %d: Window with less than %d nodes does not exist.\n", iPivot, p->nVars );
983 p->nSmallWins++;
984 return 0;
985 }
986 Hsh_VecManAdd( p->pHash, p->vAnds );
987 if ( nEntries == Hsh_VecSize(p->pHash) )
988 {
989 if ( p->fVeryVerbose )
990 printf( "Obj %d: This window was already tried.\n", iPivot );
991 p->nHashWins++;
992 return 0;
993 }
994 if ( p->fVeryVerbose )
995 printf( "\nObj = %6d : Leaf = %2d. AND = %2d. Root = %2d. LUT = %2d.\n",
996 iPivot, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds), Vec_IntSize(p->vRoots), Vec_IntSize(p->vNodes) );
997
998 if ( Vec_IntSize(p->vLeaves) > 128 || Vec_IntSize(p->vAnds) > p->nVars )
999 {
1000 if ( p->fVeryVerbose )
1001 printf( "Obj %d: Encountered window with %d inputs and %d internal nodes.\n", iPivot, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds) );
1002 p->nLargeWins++;
1003 return 0;
1004 }
1005 if ( Vec_IntSize(p->vAnds) < 10 )
1006 {
1007 if ( p->fVeryVerbose )
1008 printf( "Skipping.\n" );
1009 return 0;
1010 }
1011
1012 // derive cuts
1013 Sbl_ManComputeCuts( p );
1014 // derive SAT instance
1015 Sbl_ManCreateCnf( p );
1016
1017 if ( p->fVeryVeryVerbose )
1018 printf( "All clauses = %d. Multi clauses = %d. Binary clauses = %d. Other clauses = %d.\n\n",
1019 sat_solver_nclauses(p->pSat), Vec_IntSize(p->vAnds), Vec_WrdSize(p->vCutsI1) - Vec_IntSize(p->vAnds),
1020 sat_solver_nclauses(p->pSat) - Vec_WrdSize(p->vCutsI1) );
1021
1022 // create assumptions
1023 // cardinality
1024 Vec_IntClear( p->vAssump );
1025 Vec_IntPush( p->vAssump, -1 );
1026 // unused variables
1027 for ( i = Vec_IntSize(p->vAnds); i < p->Power2; i++ )
1028 Vec_IntPush( p->vAssump, Abc_Var2Lit(i, 1) );
1029 // root variables
1030 Vec_IntForEachEntry( p->vRootVars, Root, i )
1031 Vec_IntPush( p->vAssump, Abc_Var2Lit(Root, 0) );
1032// Vec_IntPrint( p->vAssump );
1033
1034 StartSol = Vec_IntSize(p->vSolInit) + 1;
1035// StartSol = 30;
1036 while ( fKeepTrying && StartSol-fKeepTrying > 0 )
1037 {
1038 int Count = 0, LitCount = 0;
1039 int nConfBef, nConfAft;
1040 if ( p->fVeryVerbose )
1041 printf( "Trying to find mapping with %d LUTs.\n", StartSol-fKeepTrying );
1042 // for ( i = Vec_IntSize(p->vSolInit)-5; i < nVars; i++ )
1043 // Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, i), 1) );
1044 Vec_IntWriteEntry( p->vAssump, 0, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, StartSol-fKeepTrying), 1) );
1045 // solve the problem
1046 clk2 = Abc_Clock();
1047 nConfBef = (int)p->pSat->stats.conflicts;
1048 status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), p->nBTLimit, 0, 0, 0 );
1049 p->timeSat += Abc_Clock() - clk2;
1050 nConfAft = (int)p->pSat->stats.conflicts;
1051 nConfTotal += nConfAft - nConfBef;
1052 nIters++;
1053 p->nRuns++;
1054 if ( status == l_True )
1055 p->timeSatSat += Abc_Clock() - clk2;
1056 else if ( status == l_False )
1057 p->timeSatUns += Abc_Clock() - clk2;
1058 else
1059 p->timeSatUnd += Abc_Clock() - clk2;
1060 if ( status == l_Undef )
1061 break;
1062 if ( status == l_True )
1063 {
1064 if ( p->fVeryVeryVerbose )
1065 {
1066 for ( i = 0; i < Vec_IntSize(p->vAnds); i++ )
1067 printf( "%d", sat_solver_var_value(p->pSat, i) );
1068 printf( "\n" );
1069 for ( i = 0; i < Vec_IntSize(p->vAnds); i++ )
1070 if ( sat_solver_var_value(p->pSat, i) )
1071 {
1072 printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) );
1073 Count++;
1074 }
1075 printf( "Count = %d\n", Count );
1076 }
1077// for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ )
1078// printf( "%d", sat_solver_var_value(p->pSat, i) );
1079// printf( "\n" );
1080 Count = 1;
1081 Vec_IntClear( p->vSolCur );
1082 for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ )
1083 if ( sat_solver_var_value(p->pSat, i) )
1084 {
1085 if ( p->fVeryVeryVerbose )
1086 printf( "Cut %3d : Node = %3d %6d ", Count++, Vec_IntEntry(p->vCutsObj, i-p->FirstVar), Vec_IntEntry(p->vAnds, Vec_IntEntry(p->vCutsObj, i-p->FirstVar)) );
1087 if ( p->fVeryVeryVerbose )
1088 LitCount += Sbl_ManFindAndPrintCut( p, i-p->FirstVar );
1089 Vec_IntPush( p->vSolCur, i-p->FirstVar );
1090 }
1091 //Vec_IntPrint( p->vRootVars );
1092 //Vec_IntPrint( p->vRoots );
1093 //Vec_IntPrint( p->vAnds );
1094 //Vec_IntPrint( p->vLeaves );
1095 }
1096
1097// fKeepTrying = status == l_True ? fKeepTrying + 1 : 0;
1098 // check the timing
1099 if ( status == l_True )
1100 {
1101 if ( p->fDelay && !Sbl_ManEvaluateMapping(p, p->DelayMax) )
1102 {
1103 int iLit, value;
1104 if ( p->fVeryVerbose )
1105 {
1106 printf( "Critical path of length (%d) is detected: ", Vec_IntSize(p->vPath) );
1107 Vec_IntForEachEntry( p->vPath, iLit, i )
1108 printf( "%d=%d ", i, Vec_IntEntry(p->vAnds, Abc_Lit2Var(iLit)) );
1109 printf( "\n" );
1110 }
1111 // add the clause
1112 value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vPath), Vec_IntLimit(p->vPath) );
1113 assert( value );
1114 }
1115 else
1116 {
1117 Vec_IntClear( p->vSolBest );
1118 Vec_IntAppend( p->vSolBest, p->vSolCur );
1119 fKeepTrying++;
1120 }
1121 }
1122 else
1123 fKeepTrying = 0;
1124 if ( p->fVeryVerbose )
1125 {
1126 if ( status == l_False )
1127 printf( "UNSAT " );
1128 else if ( status == l_True )
1129 printf( "SAT " );
1130 else
1131 printf( "UNDEC " );
1132 printf( "confl =%8d. ", nConfAft - nConfBef );
1133 Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
1134
1135 printf( "Total " );
1136 printf( "confl =%8d. ", nConfTotal );
1137 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1138 if ( p->fVeryVeryVerbose && status == l_True )
1139 printf( "LitCount = %d.\n", LitCount );
1140 printf( "\n" );
1141 }
1142 if ( nIters == 10 )
1143 {
1144 p->nIterOuts++;
1145 //printf( "Obj %d : Quitting after %d iterations.\n", iPivot, nIters );
1146 break;
1147 }
1148 }
1149
1150 // update solution
1151 if ( Vec_IntSize(p->vSolBest) > 0 && Vec_IntSize(p->vSolBest) < Vec_IntSize(p->vSolInit) )
1152 {
1153 int nDelayCur, nEdgesCur = 0;
1154 Sbl_ManUpdateMapping( p );
1155 if ( p->pGia->vEdge1 )
1156 {
1157 nDelayCur = Gia_ManEvalEdgeDelay( p->pGia );
1158 nEdgesCur = Gia_ManEvalEdgeCount( p->pGia );
1159 }
1160 else
1161 nDelayCur = Sbl_ManCreateTiming( p, p->DelayMax );
1162 if ( p->fVerbose )
1163 printf( "Object %5d : Saved %2d nodes (Conf =%8d) Iter =%3d Delay = %d Edges = %4d\n",
1164 iPivot, Vec_IntSize(p->vSolInit)-Vec_IntSize(p->vSolBest), nConfTotal, nIters, nDelayCur, nEdgesCur );
1165 p->timeTotal += Abc_Clock() - p->timeStart;
1166 p->nImproved++;
1167 return 2;
1168 }
1169 else
1170 {
1171// printf( "Object %5d : Saved %2d nodes (Conf =%8d) Iter =%3d\n", iPivot, 0, nConfTotal, nIters );
1172 }
1173 p->timeTotal += Abc_Clock() - p->timeStart;
1174 return 1;
1175}
1176void Sbl_ManPrintRuntime( Sbl_Man_t * p )
1177{
1178 printf( "Runtime breakdown:\n" );
1179 p->timeOther = p->timeTotal - p->timeWin - p->timeCut - p->timeSat - p->timeTime;
1180 ABC_PRTP( "Win ", p->timeWin , p->timeTotal );
1181 ABC_PRTP( "Cut ", p->timeCut , p->timeTotal );
1182 ABC_PRTP( "Sat ", p->timeSat, p->timeTotal );
1183 ABC_PRTP( " Sat ", p->timeSatSat, p->timeTotal );
1184 ABC_PRTP( " Unsat", p->timeSatUns, p->timeTotal );
1185 ABC_PRTP( " Undec", p->timeSatUnd, p->timeTotal );
1186 ABC_PRTP( "Timing", p->timeTime , p->timeTotal );
1187 ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
1188 ABC_PRTP( "ALL ", p->timeTotal, p->timeTotal );
1189}
1190void Gia_ManLutSat( Gia_Man_t * pGia, int LutSize, int nNumber, int nImproves, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVerbose, int fVeryVerbose )
1191{
1192 int iLut, nImproveCount = 0;
1193 Sbl_Man_t * p = Sbl_ManAlloc( pGia, nNumber );
1194 p->LutSize = LutSize; // LUT size
1195 p->nBTLimit = nBTLimit; // conflicts
1196 p->DelayMax = DelayMax; // external delay
1197 p->nEdges = nEdges; // the number of edges
1198 p->fDelay = fDelay; // delay mode
1199 p->fReverse = fReverse; // reverse windowing
1200 p->fVerbose = fVerbose | fVeryVerbose;
1201 p->fVeryVerbose = fVeryVerbose;
1202 if ( p->fVerbose )
1203 printf( "Parameters: WinSize = %d AIG nodes. Conf = %d. DelayMax = %d.\n", p->nVars, p->nBTLimit, p->DelayMax );
1204 // determine delay limit
1205 if ( fDelay && pGia->vEdge1 && p->DelayMax == 0 )
1206 p->DelayMax = Gia_ManEvalEdgeDelay( pGia );
1207 // iterate through the internal nodes
1208 Gia_ManComputeOneWinStart( pGia, nNumber, fReverse );
1209 Gia_ManForEachLut2( pGia, iLut )
1210 {
1211 if ( Sbl_ManTestSat( p, iLut ) != 2 )
1212 continue;
1213 if ( ++nImproveCount == nImproves )
1214 break;
1215 }
1216 Gia_ManComputeOneWin( pGia, -1, NULL, NULL, NULL, NULL );
1217 if ( p->fVerbose )
1218 printf( "Tried = %d. Used = %d. HashWin = %d. SmallWin = %d. LargeWin = %d. IterOut = %d. SAT runs = %d.\n",
1219 p->nTried, p->nImproved, p->nHashWins, p->nSmallWins, p->nLargeWins, p->nIterOuts, p->nRuns );
1220 if ( p->fVerbose )
1221 Sbl_ManPrintRuntime( p );
1222 Sbl_ManStop( p );
1223 Vec_IntFreeP( &pGia->vPacking );
1224}
1225
1237Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int Seed, int nBTLimit, int TimeOut, int fVerbose, int * pStatus )
1238{
1239 extern Vec_Int_t * Exa4_ManParse( char *pFileName );
1240 int fVerboseSolver = 0;
1241 abctime clkTotal = Abc_Clock();
1242 Vec_Int_t * vRes = NULL;
1243#ifdef _WIN32
1244 char * pKadical = "kadical.exe";
1245#else
1246 char * pKadical = "./kadical";
1247 FILE * pFile = fopen( pKadical, "rb" );
1248 if ( pFile == NULL )
1249 pKadical += 2;
1250 else
1251 fclose( pFile );
1252#endif
1253 char Command[1000], * pCommand = (char *)&Command;
1254 if ( nBTLimit ) {
1255 if ( TimeOut )
1256 sprintf( pCommand, "%s --seed=%d -c %d -t %d %s %s > %s", pKadical, Seed, nBTLimit, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
1257 else
1258 sprintf( pCommand, "%s --seed=%d -c %d %s %s > %s", pKadical, Seed, nBTLimit, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
1259 }
1260 else {
1261 if ( TimeOut )
1262 sprintf( pCommand, "%s --seed=%d -t %d %s %s > %s", pKadical, Seed, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
1263 else
1264 sprintf( pCommand, "%s --seed=%d %s %s > %s", pKadical, Seed, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut );
1265 }
1266#ifdef __wasm
1267 if ( 1 )
1268#else
1269 if ( system( pCommand ) == -1 )
1270#endif
1271 {
1272 fprintf( stdout, "Command \"%s\" did not succeed.\n", pCommand );
1273 return 0;
1274 }
1275 vRes = Exa4_ManParse( pFileNameOut );
1276 if ( fVerbose )
1277 {
1278 if ( vRes )
1279 printf( "The problem has a solution. " ), *pStatus = 0;
1280 else if ( vRes == NULL && TimeOut == 0 )
1281 printf( "The problem has no solution. " ), *pStatus = 1;
1282 else if ( vRes == NULL )
1283 printf( "The problem has no solution or reached a resource limit after %d sec. ", TimeOut ), *pStatus = -1;
1284 Abc_PrintTime( 1, "SAT solver time", Abc_Clock() - clkTotal );
1285 }
1286 return vRes;
1287}
1288
1300int Gia_SatVarReqPos( int i ) { return i*7+0; } // p
1301int Gia_SatVarReqNeg( int i ) { return i*7+1; } // n
1302int Gia_SatVarAckPos( int i ) { return i*7+2; } // P
1303int Gia_SatVarAckNeg( int i ) { return i*7+3; } // N
1304int Gia_SatVarInv ( int i ) { return i*7+4; } // i
1305int Gia_SatVarFan0 ( int i ) { return i*7+5; } // 0
1306int Gia_SatVarFan1 ( int i ) { return i*7+6; } // 1
1307
1308int Gia_SatValReqPos( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+0); } // p
1309int Gia_SatValReqNeg( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+1); } // n
1310int Gia_SatValAckPos( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+2); } // P
1311int Gia_SatValAckNeg( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+3); } // N
1312int Gia_SatValInv ( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+4); } // i
1313int Gia_SatValFan0 ( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+5); } // 0
1314int Gia_SatValFan1 ( Vec_Int_t * p, int i ) { return Vec_IntEntry(p, i*7+6); } // 1
1315
1316void Gia_SatDumpClause( Vec_Str_t * vStr, int * pLits, int nLits )
1317{
1318 for ( int i = 0; i < nLits; i++ )
1319 Vec_StrPrintF( vStr, "%d ", Abc_LitIsCompl(pLits[i]) ? -Abc_Lit2Var(pLits[i])-1 : Abc_Lit2Var(pLits[i])+1 );
1320 Vec_StrPrintF( vStr, "0\n" );
1321}
1322void Gia_SatDumpLiteral( Vec_Str_t * vStr, int Lit )
1323{
1324 Gia_SatDumpClause( vStr, &Lit, 1 );
1325}
1326void Gia_SatDumpKlause( Vec_Str_t * vStr, int nIns, int nAnds, int nBound )
1327{
1328 int i, nVars = nIns + 7*nAnds;
1329 Vec_StrPrintF( vStr, "k %d ", nVars - nBound );
1330 // counting primary inputs: n
1331 for ( i = 0; i < nIns; i++ )
1332 Vec_StrPrintF( vStr, "-%d ", Gia_SatVarReqNeg(1+i)+1 );
1333 // counting internal nodes: p, n, P, N, i, 0, 1
1334 for ( i = 0; i < 7*nAnds; i++ )
1335 Vec_StrPrintF( vStr, "-%d ", (1+nIns)*7+i+1 );
1336 Vec_StrPrintF( vStr, "0\n" );
1337}
1338
1339Vec_Str_t * Gia_ManSimpleCnf( Gia_Man_t * p, int nBound )
1340{
1341 Vec_Str_t * vStr = Vec_StrAlloc( 10000 );
1342 Gia_SatDumpKlause( vStr, Gia_ManCiNum(p), Gia_ManAndNum(p), nBound );
1343 int i, n, m, Id, pLits[4]; Gia_Obj_t * pObj;
1344 for ( n = 0; n < 7; n++ )
1345 Gia_SatDumpLiteral( vStr, Abc_Var2Lit(n, 1) );
1346 // acknowledge positive PI literals
1347 Gia_ManForEachCiId( p, Id, i )
1348 for ( n = 0; n < 7; n++ ) if ( n != 1 )
1349 Gia_SatDumpLiteral( vStr, Abc_Var2Lit(Gia_SatVarReqPos(Id)+n, n>0) );
1350 // require driving PO literals
1351 Gia_ManForEachCo( p, pObj, i )
1352 Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_SatVarReqPos(Gia_ObjFaninId0p(p, pObj)) + Gia_ObjFaninC0(pObj), 0 ) );
1353 // internal nodes
1354 Gia_ManForEachAnd( p, pObj, i ) {
1355 int fCompl[2] = { Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj) };
1356 int iFans[2] = { Gia_ObjFaninId0(pObj, i), Gia_ObjFaninId1(pObj, i) };
1357 Gia_Obj_t * pFans[2] = { Gia_ObjFanin0(pObj), Gia_ObjFanin1(pObj) };
1358 // require inverter: p & !n & N -> i, n & !p & P -> i
1359 for ( n = 0; n < 2; n++ ) {
1360 pLits[0] = Abc_Var2Lit( Gia_SatVarReqPos(i)+n, 1 );
1361 pLits[1] = Abc_Var2Lit( Gia_SatVarReqNeg(i)-n, 0 );
1362 pLits[2] = Abc_Var2Lit( Gia_SatVarAckNeg(i)-n, 1 );
1363 pLits[3] = Abc_Var2Lit( Gia_SatVarInv (i), 0 );
1364 Gia_SatDumpClause( vStr, pLits, 4 );
1365 }
1366 // exclusive acknowledge: !P + !N
1367 pLits[0] = Abc_Var2Lit( Gia_SatVarAckPos(i), 1 );
1368 pLits[1] = Abc_Var2Lit( Gia_SatVarAckNeg(i), 1 );
1369 Gia_SatDumpClause( vStr, pLits, 2 );
1370 // required acknowledge: p -> P + N, n -> P + N
1371 pLits[1] = Abc_Var2Lit( Gia_SatVarAckPos(i), 0 );
1372 pLits[2] = Abc_Var2Lit( Gia_SatVarAckNeg(i), 0 );
1373 pLits[0] = Abc_Var2Lit( Gia_SatVarReqPos(i), 1 );
1374 Gia_SatDumpClause( vStr, pLits, 3 );
1375 pLits[0] = Abc_Var2Lit( Gia_SatVarReqNeg(i), 1 );
1376 Gia_SatDumpClause( vStr, pLits, 3 );
1377 // forbid acknowledge: !p & !n -> !P, !p & !n -> !N
1378 pLits[0] = Abc_Var2Lit( Gia_SatVarReqPos(i), 0 );
1379 pLits[1] = Abc_Var2Lit( Gia_SatVarReqNeg(i), 0 );
1380 pLits[2] = Abc_Var2Lit( Gia_SatVarAckPos(i), 1 );
1381 Gia_SatDumpClause( vStr, pLits, 3 );
1382 pLits[2] = Abc_Var2Lit( Gia_SatVarAckNeg(i), 1 );
1383 Gia_SatDumpClause( vStr, pLits, 3 );
1384 // when fanins can be used: !N & !P -> !0, !N & !P -> !1
1385 pLits[0] = Abc_Var2Lit( Gia_SatVarAckPos(i), 0 );
1386 pLits[1] = Abc_Var2Lit( Gia_SatVarAckNeg(i), 0 );
1387 pLits[2] = Abc_Var2Lit( Gia_SatVarFan0(i), 1 );
1388 Gia_SatDumpClause( vStr, pLits, 3 );
1389 pLits[2] = Abc_Var2Lit( Gia_SatVarFan1(i), 1 );
1390 Gia_SatDumpClause( vStr, pLits, 3 );
1391 // when fanins are not used: 0 -> !N, 0 -> !P, 1 -> !N, 1 -> !P
1392 for ( m = 0; m < 2; m++ )
1393 for ( n = 0; n < 2; n++ ) {
1394 pLits[0] = Abc_Var2Lit( Gia_SatVarFan0(i)+n, 1 );
1395 pLits[1] = Abc_Var2Lit( Gia_SatVarReqPos(iFans[n])+m, 1 );
1396 Gia_SatDumpClause( vStr, pLits, 2 );
1397 }
1398 // can only extend both when both complemented: !(C0 & C1) -> !0 + !1
1399 pLits[0] = Abc_Var2Lit( Gia_SatVarFan0(i), 1 );
1400 pLits[1] = Abc_Var2Lit( Gia_SatVarFan1(i), 1 );
1401 if ( !fCompl[0] || !fCompl[1] )
1402 Gia_SatDumpClause( vStr, pLits, 2 );
1403 // if fanin is a primary input, cannot extend it (pi -> !0 or pi -> !1)
1404 for ( n = 0; n < 2; n++ )
1405 if ( Gia_ObjIsCi(pFans[n]) )
1406 Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_SatVarFan0(i)+n, 1 ) );
1407 // propagating assignments when fanin is not used
1408 // P & !0 -> C0 ? P0 : N0
1409 // N & !0 -> C0 ? N0 : P0
1410 // P & !1 -> C1 ? P1 : N1
1411 // N & !1 -> C1 ? N1 : P1
1412 for ( m = 0; m < 2; m++ )
1413 for ( n = 0; n < 2; n++ ) {
1414 pLits[0] = Abc_Var2Lit( Gia_SatVarAckPos(i)+m, 1 );
1415 pLits[1] = Abc_Var2Lit( Gia_SatVarFan0(i)+n, 0 );
1416 pLits[2] = Abc_Var2Lit( Gia_SatVarReqPos(iFans[n]) + !(m ^ fCompl[n]), 0 );
1417 Gia_SatDumpClause( vStr, pLits, 3 );
1418 }
1419 // propagating assignments when fanins are used
1420 // P & 0 -> (C0 ^ C00) ? P00 : N00
1421 // P & 0 -> (C0 ^ C01) ? P01 : N01
1422 // N & 0 -> (C0 ^ C00) ? N00 : P00
1423 // N & 0 -> (C0 ^ C01) ? N01 : P01
1424 // P & 1 -> (C1 ^ C10) ? P10 : N10
1425 // P & 1 -> (C1 ^ C11) ? P11 : N11
1426 // N & 1 -> (C1 ^ C10) ? N10 : P10
1427 // N & 1 -> (C1 ^ C11) ? N11 : P11
1428 for ( m = 0; m < 2; m++ )
1429 for ( n = 0; n < 2; n++ )
1430 if ( Gia_ObjIsAnd(pFans[n]) ) {
1431 pLits[0] = Abc_Var2Lit( Gia_SatVarAckPos(i)+m, 1 );
1432 pLits[1] = Abc_Var2Lit( Gia_SatVarFan0(i)+n, 1 );
1433 pLits[2] = Abc_Var2Lit( Gia_SatVarReqPos(Gia_ObjFaninId0p(p, pFans[n])) + !(m ^ fCompl[n] ^ Gia_ObjFaninC0(pFans[n])), 0 );
1434 Gia_SatDumpClause( vStr, pLits, 3 );
1435 pLits[2] = Abc_Var2Lit( Gia_SatVarReqPos(Gia_ObjFaninId1p(p, pFans[n])) + !(m ^ fCompl[n] ^ Gia_ObjFaninC1(pFans[n])), 0 );
1436 Gia_SatDumpClause( vStr, pLits, 3 );
1437 }
1438 }
1439 Vec_StrPush( vStr, '\0' );
1440 return vStr;
1441}
1442
1458
1459Vec_Int_t * Gia_ManDeriveSimpleMapping( Gia_Man_t * p, Vec_Int_t * vRes )
1460{
1461 Vec_Int_t * vMapping = Vec_IntStart( 2*Gia_ManObjNum(p) );
1462 int i, Id; Gia_Obj_t * pObj;
1463 Gia_ManForEachCiId( p, Id, i )
1464 if ( Gia_SatValReqNeg(vRes, Id) )
1465 Vec_IntWriteEntry( vMapping, Abc_Var2Lit(Id, 1), -1 );
1466 Gia_ManForEachAnd( p, pObj, i )
1467 {
1468 if ( Gia_SatValAckPos(vRes, i) + Gia_SatValAckNeg(vRes, i) == 0 )
1469 continue;
1470 assert( Gia_SatValAckPos(vRes, i) != Gia_SatValAckNeg(vRes, i) );
1471 if ( (Gia_SatValReqPos(vRes, i) && Gia_SatValReqNeg(vRes, i)) || Gia_SatValInv(vRes, i) )
1472 Vec_IntWriteEntry( vMapping, Abc_Var2Lit(i, Gia_SatValAckPos(vRes, i)), -1 );
1473 int fComp = Gia_SatValAckNeg(vRes, i);
1474 int fFan0 = Gia_SatValFan0(vRes, i);
1475 int fFan1 = Gia_SatValFan1(vRes, i);
1476 Gia_Obj_t * pFans[2] = { Gia_ObjFanin0(pObj), Gia_ObjFanin1(pObj) };
1477 Vec_IntWriteEntry( vMapping, Abc_Var2Lit(i, fComp), Vec_IntSize(vMapping) );
1478 if ( fFan0 && fFan1 ) {
1479 assert( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) );
1480 Vec_IntPush( vMapping, 4 );
1481 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC0(pFans[0]))) );
1482 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pFans[0]))) );
1483 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC0(pFans[1]))) );
1484 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC1(pFans[1]))) );
1485 Vec_IntPush( vMapping, fComp ? GIA_GATE_OAI22 : GIA_GATE_AOI22 );
1486 } else if ( fFan0 ) {
1487 Vec_IntPush( vMapping, 3 );
1488 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC0(pFans[0]))) );
1489 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pFans[0]))) );
1490 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pObj), !(fComp ^ Gia_ObjFaninC1(pObj))) );
1491 if ( Gia_ObjFaninC0(pObj) )
1492 Vec_IntPush( vMapping, fComp ? GIA_GATE_OAI21 : GIA_GATE_AOI21 );
1493 else
1494 Vec_IntPush( vMapping, fComp ? GIA_GATE_NAN3 : GIA_GATE_NOR3 );
1495 } else if ( fFan1 ) {
1496 Vec_IntPush( vMapping, 3 );
1497 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC0(pFans[1]))) );
1498 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC1(pFans[1]))) );
1499 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pObj), !(fComp ^ Gia_ObjFaninC0(pObj))) );
1500 if ( Gia_ObjFaninC1(pObj) )
1501 Vec_IntPush( vMapping, fComp ? GIA_GATE_OAI21 : GIA_GATE_AOI21 );
1502 else
1503 Vec_IntPush( vMapping, fComp ? GIA_GATE_NAN3 : GIA_GATE_NOR3 );
1504 } else {
1505 Vec_IntPush( vMapping, 2 );
1506 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pObj), !(fComp ^ Gia_ObjFaninC0(pObj))) );
1507 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pObj), !(fComp ^ Gia_ObjFaninC1(pObj))) );
1508 Vec_IntPush( vMapping, fComp ? GIA_GATE_NAN2 : GIA_GATE_NOR2 );
1509 }
1510 }
1511 return vMapping;
1512}
1513void Gia_ManSimplePrintMapping( Vec_Int_t * vRes, int nIns )
1514{
1515 int i, k, nObjs = Vec_IntSize(vRes)/7, nSteps = Abc_Base10Log(nObjs);
1516 int nCard = Vec_IntSum(vRes) - nIns; char NumStr[10];
1517 printf( "Solution with cardinality %d:\n", nCard );
1518 for ( k = 0; k < nSteps; k++ ) {
1519 printf( " " );
1520 for ( i = 0; i < nObjs; i++ ) {
1521 sprintf( NumStr, "%02d", i );
1522 printf( "%c", NumStr[k] );
1523 }
1524 printf( "\n" );
1525 }
1526 for ( k = 0; k < 7; k++ ) {
1527 printf( "%c ", "pnPNi01"[k] );
1528 for ( i = 0; i < nObjs; i++ )
1529 if ( Vec_IntEntry( vRes, i*7+k ) == 0 )
1530 printf( " " );
1531 else
1532 printf( "1" );
1533 printf( "\n" );
1534 }
1535}
1536int Gia_ManDumpCnf( char * pFileName, Vec_Str_t * vStr, int nVars )
1537{
1538 FILE * pFile = fopen( pFileName, "wb" );
1539 if ( pFile == NULL ) { printf( "Cannot open input file \"%s\".\n", pFileName ); return 0; }
1540 fprintf( pFile, "p knf %d %d\n%s\n", nVars, Vec_StrCountEntry(vStr, '\n'), Vec_StrArray(vStr) );
1541 fclose( pFile );
1542 return 1;
1543}
1544int Gia_ManDumpCnf2( Vec_Str_t * vStr, int nVars, int argc, char ** argv, abctime Time, int Status )
1545{
1546 Vec_Str_t * vFileName = Vec_StrAlloc( 100 ); int c;
1547 Vec_StrPrintF( vFileName, "%s", argv[0] + (argv[0][0] == '&') );
1548 for ( c = 1; c < argc; c++ )
1549 Vec_StrPrintF( vFileName, "_%s", argv[c] + (argv[c][0] == '-') );
1550 Vec_StrPrintF( vFileName, ".cnf" );
1551 Vec_StrPush( vFileName, '\0' );
1552 FILE * pFile = fopen( Vec_StrArray(vFileName), "wb" );
1553 if ( pFile == NULL ) { printf( "Cannot open output file \"%s\".\n", Vec_StrArray(vFileName) ); Vec_StrFree(vFileName); return 0; }
1554 Vec_StrFree(vFileName);
1555 fprintf( pFile, "c This file was generated by ABC command: \"" );
1556 fprintf( pFile, "%s", argv[0] );
1557 for ( c = 1; c < argc; c++ )
1558 fprintf( pFile, " %s", argv[c] );
1559 fprintf( pFile, "\" on %s\n", Gia_TimeStamp() );
1560 fprintf( pFile, "c Cardinality CDCL (https://github.com/jreeves3/Cardinality-CDCL) found it to be " );
1561 if ( Status == 1 )
1562 fprintf( pFile, "UNSAT" );
1563 if ( Status == 0 )
1564 fprintf( pFile, "SAT" );
1565 if ( Status == -1 )
1566 fprintf( pFile, "UNDECIDED" );
1567 fprintf( pFile, " in %.2f sec\n", 1.0*((double)(Time))/((double)CLOCKS_PER_SEC) );
1568 fprintf( pFile, "p knf %d %d\n%s\n", nVars, Vec_StrCountEntry(vStr, '\n'), Vec_StrArray(vStr) );
1569 fclose( pFile );
1570 return 1;
1571}
1572int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int Seed, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv )
1573{
1574 abctime clkStart = Abc_Clock();
1575 srand(time(NULL));
1576 int Status, Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFFF;
1577 char pFileNameI[32]; sprintf( pFileNameI, "_%06x_.cnf", Rand );
1578 char pFileNameO[32]; sprintf( pFileNameO, "_%06x_.out", Rand );
1579 if ( nBound == 0 )
1580 nBound = 5 * Gia_ManAndNum(p);
1581 Vec_Str_t * vStr = Gia_ManSimpleCnf( p, nBound/2 );
1582 int nVars = 7*(Gia_ManObjNum(p)-Gia_ManCoNum(p));
1583 if ( !Gia_ManDumpCnf(pFileNameI, vStr, nVars) ) {
1584 Vec_StrFree( vStr );
1585 return 0;
1586 }
1587 if ( fVerbose )
1588 printf( "SAT variables = %d. SAT clauses = %d. Cardinality bound = %d. Conflict limit = %d. Timeout = %d.\n",
1589 nVars, Vec_StrCountEntry(vStr, '\n'), nBound, nBTLimit, nTimeout );
1590 Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, Seed, nBTLimit, nTimeout, fVerbose, &Status );
1591 unlink( pFileNameI );
1592 //unlink( pFileNameO );
1593 if ( fKeepFile ) Gia_ManDumpCnf2( vStr, nVars, argc, argv, Abc_Clock() - clkStart, Status );
1594 Vec_StrFree( vStr );
1595 if ( vRes == NULL )
1596 return 0;
1597 Vec_IntFreeP( &p->vCellMapping );
1598 assert( p->vCellMapping == NULL );
1599 Vec_IntDrop( vRes, 0 );
1600 if ( fVerbose ) Gia_ManSimplePrintMapping( vRes, Gia_ManCiNum(p) );
1601 p->vCellMapping = Gia_ManDeriveSimpleMapping( p, vRes );
1602 Vec_IntFree( vRes );
1603 if ( fVerbose ) Abc_PrintTime( 0, "Total time", Abc_Clock() - clkStart );
1604 return 1;
1605}
1606
1618
1619#define KSAT_OBJS 24
1620#define KSAT_MINTS 64
1621#define KSAT_SPACE (4+3*KSAT_OBJS+3*KSAT_MINTS)
1622
1623int Gia_KSatVarInv( int * pMap, int i ) { return pMap[i*KSAT_SPACE+0]; }
1624int Gia_KSatVarAnd( int * pMap, int i ) { return pMap[i*KSAT_SPACE+1]; }
1625int Gia_KSatVarEqu( int * pMap, int i ) { return pMap[i*KSAT_SPACE+2]; }
1626int Gia_KSatVarRef( int * pMap, int i ) { return pMap[i*KSAT_SPACE+3]; }
1627int Gia_KSatVarFan( int * pMap, int i, int f, int k ) { return pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k]; }
1628int Gia_KSatVarMin( int * pMap, int i, int m, int k ) { return pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+3*m+k]; }
1629
1630void Gia_KSatSetInv( int * pMap, int i, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+0] ); pMap[i*KSAT_SPACE+0] = iVar; }
1631void Gia_KSatSetAnd( int * pMap, int i, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+1] ); pMap[i*KSAT_SPACE+1] = iVar; }
1632void Gia_KSatSetEqu( int * pMap, int i, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+2] ); pMap[i*KSAT_SPACE+2] = iVar; }
1633void Gia_KSatSetRef( int * pMap, int i, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+3] ); pMap[i*KSAT_SPACE+3] = iVar; }
1634void Gia_KSatSetFan( int * pMap, int i, int f, int k, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] ); pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] = iVar; }
1635void Gia_KSatSetMin( int * pMap, int i, int m, int k, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+3*m+k] ); pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+3*m+k] = iVar; }
1636
1637int Gia_KSatValInv( int * pMap, int i, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+0] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+0] ); }
1638int Gia_KSatValAnd( int * pMap, int i, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+1] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+1] ); }
1639int Gia_KSatValEqu( int * pMap, int i, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+2] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+2] ); }
1640int Gia_KSatValRef( int * pMap, int i, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+3] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+3] ); }
1641int Gia_KSatValFan( int * pMap, int i, int f, int k, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] ); }
1642int Gia_KSatValMin( int * pMap, int i, int m, int k, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+3*m+k] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+3*m+k] ); }
1643
1644int * Gia_KSatMapInit( int nIns, int nNodes, word Truth, int * pnVars )
1645{
1646 assert( nIns + nNodes <= KSAT_OBJS );
1647 assert( (1 << nIns) <= KSAT_MINTS );
1648 int n, m, f, k, nVars = 2, * pMap = ABC_FALLOC( int, KSAT_OBJS*KSAT_SPACE );
1649 for ( n = nIns; n < nIns+nNodes; n++ ) {
1650 Gia_KSatSetInv(pMap, n, nVars++);
1651 Gia_KSatSetAnd(pMap, n, nVars++);
1652 Gia_KSatSetEqu(pMap, n, nVars++);
1653 Gia_KSatSetRef(pMap, n, nVars++);
1654 }
1655 for ( n = nIns; n < nIns+nNodes; n++ ) {
1656 for ( f = 0; f < 2; f++ )
1657 for ( k = 0; k < n; k++ )
1658 Gia_KSatSetFan(pMap, n, f, k, nVars++);
1659 for ( k = n+1; k < nIns+nNodes; k++ )
1660 Gia_KSatSetFan(pMap, n, 2, k, nVars++);
1661 }
1662 for ( m = 0; m < (1<<nIns); m++ ) {
1663 for ( n = 0; n < nIns; n++ )
1664 Gia_KSatSetMin(pMap, n, m, 0, (m >> n) & 1 );
1665 Gia_KSatSetMin(pMap, nIns+nNodes-1, m, 0, (Truth >> m) & 1 );
1666 for ( n = nIns; n < nIns+nNodes; n++ )
1667 for ( k = 0; k < 3; k++ )
1668 if ( k || n < nIns+nNodes-1 )
1669 Gia_KSatSetMin(pMap, n, m, k, nVars++);
1670
1671 }
1672 if ( pnVars ) *pnVars = nVars;
1673 return pMap;
1674}
1675
1676int Gia_KSatFindFan( int * pMap, int i, int f, Vec_Int_t * vRes )
1677{
1678 assert( f < 2 );
1679 for ( int k = 0; k < i; k++ )
1680 if ( Gia_KSatValFan( pMap, i, f, k, vRes ) )
1681 return k;
1682 assert( 0 );
1683 return -1;
1684}
1685
1686Vec_Int_t * Gia_ManKSatGenLevels( char * pGuide, int nIns, int nNodes )
1687{
1688 Vec_Int_t * vRes;
1689 int i, k, Count = 0;
1690 for ( i = 0; pGuide[i]; i++ )
1691 Count += pGuide[i] - '0';
1692 if ( Count != nNodes ) {
1693 printf( "Guidance %s has %d nodes while the problem has %d nodes.\n", pGuide, Count, nNodes );
1694 return NULL;
1695 }
1696 int FirstPrev = 0;
1697 int FirstThis = nIns;
1698 int FirstNext = FirstThis;
1699 vRes = Vec_IntStartFull( 2*nIns );
1700 for ( i = 0; pGuide[i]; i++ ) {
1701 FirstNext += pGuide[i] - '0';
1702 for ( k = FirstThis; k < FirstNext; k++ )
1703 Vec_IntPushTwo( vRes, FirstPrev, FirstThis );
1704 FirstPrev = FirstThis;
1705 FirstThis = FirstNext;
1706 }
1707 assert( Vec_IntSize(vRes) == 2*(nIns + nNodes) );
1708 Count = 0;
1709 //int Start, Stop;
1710 //Vec_IntForEachEntryDouble(vRes, Start, Stop, i)
1711 // printf( "%2d : Start %2d Stop %2d\n", Count++, Start, Stop );
1712 return vRes;
1713}
1714
1715Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound, int fMultiLevel, char * pGuide )
1716{
1717 Vec_Str_t * vStr = Vec_StrAlloc( 10000 );
1718 Vec_Int_t * vRes = pGuide ? Gia_ManKSatGenLevels( pGuide, nIns, nNodes ) : NULL;
1719 int i, j, m, n, f, c, a, Start, Stop, nLits = 0, pLits[256] = {0};
1720 Gia_SatDumpLiteral( vStr, 1 );
1721 Gia_SatDumpLiteral( vStr, 2 );
1722 if ( vRes ) {
1723 n = nIns;
1724 Vec_IntForEachEntryDoubleStart( vRes, Start, Stop, i, 2*nIns ) {
1725 for ( j = 0; j < Start; j++ )
1726 Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, j), 1 ) );
1727 for ( f = 0; f < 2; f++ )
1728 for ( j = Stop; j < n; j++ )
1729 Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, j), 1 ) );
1730 n++;
1731 }
1732 assert( n == nIns + nNodes );
1733 }
1734 // fanins are connected once
1735 for ( n = nIns; n < nIns+nNodes; n++ )
1736 for ( f = 0; f < 2; f++ ) {
1737
1738 nLits = 0;
1739 for ( i = 0; i < n; i++ )
1740 pLits[nLits++] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 0 );
1741 Gia_SatDumpClause( vStr, pLits, nLits );
1742/*
1743 for ( i = 0; i < n; i++ )
1744 for ( j = 0; j < i; j++ ) {
1745 pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 );
1746 pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, j), 1 );
1747 Gia_SatDumpClause( vStr, pLits, 2 );
1748 }
1749*/
1750 Vec_StrPrintF( vStr, "k %d ", n-1 );
1751 for ( i = 0; i < n; i++ )
1752 pLits[i] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 );
1753 Gia_SatDumpClause( vStr, pLits, n );
1754 }
1755 for ( n = nIns; n < nIns+nNodes; n++ ) {
1756 // fanins are equal
1757 for ( i = 0; i < n; i++ ) {
1758 pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 0, i), 1 );
1759 pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, i), 1 );
1760 pLits[2] = Abc_Var2Lit( Gia_KSatVarEqu(pMap, n), 0 );
1761 Gia_SatDumpClause( vStr, pLits, 3 );
1762 }
1763 for ( i = 0; i < n; i++ )
1764 for ( j = i+1; j < n; j++ ) {
1765 pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 0, i), 1 );
1766 pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, j), 1 );
1767 pLits[2] = Abc_Var2Lit( Gia_KSatVarEqu(pMap, n), 1 );
1768 Gia_SatDumpClause( vStr, pLits, 3 );
1769 }
1770 // if fanins are equal, inv is used
1771 pLits[0] = Abc_Var2Lit( Gia_KSatVarEqu(pMap, n), 1 );
1772 pLits[1] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), 0 );
1773 Gia_SatDumpClause( vStr, pLits, 2 );
1774 // fanin ordering
1775 for ( i = 0; i < n; i++ )
1776 for ( j = 0; j < i; j++ ) {
1777 pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 0, i), 1 );
1778 pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, j), 1 );
1779 Gia_SatDumpClause( vStr, pLits, 2 );
1780 }
1781 }
1782 for ( n = nIns; n < nIns+nNodes-1; n++ ) {
1783 // there is a fanout to the node above
1784 for ( i = n+1; i < nIns+nNodes; i++ ) {
1785 for ( f = 0; f < 2; f++ ) {
1786 pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, i, f, n), 1 );
1787 pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, i), 0 );
1788 Gia_SatDumpClause( vStr, pLits, 2 );
1789 }
1790 pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, i, 0, n), 0 );
1791 pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, i, 1, n), 0 );
1792 pLits[2] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, i), 1 );
1793 Gia_SatDumpClause( vStr, pLits, 3 );
1794 }
1795 // there is at least one fanout, except the last one
1796 nLits = 0;
1797 for ( i = n+1; i < nIns+nNodes; i++ )
1798 pLits[nLits++] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, i), 0 );
1799 assert( nLits > 0 );
1800 Gia_SatDumpClause( vStr, pLits, nLits );
1801 }
1802 // there is more than one fanout, except the last one
1803 for ( n = nIns; n < nIns+nNodes-1; n++ ) {
1804 for ( i = n+1; i < nIns+nNodes; i++ )
1805 for ( j = i+1; j < nIns+nNodes; j++ ) {
1806 pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, i), 1 );
1807 pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, j), 1 );
1808 pLits[2] = Abc_Var2Lit( Gia_KSatVarRef(pMap, n), 0 );
1809 Gia_SatDumpClause( vStr, pLits, 3 );
1810 }
1811 // if more than one fanout, inv is used
1812 pLits[0] = Abc_Var2Lit( Gia_KSatVarRef(pMap, n), 1 );
1813 pLits[1] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), 0 );
1814 Gia_SatDumpClause( vStr, pLits, 2 );
1815 // if inv is not used, its fanins' invs are used
1816 if ( !fMultiLevel ) {
1817 pLits[0] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), 0 );
1818 for ( i = nIns; i < n; i++ )
1819 for ( f = 0; f < 2; f++ ) {
1820 pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 );
1821 pLits[2] = Abc_Var2Lit( Gia_KSatVarInv(pMap, i), 0 );
1822 Gia_SatDumpClause( vStr, pLits, 3 );
1823 }
1824 }
1825 }
1826 // the last one always uses inverter
1827 Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_KSatVarInv(pMap, nIns+nNodes-1), 0 ) );
1828/*
1829 // for each minterm, for each pair of possible fanins, the node's output is determined using and/or and inv (4*N*N*M)
1830 for ( m = 0; m < (1 << nIns); m++ )
1831 for ( n = nIns; n < nIns+nNodes; n++ )
1832 for ( c = 0; c < 2; c++ )
1833 for ( a = 0; a < 2; a++ ) {
1834 // implications: Fan(f) & Mint(m) & !And & !Inv -> Val1
1835 for ( f = 0; f < 2; f++ )
1836 for ( i = 0; i < n; i++ ) {
1837 pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 );
1838 pLits[1] = Abc_Var2Lit( Gia_KSatVarMin(pMap, i, m, 0), !a );
1839 pLits[2] = Abc_Var2Lit( Gia_KSatVarAnd(pMap, n), a );
1840 pLits[3] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), c );
1841 pLits[4] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 0), a^c );
1842 Gia_SatDumpClause( vStr, pLits, 5 );
1843 }
1844 // large clauses: Fan(0) & Fan(1) & !Mint(m) & !Mint(m) & !And & !Inv -> Val0
1845 for ( i = 0; i < n; i++ )
1846 for ( j = i; j < n; j++ ) {
1847 pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 0, i), 1 );
1848 pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, j), 1 );
1849 pLits[2] = Abc_Var2Lit( Gia_KSatVarMin(pMap, i, m, 0), a );
1850 pLits[3] = Abc_Var2Lit( Gia_KSatVarMin(pMap, j, m, 0), a );
1851 pLits[4] = Abc_Var2Lit( Gia_KSatVarAnd(pMap, n), a );
1852 pLits[5] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), c );
1853 pLits[6] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 0), a==c );
1854 Gia_SatDumpClause( vStr, pLits, 7 );
1855 }
1856 }
1857*/
1858 // for each minterm, define a fanin variable and use it to get the node's output based on and/or and inv (4*N*N*M)
1859 for ( m = 0; m < (1 << nIns); m++ )
1860 for ( n = nIns; n < nIns+nNodes; n++ ) {
1861 for ( i = 0; i < n; i++ )
1862 for ( f = 0; f < 2; f++ )
1863 for ( c = 0; c < 2; c++ ) {
1864 pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 );
1865 pLits[1] = Abc_Var2Lit( Gia_KSatVarMin(pMap, i, m, 0), c );
1866 pLits[2] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 1+f), !c );
1867 Gia_SatDumpClause( vStr, pLits, 3 );
1868 }
1869 for ( c = 0; c < 2; c++ )
1870 for ( a = 0; a < 2; a++ ) {
1871 // implications: Mint(m,f) & !And & !Inv -> Val1
1872 for ( f = 0; f < 2; f++ ) {
1873 pLits[0] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 1+f), !a );
1874 pLits[1] = Abc_Var2Lit( Gia_KSatVarAnd(pMap, n), a );
1875 pLits[2] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), c );
1876 pLits[3] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 0), a^c );
1877 Gia_SatDumpClause( vStr, pLits, 4 );
1878 }
1879 // large clauses: !Mint(m,0) & !Mint(m,1) & !And & !Inv -> Val0
1880 pLits[0] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 1), a );
1881 pLits[1] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 2), a );
1882 pLits[2] = Abc_Var2Lit( Gia_KSatVarAnd(pMap, n), a );
1883 pLits[3] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), c );
1884 pLits[4] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 0), a==c );
1885 Gia_SatDumpClause( vStr, pLits, 5 );
1886 }
1887 }
1888 // the number of nodes with duplicated fanins and without inv is maximized
1889 if ( nBound && 2*nNodes > nBound ) {
1890 Vec_StrPrintF( vStr, "k %d ", 2*nNodes-nBound );
1891 nLits = 0;
1892 for ( n = nIns; n < nIns+nNodes; n++ ) {
1893 pLits[nLits++] = Abc_Var2Lit(Gia_KSatVarEqu(pMap, n), 0);
1894 pLits[nLits++] = Abc_Var2Lit(Gia_KSatVarInv(pMap, n), 1);
1895 }
1896 Gia_SatDumpClause( vStr, pLits, nLits );
1897 }
1898 Vec_StrPush( vStr, '\0' );
1899 Vec_IntFreeP( &vRes );
1900 return vStr;
1901}
1902
1903
1923
1924Vec_Int_t * Gia_ManDeriveKSatMappingArray( Gia_Man_t * p, Vec_Int_t * vRes )
1925{
1926 Vec_Int_t * vMapping = Vec_IntStart( 2*Gia_ManObjNum(p) );
1927 int i, Id; Gia_Obj_t * pObj;
1928 Gia_ManForEachCiId( p, Id, i )
1929 if ( Vec_IntEntry(vRes, Id) )
1930 Vec_IntWriteEntry( vMapping, Abc_Var2Lit(Id, 1), -1 );
1931 Gia_ManForEachAnd( p, pObj, i ) {
1932 assert( Vec_IntEntry(vRes, i) > 0 );
1933 if ( (Vec_IntEntry(vRes, i) & 2) == 0 ) {
1934 assert( (Vec_IntEntry(vRes, i) & 1) == 0 );
1935 continue;
1936 }
1937 Gia_Obj_t * pFans[2] = { Gia_ObjFanin0(pObj), Gia_ObjFanin1(pObj) };
1938 int fComp = ((Vec_IntEntry(vRes, i) >> 2) & 1) != 0;
1939 int fFan0 = ((Vec_IntEntry(vRes, Gia_ObjFaninId0(pObj, i)) >> 1) & 1) == 0 && Gia_ObjIsAnd(pFans[0]);
1940 int fFan1 = ((Vec_IntEntry(vRes, Gia_ObjFaninId1(pObj, i)) >> 1) & 1) == 0 && Gia_ObjIsAnd(pFans[1]);
1941 if ( Vec_IntEntry(vRes, i) & 1 )
1942 Vec_IntWriteEntry( vMapping, Abc_Var2Lit(i, !fComp), -1 );
1943 Vec_IntWriteEntry( vMapping, Abc_Var2Lit(i, fComp), Vec_IntSize(vMapping) );
1944 if ( fFan0 && fFan1 ) {
1945 Vec_IntPush( vMapping, 4 );
1946 if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) {
1947 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC0(pFans[1]))) );
1948 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC1(pFans[1]))) );
1949 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC0(pFans[0]))) );
1950 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pFans[0]))) );
1951 }
1952 else {
1953 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC0(pFans[0]))) );
1954 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pFans[0]))) );
1955 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC0(pFans[1]))) );
1956 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC1(pFans[1]))) );
1957 }
1958 if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
1959 Vec_IntPush( vMapping, fComp ? GIA_GATE2_OAI22 : GIA_GATE2_AOI22 );
1960 else if ( !Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) )
1961 Vec_IntPush( vMapping, fComp ? GIA_GATE2_NAN4 : GIA_GATE2_NOR4 );
1962 else
1963 Vec_IntPush( vMapping, fComp ? GIA_GATE2_OAI211 : GIA_GATE2_AOI211 );
1964 } else if ( fFan0 ) {
1965 Vec_IntPush( vMapping, 3 );
1966 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC0(pFans[0]))) );
1967 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pFans[0]))) );
1968 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pObj), !(fComp ^ Gia_ObjFaninC1(pObj))) );
1969 if ( Gia_ObjFaninC0(pObj) )
1970 Vec_IntPush( vMapping, fComp ? GIA_GATE2_OAI21 : GIA_GATE2_AOI21 );
1971 else
1972 Vec_IntPush( vMapping, fComp ? GIA_GATE2_NAN3 : GIA_GATE2_NOR3 );
1973 } else if ( fFan1 ) {
1974 Vec_IntPush( vMapping, 3 );
1975 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC0(pFans[1]))) );
1976 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC1(pFans[1]))) );
1977 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pObj), !(fComp ^ Gia_ObjFaninC0(pObj))) );
1978 if ( Gia_ObjFaninC1(pObj) )
1979 Vec_IntPush( vMapping, fComp ? GIA_GATE2_OAI21 : GIA_GATE2_AOI21 );
1980 else
1981 Vec_IntPush( vMapping, fComp ? GIA_GATE2_NAN3 : GIA_GATE2_NOR3 );
1982 } else {
1983 Vec_IntPush( vMapping, 2 );
1984 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pObj), !(fComp ^ Gia_ObjFaninC0(pObj))) );
1985 Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pObj), !(fComp ^ Gia_ObjFaninC1(pObj))) );
1986 Vec_IntPush( vMapping, fComp ? GIA_GATE2_NAN2 : GIA_GATE2_NOR2 );
1987 }
1988 }
1989 return vMapping;
1990}
1991
1992Gia_Man_t * Gia_ManDeriveKSatMapping( Vec_Int_t * vRes, int * pMap, int nIns, int nNodes, int fVerbose )
1993{
1994 Vec_Int_t * vGuide = Vec_IntStart( 1000 );
1995 Gia_Man_t * pNew = Gia_ManStart( nIns + nNodes + 2 );
1996 pNew->pName = Abc_UtilStrsav( "test" );
1997 int i, nSave = 0, pCopy[256] = {0};
1998 for ( i = 1; i <= nIns; i++ )
1999 pCopy[i] = Gia_ManAppendCi( pNew );
2000 for ( i = nIns; i < nIns+nNodes; i++ ) {
2001 int iFan0 = Gia_KSatFindFan( pMap, i, 0, vRes );
2002 int iFan1 = Gia_KSatFindFan( pMap, i, 1, vRes );
2003 if ( iFan0 == iFan1 )
2004 pCopy[i+1] = pCopy[iFan0+1];
2005 else if ( Gia_KSatValAnd(pMap, i, vRes) )
2006 pCopy[i+1] = Gia_ManAppendAnd( pNew, pCopy[iFan0+1], pCopy[iFan1+1] );
2007 else
2008 pCopy[i+1] = Gia_ManAppendOr( pNew, pCopy[iFan0+1], pCopy[iFan1+1] );
2009 pCopy[i+1] = Abc_LitNotCond( pCopy[i+1], Gia_KSatValInv(pMap, i, vRes) );
2010 if ( iFan0 == iFan1 )
2011 *Vec_IntEntryP(vGuide, Abc_Lit2Var(pCopy[i+1])) ^= 1;
2012 else if ( Gia_KSatValAnd(pMap, i, vRes) )
2013 *Vec_IntEntryP(vGuide, Abc_Lit2Var(pCopy[i+1])) ^= 4 | (2*Gia_KSatValInv(pMap, i, vRes));
2014 else
2015 *Vec_IntEntryP(vGuide, Abc_Lit2Var(pCopy[i+1])) ^= 8 | (2*Gia_KSatValInv(pMap, i, vRes));
2016 if ( fVerbose ) {
2017 if ( i == nIns+nNodes-1 )
2018 printf( " F = " );
2019 else
2020 printf( "%2d = ", i );
2021 if ( iFan0 == iFan1 )
2022 printf( "INV( %d )\n", iFan0 );
2023 else if ( Gia_KSatValAnd(pMap, i, vRes) )
2024 printf( "%sAND( %d, %d )\n", Gia_KSatValInv(pMap, i, vRes) ? "N":"", iFan0, iFan1 );
2025 else
2026 printf( "%sOR( %d, %d )\n", Gia_KSatValInv(pMap, i, vRes) ? "N":"", iFan0, iFan1 );
2027 nSave += (iFan0 == iFan1) || !Gia_KSatValInv(pMap, i, vRes);
2028 if ( i == nIns+nNodes-1 )
2029 printf( "Solution cost = %d\n", 2*(2*nNodes - nSave) );
2030 }
2031 }
2032 Gia_ManAppendCo( pNew, pCopy[nIns+nNodes] );
2033 //pNew->vCellMapping = Gia_ManDeriveKSatMappingArray( pNew, vGuide );
2034 Vec_IntFree( vGuide );
2035 return pNew;
2036}
2037
2038word Gia_ManGetTruth( Gia_Man_t * p )
2039{
2040 Gia_Obj_t * pObj; int i, Id;
2041 word pFuncs[256] = {0}, Const[2] = {0, ~(word)0};
2042 assert( Gia_ManObjNum(p) <= 256 );
2043 Gia_ManForEachCiId( p, Id, i )
2044 pFuncs[Id] = s_Truths6[i];
2045 Gia_ManForEachAnd( p, pObj, i )
2046 pFuncs[i] = (Const[Gia_ObjFaninC0(pObj)] ^ pFuncs[Gia_ObjFaninId0(pObj, i)]) & (Const[Gia_ObjFaninC1(pObj)] ^ pFuncs[Gia_ObjFaninId1(pObj, i)]);
2047 pObj = Gia_ManCo(p, 0);
2048 return Const[Gia_ObjFaninC0(pObj)] ^ pFuncs[Gia_ObjFaninId0p(p, pObj)];
2049}
2050
2051Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int Seed, int fMultiLevel, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv, char * pGuide )
2052{
2053 abctime clkStart = Abc_Clock();
2054 Gia_Man_t * pNew = NULL;
2055 srand(time(NULL));
2056 int Status, Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFFF;
2057 char pFileNameI[32]; sprintf( pFileNameI, "_%06x_.cnf", Rand );
2058 char pFileNameO[32]; sprintf( pFileNameO, "_%06x_.out", Rand );
2059 int nVars = 0, * pMap = Gia_KSatMapInit( nIns, nNodes, Truth, &nVars );
2060 Vec_Str_t * vStr = Gia_ManKSatCnf( pMap, nIns, nNodes, nBound/2, fMultiLevel, pGuide );
2061 if ( !Gia_ManDumpCnf(pFileNameI, vStr, nVars) ) {
2062 Vec_StrFree( vStr );
2063 return NULL;
2064 }
2065 if ( fVerbose )
2066 printf( "Vars = %d. Nodes = %d. Cardinality bound = %d. SAT vars = %d. SAT clauses = %d. Conflict limit = %d. Timeout = %d.\n",
2067 nIns, nNodes, nBound, nVars, Vec_StrCountEntry(vStr, '\n'), nBTLimit, nTimeout );
2068 Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, Seed, nBTLimit, nTimeout, 1, &Status );
2069 unlink( pFileNameI );
2070 //unlink( pFileNameO );
2071 if ( fKeepFile ) Gia_ManDumpCnf2( vStr, nVars, argc, argv, Abc_Clock() - clkStart, Status );
2072 Vec_StrFree( vStr );
2073 if ( vRes == NULL )
2074 return 0;
2075 Vec_IntDrop( vRes, 0 );
2076 pNew = Gia_ManDeriveKSatMapping( vRes, pMap, nIns, nNodes, fVerbose );
2077 printf( "Verification %s. ", Truth == Gia_ManGetTruth(pNew) ? "passed" : "failed" );
2078 Abc_PrintTime( 0, "Total time", Abc_Clock() - clkStart );
2079 Vec_IntFree( vRes );
2080 ABC_FREE( pMap );
2081 return pNew;
2082}
2083
2087
2088
2089ABC_NAMESPACE_IMPL_END
2090
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_FALLOC
#define ABC_FALLOC(type, num)
Definition abc_global.h:266
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition abc_global.h:258
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
RTM_VAL_VOID
@ RTM_VAL_VOID
Definition aigRet.c:35
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Vec_Str_t
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
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
Exa4_ManParse
Vec_Int_t * Exa4_ManParse(char *pFileName)
DECLARATIONS ///.
Definition bmcMaj.c:1812
value
ABC_NAMESPACE_IMPL_START typedef signed char value
Definition cadical_kitten.c:19
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
p
Cube * p
Definition exorList.c:222
Gia_SatVarInv
int Gia_SatVarInv(int i)
Definition giaSatLut.c:1304
Sbl_ManWindow2
int Sbl_ManWindow2(Sbl_Man_t *p, int iPivot)
Definition giaSatLut.c:946
Gia_KSatSetAnd
void Gia_KSatSetAnd(int *pMap, int i, int iVar)
Definition giaSatLut.c:1631
Gia_KSatValRef
int Gia_KSatValRef(int *pMap, int i, Vec_Int_t *vRes)
Definition giaSatLut.c:1640
Sbl_ManClean
void Sbl_ManClean(Sbl_Man_t *p)
Definition giaSatLut.c:178
Gia_KSatValAnd
int Gia_KSatValAnd(int *pMap, int i, Vec_Int_t *vRes)
Definition giaSatLut.c:1638
Gia_ManSimplePrintMapping
void Gia_ManSimplePrintMapping(Vec_Int_t *vRes, int nIns)
Definition giaSatLut.c:1513
KSAT_SPACE
#define KSAT_SPACE
Definition giaSatLut.c:1621
Gia_SatVarFan0
int Gia_SatVarFan0(int i)
Definition giaSatLut.c:1305
Sbl_Man_t
typedefABC_NAMESPACE_IMPL_START struct Sbl_Man_t_ Sbl_Man_t
DECLARATIONS ///.
Definition giaSatLut.c:42
Gia_KSatVarEqu
int Gia_KSatVarEqu(int *pMap, int i)
Definition giaSatLut.c:1625
Gia_ManSimpleCnf
Vec_Str_t * Gia_ManSimpleCnf(Gia_Man_t *p, int nBound)
Definition giaSatLut.c:1339
Gia_ManDeriveSimpleMapping
Vec_Int_t * Gia_ManDeriveSimpleMapping(Gia_Man_t *p, Vec_Int_t *vRes)
Definition giaSatLut.c:1459
Gia_SatDumpLiteral
void Gia_SatDumpLiteral(Vec_Str_t *vStr, int Lit)
Definition giaSatLut.c:1322
Gia_KSatVarMin
int Gia_KSatVarMin(int *pMap, int i, int m, int k)
Definition giaSatLut.c:1628
Gia_ManDumpCnf
int Gia_ManDumpCnf(char *pFileName, Vec_Str_t *vStr, int nVars)
Definition giaSatLut.c:1536
Gia_KSatFindFan
int Gia_KSatFindFan(int *pMap, int i, int f, Vec_Int_t *vRes)
Definition giaSatLut.c:1676
Gia_ManGate2_t
Gia_ManGate2_t
Definition giaSatLut.c:1904
GIA_GATE2_INV
@ GIA_GATE2_INV
Definition giaSatLut.c:1908
GIA_GATE2_NOR2
@ GIA_GATE2_NOR2
Definition giaSatLut.c:1910
GIA_GATE2_OAI21
@ GIA_GATE2_OAI21
Definition giaSatLut.c:1914
GIA_GATE2_AOI21
@ GIA_GATE2_AOI21
Definition giaSatLut.c:1911
GIA_GATE2_NAN4
@ GIA_GATE2_NAN4
Definition giaSatLut.c:1918
GIA_GATE2_OAI211
@ GIA_GATE2_OAI211
Definition giaSatLut.c:1919
GIA_GATE2_ZERO
@ GIA_GATE2_ZERO
Definition giaSatLut.c:1905
GIA_GATE2_NAN3
@ GIA_GATE2_NAN3
Definition giaSatLut.c:1912
GIA_GATE2_NAN2
@ GIA_GATE2_NAN2
Definition giaSatLut.c:1909
GIA_GATE2_BUF
@ GIA_GATE2_BUF
Definition giaSatLut.c:1907
GIA_GATE2_OAI22
@ GIA_GATE2_OAI22
Definition giaSatLut.c:1920
GIA_GATE2_NOR3
@ GIA_GATE2_NOR3
Definition giaSatLut.c:1913
GIA_GATE2_AOI211
@ GIA_GATE2_AOI211
Definition giaSatLut.c:1916
GIA_GATE2_NOR4
@ GIA_GATE2_NOR4
Definition giaSatLut.c:1915
GIA_GATE2_ONE
@ GIA_GATE2_ONE
Definition giaSatLut.c:1906
GIA_GATE2_VOID
@ GIA_GATE2_VOID
Definition giaSatLut.c:1921
GIA_GATE2_AOI22
@ GIA_GATE2_AOI22
Definition giaSatLut.c:1917
Gia_ManKSatMapping
Gia_Man_t * Gia_ManKSatMapping(word Truth, int nIns, int nNodes, int nBound, int Seed, int fMultiLevel, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char **argv, char *pGuide)
Definition giaSatLut.c:2051
Sbl_ManAlloc
Sbl_Man_t * Sbl_ManAlloc(Gia_Man_t *pGia, int Number)
FUNCTION DEFINITIONS ///.
Definition giaSatLut.c:132
Gia_KSatValMin
int Gia_KSatValMin(int *pMap, int i, int m, int k, Vec_Int_t *vRes)
Definition giaSatLut.c:1642
Gia_ManKSatCnf
Vec_Str_t * Gia_ManKSatCnf(int *pMap, int nIns, int nNodes, int nBound, int fMultiLevel, char *pGuide)
Definition giaSatLut.c:1715
Gia_SatVarFan1
int Gia_SatVarFan1(int i)
Definition giaSatLut.c:1306
KSAT_MINTS
#define KSAT_MINTS
Definition giaSatLut.c:1620
Sbl_ManComputeDelay
int Sbl_ManComputeDelay(Sbl_Man_t *p, int iLut, Vec_Int_t *vFanins)
Definition giaSatLut.c:314
Gia_SatValReqPos
int Gia_SatValReqPos(Vec_Int_t *p, int i)
Definition giaSatLut.c:1308
Gia_SatValAckPos
int Gia_SatValAckPos(Vec_Int_t *p, int i)
Definition giaSatLut.c:1310
Gia_SatValReqNeg
int Gia_SatValReqNeg(Vec_Int_t *p, int i)
Definition giaSatLut.c:1309
Gia_SatValFan0
int Gia_SatValFan0(Vec_Int_t *p, int i)
Definition giaSatLut.c:1313
Gia_KSatSetFan
void Gia_KSatSetFan(int *pMap, int i, int f, int k, int iVar)
Definition giaSatLut.c:1634
Sbm_AddCardinSolver
sat_solver * Sbm_AddCardinSolver(int LogN, Vec_Int_t **pvVars)
Definition giaSatMap.c:456
Gia_ManKSatGenLevels
Vec_Int_t * Gia_ManKSatGenLevels(char *pGuide, int nIns, int nNodes)
Definition giaSatLut.c:1686
Gia_ManGetTruth
word Gia_ManGetTruth(Gia_Man_t *p)
Definition giaSatLut.c:2038
Gia_KSatValInv
int Gia_KSatValInv(int *pMap, int i, Vec_Int_t *vRes)
Definition giaSatLut.c:1637
Gia_KSatValEqu
int Gia_KSatValEqu(int *pMap, int i, Vec_Int_t *vRes)
Definition giaSatLut.c:1639
Gia_KSatSetInv
void Gia_KSatSetInv(int *pMap, int i, int iVar)
Definition giaSatLut.c:1630
Gia_ManDeriveKSatMappingArray
Vec_Int_t * Gia_ManDeriveKSatMappingArray(Gia_Man_t *p, Vec_Int_t *vRes)
Definition giaSatLut.c:1924
Sbl_ManCreateCnf
int Sbl_ManCreateCnf(Sbl_Man_t *p)
Definition giaSatLut.c:856
Gia_SatVarAckPos
int Gia_SatVarAckPos(int i)
Definition giaSatLut.c:1302
Gia_ManGate_t
Gia_ManGate_t
Definition giaSatLut.c:1443
GIA_GATE_AOI22
@ GIA_GATE_AOI22
Definition giaSatLut.c:1454
GIA_GATE_INV
@ GIA_GATE_INV
Definition giaSatLut.c:1447
GIA_GATE_NAN3
@ GIA_GATE_NAN3
Definition giaSatLut.c:1451
GIA_GATE_OAI21
@ GIA_GATE_OAI21
Definition giaSatLut.c:1453
GIA_GATE_ONE
@ GIA_GATE_ONE
Definition giaSatLut.c:1445
GIA_GATE_BUF
@ GIA_GATE_BUF
Definition giaSatLut.c:1446
GIA_GATE_ZERO
@ GIA_GATE_ZERO
Definition giaSatLut.c:1444
GIA_GATE_OAI22
@ GIA_GATE_OAI22
Definition giaSatLut.c:1455
GIA_GATE_NOR2
@ GIA_GATE_NOR2
Definition giaSatLut.c:1449
GIA_GATE_NAN2
@ GIA_GATE_NAN2
Definition giaSatLut.c:1448
GIA_GATE_NOR3
@ GIA_GATE_NOR3
Definition giaSatLut.c:1452
GIA_GATE_AOI21
@ GIA_GATE_AOI21
Definition giaSatLut.c:1450
Sbl_ManGetCurrentMapping
void Sbl_ManGetCurrentMapping(Sbl_Man_t *p)
Definition giaSatLut.c:268
Gia_KSatSetEqu
void Gia_KSatSetEqu(int *pMap, int i, int iVar)
Definition giaSatLut.c:1632
Gia_KSatVarRef
int Gia_KSatVarRef(int *pMap, int i)
Definition giaSatLut.c:1626
Gia_ManDeriveKSatMapping
Gia_Man_t * Gia_ManDeriveKSatMapping(Vec_Int_t *vRes, int *pMap, int nIns, int nNodes, int fVerbose)
Definition giaSatLut.c:1992
Gia_KSatVarFan
int Gia_KSatVarFan(int *pMap, int i, int f, int k)
Definition giaSatLut.c:1627
Gia_KSatVarAnd
int Gia_KSatVarAnd(int *pMap, int i)
Definition giaSatLut.c:1624
KSAT_OBJS
#define KSAT_OBJS
Definition giaSatLut.c:1619
Gia_SatVarReqNeg
int Gia_SatVarReqNeg(int i)
Definition giaSatLut.c:1301
Gia_KSatVarInv
int Gia_KSatVarInv(int *pMap, int i)
Definition giaSatLut.c:1623
Gia_SatDumpClause
void Gia_SatDumpClause(Vec_Str_t *vStr, int *pLits, int nLits)
Definition giaSatLut.c:1316
Gia_SatValInv
int Gia_SatValInv(Vec_Int_t *p, int i)
Definition giaSatLut.c:1312
Gia_SatVarAckNeg
int Gia_SatVarAckNeg(int i)
Definition giaSatLut.c:1303
Gia_KSatSetRef
void Gia_KSatSetRef(int *pMap, int i, int iVar)
Definition giaSatLut.c:1633
Sbl_ManTestSat
int Sbl_ManTestSat(Sbl_Man_t *p, int iPivot)
Definition giaSatLut.c:967
Sbl_ManUpdateMapping
void Sbl_ManUpdateMapping(Sbl_Man_t *p)
Definition giaSatLut.c:537
Sbl_ManEvaluateMapping
int Sbl_ManEvaluateMapping(Sbl_Man_t *p, int DelayGlo)
Definition giaSatLut.c:473
Gia_SatDumpKlause
void Gia_SatDumpKlause(Vec_Str_t *vStr, int nIns, int nAnds, int nBound)
Definition giaSatLut.c:1326
Gia_RunKadical
Vec_Int_t * Gia_RunKadical(char *pFileNameIn, char *pFileNameOut, int Seed, int nBTLimit, int TimeOut, int fVerbose, int *pStatus)
Definition giaSatLut.c:1237
Sbl_ManComputeCuts
int Sbl_ManComputeCuts(Sbl_Man_t *p)
Definition giaSatLut.c:740
Gia_SatVarReqPos
int Gia_SatVarReqPos(int i)
Definition giaSatLut.c:1300
Gia_ManSimpleMapping
int Gia_ManSimpleMapping(Gia_Man_t *p, int nBound, int Seed, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char **argv)
Definition giaSatLut.c:1572
Gia_ManDumpCnf2
int Gia_ManDumpCnf2(Vec_Str_t *vStr, int nVars, int argc, char **argv, abctime Time, int Status)
Definition giaSatLut.c:1544
Sbl_ManEvaluateMappingEdge
int Sbl_ManEvaluateMappingEdge(Sbl_Man_t *p, int DelayGlo)
Definition giaSatLut.c:433
Gia_SatValFan1
int Gia_SatValFan1(Vec_Int_t *p, int i)
Definition giaSatLut.c:1314
Sbl_ManStop
void Sbl_ManStop(Sbl_Man_t *p)
Definition giaSatLut.c:217
Gia_SatValAckNeg
int Gia_SatValAckNeg(Vec_Int_t *p, int i)
Definition giaSatLut.c:1311
Gia_KSatValFan
int Gia_KSatValFan(int *pMap, int i, int f, int k, Vec_Int_t *vRes)
Definition giaSatLut.c:1641
Sbl_ManCreateTiming
int Sbl_ManCreateTiming(Sbl_Man_t *p, int DelayStart)
Definition giaSatLut.c:321
Sbl_ManCriticalFanin
int Sbl_ManCriticalFanin(Sbl_Man_t *p, int iLut, Vec_Int_t *vFanins)
Definition giaSatLut.c:465
Sbl_ManWindow
void Sbl_ManWindow(Sbl_Man_t *p)
Definition giaSatLut.c:929
Gia_KSatMapInit
int * Gia_KSatMapInit(int nIns, int nNodes, word Truth, int *pnVars)
Definition giaSatLut.c:1644
Gia_ManLutSat
void Gia_ManLutSat(Gia_Man_t *pGia, int LutSize, int nNumber, int nImproves, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVerbose, int fVeryVerbose)
Definition giaSatLut.c:1190
Sbl_ManPrintRuntime
void Sbl_ManPrintRuntime(Sbl_Man_t *p)
Definition giaSatLut.c:1176
Gia_KSatSetMin
void Gia_KSatSetMin(int *pMap, int i, int m, int k, int iVar)
Definition giaSatLut.c:1635
Gia_ManForEachLut2Reverse
#define Gia_ManForEachLut2Reverse(p, i)
Definition gia.h:1170
Gia_ManEvalWindow
int Gia_ManEvalWindow(Gia_Man_t *p, Vec_Int_t *vLeaves, Vec_Int_t *vNodes, Vec_Wec_t *vWin, Vec_Int_t *vTemp, int fUseTwo)
Definition giaEdge.c:633
Gia_ManForEachLut2
#define Gia_ManForEachLut2(p, i)
Definition gia.h:1168
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManComputeOneWin
int Gia_ManComputeOneWin(Gia_Man_t *p, int iPivot, Vec_Int_t **pvRoots, Vec_Int_t **pvNodes, Vec_Int_t **pvLeaves, Vec_Int_t **pvAnds)
Definition giaSplit.c:516
Gia_ManForEachCoDriverId
#define Gia_ManForEachCoDriverId(p, DriverId, i)
Definition gia.h:1246
Gia_ManForEachObjVecReverse
#define Gia_ManForEachObjVecReverse(vVec, p, pObj, i)
Definition gia.h:1202
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManEvalEdgeCount
int Gia_ManEvalEdgeCount(Gia_Man_t *p)
Definition giaEdge.c:284
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition giaUtil.c:369
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_TimeStamp
char * Gia_TimeStamp()
Definition giaUtil.c:106
Gia_ManComputeOneWinStart
void Gia_ManComputeOneWinStart(Gia_Man_t *p, int nAnds, int fReverse)
Definition giaSplit.c:541
Gia_ManEvalEdgeDelay
int Gia_ManEvalEdgeDelay(Gia_Man_t *p)
Definition giaEdge.c:201
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManOrderWithBoxes
Vec_Int_t * Gia_ManOrderWithBoxes(Gia_Man_t *p)
Definition giaTim.c:286
Gia_ManForEachAndId
#define Gia_ManForEachAndId(p, i)
Definition gia.h:1216
Gia_ManForEachCiId
#define Gia_ManForEachCiId(p, Id, i)
Definition gia.h:1230
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
sat_solver_nclauses
int sat_solver_nclauses(sat_solver *s)
Definition satSolver.c:2375
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_rollback
void sat_solver_rollback(sat_solver *s)
Definition satSolver.c:1643
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Gia_Man_t_::vPacking
Vec_Int_t * vPacking
Definition gia.h:141
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Man_t_::vEdge1
Vec_Int_t * vEdge1
Definition gia.h:147
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Sbl_Man_t_
Definition giaSatLut.c:44
Sbl_Man_t_::nIterOuts
int nIterOuts
Definition giaSatLut.c:58
Sbl_Man_t_::nHashWins
int nHashWins
Definition giaSatLut.c:55
Sbl_Man_t_::vLeaves
Vec_Int_t * vLeaves
Definition giaSatLut.c:71
Sbl_Man_t_::fVeryVeryVerbose
int fVeryVeryVerbose
Definition giaSatLut.c:68
Sbl_Man_t_::nVars
int nVars
Definition giaSatLut.c:47
Sbl_Man_t_::nRuns
int nRuns
Definition giaSatLut.c:54
Sbl_Man_t_::Power2
int Power2
Definition giaSatLut.c:49
Sbl_Man_t_::vCutsStart
Vec_Int_t * vCutsStart
Definition giaSatLut.c:89
Sbl_Man_t_::timeSat
abctime timeSat
Definition giaSatLut.c:105
Sbl_Man_t_::vTempI2
Vec_Wrd_t * vTempI2
Definition giaSatLut.c:92
Sbl_Man_t_::fDelay
int fDelay
Definition giaSatLut.c:64
Sbl_Man_t_::vCardVars
Vec_Int_t * vCardVars
Definition giaSatLut.c:46
Sbl_Man_t_::fVerbose
int fVerbose
Definition giaSatLut.c:66
Sbl_Man_t_::nEdges
int nEdges
Definition giaSatLut.c:63
Sbl_Man_t_::vPolar
Vec_Int_t * vPolar
Definition giaSatLut.c:101
Sbl_Man_t_::timeTime
abctime timeTime
Definition giaSatLut.c:109
Sbl_Man_t_::nLargeWins
int nLargeWins
Definition giaSatLut.c:57
Sbl_Man_t_::vEdges
Vec_Int_t * vEdges
Definition giaSatLut.c:82
Sbl_Man_t_::timeSatUns
abctime timeSatUns
Definition giaSatLut.c:107
Sbl_Man_t_::timeSatSat
abctime timeSatSat
Definition giaSatLut.c:106
Sbl_Man_t_::timeTotal
abctime timeTotal
Definition giaSatLut.c:111
Sbl_Man_t_::vReqs
Vec_Int_t * vReqs
Definition giaSatLut.c:79
Sbl_Man_t_::nSmallWins
int nSmallWins
Definition giaSatLut.c:56
Sbl_Man_t_::vArrs
Vec_Int_t * vArrs
Definition giaSatLut.c:78
Sbl_Man_t_::vWindow
Vec_Wec_t * vWindow
Definition giaSatLut.c:80
Sbl_Man_t_::fReverse
int fReverse
Definition giaSatLut.c:65
Sbl_Man_t_::vCutsNum
Vec_Int_t * vCutsNum
Definition giaSatLut.c:88
Sbl_Man_t_::vCutsObj
Vec_Int_t * vCutsObj
Definition giaSatLut.c:90
Sbl_Man_t_::nBTLimit
int nBTLimit
Definition giaSatLut.c:61
Sbl_Man_t_::nImproved
int nImproved
Definition giaSatLut.c:53
Sbl_Man_t_::pHash
Hsh_VecMan_t * pHash
Definition giaSatLut.c:76
Sbl_Man_t_::timeOther
abctime timeOther
Definition giaSatLut.c:112
Sbl_Man_t_::timeSatUnd
abctime timeSatUnd
Definition giaSatLut.c:108
Sbl_Man_t_::pSat
sat_solver * pSat
Definition giaSatLut.c:45
Sbl_Man_t_::LutSize
int LutSize
Definition giaSatLut.c:60
Sbl_Man_t_::pGia
Gia_Man_t * pGia
Definition giaSatLut.c:70
Sbl_Man_t_::vNodes
Vec_Int_t * vNodes
Definition giaSatLut.c:73
Sbl_Man_t_::vSolInit
Vec_Int_t * vSolInit
Definition giaSatLut.c:95
Sbl_Man_t_::FirstVar
int FirstVar
Definition giaSatLut.c:50
Sbl_Man_t_::vAssump
Vec_Int_t * vAssump
Definition giaSatLut.c:100
Sbl_Man_t_::LogN
int LogN
Definition giaSatLut.c:48
Sbl_Man_t_::vTempN1
Vec_Wrd_t * vTempN1
Definition giaSatLut.c:93
Sbl_Man_t_::vRootVars
Vec_Int_t * vRootVars
Definition giaSatLut.c:75
Sbl_Man_t_::vCutsI2
Vec_Wrd_t * vCutsI2
Definition giaSatLut.c:85
Sbl_Man_t_::vTempI1
Vec_Wrd_t * vTempI1
Definition giaSatLut.c:91
Sbl_Man_t_::timeWin
abctime timeWin
Definition giaSatLut.c:103
Sbl_Man_t_::timeCut
abctime timeCut
Definition giaSatLut.c:104
Sbl_Man_t_::vPath
Vec_Int_t * vPath
Definition giaSatLut.c:81
Sbl_Man_t_::vCutsI1
Vec_Wrd_t * vCutsI1
Definition giaSatLut.c:84
Sbl_Man_t_::vSolCur
Vec_Int_t * vSolCur
Definition giaSatLut.c:96
Sbl_Man_t_::vCutsN2
Vec_Wrd_t * vCutsN2
Definition giaSatLut.c:87
Sbl_Man_t_::vLits
Vec_Int_t * vLits
Definition giaSatLut.c:99
Sbl_Man_t_::timeStart
abctime timeStart
Definition giaSatLut.c:110
Sbl_Man_t_::vRoots
Vec_Int_t * vRoots
Definition giaSatLut.c:74
Sbl_Man_t_::fVeryVerbose
int fVeryVerbose
Definition giaSatLut.c:67
Sbl_Man_t_::DelayMax
int DelayMax
Definition giaSatLut.c:62
Sbl_Man_t_::vTempN2
Vec_Wrd_t * vTempN2
Definition giaSatLut.c:94
Sbl_Man_t_::vCutsN1
Vec_Wrd_t * vCutsN1
Definition giaSatLut.c:86
Sbl_Man_t_::vAnds
Vec_Int_t * vAnds
Definition giaSatLut.c:72
Sbl_Man_t_::vSolBest
Vec_Int_t * vSolBest
Definition giaSatLut.c:97
Sbl_Man_t_::nTried
int nTried
Definition giaSatLut.c:52
Tim_ManSetCoArrival
void Tim_ManSetCoArrival(Tim_Man_t *p, int iCo, float Delay)
Definition timTime.c:116
Tim_ManBoxNum
int Tim_ManBoxNum(Tim_Man_t *p)
Definition timMan.c:722
Tim_Man_t
typedefABC_NAMESPACE_HEADER_START struct Tim_Man_t_ Tim_Man_t
INCLUDES ///.
Definition tim.h:92
Tim_ManIncrementTravId
void Tim_ManIncrementTravId(Tim_Man_t *p)
DECLARATIONS ///.
Definition timTrav.c:44
Tim_ManSetCiRequired
void Tim_ManSetCiRequired(Tim_Man_t *p, int iCi, float Delay)
Definition timTime.c:135
Tim_ManInitPoRequiredAll
void Tim_ManInitPoRequiredAll(Tim_Man_t *p, float Delay)
Definition timTime.c:97
Tim_ManGetCiArrival
float Tim_ManGetCiArrival(Tim_Man_t *p, int iCi)
Definition timTime.c:174
Tim_ManGetCoRequired
float Tim_ManGetCoRequired(Tim_Man_t *p, int iCo)
Definition timTime.c:222
assert
#define assert(ex)
Definition util_old.h:213
system
int system()
sprintf
char * sprintf()
Hsh_VecMan_t
struct Hsh_VecMan_t_ Hsh_VecMan_t
Definition vecHsh.h:85
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryDoubleStart
#define Vec_IntForEachEntryDoubleStart(vVec, Entry1, Entry2, i, Start)
Definition vecInt.h:74
Vec_WecForEachLevel
#define Vec_WecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecWec.h:55
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42