diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-08-08 09:43:57 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-08-08 09:43:57 -0700 |
| commit | a8e59b2c421c7b3a565ccb587d57fdc09500dcdf (patch) | |
| tree | 6b556dbf566f746082430e630db6488e8f0627f6 /src/aig/gia/gia.h | |
| parent | 8daf610ebaf3d0c83166433897a64c5ab56080a9 (diff) | |
| download | abc-a8e59b2c421c7b3a565ccb587d57fdc09500dcdf.tar.gz abc-a8e59b2c421c7b3a565ccb587d57fdc09500dcdf.tar.bz2 abc-a8e59b2c421c7b3a565ccb587d57fdc09500dcdf.zip | |
Added generation of values of internal nodes for GIA manager.
Diffstat (limited to 'src/aig/gia/gia.h')
| -rw-r--r-- | src/aig/gia/gia.h | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 2d7a0695..3a22f8f4 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -154,6 +154,7 @@ struct Gia_Man_t_ void * pLutLib; // LUT library word nHashHit; // hash table hit word nHashMiss; // hash table miss + unsigned * pData2; // storage for object values int fVerbose; // verbose reports // truth table computation for small functions int nTtVars; // truth table variables @@ -740,6 +741,12 @@ extern void Gia_WriteAigerSimple( Gia_Man_t * pInit, char * pFile /*=== giaBidec.c ===========================================================*/ extern unsigned * Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited ); extern Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose ); +/*=== giaCex.c ============================================================*/ +extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ); +extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ); +extern void Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex ); +extern void Gia_ManCounterExampleValueStop( Gia_Man_t * pGia ); +extern int Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, int Id, int iFrame ); /*=== giaCsatOld.c ============================================================*/ extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); /*=== giaCsat.c ============================================================*/ @@ -959,8 +966,6 @@ extern int Gia_ManHasDangling( Gia_Man_t * p ); extern int Gia_ManMarkDangling( Gia_Man_t * p ); extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p ); extern void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj ); -extern int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ); -extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ); extern void Gia_ManInvertConstraints( Gia_Man_t * pAig ); extern void Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj ); extern unsigned * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj ); |