abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
decFactor.c File Reference
#include "base/abc/abc.h"
#include "base/main/main.h"
#include "misc/mvc/mvc.h"
#include "misc/extra/extraBdd.h"
#include "dec.h"

Go to the source code of this file.

Functions

static
ABC_NAMESPACE_IMPL_START
Dec_Edge_t 
Dec_Factor_rec (Dec_Graph_t *pFForm, Mvc_Cover_t *pCover)
 DECLARATIONS ///. More...
 
static Dec_Edge_t Dec_FactorLF_rec (Dec_Graph_t *pFForm, Mvc_Cover_t *pCover, Mvc_Cover_t *pSimple)
 
static Dec_Edge_t Dec_FactorTrivial (Dec_Graph_t *pFForm, Mvc_Cover_t *pCover)
 
static Dec_Edge_t Dec_FactorTrivialCube (Dec_Graph_t *pFForm, Mvc_Cover_t *pCover, Mvc_Cube_t *pCube, Vec_Int_t *vEdgeLits)
 
static Dec_Edge_t Dec_FactorTrivialTree_rec (Dec_Graph_t *pFForm, Dec_Edge_t *peNodes, int nNodes, int fNodeOr)
 
static int Dec_FactorVerify (char *pSop, Dec_Graph_t *pFForm)
 
static Mvc_Cover_tDec_ConvertSopToMvc (char *pSop)
 
Dec_Graph_tDec_Factor (char *pSop)
 FUNCTION DEFINITIONS ///. More...
 

Function Documentation

Mvc_Cover_t * Dec_ConvertSopToMvc ( char *  pSop)
static

Function*************************************************************

Synopsis [Converts SOP into MVC.]

Description []

SideEffects []

SeeAlso []

Definition at line 326 of file decFactor.c.

327 {
328  Dec_Man_t * pManDec = (Dec_Man_t *)Abc_FrameReadManDec();
329  Mvc_Manager_t * pMem = (Mvc_Manager_t *)pManDec->pMvcMem;
330  Mvc_Cover_t * pMvc;
331  Mvc_Cube_t * pMvcCube;
332  char * pCube;
333  int nVars, Value, v;
334 
335  // start the cover
336  nVars = Abc_SopGetVarNum(pSop);
337  pMvc = Mvc_CoverAlloc( pMem, nVars * 2 );
338  // check the logic function of the node
339  Abc_SopForEachCube( pSop, nVars, pCube )
340  {
341  // create and add the cube
342  pMvcCube = Mvc_CubeAlloc( pMvc );
343  Mvc_CoverAddCubeTail( pMvc, pMvcCube );
344  // fill in the literals
345  Mvc_CubeBitFill( pMvcCube );
346  Abc_CubeForEachVar( pCube, Value, v )
347  {
348  if ( Value == '0' )
349  Mvc_CubeBitRemove( pMvcCube, v * 2 + 1 );
350  else if ( Value == '1' )
351  Mvc_CubeBitRemove( pMvcCube, v * 2 );
352  }
353  }
354  return pMvc;
355 }
#define Mvc_CoverAddCubeTail(pCover, pCube)
Definition: mvc.h:501
void * pMvcMem
Definition: dec.h:82
#define Abc_SopForEachCube(pSop, nFanins, pCube)
Definition: abc.h:531
#define Abc_CubeForEachVar(pCube, Value, i)
Definition: abc.h:529
ABC_DLL void * Abc_FrameReadManDec()
Definition: mainFrame.c:61
Mvc_Cube_t * Mvc_CubeAlloc(Mvc_Cover_t *pCover)
DECLARATIONS ///.
Definition: mvcCube.c:43
#define Mvc_CubeBitRemove(Cube, Bit)
Definition: mvc.h:140
#define Mvc_CubeBitFill(Cube)
Definition: mvc.h:385
ABC_DLL int Abc_SopGetVarNum(char *pSop)
Definition: abcSop.c:536
Definition: dec.h:80
Mvc_Cover_t * Mvc_CoverAlloc(Mvc_Manager_t *pMem, int nBits)
DECLARATIONS ///.
Definition: mvcCover.c:43
Dec_Graph_t* Dec_Factor ( char *  pSop)

