summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/abs/abs.h9
-rw-r--r--src/proof/abs/absDup.c4
-rw-r--r--src/proof/abs/absGla.c10
-rw-r--r--src/proof/abs/absGlaOld.c2
-rw-r--r--src/proof/abs/absRef.c329
-rw-r--r--src/proof/abs/absRef.h74
-rw-r--r--src/proof/abs/absRefJ.c (renamed from src/proof/abs/absRef2.c)2
-rw-r--r--src/proof/abs/absRefJ.h (renamed from src/proof/abs/absRef2.h)2
-rw-r--r--src/proof/abs/absRefSelect.c220
-rw-r--r--src/proof/abs/module.make2
10 files changed, 343 insertions, 311 deletions
diff --git a/src/proof/abs/abs.h b/src/proof/abs/abs.h
index e7ab9e7d..11eda38c 100644
--- a/src/proof/abs/abs.h
+++ b/src/proof/abs/abs.h
@@ -61,6 +61,7 @@ struct Abs_Par_t_
int fUseRollback; // use rollback to the starting number of frames
int fPropFanout; // propagate fanout implications
int fAddLayer; // refinement strategy by adding layers
+ int fNewRefine; // uses new refinement heuristics
int fUseSkip; // skip proving intermediate timeframes
int fUseSimple; // use simple CNF construction
int fSkipHash; // skip hashing CNF while unrolling
@@ -81,6 +82,13 @@ struct Abs_Par_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
+static inline int Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj)); }
+static inline int Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj)); }
+static inline int * Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1); }
+static inline unsigned Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1); }
+static inline int Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2); }
+static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj ) { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v; }
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -114,6 +122,7 @@ extern Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla );
extern int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla );
extern int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla );
+
/*=== absOldCex.c ==========================================================*/
extern Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect );
extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
diff --git a/src/proof/abs/absDup.c b/src/proof/abs/absDup.c
index 247137bd..94215575 100644
--- a/src/proof/abs/absDup.c
+++ b/src/proof/abs/absDup.c
@@ -53,7 +53,7 @@ void Gia_ManDupAbsFlops_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
/**Function*************************************************************
- Synopsis [Performs abstraction of the AIG to preserve the included flops.]
+ Synopsis [Extractes a flop-level abstraction given a flop map.]
Description []
@@ -207,7 +207,7 @@ void Gia_ManDupAbsGates_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
/**Function*************************************************************
- Synopsis [Performs abstraction of the AIG to preserve the included gates.]
+ Synopsis [Extractes a gate-level abstraction given a gate map.]
Description [The array contains 1 for those objects (const, RO, AND)
that are included in the abstraction; 0, otherwise.]
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index 76b6c231..260a649c 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -78,13 +78,6 @@ struct Ga2_Man_t_
clock_t timeOther;
};
-static inline int Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj)); }
-static inline int Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj)); }
-static inline int * Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1); }
-static inline unsigned Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1); }
-static inline int Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2); }
-static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj ) { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v; }
-
static inline int Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj)); }
static inline void Ga2_ObjSetId( Ga2_Man_t * p, Gia_Obj_t * pObj, int i ) { Vec_IntWriteEntry(p->vIds, Gia_ObjId(p->pGia, pObj), i); }
@@ -1329,7 +1322,7 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p )
}
Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap );
// Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 );
- vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1, 1 );
+ vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, p->pPars->fNewRefine, 1 );
// printf( "Refinement %d\n", Vec_IntSize(vVec) );
Abc_CexFree( pCex );
if ( Vec_IntSize(vVec) == 0 )
@@ -1644,6 +1637,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
// perform refinement
clk2 = clock();
+ Rnm_ManSetRefId( p->pRnm, c );
vPPis = Ga2_ManRefine( p );
p->timeCex += clock() - clk2;
if ( vPPis == NULL )
diff --git a/src/proof/abs/absGlaOld.c b/src/proof/abs/absGlaOld.c
index 5ee69739..4ab956f7 100644
--- a/src/proof/abs/absGlaOld.c
+++ b/src/proof/abs/absGlaOld.c
@@ -503,7 +503,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
Gia_Obj_t * pObj;
int i;
Gia_GlaPrepareCexAndMap( p, &pCex, &vMap );
- vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 0, 1 );
+ vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, p->pPars->fNewRefine, 1 );
Abc_CexFree( pCex );
if ( Vec_IntSize(vVec) == 0 )
{
diff --git a/src/proof/abs/absRef.c b/src/proof/abs/absRef.c
index 3aea96ee..64e1f55c 100644
--- a/src/proof/abs/absRef.c
+++ b/src/proof/abs/absRef.c
@@ -73,80 +73,20 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-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 fVisit0 : 1; // visited object
- unsigned fPPi : 1; // PPI object
- unsigned Prio : 24; // priority (0 - highest)
-};
-
-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
- // traversing data
- Vec_Int_t * vObjs; // internal objects used in value propagation
- 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 int Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj)); }
-static inline int Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj)); }
-static inline int * Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1); }
-static inline unsigned Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1); }
-static inline int Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2); }
-static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj ) { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v; }
-
-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_ObjSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry( p->vSatVars, Gia_ObjId(p->pGia, pObj) ); }
static inline void Rnm_ObjSetSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj, int c) { Vec_IntWriteEntry( p->vSatVars, Gia_ObjId(p->pGia, pObj), c ); }
static inline int Rnm_ObjFindOrAddSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj) { if ( Rnm_ObjSatVar(p, pObj) == 0 ) { Rnm_ObjSetSatVar(p, pObj, Vec_IntSize(p->vSat2Ids)); Vec_IntPush(p->vSat2Ids, Gia_ObjId(p->pGia, pObj)); }; return 2*Rnm_ObjSatVar(p, pObj); }
-
+*/
extern void Ga2_ManCnfAddStatic( sat_solver2 * pSat, Vec_Int_t * vCnf0, Vec_Int_t * vCnf1, int * pLits, int iLitOut, int ProofId );
-
extern Vec_Int_t * Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCover );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
+#if 0
+
/**Function*************************************************************
Synopsis [Performs UNSAT-core-based refinement.]
@@ -308,6 +248,7 @@ Vec_Int_t * Rnm_ManRefineUnsatCore( Rnm_Man_t * p, Vec_Int_t * vPPIs )
return vCoreFinal;
}
+#endif
/**Function*************************************************************
@@ -329,9 +270,9 @@ Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia )
p->vObjs = Vec_IntAlloc( 100 );
p->vCounts = Vec_StrStart( Gia_ManObjNum(pGia) );
p->vFanins = Vec_IntAlloc( 1000 );
- p->vSatVars = Vec_IntAlloc( 0 );
- p->vSat2Ids = Vec_IntAlloc( 1000 );
- p->vIsopMem = Vec_IntAlloc( 0 );
+// p->vSatVars = Vec_IntAlloc( 0 );
+// p->vSat2Ids = Vec_IntAlloc( 1000 );
+// p->vIsopMem = Vec_IntAlloc( 0 );
p->nObjsAlloc = 10000;
p->pObjs = ABC_ALLOC( Rnm_Obj_t, p->nObjsAlloc );
if ( p->pGia->vFanout == NULL )
@@ -364,9 +305,9 @@ void Rnm_ManStop( Rnm_Man_t * p, int fProfile )
Gia_ManCleanMark1(p->pGia);
Gia_ManStaticFanoutStop(p->pGia);
// Gia_ManSetPhase(p->pGia);
- Vec_IntFree( p->vIsopMem );
- Vec_IntFree( p->vSatVars );
- Vec_IntFree( p->vSat2Ids );
+// Vec_IntFree( p->vIsopMem );
+// Vec_IntFree( p->vSatVars );
+// Vec_IntFree( p->vSat2Ids );
Vec_StrFree( p->vCounts );
Vec_IntFree( p->vFanins );
Vec_IntFree( p->vObjs );
@@ -533,9 +474,9 @@ void Rnm_ManJustifyPropFanout_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_I
int i, k;//, Id = Gia_ObjId(p->pGia, pObj);
assert( pRnm->fVisit == 0 );
pRnm->fVisit = 1;
- if ( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 )
+ if ( Rnm_ManObj( p, pObj, 0 )->fVisitJ == 0 )
{
- Rnm_ManObj( p, pObj, 0 )->fVisit0 = 1;
+ Rnm_ManObj( p, pObj, 0 )->fVisitJ = 1;
p->nVisited++;
}
if ( pRnm->fPPi )
@@ -591,9 +532,9 @@ void Rnm_ManJustify_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSe
else
{
pRnm->fVisit = 1;
- if ( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 )
+ if ( Rnm_ManObj( p, pObj, 0 )->fVisitJ == 0 )
{
- Rnm_ManObj( p, pObj, 0 )->fVisit0 = 1;
+ Rnm_ManObj( p, pObj, 0 )->fVisitJ = 1;
p->nVisited++;
}
}
@@ -720,177 +661,6 @@ void Rnm_ManVerifyUsingTerSim( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap
/**Function*************************************************************
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Rnm_ManPrintSelected( Rnm_Man_t * p, Vec_Int_t * vSelected )
-{
- Gia_Obj_t * pObj;
- int i, Counter = 0;
- Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
- {
- if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI
- {
- if ( Vec_IntFind(vSelected, Gia_ObjId(p->pGia, pObj)) >= 0 )
- printf( "1" ), Counter++;
- else
- printf( "0" );
- }
- else
- printf( "-" );
- }
- printf( " %3d\n", Counter );
-}
-
-
-
-
-
-/**Function*************************************************************
-
- Synopsis [Perform structural analysis.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ga2_StructAnalize( Gia_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInter, Vec_Int_t * vSelect )
-{
- Vec_Int_t * vLeaves;
- Gia_Obj_t * pObj, * pFanin;
- int i, k;
- // clean labels
- Gia_ManForEachObj( p, pObj, i )
- pObj->fMark0 = pObj->fMark1 = 0;
- // label frontier
- Gia_ManForEachObjVec( vFront, p, pObj, i )
- pObj->fMark0 = 1, pObj->fMark1 = 0;
- // label objects
- Gia_ManForEachObjVec( vInter, p, pObj, i )
- pObj->fMark1 = 0, pObj->fMark1 = 1;
- // label selected
- Gia_ManForEachObjVec( vSelect, p, pObj, i )
- pObj->fMark1 = 1, pObj->fMark1 = 1;
- // explore selected
- printf( "\n" );
- Gia_ManForEachObjVec( vSelect, p, pObj, i )
- {
- printf( "Selected %6d : ", Gia_ObjId(p, pObj) );
- printf( "\n" );
- vLeaves = Ga2_ObjLeaves( p, pObj );
- Gia_ManForEachObjVec( vLeaves, p, pFanin, k )
- {
- printf( " " );
- printf( "%6d ", Gia_ObjId(p, pFanin) );
- if ( pFanin->fMark0 && pFanin->fMark1 )
- printf( "select" );
- else if ( pFanin->fMark0 && !pFanin->fMark1 )
- printf( "front" );
- else if ( !pFanin->fMark0 && pFanin->fMark1 )
- printf( "internal" );
- else if ( !pFanin->fMark0 && !pFanin->fMark1 )
- printf( "new" );
- printf( "\n" );
- }
- }
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Finds essential objects.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Int_t * Ga2_FilterSelected( Rnm_Man_t * p, Vec_Int_t * vSelect )
-{
- Vec_Int_t * vNew, * vLeaves;
- Gia_Obj_t * pObj, * pFanin;
- int i, k, RetValue;//, Counters[3] = {0};
-/*
- // check that selected are not visited
- Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i )
- assert( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 1 );
- Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
- if ( Vec_IntFind(vSelect, Gia_ObjId(p->pGia, pObj)) == -1 )
- assert( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 );
-*/
-
- // verify
-// Gia_ManForEachObj( p->pGia, pObj, i )
-// assert( Rnm_ObjCount(p, pObj) == 0 );
-
- // increment fanin counters
- Vec_IntClear( p->vFanins );
- Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i )
- {
- vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
- Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
- if ( Rnm_ObjAddToCount(p, pFanin) == 0 )
- Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin) );
- }
-
- // find selected objects, which create potential constraints
- // - flop objects
- // - objects whose fanin belongs to the justified area
- // - objects whose fanins overlap
- // (these do not guantee reconvergence, but may potentially have it)
- // (other objects cannot have reconvergence, even if they are added)
- vNew = Vec_IntAlloc( 100 );
- Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i )
- {
- if ( Gia_ObjIsRo(p->pGia, pObj) )
- {
- Vec_IntPush( vNew, Gia_ObjId(p->pGia, pObj) );
- continue;
- }
- vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
- Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
- {
- if ( Gia_ObjIsConst0(pFanin)
- || (pFanin->Value && Rnm_ManObj(p, pFanin, 0)->fVisit0 == 1)
- || Rnm_ObjCount(p, pFanin) > 1
- )
- {
- Vec_IntPush( vNew, Gia_ObjId(p->pGia, pObj) );
- break;
- }
- }
-// Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
-// {
-// Counters[1] += (pFanin->Value && Rnm_ManObj( p, pFanin, 0 )->fVisit0 == 1);
-// Counters[2] += (Rnm_ObjCount(p, pFanin) > 1);
-// }
- }
- RetValue = Vec_IntUniqify( vNew );
- assert( RetValue == 0 );
-
-// printf( "\n*** Select = %5d. New = %5d. Flops = %5d. Visited = %5d. Fanins = %5d.\n",
-// Vec_IntSize(vSelect), Vec_IntSize(vNew), Counters[0], Counters[1], Counters[2] );
-
- // clear fanin counters
- Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i )
- Rnm_ObjSetCount( p, pObj, 0 );
- return vNew;
-}
-
-
-/**Function*************************************************************
-
Synopsis [Computes the refinement for a given counter-example.]
Description []
@@ -900,12 +670,10 @@ Vec_Int_t * Ga2_FilterSelected( Rnm_Man_t * p, Vec_Int_t * vSelect )
SeeAlso []
***********************************************************************/
-Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fPostProcess, int fVerbose )
+Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fNewRefinement, int fVerbose )
{
int fVerify = 0;
-// int fPostProcess = 1;
- Vec_Int_t * vSelected = Vec_IntAlloc( 100 );
- Vec_Int_t * vNew;
+ Vec_Int_t * vGoodPPis, * vNewPPis;
clock_t clk, clk2 = clock();
int RetValue;
p->nCalls++;
@@ -925,71 +693,50 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
memset( p->pObjs, 0, sizeof(Rnm_Obj_t) * p->nObjs );
// propagate priorities
clk = clock();
+ vGoodPPis = Vec_IntAlloc( 100 );
if ( Rnm_ManSensitize( p ) ) // the CEX is not a true CEX
{
p->timeFwd += clock() - clk;
// select refinement
clk = clock();
p->nVisited = 0;
- Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), pCex->iFrame, vSelected );
- RetValue = Vec_IntUniqify( vSelected );
+ Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), pCex->iFrame, vGoodPPis );
+ RetValue = Vec_IntUniqify( vGoodPPis );
// assert( RetValue == 0 );
p->timeBwd += clock() - clk;
}
-
- if ( fPostProcess )
- {
- vNew = Ga2_FilterSelected( p, vSelected );
- if ( Vec_IntSize(vNew) > 0 )
- {
- Vec_IntFree( vSelected );
- vSelected = vNew;
- }
- else
- {
- Vec_IntFree( vNew );
- // printf( "\nBig refinement.\n" );
- }
- }
- else
+ // at this point array vGoodPPis contains the set of important PPIs
+ if ( Vec_IntSize(vGoodPPis) > 0 ) // spurious CEX resulting in a non-trivial refinement
{
-/*
- vNew = Rnm_ManRefineUnsatCore( p, vSelected );
- if ( Vec_IntSize(vNew) > 0 )
- {
- Vec_IntFree( vSelected );
- vSelected = vNew;
-// Vec_IntFree( vNew );
- }
- else
- {
- Vec_IntFree( vNew );
- // printf( "\nBig refinement.\n" );
- }
-*/
+ // filter selected set
+ if ( !fNewRefinement ) // default
+ vNewPPis = Rnm_ManFilterSelected( p, vGoodPPis );
+ else // this is enabled when &gla is called with -r (&gla -r)
+ vNewPPis = Rnm_ManFilterSelectedNew( p, vGoodPPis );
+
+ // replace the PPI array if necessary
+ if ( Vec_IntSize(vNewPPis) > 0 ) // something to select, replace current refinement
+ Vec_IntFree( vGoodPPis ), vGoodPPis = vNewPPis;
+ else // if there is nothing to select, do not change the current refinement array
+ Vec_IntFree( vNewPPis );
}
// clean values
Rnm_ManCleanValues( p );
// verify (empty) refinement
+ // (only works when post-processing is not applied)
if ( fVerify )
{
clk = clock();
- Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected );
+ Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vGoodPPis );
p->timeVer += clock() - clk;
}
-// printf( "\nOriginal (%d): \n", Vec_IntSize(p->vMap) );
-// Rnm_ManPrintSelected( p, vSelected );
-
-// Ga2_StructAnalize( p->pGia, vMap, p->vObjs, vSelected );
-// printf( "\nObjects = %5d. Visited = %5d.\n", Vec_IntSize(p->vObjs), p->nVisited );
-
-// Vec_IntReverseOrder( vSelected );
+// Vec_IntReverseOrder( vGoodPPis );
p->timeTotal += clock() - clk2;
- p->nRefines += Vec_IntSize(vSelected);
- return vSelected;
+ p->nRefines += Vec_IntSize(vGoodPPis);
+ return vGoodPPis;
}
////////////////////////////////////////////////////////////////////////
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
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/abs/absRef2.c b/src/proof/abs/absRefJ.c
index 7fb26e5a..aa5ea7bb 100644
--- a/src/proof/abs/absRef2.c
+++ b/src/proof/abs/absRefJ.c
@@ -6,7 +6,7 @@
PackageName [Abstraction package.]
- Synopsis [Refinement manager.]
+ Synopsis [Refinement manager to compute all justifying subsets.]
Author [Alan Mishchenko]
diff --git a/src/proof/abs/absRef2.h b/src/proof/abs/absRefJ.h
index df7774c0..0c56d2dd 100644
--- a/src/proof/abs/absRef2.h
+++ b/src/proof/abs/absRefJ.h
@@ -6,7 +6,7 @@
PackageName [Abstraction package.]
- Synopsis [Refinement manager.]
+ Synopsis [Refinement manager to compute all justifying subsets.]
Author [Alan Mishchenko]
diff --git a/src/proof/abs/absRefSelect.c b/src/proof/abs/absRefSelect.c
new file mode 100644
index 00000000..871eb79b
--- /dev/null
+++ b/src/proof/abs/absRefSelect.c
@@ -0,0 +1,220 @@
+/**CFile****************************************************************
+
+ FileName [absRefSelect.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Abstraction package.]
+
+ Synopsis [Post-processes the set of selected refinement objects.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: absRefSelect.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abs.h"
+#include "absRef.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rnm_ManPrintSelected( Rnm_Man_t * p, Vec_Int_t * vNewPPis )
+{
+ Gia_Obj_t * pObj;
+ int i, Counter = 0;
+ Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
+ if ( Gia_ObjIsPi(p->pGia, pObj) )
+ printf( "-" );
+ else if ( Vec_IntFind(vNewPPis, Gia_ObjId(p->pGia, pObj)) >= 0 )// this is PPI
+ printf( "1" ), Counter++;
+ else
+ printf( "0" );
+ printf( " %3d\n", Counter );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Perform structural analysis.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ga2_StructAnalize( Gia_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInter, Vec_Int_t * vNewPPis )
+{
+ Vec_Int_t * vLeaves;
+ Gia_Obj_t * pObj, * pFanin;
+ int i, k;
+ // clean labels
+ Gia_ManForEachObj( p, pObj, i )
+ pObj->fMark0 = pObj->fMark1 = 0;
+ // label frontier
+ Gia_ManForEachObjVec( vFront, p, pObj, i )
+ pObj->fMark0 = 1, pObj->fMark1 = 0;
+ // label objects
+ Gia_ManForEachObjVec( vInter, p, pObj, i )
+ pObj->fMark1 = 0, pObj->fMark1 = 1;
+ // label selected
+ Gia_ManForEachObjVec( vNewPPis, p, pObj, i )
+ pObj->fMark1 = 1, pObj->fMark1 = 1;
+ // explore selected
+ Gia_ManForEachObjVec( vNewPPis, p, pObj, i )
+ {
+ printf( "Selected PPI %3d : ", i+1 );
+ printf( "%6d ", Gia_ObjId(p, pObj) );
+ printf( "\n" );
+ vLeaves = Ga2_ObjLeaves( p, pObj );
+ Gia_ManForEachObjVec( vLeaves, p, pFanin, k )
+ {
+ printf( " " );
+ printf( "%6d ", Gia_ObjId(p, pFanin) );
+ if ( pFanin->fMark0 && pFanin->fMark1 )
+ printf( "selected PPI" );
+ else if ( pFanin->fMark0 && !pFanin->fMark1 )
+ printf( "frontier (original PI or PPI)" );
+ else if ( !pFanin->fMark0 && pFanin->fMark1 )
+ printf( "abstracted node" );
+ else if ( !pFanin->fMark0 && !pFanin->fMark1 )
+ printf( "free variable" );
+ printf( "\n" );
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Postprocessing the set of PPIs using structural analysis.]
+
+ Description [The following sets are used:
+ The set of all PI+PPI is in p->vMap.
+ The set of all abstracted objects is in p->vObjs;
+ The set of important PPIs is in vOldPPis.
+ The new set of selected PPIs is in vNewPPis.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis )
+{
+ int fVerbose = 0;
+ Vec_Int_t * vNewPPis, * vLeaves;
+ Gia_Obj_t * pObj, * pFanin;
+ int i, k, RetValue, Counters[3] = {0};
+
+ // (0) make sure fanin counters are 0 at the beginning
+// Gia_ManForEachObj( p->pGia, pObj, i )
+// assert( Rnm_ObjCount(p, pObj) == 0 );
+
+ // (1) increment PPI fanin counters
+ Vec_IntClear( p->vFanins );
+ Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
+ {
+ vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
+ Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
+ if ( Rnm_ObjAddToCount(p, pFanin) == 0 ) // fanin counter is 0 -- save it
+ Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin) );
+ }
+
+ // (3) select objects with reconvergence, which create potential constraints
+ // - flop objects
+ // - objects whose fanin belongs to the justified area
+ // - objects whose fanins overlap
+ // (these do not guantee reconvergence, but may potentially have it)
+ // (other objects cannot have reconvergence, even if they are added)
+ vNewPPis = Vec_IntAlloc( 100 );
+ Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
+ {
+ if ( Gia_ObjIsRo(p->pGia, pObj) )
+ {
+ if ( fVerbose )
+ Counters[0]++;
+ Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
+ continue;
+ }
+ vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
+ Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
+ {
+ if ( Rnm_ObjIsJust(p, pFanin) || Rnm_ObjCount(p, pFanin) > 1 )
+ {
+ if ( fVerbose )
+ Counters[1] += Rnm_ObjIsJust(p, pFanin);
+ if ( fVerbose )
+ Counters[2] += (Rnm_ObjCount(p, pFanin) > 1);
+ Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
+ break;
+ }
+ }
+ }
+ RetValue = Vec_IntUniqify( vNewPPis );
+ assert( RetValue == 0 );
+
+ // (4) clear fanin counters
+ // this is important for counters to be correctly set in the future iterations -- see step (0)
+ Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i )
+ Rnm_ObjSetCount( p, pObj, 0 );
+
+ // visualize
+ if ( fVerbose )
+ printf( "*** Refinement %3d : PI+PPI =%4d. Old =%4d. New =%4d. FF =%4d. Just =%4d. Shared =%4d.\n",
+ p->nRefId, Vec_IntSize(p->vMap), Vec_IntSize(vOldPPis), Vec_IntSize(vNewPPis), Counters[0], Counters[1], Counters[2] );
+
+// Rnm_ManPrintSelected( p, vNewPPis );
+// Ga2_StructAnalize( p->pGia, p->vMap, p->vObjs, vNewPPis );
+ return vNewPPis;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Improved postprocessing the set of PPIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Rnm_ManFilterSelectedNew( Rnm_Man_t * p, Vec_Int_t * vOldPPis )
+{
+ Vec_Int_t * vNewPPis;
+ vNewPPis = Vec_IntDup( vOldPPis );
+ return vNewPPis;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/abs/module.make b/src/proof/abs/module.make
index 4e652afd..4dd463e2 100644
--- a/src/proof/abs/module.make
+++ b/src/proof/abs/module.make
@@ -10,6 +10,6 @@ SRC += src/proof/abs/abs.c \
src/proof/abs/absOut.c \
src/proof/abs/absPth.c \
src/proof/abs/absRef.c \
- src/proof/abs/absRef2.c \
+ src/proof/abs/absRefSelect.c \
src/proof/abs/absVta.c \
src/proof/abs/absUtil.c
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 13:35:43 +0000