summaryrefslogtreecommitdiffstats
path: root/src/proof/abs/absRef.h
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-09-16 09:54:19 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-09-16 09:54:19 -0700
commit5953beb2da3e9ee4bcc2fc03487cb8c8ef36877c (patch)
tree09fb7edbdbb0442bdeb2555503f0eba8963a4a16 /src/proof/abs/absRef.h
parent5a4f1fe44c94ee48e707246898db1ac2d66231e9 (diff)
downloadabc-5953beb2da3e9ee4bcc2fc03487cb8c8ef36877c.tar.gz
abc-5953beb2da3e9ee4bcc2fc03487cb8c8ef36877c.tar.bz2
abc-5953beb2da3e9ee4bcc2fc03487cb8c8ef36877c.zip
Restructured the code to post-process object used during refinement in &gla.
Diffstat (limited to 'src/proof/abs/absRef.h')
-rw-r--r--src/proof/abs/absRef.h74
1 files changed, 68 insertions, 6 deletions
diff --git a/src/proof/abs/absRef.h b/src/proof/abs/absRef.h
index ca46c776..9bae40a3 100644
--- a/src/proof/abs/absRef.h
+++ b/src/proof/abs/absRef.h
@@ -37,28 +37,90 @@ ABC_NAMESPACE_HEADER_START
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
-typedef struct Rnm_Man_t_ Rnm_Man_t; // refinement manager
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
+typedef struct Rnm_Obj_t_ Rnm_Obj_t; // refinement object
+struct Rnm_Obj_t_
+{
+ unsigned Value : 1; // binary value
+ unsigned fVisit : 1; // visited object
+ unsigned fVisitJ : 1; // justified visited object
+ unsigned fPPi : 1; // PPI object
+ unsigned Prio : 24; // priority (0 - highest)
+};
+
+typedef struct Rnm_Man_t_ Rnm_Man_t; // refinement manager
+struct Rnm_Man_t_
+{
+ // user data
+ Gia_Man_t * pGia; // working AIG manager (it is completely owned by this package)
+ Abc_Cex_t * pCex; // counter-example
+ Vec_Int_t * vMap; // mapping of CEX inputs into objects (PI + PPI, in any order)
+ int fPropFanout; // propagate fanouts
+ int fVerbose; // verbose flag
+ int nRefId; // refinement ID
+ // traversing data
+ Vec_Int_t * vObjs; // internal objects used in value propagation
+ // filtering of selected objects
+ Vec_Str_t * vCounts; // fanin counters
+ Vec_Int_t * vFanins; // fanins
+/*
+ // SAT solver
+ sat_solver2 * pSat; // incremental SAT solver
+ Vec_Int_t * vSatVars; // SAT variables
+ Vec_Int_t * vSat2Ids; // mapping of SAT variables into object IDs
+ Vec_Int_t * vIsopMem; // memory for ISOP computation
+*/
+ // internal data
+ Rnm_Obj_t * pObjs; // refinement objects
+ int nObjs; // the number of used objects
+ int nObjsAlloc; // the number of allocated objects
+ int nObjsFrame; // the number of used objects in each frame
+ int nCalls; // total number of calls
+ int nRefines; // total refined objects
+ int nVisited; // visited during justification
+ // statistics
+ clock_t timeFwd; // forward propagation
+ clock_t timeBwd; // backward propagation
+ clock_t timeVer; // ternary simulation
+ clock_t timeTotal; // other time
+};
+
+// accessing the refinement object
+static inline Rnm_Obj_t * Rnm_ManObj( Rnm_Man_t * p, Gia_Obj_t * pObj, int f )
+{
+ assert( Gia_ObjIsConst0(pObj) || pObj->Value );
+ assert( (int)pObj->Value < p->nObjsFrame );
+ assert( f >= 0 && f <= p->pCex->iFrame );
+ return p->pObjs + f * p->nObjsFrame + pObj->Value;
+}
+static inline void Rnm_ManSetRefId( Rnm_Man_t * p, int RefId ) { p->nRefId = RefId; }
+
+static inline int Rnm_ObjCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) { return Vec_StrEntry( p->vCounts, Gia_ObjId(p->pGia, pObj) ); }
+static inline void Rnm_ObjSetCount( Rnm_Man_t * p, Gia_Obj_t * pObj, int c ) { Vec_StrWriteEntry( p->vCounts, Gia_ObjId(p->pGia, pObj), (char)c ); }
+static inline int Rnm_ObjAddToCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) { int c = Rnm_ObjCount(p, pObj); if ( c < 16 ) Rnm_ObjSetCount(p, pObj, c+1); return c; }
+
+static inline int Rnm_ObjIsJust( Rnm_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsConst0(pObj) || (pObj->Value && Rnm_ManObj(p, pObj, 0)->fVisitJ); }
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-/*=== giaAbsRef.c ===========================================================*/
+/*=== absRef.c ===========================================================*/
extern Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia );
extern void Rnm_ManStop( Rnm_Man_t * p, int fProfile );
extern double Rnm_ManMemoryUsage( Rnm_Man_t * p );
-extern Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fPostProcess, int fVerbose );
-
+extern Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fNewRefinement, int fVerbose );
+/*=== absRefSelected.c ===========================================================*/
+extern Vec_Int_t * Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis );
+extern Vec_Int_t * Rnm_ManFilterSelectedNew( Rnm_Man_t * p, Vec_Int_t * vOldPPis );
ABC_NAMESPACE_HEADER_END
-
-
#endif
////////////////////////////////////////////////////////////////////////