FUNCTION DEFINITIONS ///.

FUNCTION DECLARATIONS ///.

Function*************************************************************

Synopsis [Factors the cover.]

Description []

SideEffects []

SeeAlso []

Definition at line 55 of file decFactor.c.

56 {
57  Mvc_Cover_t * pCover;
58  Dec_Graph_t * pFForm;
59  Dec_Edge_t eRoot;
60 
61  // derive the cover from the SOP representation
62  pCover = Dec_ConvertSopToMvc( pSop );
63 
64  // make sure the cover is CCS free (should be done before CST)
65  Mvc_CoverContain( pCover );
66  // check for trivial functions
67  if ( Mvc_CoverIsEmpty(pCover) )
68  {
69  Mvc_CoverFree( pCover );
70  return Dec_GraphCreateConst0();
71  }
72  if ( Mvc_CoverIsTautology(pCover) )
73  {
74  Mvc_CoverFree( pCover );
75  return Dec_GraphCreateConst1();
76  }
77 
78  // perform CST
79  Mvc_CoverInverse( pCover ); // CST
80  // start the factored form
81  pFForm = Dec_GraphCreate( Abc_SopGetVarNum(pSop) );
82  // factor the cover
83  eRoot = Dec_Factor_rec( pFForm, pCover );
84  // finalize the factored form
85  Dec_GraphSetRoot( pFForm, eRoot );
86  // complement the factored form if SOP is complemented
87  if ( Abc_SopIsComplement(pSop) )
88  Dec_GraphComplement( pFForm );
89  // verify the factored form
90 // if ( !Dec_FactorVerify( pSop, pFForm ) )
91 // printf( "Verification has failed.\n" );
92 // Mvc_CoverInverse( pCover ); // undo CST
93  Mvc_CoverFree( pCover );
94  return pFForm;
95 }
int Mvc_CoverContain(Mvc_Cover_t *pCover)
FUNCTION DEFINITIONS ///.
Definition: mvcContain.c:47
void Mvc_CoverFree(Mvc_Cover_t *pCover)
Definition: mvcCover.c:138
static ABC_NAMESPACE_IMPL_START Dec_Edge_t Dec_Factor_rec(Dec_Graph_t *pFForm, Mvc_Cover_t *pCover)
DECLARATIONS ///.
Definition: decFactor.c:108
static Mvc_Cover_t * Dec_ConvertSopToMvc(char *pSop)
Definition: decFactor.c:326
typedefABC_NAMESPACE_HEADER_START struct Dec_Edge_t_ Dec_Edge_t
INCLUDES ///.
Definition: dec.h:42
static Dec_Graph_t * Dec_GraphCreateConst1()
Definition: dec.h:266
void Mvc_CoverInverse(Mvc_Cover_t *pCover)
Definition: mvcUtils.c:477
int Mvc_CoverIsTautology(Mvc_Cover_t *pCover)
Definition: mvcApi.c:109
static Dec_Graph_t * Dec_GraphCreateConst0()
Definition: dec.h:245
static void Dec_GraphSetRoot(Dec_Graph_t *pGraph, Dec_Edge_t eRoot)
Definition: dec.h:551
static Dec_Graph_t * Dec_GraphCreate(int nLeaves)
Definition: dec.h:221
ABC_DLL int Abc_SopGetVarNum(char *pSop)
Definition: abcSop.c:536
ABC_DLL int Abc_SopIsComplement(char *pSop)
Definition: abcSop.c:655
int Mvc_CoverIsEmpty(Mvc_Cover_t *pCover)
Definition: mvcApi.c:93
static void Dec_GraphComplement(Dec_Graph_t *pGraph)
Definition: dec.h:388
Dec_Edge_t Dec_Factor_rec ( Dec_Graph_t pFForm,
Mvc_Cover_t pCover 
)
static

DECLARATIONS ///.

CFile****************************************************************

FileName [ftFactor.c]

PackageName [MVSIS 2.0: Multi-valued logic synthesis system.]

Synopsis [Procedures for algebraic factoring.]

Author [MVSIS Group]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - February 1, 2003.]

