abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraigSat.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [fraigSat.c]
4 
5  PackageName [FRAIG: Functionally reduced AND-INV graphs.]
6 
7  Synopsis [Proving functional equivalence using SAT.]
8 
9  Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
10 
11  Affiliation [UC Berkeley]
12 
13  Date [Ver. 2.0. Started - October 1, 2004]
14 
15  Revision [$Id: fraigSat.c,v 1.10 2005/07/08 01:01:32 alanmi Exp $]
16 
17 ***********************************************************************/
18 
19 #include <math.h>
20 #include "fraigInt.h"
21 #include "sat/msat/msatInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 static void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
31 static void Fraig_SetupAdjacent( Fraig_Man_t * pMan, Msat_IntVec_t * vConeVars );
32 static void Fraig_SetupAdjacentMark( Fraig_Man_t * pMan, Msat_IntVec_t * vConeVars );
33 static void Fraig_PrepareCones( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
34 static void Fraig_PrepareCones_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
35 
36 static void Fraig_SupergateAddClauses( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper );
37 static void Fraig_SupergateAddClausesExor( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
38 static void Fraig_SupergateAddClausesMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
39 //static void Fraig_DetectFanoutFreeCone( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
40 static void Fraig_DetectFanoutFreeConeMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
41 static 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 
48 static int nMuxes;
49 
50 ////////////////////////////////////////////////////////////////////////
51 /// FUNCTION DEFINITIONS ///
52 ////////////////////////////////////////////////////////////////////////
53 
54 /**Function*************************************************************
55 
56  Synopsis [Checks equivalence of two nodes.]
57 
58  Description [Returns 1 iff the nodes are equivalent.]
59 
60  SideEffects []
61 
62  SeeAlso []
63 
64 ***********************************************************************/
65 int 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 
74 /**Function*************************************************************
75 
76  Synopsis [Tries to prove the final miter.]
77 
78  Description []
79 
80  SideEffects []
81 
82  SeeAlso []
83 
84 ***********************************************************************/
85 void 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 
119 /**Function*************************************************************
120 
121  Synopsis [Returns 1 if the miter is unsat; 0 if sat; -1 if undecided.]
122 
123  Description []
124 
125  SideEffects []
126 
127  SeeAlso []
128 
129 ***********************************************************************/
130 int 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 
162 /**Function*************************************************************
163 
164  Synopsis [Returns 1 if pOld is in the TFI of pNew.]
165 
166  Description []
167 
168  SideEffects []
169 
170  SeeAlso []
171 
172 ***********************************************************************/
173 int 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 
187 /**Function*************************************************************
188 
189  Synopsis [Returns 1 if pOld is in the TFI of pNew.]
190 
191  Description []
192 
193  SideEffects []
194 
195  SeeAlso []
196 
197 ***********************************************************************/
198 int 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 
218 /**Function*************************************************************
219 
220  Synopsis [Returns 1 if pOld is in the TFI of pNew.]
221 
222  Description []
223 
224  SideEffects []
225 
226  SeeAlso []
227 
228 ***********************************************************************/
229 int 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 
249 /**Function*************************************************************
250 
251  Synopsis []
252 
253  Description []
254 
255  SideEffects []
256 
257  SeeAlso []
258 
259 ***********************************************************************/
260 void 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 
288 /**Function*************************************************************
289 
290  Synopsis [Checks whether two nodes are functinally equivalent.]
291 
292  Description [The flag (fComp) tells whether the nodes to be checked
293  are in the opposite polarity. The second flag (fSkipZeros) tells whether
294  the checking should be performed if the simulation vectors are zeros.
295  Returns 1 if the nodes are equivalent; 0 othewise.]
296 
297  SideEffects []
298 
299  SeeAlso []
300 
301 ***********************************************************************/
302 int 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
352 clk = Abc_Clock();
353 // Fraig_VarsStudy( p, pOld, pNew );
354  Fraig_OrderVariables( p, pOld, pNew );
355 // Fraig_PrepareCones( p, pOld, pNew );
356 p->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 
372  ////////////////////////////////////////////
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
388 clk = Abc_Clock();
389  RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
390 p->timeSat += Abc_Clock() - clk;
391 
392  if ( RetValue1 == MSAT_FALSE )
393  {
394 //p->time1 += Abc_Clock() - clk;
395 
396 if ( 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 
414 if ( 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  {
433 p->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 
454  ////////////////////////////////////////////
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
465 clk = Abc_Clock();
466  RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
467 p->timeSat += Abc_Clock() - clk;
468 
469  if ( RetValue1 == MSAT_FALSE )
470  {
471 //p->time1 += Abc_Clock() - clk;
472 
473 if ( 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 
491 if ( 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  {
510 p->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 
540 /**Function*************************************************************
541 
542  Synopsis [Checks whether pOld => pNew.]
543 
544  Description []
545 
546  SideEffects []
547 
548  SeeAlso []
549 
550 ***********************************************************************/
551 int Fraig_NodeIsImplication( 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
572 clk = Abc_Clock();
573  Fraig_OrderVariables( p, pOld, pNew );
574 // Fraig_PrepareCones( p, pOld, pNew );
575 p->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 
585  ////////////////////////////////////////////
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
597 clk = Abc_Clock();
598  RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
599 p->timeSat += Abc_Clock() - clk;
600 
601  if ( RetValue1 == MSAT_FALSE )
602  {
603 //p->time1 += Abc_Clock() - clk;
604 
605 if ( 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 
624 if ( 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  {
636 p->time3 += Abc_Clock() - clk;
637  p->nSatFailsImp++;
638  return 0;
639  }
640 }
641 
642 /**Function*************************************************************
643 
644  Synopsis [Prepares the SAT solver to run on the two nodes.]
645 
646  Description []
647 
648  SideEffects []
649 
650  SeeAlso []
651 
652 ***********************************************************************/
653 int 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
672 clk = Abc_Clock();
673  Fraig_OrderVariables( p, pNode1R, pNode2R );
674 // Fraig_PrepareCones( p, pNode1R, pNode2R );
675 p->timeTrav += Abc_Clock() - clk;
676 
677  ////////////////////////////////////////////
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
689 clk = Abc_Clock();
690  RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
691 p->timeSat += Abc_Clock() - clk;
692 
693  if ( RetValue1 == MSAT_FALSE )
694  {
695 //p->time1 += Abc_Clock() - clk;
696 
697 if ( 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 
716 if ( 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  {
728 p->time3 += Abc_Clock() - clk;
729  p->nSatFailsImp++;
730  return 0;
731  }
732 }
733 
734 
735 /**Function*************************************************************
736 
737  Synopsis [Prepares the SAT solver to run on the two nodes.]
738 
739  Description []
740 
741  SideEffects []
742 
743  SeeAlso []
744 
745 ***********************************************************************/
746 void 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 
782 /**Function*************************************************************
783 
784  Synopsis [Traverses the cone, collects the numbers and adds the clauses.]
785 
786  Description []
787 
788  SideEffects []
789 
790  SeeAlso []
791 
792 ***********************************************************************/
793 void 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 
863 /**Function*************************************************************
864 
865  Synopsis [Collect variables using their proximity from the nodes.]
866 
867  Description [This procedure creates a variable order based on collecting
868  first the nodes that are the closest to the given two target nodes.]
869 
870  SideEffects []
871 
872  SeeAlso []
873 
874 ***********************************************************************/
875 void 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 
963 /**Function*************************************************************
964 
965  Synopsis [Set up the adjacent variable information.]
966 
967  Description []
968 
969  SideEffects []
970 
971  SeeAlso []
972 
973 ***********************************************************************/
974 void 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 
1023 /**Function*************************************************************
1024 
1025  Synopsis [Set up the adjacent variable information.]
1026 
1027  Description []
1028 
1029  SideEffects []
1030 
1031  SeeAlso []
1032 
1033 ***********************************************************************/
1034 void 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 
1093 /**Function*************************************************************
1094 
1095  Synopsis [Adds clauses to the solver.]
1096 
1097  Description []
1098 
1099  SideEffects []
1100 
1101  SeeAlso []
1102 
1103 ***********************************************************************/
1104 void 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 
1152 /**Function*************************************************************
1153 
1154  Synopsis [Adds clauses to the solver.]
1155 
1156  Description []
1157 
1158  SideEffects []
1159 
1160  SeeAlso []
1161 
1162 ***********************************************************************/
1163 void 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 
1203 /**Function*************************************************************
1204 
1205  Synopsis [Adds clauses to the solver.]
1206 
1207  Description []
1208 
1209  SideEffects []
1210 
1211  SeeAlso []
1212 
1213 ***********************************************************************/
1214 void 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 
1297 /**Function*************************************************************
1298 
1299  Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]
1300 
1301  Description []
1302 
1303  SideEffects []
1304 
1305  SeeAlso []
1306 
1307 ***********************************************************************/
1308 void 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 
1325 /**Function*************************************************************
1326 
1327  Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]
1328 
1329  Description []
1330 
1331  SideEffects []
1332 
1333  SeeAlso []
1334 
1335 ***********************************************************************/
1336 /*
1337 void 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 
1352 printf( "%d(%d)", vFanins->nSize, nCubes );
1353  Fraig_NodeVecFree( vFanins );
1354  Fraig_NodeVecFree( vInside );
1355 }
1356 */
1357 
1358 
1359 
1360 /**Function*************************************************************
1361 
1362  Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]
1363 
1364  Description []
1365 
1366  SideEffects []
1367 
1368  SeeAlso []
1369 
1370 ***********************************************************************/
1371 void 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 
1390 /**Function*************************************************************
1391 
1392  Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]
1393 
1394  Description []
1395 
1396  SideEffects []
1397 
1398  SeeAlso []
1399 
1400 ***********************************************************************/
1401 void 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 
1417 printf( "%d(%d)", vFanins->nSize, nCubes );
1418  Fraig_NodeVecFree( vFanins );
1419  Fraig_NodeVecFree( vInside );
1420 }
1421 
1422 
1423 
1424 /**Function*************************************************************
1425 
1426  Synopsis [Collect variables using their proximity from the nodes.]
1427 
1428  Description [This procedure creates a variable order based on collecting
1429  first the nodes that are the closest to the given two target nodes.]
1430 
1431  SideEffects []
1432 
1433  SeeAlso []
1434 
1435 ***********************************************************************/
1436 void 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 
1457 ////////////////////////////////////////////////////////////////////////
1458 /// END OF FILE ///
1459 ////////////////////////////////////////////////////////////////////////
1460 
1461 
1462 ABC_NAMESPACE_IMPL_END
1463 
Fraig_ManAllocCounterExample
int * Fraig_ManAllocCounterExample(Fraig_Man_t *p)
Definition: fraigFeed.c:787
Fraig_CollectSupergate
Fraig_NodeVec_t * Fraig_CollectSupergate(Fraig_Node_t *pNode, int fStopAtMux)
Definition: fraigUtil.c:960
Fraig_ManCheckClauseUsingSat
int Fraig_ManCheckClauseUsingSat(Fraig_Man_t *p, Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int nBTLimit)
Definition: fraigSat.c:653
Fraig_SupergateAddClausesMux
static void Fraig_SupergateAddClausesMux(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition: fraigSat.c:1214
Fraig_NodeStruct_t_::TravId
int TravId
Definition: fraigInt.h:214
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_Man_t
typedefABC_NAMESPACE_HEADER_START struct Fraig_ManStruct_t_ Fraig_Man_t
INCLUDES ///.
Definition: fraig.h:40
Fraig_ManCheckMiter
int Fraig_ManCheckMiter(Fraig_Man_t *p)
Definition: fraigSat.c:130
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Msat_SolverReadModelArray
int * Msat_SolverReadModelArray(Msat_Solver_t *p)
Definition: msatSolverApi.c:57
Msat_SolverAddClause
int Msat_SolverAddClause(Msat_Solver_t *p, Msat_IntVec_t *pLits)
Definition: msatSolverCore.c:65
nMuxes
static int nMuxes
Definition: fraigSat.c:48
Msat_ClauseVecReadEntry
Msat_Clause_t * Msat_ClauseVecReadEntry(Msat_ClauseVec_t *p, int i)
Definition: msatClauseVec.c:225
Fraig_NodeComparePhase
int Fraig_NodeComparePhase(Fraig_Node_t *p1, Fraig_Node_t *p2)
Definition: fraigApi.c:154
Fraig_SupergateAddClausesExor
static void Fraig_SupergateAddClausesExor(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition: fraigSat.c:1163
Fraig_CompareSimInfo
int Fraig_CompareSimInfo(Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int iWordLast, int fUseRand)
Definition: fraigTable.c:351
Msat_IntVec_t_
Definition: msatInt.h:162
Msat_IntVecClear
void Msat_IntVecClear(Msat_IntVec_t *p)
Definition: msatVec.c:335
Fraig_NodeVecPushUnique
int Fraig_NodeVecPushUnique(Fraig_NodeVec_t *p, Fraig_Node_t *Entry)
Definition: fraigVec.c:212
MSAT_TRUE
Definition: msat.h:50
Msat_SolverReadFactors
float * Msat_SolverReadFactors(Msat_Solver_t *p)
Definition: msatSolverApi.c:70
Fraig_NodeStruct_t_::fClauses
unsigned fClauses
Definition: fraigInt.h:220
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Fraig_NodeStruct_t_::p2
Fraig_Node_t * p2
Definition: fraigInt.h:233
Fraig_ManProveMiter
void Fraig_ManProveMiter(Fraig_Man_t *p)
Definition: fraigSat.c:85
Fraig_SetupAdjacentMark
static void Fraig_SetupAdjacentMark(Fraig_Man_t *pMan, Msat_IntVec_t *vConeVars)
Definition: fraigSat.c:1034
Fraig_CountPis
int Fraig_CountPis(Fraig_Man_t *p, Msat_IntVec_t *vVarNums)
Definition: fraigUtil.c:817
Fraig_NodeStruct_t_::nRefs
int nRefs
Definition: fraigInt.h:213
Fraig_PrepareCones_rec
static void Fraig_PrepareCones_rec(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition: fraigSat.c:793
Msat_SolverAddVar
int Msat_SolverAddVar(Msat_Solver_t *p, int Level)
DECLARATIONS ///.
Definition: msatSolverCore.c:45
Fraig_SupergateAddClauses
static void Fraig_SupergateAddClauses(Fraig_Man_t *pMan, Fraig_Node_t *pNode, Fraig_NodeVec_t *vSuper)
Definition: fraigSat.c:1104
Fraig_NodeRecognizeMux
Fraig_Node_t * Fraig_NodeRecognizeMux(Fraig_Node_t *pNode, Fraig_Node_t **ppNodeT, Fraig_Node_t **ppNodeE)
Definition: fraigUtil.c:658
Fraig_MarkTfi3_rec
int Fraig_MarkTfi3_rec(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition: fraigSat.c:229
Fraig_NodeStruct_t_::NumPi
int NumPi
Definition: fraigInt.h:211
Fraig_Not
#define Fraig_Not(p)
Definition: fraig.h:109
Msat_IntVecReadSize
int Msat_IntVecReadSize(Msat_IntVec_t *p)
Definition: msatVec.c:233
Msat_IntVecPush
void Msat_IntVecPush(Msat_IntVec_t *p, int Entry)
Definition: msatVec.c:351
Fraig_SetupAdjacent
static void Fraig_SetupAdjacent(Fraig_Man_t *pMan, Msat_IntVec_t *vConeVars)
Definition: fraigSat.c:974
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_NodeVecFree
void Fraig_NodeVecFree(Fraig_NodeVec_t *p)
Definition: fraigVec.c:66
Fraig_NodeVecAlloc
Fraig_NodeVec_t * Fraig_NodeVecAlloc(int nCap)
DECLARATIONS ///.
Definition: fraigVec.c:43
Fraig_NodeIsExor
int Fraig_NodeIsExor(Fraig_Node_t *pNode)
Definition: fraigUtil.c:633
Fraig_NodeStruct_t_
Definition: fraigInt.h:207
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
Msat_IntVecFill
void Msat_IntVecFill(Msat_IntVec_t *p, int nSize, int Entry)
Definition: msatVec.c:177
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Fraig_NodeStruct_t_::p1
Fraig_Node_t * p1
Definition: fraigInt.h:232
Fraig_DetectFanoutFreeConeMux
static void Fraig_DetectFanoutFreeConeMux(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition: fraigSat.c:1401
Msat_SolverPrepare
void Msat_SolverPrepare(Msat_Solver_t *pSat, Msat_IntVec_t *vVars)
Definition: msatSolverApi.c:451
Msat_IntVecReadEntry
int Msat_IntVecReadEntry(Msat_IntVec_t *p, int i)
Definition: msatVec.c:249
Fraig_NodeIsAnd
int Fraig_NodeIsAnd(Fraig_Node_t *p)
Definition: fraigApi.c:153
Fraig_SetActivity
static void Fraig_SetActivity(Fraig_Man_t *pMan, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
Definition: fraigSat.c:1436
Fraig_PrepareCones
static void Fraig_PrepareCones(Fraig_Man_t *pMan, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
Definition: fraigSat.c:746
Fraig_ManCreateSolver
void Fraig_ManCreateSolver(Fraig_Man_t *p)
Definition: fraigMan.c:325
Fraig_NodeIsImplication
int Fraig_NodeIsImplication(Fraig_Man_t *p, Fraig_Node_t *pOld, Fraig_Node_t *pNew, int nBTLimit)
Definition: fraigSat.c:551
Fraig_ManSaveCounterExample
int * Fraig_ManSaveCounterExample(Fraig_Man_t *p, Fraig_Node_t *pNode)
Definition: fraigFeed.c:860
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_IsComplement
#define Fraig_IsComplement(p)
GLOBAL VARIABLES ///.
Definition: fraig.h:107
Fraig_MarkTfi2_rec
int Fraig_MarkTfi2_rec(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition: fraigSat.c:198
Fraig_MarkTfi_rec
int Fraig_MarkTfi_rec(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition: fraigSat.c:173
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Fraig_NodeStruct_t_::Num
int Num
Definition: fraigInt.h:210
Fraig_NodeIsMuxType
int Fraig_NodeIsMuxType(Fraig_Node_t *pNode)
Definition: fraigUtil.c:591
Fraig_NodeStruct_t_::fFailTfo
unsigned fFailTfo
Definition: fraigInt.h:227
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Fraig_NodeVecStruct_t_::pArray
Fraig_Node_t ** pArray
Definition: fraigInt.h:267
Fraig_Regular
#define Fraig_Regular(p)
Definition: fraig.h:108
Fraig_NodeStruct_t_::Level
int Level
Definition: fraigInt.h:212
Msat_SolverReadVarNum
int Msat_SolverReadVarNum(Msat_Solver_t *p)
FUNCTION DEFINITIONS ///.
Definition: msatSolverApi.c:47
Msat_IntVecReadArray
int * Msat_IntVecReadArray(Msat_IntVec_t *p)
Definition: msatVec.c:217
Minisat::Var
int Var
Definition: SolverTypes.h:42
MSAT_VAR2LIT
#define MSAT_VAR2LIT(v, s)
Definition: msat.h:56
Fraig_NodeIsVar
int Fraig_NodeIsVar(Fraig_Node_t *p)
Definition: fraigApi.c:152
Fraig_VarsStudy
void Fraig_VarsStudy(Fraig_Man_t *p, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
Definition: fraigSat.c:260
Msat_IntVecWriteEntry
void Msat_IntVecWriteEntry(Msat_IntVec_t *p, int i, int Entry)
Definition: msatVec.c:266
assert
#define assert(ex)
Definition: util_old.h:213
Fraig_OrderVariables
static ABC_NAMESPACE_IMPL_START void Fraig_OrderVariables(Fraig_Man_t *pMan, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
DECLARATIONS ///.
Definition: fraigSat.c:875
Fraig_NodeVecStruct_t_::nSize
int nSize
Definition: fraigInt.h:266
Fraig_NodeStruct_t_::fMark2
unsigned fMark2
Definition: fraigInt.h:223
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
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Fraig_NodeStruct_t_::vFanins
Fraig_NodeVec_t * vFanins
Definition: fraigInt.h:234
Fraig_NodeIsExorType
int Fraig_NodeIsExorType(Fraig_Node_t *pNode)
Definition: fraigUtil.c:558
Msat_SolverSolve
int Msat_SolverSolve(Msat_Solver_t *p, Msat_IntVec_t *pVecAssumps, int nBackTrackLimit, int nTimeLimit)
Definition: msatSolverCore.c:138
Fraig_NodeVecStruct_t_
Definition: fraigInt.h:263