ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
fraigSat.c
Go to the documentation of this file.
1
18
19#include <math.h>
20#include "fraigInt.h"
21#include "sat/msat/msatInt.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
29
30static void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
31static void Fraig_SetupAdjacent( Fraig_Man_t * pMan, Msat_IntVec_t * vConeVars );
32static void Fraig_SetupAdjacentMark( Fraig_Man_t * pMan, Msat_IntVec_t * vConeVars );
33static void Fraig_PrepareCones( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
34static void Fraig_PrepareCones_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
35
36static void Fraig_SupergateAddClauses( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper );
37static void Fraig_SupergateAddClausesExor( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
38static void Fraig_SupergateAddClausesMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
39//static void Fraig_DetectFanoutFreeCone( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
40static void Fraig_DetectFanoutFreeConeMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
41static void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
42
43// The lesson learned seems to be that variable should be in reverse topological order
44// from the output of the miter. The ordering of adjacency lists is very important.
45// The best way seems to be fanins followed by fanouts. Slight changes to this order
46// leads to big degradation in quality.
47
48static int nMuxes;
49
53
65int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit, int nTimeLimit )
66{
67 if ( pNode1 == pNode2 )
68 return 1;
69 if ( pNode1 == Fraig_Not(pNode2) )
70 return 0;
71 return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit, nTimeLimit );
72}
73
85void Fraig_ManProveMiter( Fraig_Man_t * p )
86{
87 Fraig_Node_t * pNode;
88 int i;
89 abctime clk;
90
91 if ( !p->fTryProve )
92 return;
93
94 clk = Abc_Clock();
95 // consider all outputs of the multi-output miter
96 for ( i = 0; i < p->vOutputs->nSize; i++ )
97 {
98 pNode = Fraig_Regular(p->vOutputs->pArray[i]);
99 // skip already constant nodes
100 if ( pNode == p->pConst1 )
101 continue;
102 // skip nodes that are different according to simulation
103 if ( !Fraig_CompareSimInfo( pNode, p->pConst1, p->nWordsRand, 1 ) )
104 continue;
105 if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1, p->nSeconds ) )
106 {
107 if ( Fraig_IsComplement(p->vOutputs->pArray[i]) ^ Fraig_NodeComparePhase(p->pConst1, pNode) )
108 p->vOutputs->pArray[i] = Fraig_Not(p->pConst1);
109 else
110 p->vOutputs->pArray[i] = p->pConst1;
111 }
112 }
113 if ( p->fVerboseP )
114 {
115// ABC_PRT( "Final miter proof time", Abc_Clock() - clk );
116 }
117}
118
130int Fraig_ManCheckMiter( Fraig_Man_t * p )
131{
132 Fraig_Node_t * pNode;
133 int i;
134 ABC_FREE( p->pModel );
135 for ( i = 0; i < p->vOutputs->nSize; i++ )
136 {
137 // get the output node (it can be complemented!)
138 pNode = p->vOutputs->pArray[i];
139 // if the miter is constant 0, the problem is UNSAT
140 if ( pNode == Fraig_Not(p->pConst1) )
141 continue;
142 // consider the special case when the miter is constant 1
143 if ( pNode == p->pConst1 )
144 {
145 // in this case, any counter example will do to distinquish it from constant 0
146 // here we pick the counter example composed of all zeros
147 p->pModel = Fraig_ManAllocCounterExample( p );
148 return 0;
149 }
150 // save the counter example
151 p->pModel = Fraig_ManSaveCounterExample( p, pNode );
152 // if the model is not found, return undecided
153 if ( p->pModel == NULL )
154 return -1;
155 else
156 return 0;
157 }
158 return 1;
159}
160
161
173int Fraig_MarkTfi_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
174{
175 // skip the visited node
176 if ( pNode->TravId == pMan->nTravIds )
177 return 0;
178 pNode->TravId = pMan->nTravIds;
179 // skip the PI node
180 if ( pNode->NumPi >= 0 )
181 return 1;
182 // check the children
183 return Fraig_MarkTfi_rec( pMan, Fraig_Regular(pNode->p1) ) +
184 Fraig_MarkTfi_rec( pMan, Fraig_Regular(pNode->p2) );
185}
186
198int Fraig_MarkTfi2_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
199{
200 // skip the visited node
201 if ( pNode->TravId == pMan->nTravIds )
202 return 0;
203 // skip the boundary node
204 if ( pNode->TravId == pMan->nTravIds-1 )
205 {
206 pNode->TravId = pMan->nTravIds;
207 return 1;
208 }
209 pNode->TravId = pMan->nTravIds;
210 // skip the PI node
211 if ( pNode->NumPi >= 0 )
212 return 1;
213 // check the children
214 return Fraig_MarkTfi2_rec( pMan, Fraig_Regular(pNode->p1) ) +
215 Fraig_MarkTfi2_rec( pMan, Fraig_Regular(pNode->p2) );
216}
217
229int Fraig_MarkTfi3_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
230{
231 // skip the visited node
232 if ( pNode->TravId == pMan->nTravIds )
233 return 1;
234 // skip the boundary node
235 if ( pNode->TravId == pMan->nTravIds-1 )
236 {
237 pNode->TravId = pMan->nTravIds;
238 return 1;
239 }
240 pNode->TravId = pMan->nTravIds;
241 // skip the PI node
242 if ( pNode->NumPi >= 0 )
243 return 0;
244 // check the children
245 return Fraig_MarkTfi3_rec( pMan, Fraig_Regular(pNode->p1) ) *
246 Fraig_MarkTfi3_rec( pMan, Fraig_Regular(pNode->p2) );
247}
248
260void Fraig_VarsStudy( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
261{
262 int NumPis, NumCut, fContain;
263
264 // mark the TFI of pNew
265 p->nTravIds++;
266 NumPis = Fraig_MarkTfi_rec( p, pNew );
267 printf( "(%d)(%d,%d):", NumPis, pOld->Level, pNew->Level );
268
269 // check if the old is in the TFI
270 if ( pOld->TravId == p->nTravIds )
271 {
272 printf( "* " );
273 return;
274 }
275
276 // count the boundary of nodes in pOld
277 p->nTravIds++;
278 NumCut = Fraig_MarkTfi2_rec( p, pOld );
279 printf( "%d", NumCut );
280
281 // check if the new is contained in the old's support
282 p->nTravIds++;
283 fContain = Fraig_MarkTfi3_rec( p, pNew );
284 printf( "%c ", fContain? '+':'-' );
285}
286
287
302int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit )
303{
304 int RetValue, RetValue1, i, fComp;
305 abctime clk;
306 int fVerbose = 0;
307 int fSwitch = 0;
308
309 // make sure the nodes are not complemented
310 assert( !Fraig_IsComplement(pNew) );
311 assert( !Fraig_IsComplement(pOld) );
312 assert( pNew != pOld );
313
314 // if at least one of the nodes is a failed node, perform adjustments:
315 // if the backtrack limit is small, simply skip this node
316 // if the backtrack limit is > 10, take the quare root of the limit
317 if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
318 {
319 p->nSatFails++;
320// return 0;
321// if ( nBTLimit > 10 )
322// nBTLimit /= 10;
323 if ( nBTLimit <= 10 )
324 return 0;
325 nBTLimit = (int)sqrt((double)nBTLimit);
326// fSwitch = 1;
327 }
328
329 p->nSatCalls++;
330
331 // make sure the solver is allocated and has enough variables
332 if ( p->pSat == NULL )
333 Fraig_ManCreateSolver( p );
334 // make sure the SAT solver has enough variables
335 for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
336 Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
337
338
339
340/*
341 {
342 Fraig_Node_t * ppNodes[2] = { pOld, pNew };
343 extern void Fraig_MappingShowNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppRoots, int nRoots, char * pFileName );
344 Fraig_MappingShowNodes( p, ppNodes, 2, "temp_aig" );
345 }
346*/
347
348 nMuxes = 0;
349
350
351 // get the logic cone
352clk = Abc_Clock();
353// Fraig_VarsStudy( p, pOld, pNew );
354 Fraig_OrderVariables( p, pOld, pNew );
355// Fraig_PrepareCones( p, pOld, pNew );
356p->timeTrav += Abc_Clock() - clk;
357
358// printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) );
359// ABC_PRT( "Time", Abc_Clock() - clk );
360
361 if ( fVerbose )
362 printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
363
364
365 // prepare variable activity
366 Fraig_SetActivity( p, pOld, pNew );
367
368 // get the complemented attribute
369 fComp = Fraig_NodeComparePhase( pOld, pNew );
370//Msat_SolverPrintClauses( p->pSat );
371
373 // prepare the solver to run incrementally on these variables
374//clk = Abc_Clock();
375 Msat_SolverPrepare( p->pSat, p->vVarsInt );
376//p->time3 += Abc_Clock() - clk;
377
378
379 // solve under assumptions
380 // A = 1; B = 0 OR A = 1; B = 1
381 Msat_IntVecClear( p->vProj );
382 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
383 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
384
385//Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" );
386
387 // run the solver
388clk = Abc_Clock();
389 RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
390p->timeSat += Abc_Clock() - clk;
391
392 if ( RetValue1 == MSAT_FALSE )
393 {
394//p->time1 += Abc_Clock() - clk;
395
396if ( fVerbose )
397{
398// printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) );
399//ABC_PRT( "time", Abc_Clock() - clk );
400}
401
402 // add the clause
403 Msat_IntVecClear( p->vProj );
404 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) );
405 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
406 RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
407 assert( RetValue );
408 // continue solving the other implication
409 }
410 else if ( RetValue1 == MSAT_TRUE )
411 {
412//p->time2 += Abc_Clock() - clk;
413
414if ( fVerbose )
415{
416// printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) );
417//ABC_PRT( "time", Abc_Clock() - clk );
418}
419
420 // record the counter example
421 Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
422
423// if ( pOld->fFailTfo || pNew->fFailTfo )
424// printf( "*" );
425// printf( "s(%d)", pNew->Level );
426 if ( fSwitch )
427 printf( "s(%d)", pNew->Level );
428 p->nSatCounter++;
429 return 0;
430 }
431 else // if ( RetValue1 == MSAT_UNKNOWN )
432 {
433p->time3 += Abc_Clock() - clk;
434
435// if ( pOld->fFailTfo || pNew->fFailTfo )
436// printf( "*" );
437// printf( "T(%d)", pNew->Level );
438
439 // mark the node as the failed node
440 if ( pOld != p->pConst1 )
441 pOld->fFailTfo = 1;
442 pNew->fFailTfo = 1;
443// p->nSatFails++;
444 if ( fSwitch )
445 printf( "T(%d)", pNew->Level );
446 p->nSatFailsReal++;
447 return 0;
448 }
449
450 // if the old node was constant 0, we already know the answer
451 if ( pOld == p->pConst1 )
452 return 1;
453
455 // prepare the solver to run incrementally
456//clk = Abc_Clock();
457 Msat_SolverPrepare( p->pSat, p->vVarsInt );
458//p->time3 += Abc_Clock() - clk;
459 // solve under assumptions
460 // A = 0; B = 1 OR A = 0; B = 0
461 Msat_IntVecClear( p->vProj );
462 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) );
463 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
464 // run the solver
465clk = Abc_Clock();
466 RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
467p->timeSat += Abc_Clock() - clk;
468
469 if ( RetValue1 == MSAT_FALSE )
470 {
471//p->time1 += Abc_Clock() - clk;
472
473if ( fVerbose )
474{
475// printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) );
476//ABC_PRT( "time", Abc_Clock() - clk );
477}
478
479 // add the clause
480 Msat_IntVecClear( p->vProj );
481 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
482 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
483 RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
484 assert( RetValue );
485 // continue solving the other implication
486 }
487 else if ( RetValue1 == MSAT_TRUE )
488 {
489//p->time2 += Abc_Clock() - clk;
490
491if ( fVerbose )
492{
493// printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) );
494//ABC_PRT( "time", Abc_Clock() - clk );
495}
496
497 // record the counter example
498 Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
499 p->nSatCounter++;
500
501// if ( pOld->fFailTfo || pNew->fFailTfo )
502// printf( "*" );
503// printf( "s(%d)", pNew->Level );
504 if ( fSwitch )
505 printf( "s(%d)", pNew->Level );
506 return 0;
507 }
508 else // if ( RetValue1 == MSAT_UNKNOWN )
509 {
510p->time3 += Abc_Clock() - clk;
511
512// if ( pOld->fFailTfo || pNew->fFailTfo )
513// printf( "*" );
514// printf( "T(%d)", pNew->Level );
515 if ( fSwitch )
516 printf( "T(%d)", pNew->Level );
517
518 // mark the node as the failed node
519 pOld->fFailTfo = 1;
520 pNew->fFailTfo = 1;
521// p->nSatFails++;
522 p->nSatFailsReal++;
523 return 0;
524 }
525
526 // return SAT proof
527 p->nSatProof++;
528
529// if ( pOld->fFailTfo || pNew->fFailTfo )
530// printf( "*" );
531// printf( "u(%d)", pNew->Level );
532
533 if ( fSwitch )
534 printf( "u(%d)", pNew->Level );
535
536 return 1;
537}
538
539
551int Fraig_NodeIsImplification( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit )
552{
553 int RetValue, RetValue1, i, fComp;
554 abctime clk;
555 int fVerbose = 0;
556
557 // make sure the nodes are not complemented
558 assert( !Fraig_IsComplement(pNew) );
559 assert( !Fraig_IsComplement(pOld) );
560 assert( pNew != pOld );
561
562 p->nSatCallsImp++;
563
564 // make sure the solver is allocated and has enough variables
565 if ( p->pSat == NULL )
566 Fraig_ManCreateSolver( p );
567 // make sure the SAT solver has enough variables
568 for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
569 Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
570
571 // get the logic cone
572clk = Abc_Clock();
573 Fraig_OrderVariables( p, pOld, pNew );
574// Fraig_PrepareCones( p, pOld, pNew );
575p->timeTrav += Abc_Clock() - clk;
576
577 if ( fVerbose )
578 printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
579
580
581 // get the complemented attribute
582 fComp = Fraig_NodeComparePhase( pOld, pNew );
583//Msat_SolverPrintClauses( p->pSat );
584
586 // prepare the solver to run incrementally on these variables
587//clk = Abc_Clock();
588 Msat_SolverPrepare( p->pSat, p->vVarsInt );
589//p->time3 += Abc_Clock() - clk;
590
591 // solve under assumptions
592 // A = 1; B = 0 OR A = 1; B = 1
593 Msat_IntVecClear( p->vProj );
594 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
595 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
596 // run the solver
597clk = Abc_Clock();
598 RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
599p->timeSat += Abc_Clock() - clk;
600
601 if ( RetValue1 == MSAT_FALSE )
602 {
603//p->time1 += Abc_Clock() - clk;
604
605if ( fVerbose )
606{
607// printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) );
608//ABC_PRT( "time", Abc_Clock() - clk );
609}
610
611 // add the clause
612 Msat_IntVecClear( p->vProj );
613 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) );
614 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
615 RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
616 assert( RetValue );
617// p->nSatProofImp++;
618 return 1;
619 }
620 else if ( RetValue1 == MSAT_TRUE )
621 {
622//p->time2 += Abc_Clock() - clk;
623
624if ( fVerbose )
625{
626// printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) );
627//ABC_PRT( "time", Abc_Clock() - clk );
628}
629 // record the counter example
630 Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
631 p->nSatCounterImp++;
632 return 0;
633 }
634 else // if ( RetValue1 == MSAT_UNKNOWN )
635 {
636p->time3 += Abc_Clock() - clk;
637 p->nSatFailsImp++;
638 return 0;
639 }
640}
641
653int Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit )
654{
655 Fraig_Node_t * pNode1R, * pNode2R;
656 int RetValue, RetValue1, i;
657 abctime clk;
658 int fVerbose = 0;
659
660 pNode1R = Fraig_Regular(pNode1);
661 pNode2R = Fraig_Regular(pNode2);
662 assert( pNode1R != pNode2R );
663
664 // make sure the solver is allocated and has enough variables
665 if ( p->pSat == NULL )
666 Fraig_ManCreateSolver( p );
667 // make sure the SAT solver has enough variables
668 for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
669 Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
670
671 // get the logic cone
672clk = Abc_Clock();
673 Fraig_OrderVariables( p, pNode1R, pNode2R );
674// Fraig_PrepareCones( p, pNode1R, pNode2R );
675p->timeTrav += Abc_Clock() - clk;
676
678 // prepare the solver to run incrementally on these variables
679//clk = Abc_Clock();
680 Msat_SolverPrepare( p->pSat, p->vVarsInt );
681//p->time3 += Abc_Clock() - clk;
682
683 // solve under assumptions
684 // A = 1; B = 0 OR A = 1; B = 1
685 Msat_IntVecClear( p->vProj );
686 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, !Fraig_IsComplement(pNode1)) );
687 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, !Fraig_IsComplement(pNode2)) );
688 // run the solver
689clk = Abc_Clock();
690 RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
691p->timeSat += Abc_Clock() - clk;
692
693 if ( RetValue1 == MSAT_FALSE )
694 {
695//p->time1 += Abc_Clock() - clk;
696
697if ( fVerbose )
698{
699// printf( "unsat %d ", Msat_SolverReadBackTracks(p->pSat) );
700//ABC_PRT( "time", Abc_Clock() - clk );
701}
702
703 // add the clause
704 Msat_IntVecClear( p->vProj );
705 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, Fraig_IsComplement(pNode1)) );
706 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, Fraig_IsComplement(pNode2)) );
707 RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
708 assert( RetValue );
709// p->nSatProofImp++;
710 return 1;
711 }
712 else if ( RetValue1 == MSAT_TRUE )
713 {
714//p->time2 += Abc_Clock() - clk;
715
716if ( fVerbose )
717{
718// printf( "sat %d ", Msat_SolverReadBackTracks(p->pSat) );
719//ABC_PRT( "time", Abc_Clock() - clk );
720}
721 // record the counter example
722// Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pNode1R, pNode2R );
723 p->nSatCounterImp++;
724 return 0;
725 }
726 else // if ( RetValue1 == MSAT_UNKNOWN )
727 {
728p->time3 += Abc_Clock() - clk;
729 p->nSatFailsImp++;
730 return 0;
731 }
732}
733
734
746void Fraig_PrepareCones( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
747{
748// Msat_IntVec_t * vAdjs;
749// int * pVars, nVars, i, k;
750 int nVarsAlloc;
751
752 assert( pOld != pNew );
753 assert( !Fraig_IsComplement(pOld) );
754 assert( !Fraig_IsComplement(pNew) );
755 // clean the variables
756 nVarsAlloc = Msat_IntVecReadSize(pMan->vVarsUsed);
757 Msat_IntVecFill( pMan->vVarsUsed, nVarsAlloc, 0 );
758 Msat_IntVecClear( pMan->vVarsInt );
759
760 pMan->nTravIds++;
761 Fraig_PrepareCones_rec( pMan, pNew );
762 Fraig_PrepareCones_rec( pMan, pOld );
763
764
765/*
766 nVars = Msat_IntVecReadSize( pMan->vVarsInt );
767 pVars = Msat_IntVecReadArray( pMan->vVarsInt );
768 for ( i = 0; i < nVars; i++ )
769 {
770 // process its connections
771 vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] );
772 printf( "%d=%d { ", pVars[i], Msat_IntVecReadSize(vAdjs) );
773 for ( k = 0; k < Msat_IntVecReadSize(vAdjs); k++ )
774 printf( "%d ", Msat_IntVecReadEntry(vAdjs,k) );
775 printf( "}\n" );
776
777 }
778 i = 0;
779*/
780}
781
793void Fraig_PrepareCones_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
794{
795 Fraig_Node_t * pFanin;
796 Msat_IntVec_t * vAdjs;
797 int fUseMuxes = 1, i;
798 int fItIsTime;
799
800 // skip if the node is aleady visited
801 assert( !Fraig_IsComplement(pNode) );
802 if ( pNode->TravId == pMan->nTravIds )
803 return;
804 pNode->TravId = pMan->nTravIds;
805
806 // collect the node's number (closer to reverse topological order)
807 Msat_IntVecPush( pMan->vVarsInt, pNode->Num );
808 Msat_IntVecWriteEntry( pMan->vVarsUsed, pNode->Num, 1 );
809 if ( !Fraig_NodeIsAnd( pNode ) )
810 return;
811
812 // if the node does not have fanins, create them
813 fItIsTime = 0;
814 if ( pNode->vFanins == NULL )
815 {
816 fItIsTime = 1;
817 // create the fanins of the supergate
818 assert( pNode->fClauses == 0 );
819 if ( fUseMuxes && Fraig_NodeIsMuxType(pNode) )
820 {
821 pNode->vFanins = Fraig_NodeVecAlloc( 4 );
822 Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p1) );
823 Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p2) );
824 Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p1) );
825 Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) );
826 Fraig_SupergateAddClausesMux( pMan, pNode );
827 }
828 else
829 {
830 pNode->vFanins = Fraig_CollectSupergate( pNode, fUseMuxes );
831 Fraig_SupergateAddClauses( pMan, pNode, pNode->vFanins );
832 }
833 assert( pNode->vFanins->nSize > 1 );
834 pNode->fClauses = 1;
835 pMan->nVarsClauses++;
836
837 // add fanins
838 vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pNode->Num );
839 assert( Msat_IntVecReadSize( vAdjs ) == 0 );
840 for ( i = 0; i < pNode->vFanins->nSize; i++ )
841 {
842 pFanin = Fraig_Regular(pNode->vFanins->pArray[i]);
843 Msat_IntVecPush( vAdjs, pFanin->Num );
844 }
845 }
846
847 // recursively visit the fanins
848 for ( i = 0; i < pNode->vFanins->nSize; i++ )
849 Fraig_PrepareCones_rec( pMan, Fraig_Regular(pNode->vFanins->pArray[i]) );
850
851 if ( fItIsTime )
852 {
853 // recursively visit the fanins
854 for ( i = 0; i < pNode->vFanins->nSize; i++ )
855 {
856 pFanin = Fraig_Regular(pNode->vFanins->pArray[i]);
857 vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pFanin->Num );
858 Msat_IntVecPush( vAdjs, pNode->Num );
859 }
860 }
861}
862
875void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
876{
877 Fraig_Node_t * pNode, * pFanin;
878 int i, k, Number, fUseMuxes = 1;
879 int nVarsAlloc;
880
881 assert( pOld != pNew );
882 assert( !Fraig_IsComplement(pOld) );
883 assert( !Fraig_IsComplement(pNew) );
884
885 pMan->nTravIds++;
886
887 // clean the variables
888 nVarsAlloc = Msat_IntVecReadSize(pMan->vVarsUsed);
889 Msat_IntVecFill( pMan->vVarsUsed, nVarsAlloc, 0 );
890 Msat_IntVecClear( pMan->vVarsInt );
891
892 // add the first node
893 Msat_IntVecPush( pMan->vVarsInt, pOld->Num );
894 Msat_IntVecWriteEntry( pMan->vVarsUsed, pOld->Num, 1 );
895 pOld->TravId = pMan->nTravIds;
896
897 // add the second node
898 Msat_IntVecPush( pMan->vVarsInt, pNew->Num );
899 Msat_IntVecWriteEntry( pMan->vVarsUsed, pNew->Num, 1 );
900 pNew->TravId = pMan->nTravIds;
901
902 // create the variable order
903 for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ )
904 {
905 // get the new node on the frontier
906 Number = Msat_IntVecReadEntry(pMan->vVarsInt, i);
907 pNode = pMan->vNodes->pArray[Number];
908 if ( !Fraig_NodeIsAnd(pNode) )
909 continue;
910
911 // if the node does not have fanins, create them
912 if ( pNode->vFanins == NULL )
913 {
914 // create the fanins of the supergate
915 assert( pNode->fClauses == 0 );
916 // detecting a fanout-free cone (experiment only)
917// Fraig_DetectFanoutFreeCone( pMan, pNode );
918
919 if ( fUseMuxes && Fraig_NodeIsMuxType(pNode) )
920 {
921 pNode->vFanins = Fraig_NodeVecAlloc( 4 );
922 Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p1) );
923 Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p2) );
924 Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p1) );
925 Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) );
926 Fraig_SupergateAddClausesMux( pMan, pNode );
927// Fraig_DetectFanoutFreeConeMux( pMan, pNode );
928
929 nMuxes++;
930 }
931 else
932 {
933 pNode->vFanins = Fraig_CollectSupergate( pNode, fUseMuxes );
934 Fraig_SupergateAddClauses( pMan, pNode, pNode->vFanins );
935 }
936 assert( pNode->vFanins->nSize > 1 );
937 pNode->fClauses = 1;
938 pMan->nVarsClauses++;
939
940 pNode->fMark2 = 1; // goes together with Fraig_SetupAdjacentMark()
941 }
942
943 // explore the implication fanins of pNode
944 for ( k = 0; k < pNode->vFanins->nSize; k++ )
945 {
946 pFanin = Fraig_Regular(pNode->vFanins->pArray[k]);
947 if ( pFanin->TravId == pMan->nTravIds ) // already collected
948 continue;
949 // collect and mark
950 Msat_IntVecPush( pMan->vVarsInt, pFanin->Num );
951 Msat_IntVecWriteEntry( pMan->vVarsUsed, pFanin->Num, 1 );
952 pFanin->TravId = pMan->nTravIds;
953 }
954 }
955
956 // set up the adjacent variable information
957// Fraig_SetupAdjacent( pMan, pMan->vVarsInt );
958 Fraig_SetupAdjacentMark( pMan, pMan->vVarsInt );
959}
960
961
962
974void Fraig_SetupAdjacent( Fraig_Man_t * pMan, Msat_IntVec_t * vConeVars )
975{
976 Fraig_Node_t * pNode, * pFanin;
977 Msat_IntVec_t * vAdjs;
978 int * pVars, nVars, i, k;
979
980 // clean the adjacents for the variables
981 nVars = Msat_IntVecReadSize( vConeVars );
982 pVars = Msat_IntVecReadArray( vConeVars );
983 for ( i = 0; i < nVars; i++ )
984 {
985 // process its connections
986 vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] );
987 Msat_IntVecClear( vAdjs );
988
989 pNode = pMan->vNodes->pArray[pVars[i]];
990 if ( !Fraig_NodeIsAnd(pNode) )
991 continue;
992
993 // add fanins
994 vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] );
995 for ( k = 0; k < pNode->vFanins->nSize; k++ )
996// for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- )
997 {
998 pFanin = Fraig_Regular(pNode->vFanins->pArray[k]);
999 Msat_IntVecPush( vAdjs, pFanin->Num );
1000// Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num );
1001 }
1002 }
1003 // add the fanouts
1004 for ( i = 0; i < nVars; i++ )
1005 {
1006 pNode = pMan->vNodes->pArray[pVars[i]];
1007 if ( !Fraig_NodeIsAnd(pNode) )
1008 continue;
1009
1010 // add the edges
1011 for ( k = 0; k < pNode->vFanins->nSize; k++ )
1012// for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- )
1013 {
1014 pFanin = Fraig_Regular(pNode->vFanins->pArray[k]);
1015 vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pFanin->Num );
1016 Msat_IntVecPush( vAdjs, pNode->Num );
1017// Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num );
1018 }
1019 }
1020}
1021
1022
1034void Fraig_SetupAdjacentMark( Fraig_Man_t * pMan, Msat_IntVec_t * vConeVars )
1035{
1036 Fraig_Node_t * pNode, * pFanin;
1037 Msat_IntVec_t * vAdjs;
1038 int * pVars, nVars, i, k;
1039
1040 // clean the adjacents for the variables
1041 nVars = Msat_IntVecReadSize( vConeVars );
1042 pVars = Msat_IntVecReadArray( vConeVars );
1043 for ( i = 0; i < nVars; i++ )
1044 {
1045 pNode = pMan->vNodes->pArray[pVars[i]];
1046 if ( pNode->fMark2 == 0 )
1047 continue;
1048// pNode->fMark2 = 0;
1049
1050 // process its connections
1051// vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] );
1052// Msat_IntVecClear( vAdjs );
1053
1054 if ( !Fraig_NodeIsAnd(pNode) )
1055 continue;
1056
1057 // add fanins
1058 vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pVars[i] );
1059 for ( k = 0; k < pNode->vFanins->nSize; k++ )
1060// for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- )
1061 {
1062 pFanin = Fraig_Regular(pNode->vFanins->pArray[k]);
1063 Msat_IntVecPush( vAdjs, pFanin->Num );
1064// Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num );
1065 }
1066 }
1067 // add the fanouts
1068 for ( i = 0; i < nVars; i++ )
1069 {
1070 pNode = pMan->vNodes->pArray[pVars[i]];
1071 if ( pNode->fMark2 == 0 )
1072 continue;
1073 pNode->fMark2 = 0;
1074
1075 if ( !Fraig_NodeIsAnd(pNode) )
1076 continue;
1077
1078 // add the edges
1079 for ( k = 0; k < pNode->vFanins->nSize; k++ )
1080// for ( k = pNode->vFanins->nSize - 1; k >= 0; k-- )
1081 {
1082 pFanin = Fraig_Regular(pNode->vFanins->pArray[k]);
1083 vAdjs = (Msat_IntVec_t *)Msat_ClauseVecReadEntry( pMan->vAdjacents, pFanin->Num );
1084 Msat_IntVecPush( vAdjs, pNode->Num );
1085// Msat_IntVecPushUniqueOrder( vAdjs, pFanin->Num );
1086 }
1087 }
1088}
1089
1090
1091
1092
1104void Fraig_SupergateAddClauses( Fraig_Man_t * p, Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper )
1105{
1106 int fComp1, RetValue, nVars, Var, Var1, i;
1107
1108 assert( Fraig_NodeIsAnd( pNode ) );
1109 nVars = Msat_SolverReadVarNum(p->pSat);
1110
1111 Var = pNode->Num;
1112 assert( Var < nVars );
1113 for ( i = 0; i < vSuper->nSize; i++ )
1114 {
1115 // get the predecessor nodes
1116 // get the complemented attributes of the nodes
1117 fComp1 = Fraig_IsComplement(vSuper->pArray[i]);
1118 // determine the variable numbers
1119 Var1 = Fraig_Regular(vSuper->pArray[i])->Num;
1120 // check that the variables are in the SAT manager
1121 assert( Var1 < nVars );
1122
1123 // suppose the AND-gate is A * B = C
1124 // add !A => !C or A + !C
1125 // fprintf( pFile, "%d %d 0%c", Var1, -Var, 10 );
1126 Msat_IntVecClear( p->vProj );
1127 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var1, fComp1) );
1128 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var, 1) );
1129 RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
1130 assert( RetValue );
1131 }
1132
1133 // add A & B => C or !A + !B + C
1134// fprintf( pFile, "%d %d %d 0%c", -Var1, -Var2, Var, 10 );
1135 Msat_IntVecClear( p->vProj );
1136 for ( i = 0; i < vSuper->nSize; i++ )
1137 {
1138 // get the predecessor nodes
1139 // get the complemented attributes of the nodes
1140 fComp1 = Fraig_IsComplement(vSuper->pArray[i]);
1141 // determine the variable numbers
1142 Var1 = Fraig_Regular(vSuper->pArray[i])->Num;
1143
1144 // add this variable to the array
1145 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var1, !fComp1) );
1146 }
1147 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(Var, 0) );
1148 RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
1149 assert( RetValue );
1150}
1151
1163void Fraig_SupergateAddClausesExor( Fraig_Man_t * p, Fraig_Node_t * pNode )
1164{
1165 Fraig_Node_t * pNode1, * pNode2;
1166 int fComp, RetValue;
1167
1168 assert( !Fraig_IsComplement( pNode ) );
1169 assert( Fraig_NodeIsExorType( pNode ) );
1170 // get nodes
1171 pNode1 = Fraig_Regular(Fraig_Regular(pNode->p1)->p1);
1172 pNode2 = Fraig_Regular(Fraig_Regular(pNode->p1)->p2);
1173 // get the complemented attribute of the EXOR/NEXOR gate
1174 fComp = Fraig_NodeIsExor( pNode ); // 1 if EXOR, 0 if NEXOR
1175
1176 // create four clauses
1177 Msat_IntVecClear( p->vProj );
1178 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, fComp) );
1179 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num, fComp) );
1180 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num, fComp) );
1181 RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
1182 assert( RetValue );
1183 Msat_IntVecClear( p->vProj );
1184 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, fComp) );
1185 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num, !fComp) );
1186 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num, !fComp) );
1187 RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
1188 assert( RetValue );
1189 Msat_IntVecClear( p->vProj );
1190 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, !fComp) );
1191 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num, fComp) );
1192 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num, !fComp) );
1193 RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
1194 assert( RetValue );
1195 Msat_IntVecClear( p->vProj );
1196 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, !fComp) );
1197 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1->Num, !fComp) );
1198 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2->Num, fComp) );
1199 RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
1200 assert( RetValue );
1201}
1202
1214void Fraig_SupergateAddClausesMux( Fraig_Man_t * p, Fraig_Node_t * pNode )
1215{
1216 Fraig_Node_t * pNodeI, * pNodeT, * pNodeE;
1217 int RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
1218
1219 assert( !Fraig_IsComplement( pNode ) );
1220 assert( Fraig_NodeIsMuxType( pNode ) );
1221 // get nodes (I = if, T = then, E = else)
1222 pNodeI = Fraig_NodeRecognizeMux( pNode, &pNodeT, &pNodeE );
1223 // get the variable numbers
1224 VarF = pNode->Num;
1225 VarI = pNodeI->Num;
1226 VarT = Fraig_Regular(pNodeT)->Num;
1227 VarE = Fraig_Regular(pNodeE)->Num;
1228 // get the complementation flags
1229 fCompT = Fraig_IsComplement(pNodeT);
1230 fCompE = Fraig_IsComplement(pNodeE);
1231
1232 // f = ITE(i, t, e)
1233
1234 // i' + t' + f
1235 // i' + t + f'
1236 // i + e' + f
1237 // i + e + f'
1238
1239 // create four clauses
1240 Msat_IntVecClear( p->vProj );
1241 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI, 1) );
1242 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 1^fCompT) );
1243 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) );
1244 RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
1245 assert( RetValue );
1246 Msat_IntVecClear( p->vProj );
1247 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI, 1) );
1248 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 0^fCompT) );
1249 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 1) );
1250 RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
1251 assert( RetValue );
1252 Msat_IntVecClear( p->vProj );
1253 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI, 0) );
1254 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 1^fCompE) );
1255 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) );
1256 RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
1257 assert( RetValue );
1258 Msat_IntVecClear( p->vProj );
1259 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarI, 0) );
1260 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 0^fCompE) );
1261 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 1) );
1262 RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
1263 assert( RetValue );
1264
1265 // two additional clauses
1266 // t' & e' -> f'
1267 // t & e -> f
1268
1269 // t + e + f'
1270 // t' + e' + f
1271
1272 if ( VarT == VarE )
1273 {
1274// assert( fCompT == !fCompE );
1275 return;
1276 }
1277
1278 Msat_IntVecClear( p->vProj );
1279 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 0^fCompT) );
1280 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 0^fCompE) );
1281 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 1) );
1282 RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
1283 assert( RetValue );
1284 Msat_IntVecClear( p->vProj );
1285 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarT, 1^fCompT) );
1286 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarE, 1^fCompE) );
1287 Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(VarF, 0) );
1288 RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
1289 assert( RetValue );
1290
1291}
1292
1293
1294
1295
1296
1308void Fraig_DetectFanoutFreeCone_rec( Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper, Fraig_NodeVec_t * vInside, int fFirst )
1309{
1310 // make the pointer regular
1311 pNode = Fraig_Regular(pNode);
1312 // if the new node is complemented or a PI, another gate begins
1313 if ( (!fFirst && pNode->nRefs > 1) || Fraig_NodeIsVar(pNode) )
1314 {
1315 Fraig_NodeVecPushUnique( vSuper, pNode );
1316 return;
1317 }
1318 // go through the branches
1319 Fraig_DetectFanoutFreeCone_rec( pNode->p1, vSuper, vInside, 0 );
1320 Fraig_DetectFanoutFreeCone_rec( pNode->p2, vSuper, vInside, 0 );
1321 // add the node
1322 Fraig_NodeVecPushUnique( vInside, pNode );
1323}
1324
1336/*
1337void Fraig_DetectFanoutFreeCone( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
1338{
1339 Fraig_NodeVec_t * vFanins;
1340 Fraig_NodeVec_t * vInside;
1341 int nCubes;
1342 extern int Fraig_CutSopCountCubes( Fraig_Man_t * pMan, Fraig_NodeVec_t * vFanins, Fraig_NodeVec_t * vInside );
1343
1344 vFanins = Fraig_NodeVecAlloc( 8 );
1345 vInside = Fraig_NodeVecAlloc( 8 );
1346
1347 Fraig_DetectFanoutFreeCone_rec( pNode, vFanins, vInside, 1 );
1348 assert( vInside->pArray[vInside->nSize-1] == pNode );
1349
1350 nCubes = Fraig_CutSopCountCubes( pMan, vFanins, vInside );
1351
1352printf( "%d(%d)", vFanins->nSize, nCubes );
1353 Fraig_NodeVecFree( vFanins );
1354 Fraig_NodeVecFree( vInside );
1355}
1356*/
1357
1358
1359
1371void Fraig_DetectFanoutFreeConeMux_rec( Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper, Fraig_NodeVec_t * vInside, int fFirst )
1372{
1373 // make the pointer regular
1374 pNode = Fraig_Regular(pNode);
1375 // if the new node is complemented or a PI, another gate begins
1376 if ( (!fFirst && pNode->nRefs > 1) || Fraig_NodeIsVar(pNode) || !Fraig_NodeIsMuxType(pNode) )
1377 {
1378 Fraig_NodeVecPushUnique( vSuper, pNode );
1379 return;
1380 }
1381 // go through the branches
1382 Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p1)->p1, vSuper, vInside, 0 );
1383 Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p1)->p2, vSuper, vInside, 0 );
1384 Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p2)->p1, vSuper, vInside, 0 );
1385 Fraig_DetectFanoutFreeConeMux_rec( Fraig_Regular(pNode->p2)->p2, vSuper, vInside, 0 );
1386 // add the node
1387 Fraig_NodeVecPushUnique( vInside, pNode );
1388}
1389
1401void Fraig_DetectFanoutFreeConeMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
1402{
1403 Fraig_NodeVec_t * vFanins;
1404 Fraig_NodeVec_t * vInside;
1405 int nCubes;
1406 extern int Fraig_CutSopCountCubes( Fraig_Man_t * pMan, Fraig_NodeVec_t * vFanins, Fraig_NodeVec_t * vInside );
1407
1408 vFanins = Fraig_NodeVecAlloc( 8 );
1409 vInside = Fraig_NodeVecAlloc( 8 );
1410
1411 Fraig_DetectFanoutFreeConeMux_rec( pNode, vFanins, vInside, 1 );
1412 assert( vInside->pArray[vInside->nSize-1] == pNode );
1413
1414// nCubes = Fraig_CutSopCountCubes( pMan, vFanins, vInside );
1415 nCubes = 0;
1416
1417printf( "%d(%d)", vFanins->nSize, nCubes );
1418 Fraig_NodeVecFree( vFanins );
1419 Fraig_NodeVecFree( vInside );
1420}
1421
1422
1423
1436void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
1437{
1438 Fraig_Node_t * pNode;
1439 int i, Number, MaxLevel;
1440 float * pFactors = Msat_SolverReadFactors(pMan->pSat);
1441 if ( pFactors == NULL )
1442 return;
1443 MaxLevel = Abc_MaxInt( pOld->Level, pNew->Level );
1444 // create the variable order
1445 for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ )
1446 {
1447 // get the new node on the frontier
1448 Number = Msat_IntVecReadEntry(pMan->vVarsInt, i);
1449 pNode = pMan->vNodes->pArray[Number];
1450 pFactors[pNode->Num] = (float)pow( 0.97, MaxLevel - pNode->Level );
1451// if ( pNode->Num % 50 == 0 )
1452// printf( "(%d) %.2f ", MaxLevel - pNode->Level, pFactors[pNode->Num] );
1453 }
1454// printf( "\n" );
1455}
1456
1460
1461
1462ABC_NAMESPACE_IMPL_END
1463
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
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
p
Cube * p
Definition exorList.c:222
Var
int Var
Definition exorList.c:228
Fraig_ManAllocCounterExample
int * Fraig_ManAllocCounterExample(Fraig_Man_t *p)
Definition fraigFeed.c:787
Fraig_FeedBack
void Fraig_FeedBack(Fraig_Man_t *p, int *pModel, Msat_IntVec_t *vVars, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
Definition fraigFeed.c:80
Fraig_ManSaveCounterExample
int * Fraig_ManSaveCounterExample(Fraig_Man_t *p, Fraig_Node_t *pNode)
Definition fraigFeed.c:860
Fraig_NodeIsExorType
int Fraig_NodeIsExorType(Fraig_Node_t *pNode)
Definition fraigUtil.c:558
Fraig_CompareSimInfo
int Fraig_CompareSimInfo(Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int iWordLast, int fUseRand)
Definition fraigTable.c:351
Fraig_ManCreateSolver
void Fraig_ManCreateSolver(Fraig_Man_t *p)
Definition fraigMan.c:325
Fraig_NodeIsExor
int Fraig_NodeIsExor(Fraig_Node_t *pNode)
Definition fraigUtil.c:633
Fraig_NodeIsMuxType
int Fraig_NodeIsMuxType(Fraig_Node_t *pNode)
Definition fraigUtil.c:591
Fraig_CountPis
int Fraig_CountPis(Fraig_Man_t *p, Msat_IntVec_t *vVarNums)
Definition fraigUtil.c:817
Fraig_NodeRecognizeMux
Fraig_Node_t * Fraig_NodeRecognizeMux(Fraig_Node_t *pNode, Fraig_Node_t **ppNodeT, Fraig_Node_t **ppNodeE)
Definition fraigUtil.c:658
Fraig_ManProveMiter
void Fraig_ManProveMiter(Fraig_Man_t *p)
Definition fraigSat.c:85
Fraig_MarkTfi2_rec
int Fraig_MarkTfi2_rec(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition fraigSat.c:198
Fraig_ManCheckMiter
int Fraig_ManCheckMiter(Fraig_Man_t *p)
Definition fraigSat.c:130
Fraig_MarkTfi3_rec
int Fraig_MarkTfi3_rec(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition fraigSat.c:229
Fraig_ManCheckClauseUsingSat
int Fraig_ManCheckClauseUsingSat(Fraig_Man_t *p, Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int nBTLimit)
Definition fraigSat.c:653
Fraig_VarsStudy
void Fraig_VarsStudy(Fraig_Man_t *p, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
Definition fraigSat.c:260
Fraig_NodeIsImplification
int Fraig_NodeIsImplification(Fraig_Man_t *p, Fraig_Node_t *pOld, Fraig_Node_t *pNew, int nBTLimit)
Definition fraigSat.c:551
Fraig_NodesAreEqual
int Fraig_NodesAreEqual(Fraig_Man_t *p, Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int nBTLimit, int nTimeLimit)
FUNCTION DEFINITIONS ///.
Definition fraigSat.c:65
Fraig_DetectFanoutFreeConeMux_rec
void Fraig_DetectFanoutFreeConeMux_rec(Fraig_Node_t *pNode, Fraig_NodeVec_t *vSuper, Fraig_NodeVec_t *vInside, int fFirst)
Definition fraigSat.c:1371
Fraig_DetectFanoutFreeCone_rec
void Fraig_DetectFanoutFreeCone_rec(Fraig_Node_t *pNode, Fraig_NodeVec_t *vSuper, Fraig_NodeVec_t *vInside, int fFirst)
Definition fraigSat.c:1308
Fraig_NodeIsEquivalent
int Fraig_NodeIsEquivalent(Fraig_Man_t *p, Fraig_Node_t *pOld, Fraig_Node_t *pNew, int nBTLimit, int nTimeLimit)
Definition fraigSat.c:302
Fraig_MarkTfi_rec
int Fraig_MarkTfi_rec(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition fraigSat.c:173
Fraig_NodeVecFree
void Fraig_NodeVecFree(Fraig_NodeVec_t *p)
Definition fraigVec.c:66
Fraig_IsComplement
#define Fraig_IsComplement(p)
GLOBAL VARIABLES ///.
Definition fraig.h:107
Fraig_CollectSupergate
Fraig_NodeVec_t * Fraig_CollectSupergate(Fraig_Node_t *pNode, int fStopAtMux)
Definition fraigUtil.c:960
Fraig_Regular
#define Fraig_Regular(p)
Definition fraig.h:108
Fraig_Not
#define Fraig_Not(p)
Definition fraig.h:109
Fraig_NodeComparePhase
int Fraig_NodeComparePhase(Fraig_Node_t *p1, Fraig_Node_t *p2)
Definition fraigApi.c:154
Fraig_NodeVecPushUnique
int Fraig_NodeVecPushUnique(Fraig_NodeVec_t *p, Fraig_Node_t *Entry)
Definition fraigVec.c:212
Fraig_NodeVec_t
struct Fraig_NodeVecStruct_t_ Fraig_NodeVec_t
Definition fraig.h:42
Fraig_NodeIsAnd
int Fraig_NodeIsAnd(Fraig_Node_t *p)
Definition fraigApi.c:153
Fraig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Fraig_ManStruct_t_ Fraig_Man_t
INCLUDES ///.
Definition fraig.h:40
Fraig_NodeVecAlloc
Fraig_NodeVec_t * Fraig_NodeVecAlloc(int nCap)
DECLARATIONS ///.
Definition fraigVec.c:43
Fraig_Node_t
struct Fraig_NodeStruct_t_ Fraig_Node_t
Definition fraig.h:41
Fraig_NodeIsVar
int Fraig_NodeIsVar(Fraig_Node_t *p)
Definition fraigApi.c:152
Msat_ClauseVecReadEntry
Msat_Clause_t * Msat_ClauseVecReadEntry(Msat_ClauseVec_t *p, int i)
Definition msatClauseVec.c:225
Msat_SolverAddClause
int Msat_SolverAddClause(Msat_Solver_t *p, Msat_IntVec_t *pLits)
Definition msatSolverCore.c:65
Msat_SolverSolve
int Msat_SolverSolve(Msat_Solver_t *p, Msat_IntVec_t *pVecAssumps, int nBackTrackLimit, int nTimeLimit)
Definition msatSolverCore.c:138
Msat_IntVec_t
struct Msat_IntVec_t_ Msat_IntVec_t
Definition msat.h:45
MSAT_VAR2LIT
#define MSAT_VAR2LIT(v, s)
Definition msat.h:56
Msat_SolverReadVarNum
int Msat_SolverReadVarNum(Msat_Solver_t *p)
FUNCTION DEFINITIONS ///.
Definition msatSolverApi.c:47
Msat_SolverReadFactors
float * Msat_SolverReadFactors(Msat_Solver_t *p)
Definition msatSolverApi.c:70
Msat_IntVecReadEntry
int Msat_IntVecReadEntry(Msat_IntVec_t *p, int i)
Definition msatVec.c:249
MSAT_TRUE
@ MSAT_TRUE
Definition msat.h:50
MSAT_FALSE
@ MSAT_FALSE
Definition msat.h:50
Msat_SolverReadModelArray
int * Msat_SolverReadModelArray(Msat_Solver_t *p)
Definition msatSolverApi.c:57
Msat_IntVecFill
void Msat_IntVecFill(Msat_IntVec_t *p, int nSize, int Entry)
Definition msatVec.c:177
Msat_IntVecWriteEntry
void Msat_IntVecWriteEntry(Msat_IntVec_t *p, int i, int Entry)
Definition msatVec.c:266
Msat_IntVecReadSize
int Msat_IntVecReadSize(Msat_IntVec_t *p)
Definition msatVec.c:233
Msat_IntVecClear
void Msat_IntVecClear(Msat_IntVec_t *p)
Definition msatVec.c:335
Msat_SolverPrepare
void Msat_SolverPrepare(Msat_Solver_t *pSat, Msat_IntVec_t *vVars)
Definition msatSolverApi.c:451
Msat_IntVecPush
void Msat_IntVecPush(Msat_IntVec_t *p, int Entry)
Definition msatVec.c:351
Msat_SolverAddVar
int Msat_SolverAddVar(Msat_Solver_t *p, int Level)
DECLARATIONS ///.
Definition msatSolverCore.c:45
Msat_IntVecReadArray
int * Msat_IntVecReadArray(Msat_IntVec_t *p)
Definition msatVec.c:217
Fraig_NodeStruct_t_::TravId
int TravId
Definition fraigInt.h:214
Fraig_NodeStruct_t_::vFanins
Fraig_NodeVec_t * vFanins
Definition fraigInt.h:234
Fraig_NodeStruct_t_::NumPi
int NumPi
Definition fraigInt.h:211
Fraig_NodeStruct_t_::p2
Fraig_Node_t * p2
Definition fraigInt.h:233
Fraig_NodeStruct_t_::nRefs
int nRefs
Definition fraigInt.h:213
Fraig_NodeStruct_t_::Num
int Num
Definition fraigInt.h:210
Fraig_NodeStruct_t_::p1
Fraig_Node_t * p1
Definition fraigInt.h:232
Fraig_NodeStruct_t_::fMark2
unsigned fMark2
Definition fraigInt.h:223
Fraig_NodeStruct_t_::fFailTfo
unsigned fFailTfo
Definition fraigInt.h:227
Fraig_NodeStruct_t_::fClauses
unsigned fClauses
Definition fraigInt.h:220
Fraig_NodeStruct_t_::Level
int Level
Definition fraigInt.h:212
Fraig_NodeVecStruct_t_::pArray
Fraig_Node_t ** pArray
Definition fraigInt.h:267
Fraig_NodeVecStruct_t_::nSize
int nSize
Definition fraigInt.h:266
assert
#define assert(ex)
Definition util_old.h:213
Var1
@ Var1
Definition xsatSolver.h:56