Revision [

Id:
ftFactor.c,v 1.3 2003/09/01 04:56:43 alanmi Exp

]

Function*************************************************************

Synopsis [Internal recursive factoring procedure.]

Description []

SideEffects []

SeeAlso []

Definition at line 108 of file decFactor.c.

109 {
110  Mvc_Cover_t * pDiv, * pQuo, * pRem, * pCom;
111  Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
112  Dec_Edge_t eNodeAnd, eNode;
113 
114  // make sure the cover contains some cubes
115  assert( Mvc_CoverReadCubeNum(pCover) );
116 
117  // get the divisor
118  pDiv = Mvc_CoverDivisor( pCover );
119  if ( pDiv == NULL )
120  return Dec_FactorTrivial( pFForm, pCover );
121 
122  // divide the cover by the divisor
123  Mvc_CoverDivideInternal( pCover, pDiv, &pQuo, &pRem );
124  assert( Mvc_CoverReadCubeNum(pQuo) );
125 
126  Mvc_CoverFree( pDiv );
127  Mvc_CoverFree( pRem );
128 
129  // check the trivial case
130  if ( Mvc_CoverReadCubeNum(pQuo) == 1 )
131  {
132  eNode = Dec_FactorLF_rec( pFForm, pCover, pQuo );
133  Mvc_CoverFree( pQuo );
134  return eNode;
135  }
136 
137  // make the quotient cube ABC_FREE
138  Mvc_CoverMakeCubeFree( pQuo );
139 
140  // divide the cover by the quotient
141  Mvc_CoverDivideInternal( pCover, pQuo, &pDiv, &pRem );
142 
143  // check the trivial case
144  if ( Mvc_CoverIsCubeFree( pDiv ) )
145  {
146  eNodeDiv = Dec_Factor_rec( pFForm, pDiv );
147  eNodeQuo = Dec_Factor_rec( pFForm, pQuo );
148  Mvc_CoverFree( pDiv );
149  Mvc_CoverFree( pQuo );
150  eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
151  if ( Mvc_CoverReadCubeNum(pRem) == 0 )
152  {
153  Mvc_CoverFree( pRem );
154  return eNodeAnd;
155  }
156  else
157  {
158  eNodeRem = Dec_Factor_rec( pFForm, pRem );
159  Mvc_CoverFree( pRem );
160  return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
161  }
162  }
163 
164  // get the common cube
165  pCom = Mvc_CoverCommonCubeCover( pDiv );
166  Mvc_CoverFree( pDiv );
167  Mvc_CoverFree( pQuo );
168  Mvc_CoverFree( pRem );
169 
170  // solve the simple problem
171  eNode = Dec_FactorLF_rec( pFForm, pCover, pCom );
172  Mvc_CoverFree( pCom );
173  return eNode;
174 }
void Mvc_CoverFree(Mvc_Cover_t *pCover)
Definition: mvcCover.c:138
static ABC_NAMESPACE_IMPL_START Dec_Edge_t Dec_Factor_rec(Dec_Graph_t *pFForm, Mvc_Cover_t *pCover)
DECLARATIONS ///.
Definition: decFactor.c:108
Mvc_Cover_t * Mvc_CoverCommonCubeCover(Mvc_Cover_t *pCover)
Definition: mvcUtils.c:220
void Mvc_CoverDivideInternal(Mvc_Cover_t *pCover, Mvc_Cover_t *pDiv, Mvc_Cover_t **ppQuo, Mvc_Cover_t **ppRem)
Definition: mvcDivide.c:81
typedefABC_NAMESPACE_HEADER_START struct Dec_Edge_t_ Dec_Edge_t
INCLUDES ///.
Definition: dec.h:42
void Mvc_CoverMakeCubeFree(Mvc_Cover_t *pCover)
Definition: mvcUtils.c:198
static Dec_Edge_t Dec_GraphAddNodeAnd(Dec_Graph_t *pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1)
Definition: dec.h:591
int Mvc_CoverReadCubeNum(Mvc_Cover_t *pCover)
Definition: mvcApi.c:45
static Dec_Edge_t Dec_GraphAddNodeOr(Dec_Graph_t *pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1)
Definition: dec.h:615
static Dec_Edge_t Dec_FactorTrivial(Dec_Graph_t *pFForm, Mvc_Cover_t *pCover)
Definition: decFactor.c:233
int Mvc_CoverIsCubeFree(Mvc_Cover_t *pCover)
Definition: mvcUtils.c:176
static Dec_Edge_t Dec_FactorLF_rec(Dec_Graph_t *pFForm, Mvc_Cover_t *pCover, Mvc_Cover_t *pSimple)
Definition: decFactor.c:188
#define assert(ex)
Definition: util_old.h:213
Mvc_Cover_t * Mvc_CoverDivisor(Mvc_Cover_t *pCover)
FUNCTION DEFINITIONS ///.
Definition: mvcDivisor.c:46
Dec_Edge_t Dec_FactorLF_rec ( Dec_Graph_t pFForm,
Mvc_Cover_t pCover,
Mvc_Cover_t pSimple 
)
static

