ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
bbr.h
Go to the documentation of this file.
1
20
21#ifndef ABC__aig__bbr__bbr_h
22#define ABC__aig__bbr__bbr_h
23
24
28
29#include <stdio.h>
30#include "aig/aig/aig.h"
31#include "aig/saig/saig.h"
32#include "bdd/cudd/cuddInt.h"
33
37
38
39
41
42
46
50
51static inline DdNode * Aig_ObjGlobalBdd( Aig_Obj_t * pObj ) { return (DdNode *)pObj->pData; }
52
56
57/*=== bbrImage.c ==========================================================*/
60 DdManager * dd, DdNode * bCare,
61 int nParts, DdNode ** pbParts,
62 int nVars, DdNode ** pbVars, int nBddMax, int fVerbose );
63extern DdNode * Bbr_bddImageCompute( Bbr_ImageTree_t * pTree, DdNode * bCare );
64extern void Bbr_bddImageTreeDelete( Bbr_ImageTree_t * pTree );
65extern DdNode * Bbr_bddImageRead( Bbr_ImageTree_t * pTree );
68 DdManager * dd, DdNode * bCare,
69 int nParts, DdNode ** pbParts,
70 int nVars, DdNode ** pbVars, int fVerbose );
71extern DdNode * Bbr_bddImageCompute2( Bbr_ImageTree2_t * pTree, DdNode * bCare );
72extern void Bbr_bddImageTreeDelete2( Bbr_ImageTree2_t * pTree );
73extern DdNode * Bbr_bddImageRead2( Bbr_ImageTree2_t * pTree );
74/*=== bbrNtbdd.c ==========================================================*/
75extern void Aig_ManFreeGlobalBdds( Aig_Man_t * p, DdManager * dd );
76extern int Aig_ManSizeOfGlobalBdds( Aig_Man_t * p );
77extern DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose );
78/*=== bbrReach.c ==========================================================*/
79extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, Saig_ParBbr_t * pPars );
81
82
83
85
86
87
88#endif
89
93
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_HEADER_START
NAMESPACES ///.
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
void Bbr_bddImageTreeDelete(Bbr_ImageTree_t *pTree)
Definition bbrImage.c:307
DdNode * Bbr_bddImageCompute2(Bbr_ImageTree2_t *pTree, DdNode *bCare)
Definition bbrImage.c:1273
int Aig_ManVerifyUsingBdds(Aig_Man_t *p, Saig_ParBbr_t *pPars)
Definition saigDup.c:592
void Bbr_bddImageTreeDelete2(Bbr_ImageTree2_t *pTree)
Definition bbrImage.c:1293
DdNode * Bbr_bddImageRead2(Bbr_ImageTree2_t *pTree)
Definition bbrImage.c:1315
struct Bbr_ImageTree2_t_ Bbr_ImageTree2_t
Definition bbr.h:66
Bbr_ImageTree_t * Bbr_bddImageStart(DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int nBddMax, int fVerbose)
Definition bbrImage.c:168
DdNode * Bbr_bddImageCompute(Bbr_ImageTree_t *pTree, DdNode *bCare)
Definition bbrImage.c:253
DdNode * Bbr_bddImageRead(Bbr_ImageTree_t *pTree)
Definition bbrImage.c:326
void Bbr_ManSetDefaultParams(Saig_ParBbr_t *p)
FUNCTION DEFINITIONS ///.
Definition saigDup.c:593
DdManager * Aig_ManComputeGlobalBdds(Aig_Man_t *p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose)
Definition bbrNtbdd.c:157
struct Bbr_ImageTree_t_ Bbr_ImageTree_t
FUNCTION DECLARATIONS ///.
Definition bbr.h:58
Bbr_ImageTree2_t * Bbr_bddImageStart2(DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int fVerbose)
Definition bbrImage.c:1231
int Aig_ManSizeOfGlobalBdds(Aig_Man_t *p)
Definition bbrNtbdd.c:132
void Aig_ManFreeGlobalBdds(Aig_Man_t *p, DdManager *dd)
Definition bbrNtbdd.c:112
Cube * p
Definition exorList.c:222
struct Saig_ParBbr_t_ Saig_ParBbr_t
Definition saig.h:53
void * pData
Definition aig.h:87
DdManager * dd
Definition bbrImage.c:1214