Function*************************************************************

Synopsis [Internal recursive factoring procedure for the leaf case.]

Description []

SideEffects []

SeeAlso []

Definition at line 188 of file decFactor.c.

189 {
190  Dec_Man_t * pManDec = (Dec_Man_t *)Abc_FrameReadManDec();
191  Vec_Int_t * vEdgeLits = pManDec->vLits;
192  Mvc_Cover_t * pDiv, * pQuo, * pRem;
193  Dec_Edge_t eNodeDiv, eNodeQuo, eNodeRem;
194  Dec_Edge_t eNodeAnd;
195 
196  // get the most often occurring literal
197  pDiv = Mvc_CoverBestLiteralCover( pCover, pSimple );
198  // divide the cover by the literal
199  Mvc_CoverDivideByLiteral( pCover, pDiv, &pQuo, &pRem );
200  // get the node pointer for the literal
201  eNodeDiv = Dec_FactorTrivialCube( pFForm, pDiv, Mvc_CoverReadCubeHead(pDiv), vEdgeLits );
202  Mvc_CoverFree( pDiv );
203  // factor the quotient and remainder
204  eNodeQuo = Dec_Factor_rec( pFForm, pQuo );
205  Mvc_CoverFree( pQuo );
206  eNodeAnd = Dec_GraphAddNodeAnd( pFForm, eNodeDiv, eNodeQuo );
207  if ( Mvc_CoverReadCubeNum(pRem) == 0 )
208  {
209  Mvc_CoverFree( pRem );
210  return eNodeAnd;
211  }
212  else
213  {
214  eNodeRem = Dec_Factor_rec( pFForm, pRem );
215  Mvc_CoverFree( pRem );
216  return Dec_GraphAddNodeOr( pFForm, eNodeAnd, eNodeRem );
217  }
218 }
void Mvc_CoverFree(Mvc_Cover_t *pCover)
Definition: mvcCover.c:138
static ABC_NAMESPACE_IMPL_START Dec_Edge_t Dec_Factor_rec(Dec_Graph_t *pFForm, Mvc_Cover_t *pCover)
DECLARATIONS ///.
Definition: decFactor.c:108
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static Dec_Edge_t Dec_FactorTrivialCube(Dec_Graph_t *pFForm, Mvc_Cover_t *pCover, Mvc_Cube_t *pCube, Vec_Int_t *vEdgeLits)
Definition: decFactor.c:262
typedefABC_NAMESPACE_HEADER_START struct Dec_Edge_t_ Dec_Edge_t
INCLUDES ///.
Definition: dec.h:42
static Dec_Edge_t Dec_GraphAddNodeAnd(Dec_Graph_t *pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1)
Definition: dec.h:591
ABC_DLL void * Abc_FrameReadManDec()
Definition: mainFrame.c:61
int Mvc_CoverReadCubeNum(Mvc_Cover_t *pCover)
Definition: mvcApi.c:45
Vec_Int_t * vLits
Definition: dec.h:84
static Dec_Edge_t Dec_GraphAddNodeOr(Dec_Graph_t *pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1)
Definition: dec.h:615
Mvc_Cover_t * Mvc_CoverBestLiteralCover(Mvc_Cover_t *pCover, Mvc_Cover_t *pSimple)
Definition: mvcLits.c:223
void Mvc_CoverDivideByLiteral(Mvc_Cover_t *pCover, Mvc_Cover_t *pDiv, Mvc_Cover_t **ppQuo, Mvc_Cover_t **ppRem)
Definition: mvcDivide.c:323
Definition: dec.h:80
Mvc_Cube_t * Mvc_CoverReadCubeHead(Mvc_Cover_t *pCover)
Definition: mvcApi.c:46
Dec_Edge_t Dec_FactorTrivial ( Dec_Graph_t pFForm,
Mvc_Cover_t pCover 
)
static

Function*************************************************************

Synopsis [Factoring the cover, which has no algebraic divisors.]

Description []

SideEffects []

SeeAlso []

Definition at line 233 of file decFactor.c.

234 {
235  Dec_Man_t * pManDec = (Dec_Man_t *)Abc_FrameReadManDec();
236  Vec_Int_t * vEdgeCubes = pManDec->vCubes;
237  Vec_Int_t * vEdgeLits = pManDec->vLits;
238  Dec_Edge_t eNode;
239  Mvc_Cube_t * pCube;
240  // create the factored form for each cube
241  Vec_IntClear( vEdgeCubes );
242  Mvc_CoverForEachCube( pCover, pCube )
243  {
244  eNode = Dec_FactorTrivialCube( pFForm, pCover, pCube, vEdgeLits );
245  Vec_IntPush( vEdgeCubes, Dec_EdgeToInt_(eNode) );
246  }
247  // balance the factored forms
248  return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeCubes->pArray, vEdgeCubes->nSize, 1 );
249 }
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_Int_t * vCubes
Definition: dec.h:83
static Dec_Edge_t Dec_FactorTrivialCube(Dec_Graph_t *pFForm, Mvc_Cover_t *pCover, Mvc_Cube_t *pCube, Vec_Int_t *vEdgeLits)
Definition: decFactor.c:262
typedefABC_NAMESPACE_HEADER_START struct Dec_Edge_t_ Dec_Edge_t
INCLUDES ///.
Definition: dec.h:42
int nSize
Definition: dec.h:73
ABC_DLL void * Abc_FrameReadManDec()
Definition: mainFrame.c:61
Vec_Int_t * vLits
Definition: dec.h:84
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
#define Mvc_CoverForEachCube(Cover, Cube)
Definition: mvc.h:528
static unsigned Dec_EdgeToInt_(Dec_Edge_t m)
Definition: dec.h:183
Definition: dec.h:80
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
static Dec_Edge_t Dec_FactorTrivialTree_rec(Dec_Graph_t *pFForm, Dec_Edge_t *peNodes, int nNodes, int fNodeOr)
Definition: decFactor.c:289
Dec_Edge_t Dec_FactorTrivialCube ( Dec_Graph_t pFForm,
Mvc_Cover_t pCover,
Mvc_Cube_t pCube,
Vec_Int_t vEdgeLits 
)
static

Function*************************************************************

Synopsis [Factoring the cube.]

Description []

SideEffects []

SeeAlso []

Definition at line 262 of file decFactor.c.

263 {
264  Dec_Edge_t eNode;
265  int iBit, Value;
266  // create the factored form for each literal
267  Vec_IntClear( vEdgeLits );
268  Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
269  if ( Value )
270  {
271  eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST
272  Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) );
273  }
274  // balance the factored forms
275  return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeLits->pArray, vEdgeLits->nSize, 0 );
276 }
static Dec_Edge_t Dec_EdgeCreate(int Node, int fCompl)
FUNCTION DEFINITIONS ///.
Definition: dec.h:134
typedefABC_NAMESPACE_HEADER_START struct Dec_Edge_t_ Dec_Edge_t
INCLUDES ///.
Definition: dec.h:42
int nSize
Definition: dec.h:73
if(last==0)
Definition: sparse_int.h:34
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
#define Mvc_CubeForEachBit(Cover, Cube, iBit, Value)
Definition: mvc.h:553
static unsigned Dec_EdgeToInt_(Dec_Edge_t m)
Definition: dec.h:183
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
static Dec_Edge_t Dec_FactorTrivialTree_rec(Dec_Graph_t *pFForm, Dec_Edge_t *peNodes, int nNodes, int fNodeOr)
Definition: decFactor.c:289
Dec_Edge_t Dec_FactorTrivialTree_rec ( Dec_Graph_t pFForm,
Dec_Edge_t peNodes,
int  nNodes,
int  fNodeOr 
)
static

Function*************************************************************

Synopsis [Create the well-balanced tree of nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 289 of file decFactor.c.

290 {
291  Dec_Edge_t eNode1, eNode2;
292  int nNodes1, nNodes2;
293 
294  if ( nNodes == 1 )
295  return peNodes[0];
296 
297  // split the nodes into two parts
298  nNodes1 = nNodes/2;
299  nNodes2 = nNodes - nNodes1;
300 // nNodes2 = nNodes/2;
301 // nNodes1 = nNodes - nNodes2;
302 
303  // recursively construct the tree for the parts
304  eNode1 = Dec_FactorTrivialTree_rec( pFForm, peNodes, nNodes1, fNodeOr );
305  eNode2 = Dec_FactorTrivialTree_rec( pFForm, peNodes + nNodes1, nNodes2, fNodeOr );
306 
307  if ( fNodeOr )
308  return Dec_GraphAddNodeOr( pFForm, eNode1, eNode2 );
309  else
310  return Dec_GraphAddNodeAnd( pFForm, eNode1, eNode2 );
311 }
typedefABC_NAMESPACE_HEADER_START struct Dec_Edge_t_ Dec_Edge_t
INCLUDES ///.
Definition: dec.h:42
static Dec_Edge_t Dec_GraphAddNodeAnd(Dec_Graph_t *pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1)
Definition: dec.h:591
static Dec_Edge_t Dec_GraphAddNodeOr(Dec_Graph_t *pGraph, Dec_Edge_t eEdge0, Dec_Edge_t eEdge1)
Definition: dec.h:615
static Dec_Edge_t Dec_FactorTrivialTree_rec(Dec_Graph_t *pFForm, Dec_Edge_t *peNodes, int nNodes, int fNodeOr)
Definition: decFactor.c:289
int Dec_FactorVerify ( char *  pSop,
Dec_Graph_t pFForm 
)
static

Function*************************************************************

Synopsis [Verifies that the factoring is correct.]

Description []

SideEffects []

SeeAlso []

Definition at line 368 of file decFactor.c.

369 {
370  extern DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, DdNode ** pbVars );
371  extern DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph );
373  DdNode * bFunc1, * bFunc2;
374  int RetValue;
375  bFunc1 = Abc_ConvertSopToBdd( dd, pSop, NULL ); Cudd_Ref( bFunc1 );
376  bFunc2 = Dec_GraphDeriveBdd( dd, pFForm ); Cudd_Ref( bFunc2 );
377 //Extra_bddPrint( dd, bFunc1 ); printf("\n");
378 //Extra_bddPrint( dd, bFunc2 ); printf("\n");
379  RetValue = (bFunc1 == bFunc2);
380  if ( bFunc1 != bFunc2 )
381  {
382  int s;
383  Extra_bddPrint( dd, bFunc1 ); printf("\n");
384  Extra_bddPrint( dd, bFunc2 ); printf("\n");
385  s = 0;
386  }
387  Cudd_RecursiveDeref( dd, bFunc1 );
388  Cudd_RecursiveDeref( dd, bFunc2 );
389  return RetValue;
390 }
ABC_DLL void * Abc_FrameReadManDd()
Definition: mainFrame.c:60
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Definition: cudd.h:278
void Extra_bddPrint(DdManager *dd, DdNode *F)
Definition: extraBddMisc.c:246
DdNode * Abc_ConvertSopToBdd(DdManager *dd, char *pSop, DdNode **pbVars)
FUNCTION DEFINITIONS ///.
Definition: abcFunc.c:56
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
ABC_NAMESPACE_IMPL_START DdNode * Dec_GraphDeriveBdd(DdManager *dd, Dec_Graph_t *pGraph)
DECLARATIONS ///.
Definition: decUtil.c:45