Skip to content

A
abc
Commit 5b80d704 by Alan Mishchenko
Options

Improved abstraction refinement.

parent d01c0807
Showing with 491 additions and 44 deletions
src/aig/gia/giaAbsGla2.c
......@@ -20,7 +20,7 @@
#include "gia.h"
#include "giaAbsRef.h"
#include "giaAbsRef2.h"
//#include "giaAbsRef2.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver2.h"
#include "base/main/main.h"
......@@ -52,7 +52,7 @@ struct Ga2_Man_t_
int nMarked; // total number of marked nodes and flops
// refinement
Rnm_Man_t * pRnm; // refinement manager
Rf2_Man_t * pRf2; // refinement manager
// Rf2_Man_t * pRf2; // refinement manager
// SAT solver and variables
Vec_Ptr_t * vId2Lit; // mapping, for each timeframe, of object ID into SAT literal
sat_solver2 * pSat; // incremental SAT solver
......@@ -396,7 +396,7 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
Vec_IntPush( p->vAbs, 0 );
// refinement
p->pRnm = Rnm_ManStart( pGia );
p->pRf2 = Rf2_ManStart( pGia );
// p->pRf2 = Rf2_ManStart( pGia );
// SAT solver and variables
p->vId2Lit = Vec_PtrAlloc( 1000 );
// temporaries
......@@ -459,7 +459,7 @@ void Ga2_ManStop( Ga2_Man_t * p )
Vec_IntFree( p->vLits );
Vec_IntFree( p->vIsopMem );
Rnm_ManStop( p->pRnm, p->pPars->fVerbose );
Rf2_ManStop( p->pRf2, p->pPars->fVerbose );
// Rf2_ManStop( p->pRf2, p->pPars->fVerbose );
ABC_FREE( p->pTable );
ABC_FREE( p->pSopSizes );
ABC_FREE( p->pSops[1] );
......@@ -1224,11 +1224,9 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p )
Gia_Obj_t * pObj;
int i;
Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap );
// Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 );
// Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 );
vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1 );
// printf( "Refinement %d\n", Vec_IntSize(vVec) );
Abc_CexFree( pCex );
if ( Vec_IntSize(vVec) == 0 )
{
......
src/aig/gia/giaAbsRef.c
......@@ -77,6 +77,7 @@ 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)
};
......@@ -91,6 +92,8 @@ struct Rnm_Man_t_
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
// internal data
Rnm_Obj_t * pObjs; // refinement objects
int nObjs; // the number of used objects
......@@ -98,6 +101,7 @@ struct Rnm_Man_t_
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
......@@ -114,6 +118,17 @@ static inline Rnm_Obj_t * Rnm_ManObj( Rnm_Man_t * p, Gia_Obj_t * pObj, int f )
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; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -136,6 +151,8 @@ Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia )
p = ABC_CALLOC( Rnm_Man_t, 1 );
p->pGia = pGia;
p->vObjs = Vec_IntAlloc( 100 );
p->vCounts = Vec_StrStart( Gia_ManObjNum(pGia) );
p->vFanins = Vec_IntAlloc( 100 );
p->nObjsAlloc = 10000;
p->pObjs = ABC_ALLOC( Rnm_Obj_t, p->nObjsAlloc );
if ( p->pGia->vFanout == NULL )
......@@ -168,6 +185,8 @@ void Rnm_ManStop( Rnm_Man_t * p, int fProfile )
Gia_ManCleanMark1(p->pGia);
Gia_ManStaticFanoutStop(p->pGia);
// Gia_ManSetPhase(p->pGia);
Vec_StrFree( p->vCounts );
Vec_IntFree( p->vFanins );
Vec_IntFree( p->vObjs );
ABC_FREE( p->pObjs );
ABC_FREE( p );
......@@ -332,6 +351,11 @@ 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 )
{
Rnm_ManObj( p, pObj, 0 )->fVisit0 = 1;
p->nVisited++;
}
if ( pRnm->fPPi )
{
assert( (int)pRnm->Prio > 0 );
......@@ -383,7 +407,14 @@ void Rnm_ManJustify_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSe
if ( p->fPropFanout )
Rnm_ManJustifyPropFanout_rec( p, pObj, f, vSelect );
else
{
pRnm->fVisit = 1;
if ( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 )
{
Rnm_ManObj( p, pObj, 0 )->fVisit0 = 1;
p->nVisited++;
}
}
if ( pRnm->fPPi )
{
assert( (int)pRnm->Prio > 0 );
......@@ -507,6 +538,177 @@ 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 []
......@@ -518,8 +720,11 @@ void Rnm_ManVerifyUsingTerSim( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap
***********************************************************************/
Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose )
{
int fVerify = 0;
Vec_Int_t * vSelected = Vec_IntAlloc( 100 );
Vec_Int_t * vNew;
clock_t clk, clk2 = clock();
int RetValue;
p->nCalls++;
// Gia_ManCleanValue( p->pGia );
// initialize
......@@ -542,17 +747,43 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
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 );
// assert( RetValue == 0 );
p->timeBwd += clock() - clk;
}
vNew = Ga2_FilterSelected( p, vSelected );
if ( Vec_IntSize(vNew) > 0 )
{
Vec_IntFree( vSelected );
vSelected = vNew;
}
else
{
Vec_IntFree( vNew );
// printf( "\nBig refinement.\n" );
}
// clean values
Rnm_ManCleanValues( p );
// verify (empty) refinement
clk = clock();
Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected );
Vec_IntUniqify( vSelected );
if ( fVerify )
{
clk = clock();
Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected );
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 );
p->timeVer += clock() - clk;
p->timeTotal += clock() - clk2;
p->nRefines += Vec_IntSize(vSelected);
return vSelected;
......
src/aig/gia/giaAbsRef2.c
......@@ -93,7 +93,8 @@ struct Rf2_Man_t_
Vec_Int_t * vObjs; // internal objects used in value propagation
Vec_Int_t * vFanins; // fanins of the PPI nodes
Vec_Int_t * pvVecs; // vectors of integers for each object
Vec_Vec_t * vNod2Ppi; // for each node, the set of PPIs to include
Vec_Vec_t * vGrp2Ppi; // for each node, the set of PPIs to include
int nMapWords;
// internal data
Rf2_Obj_t * pObjs; // refinement objects
int nObjs; // the number of used objects
......@@ -122,6 +123,76 @@ static inline Vec_Int_t * Rf2_ObjVec( Rf2_Man_t * p, Gia_Obj_t * pObj )
return p->pvVecs + Gia_ObjId(p->pGia, pObj);
}
static inline unsigned * Rf2_ObjA( Rf2_Man_t * p, Gia_Obj_t * pObj )
{
return (unsigned *)Vec_IntArray(Rf2_ObjVec(p, pObj));
}
static inline unsigned * Rf2_ObjN( Rf2_Man_t * p, Gia_Obj_t * pObj )
{
return (unsigned *)Vec_IntArray(Rf2_ObjVec(p, pObj)) + p->nMapWords;
}
static inline void Rf2_ObjClear( Rf2_Man_t * p, Gia_Obj_t * pObj )
{
Vec_IntFill( Rf2_ObjVec(p, pObj), 2*p->nMapWords, 0 );
}
static inline void Rf2_ObjStart( Rf2_Man_t * p, Gia_Obj_t * pObj, int i )
{
Vec_Int_t * vVec = Rf2_ObjVec(p, pObj);
int w;
Vec_IntClear( vVec );
for ( w = 0; w < p->nMapWords; w++ )
Vec_IntPush( vVec, 0 );
for ( w = 0; w < p->nMapWords; w++ )
Vec_IntPush( vVec, ~0 );
Abc_InfoSetBit( Rf2_ObjA(p, pObj), i );
Abc_InfoXorBit( Rf2_ObjN(p, pObj), i );
}
static inline void Rf2_ObjCopy( Rf2_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanin )
{
assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 2*p->nMapWords );
memcpy( Rf2_ObjA(p, pObj), Rf2_ObjA(p, pFanin), sizeof(unsigned) * 2 * p->nMapWords );
}
static inline void Rf2_ObjDeriveAnd( Rf2_Man_t * p, Gia_Obj_t * pObj, int One )
{
unsigned * pInfo, * pInfo0, * pInfo1;
int i;
assert( Gia_ObjIsAnd(pObj) );
assert( One == (int)pObj->fMark0 );
assert( One == (int)(Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) );
assert( One == (int)(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) );
assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 2*p->nMapWords );
pInfo = Rf2_ObjA( p, pObj );
pInfo0 = Rf2_ObjA( p, Gia_ObjFanin0(pObj) );
pInfo1 = Rf2_ObjA( p, Gia_ObjFanin1(pObj) );
for ( i = 0; i < p->nMapWords; i++ )
pInfo[i] = One ? (pInfo0[i] & pInfo1[i]) : (pInfo0[i] | pInfo1[i]);
pInfo = Rf2_ObjN( p, pObj );
pInfo0 = Rf2_ObjN( p, Gia_ObjFanin0(pObj) );
pInfo1 = Rf2_ObjN( p, Gia_ObjFanin1(pObj) );
for ( i = 0; i < p->nMapWords; i++ )
pInfo[i] = One ? (pInfo0[i] | pInfo1[i]) : (pInfo0[i] & pInfo1[i]);
}
static inline void Rf2_ObjPrint( Rf2_Man_t * p, Gia_Obj_t * pRoot )
{
Gia_Obj_t * pObj;
unsigned * pInfo;
int i;
pInfo = Rf2_ObjA( p, pRoot );
Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
if ( !Gia_ObjIsPi(p->pGia, pObj) )
printf( "%d", Abc_InfoHasBit(pInfo, i) );
printf( "\n" );
pInfo = Rf2_ObjN( p, pRoot );
Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
if ( !Gia_ObjIsPi(p->pGia, pObj) )
printf( "%d", !Abc_InfoHasBit(pInfo, i) );
printf( "\n" );
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -146,7 +217,7 @@ Rf2_Man_t * Rf2_ManStart( Gia_Man_t * pGia )
p->vObjs = Vec_IntAlloc( 1000 );
p->vFanins = Vec_IntAlloc( 1000 );
p->pvVecs = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(pGia) );
p->vNod2Ppi = Vec_VecStart( 100 );
p->vGrp2Ppi = Vec_VecStart( 100 );
Gia_ManCleanMark0(pGia);
Gia_ManCleanMark1(pGia);
return p;
......@@ -171,7 +242,7 @@ void Rf2_ManStop( Rf2_Man_t * p, int fProfile )
}
Vec_IntFree( p->vObjs );
Vec_IntFree( p->vFanins );
Vec_VecFree( p->vNod2Ppi );
Vec_VecFree( p->vGrp2Ppi );
ABC_FREE( p->pvVecs );
ABC_FREE( p );
}
......@@ -471,9 +542,14 @@ void Rf2_ManGatherFanins( Rf2_Man_t * p, int Depth )
SeeAlso []
***********************************************************************/
int Rf2_ManCountPis( Rf2_Man_t * p )
static inline int Rf2_ManCountPpis( Rf2_Man_t * p )
{
return 0;
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
Counter++;
return Counter;
}
/**Function*************************************************************
......@@ -487,9 +563,40 @@ int Rf2_ManCountPis( Rf2_Man_t * p )
SeeAlso []
***********************************************************************/
void Rf2_ManProcessVector( Vec_Int_t * p, int Limit )
static inline void Rf2_ManPrintVector( Vec_Int_t * p, int Num )
{
int i, k, Entry;
Vec_IntForEachEntry( p, Entry, i )
{
for ( k = 0; k < Num; k++ )
printf( "%c", '0' + ((Entry>>k) & 1) );
printf( "\n" );
}
}
/**Function*************************************************************
Synopsis [Sort, make dup- and containment-free, and filter.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Rf2_ManProcessVector( Vec_Int_t * p, int Limit )
{
// int Start = Vec_IntSize(p);
int Start = 0;
int i, j, k, Entry, Entry2;
// printf( "%d", Vec_IntSize(p) );
if ( Start > 5 )
{
printf( "Before: \n" );
Rf2_ManPrintVector( p, 31 );
}
k = 0;
Vec_IntForEachEntry( p, Entry, i )
if ( Gia_WordCountOnes((unsigned)Entry) <= Limit )
......@@ -506,11 +613,18 @@ void Rf2_ManProcessVector( Vec_Int_t * p, int Limit )
Vec_IntWriteEntry( p, k++, Entry );
}
Vec_IntShrink( p, k );
// printf( "->%d ", Vec_IntSize(p) );
if ( Start > 5 )
{
printf( "After: \n" );
Rf2_ManPrintVector( p, 31 );
k = 0;
}
}
/**Function*************************************************************
Synopsis [Sort, make dup- and containment-free, and filter.]
Synopsis [Assigns a unique justifification ID for each PPI.]
Description []
......@@ -519,18 +633,23 @@ void Rf2_ManProcessVector( Vec_Int_t * p, int Limit )
SeeAlso []
***********************************************************************/
void Rf2_ManPrintVector( Vec_Int_t * p, int Num )
int Rf2_ManAssignJustIds( Rf2_Man_t * p )
{
extern void Extra_PrintBinary( FILE * pFile, unsigned * p, int nBits );
int i, Entry;
printf( "Justification containing %d subsets.\n", Vec_IntSize(p) );
Vec_IntForEachEntry( p, Entry, i )
Extra_PrintBinary( stdout, (unsigned *)&Entry, Num ), printf( "\n" );
Gia_Obj_t * pObj;
int nPpis = Rf2_ManCountPpis( p );
int nGroupSize = (nPpis / 30) + (nPpis % 30 > 0);
int i, k = 0;
Vec_VecClear( p->vGrp2Ppi );
Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI
Vec_VecPushInt( p->vGrp2Ppi, (k++ / nGroupSize), i );
printf( "Considering %d PPIs combined into %d groups of size %d.\n", k, (k-1)/nGroupSize+1, nGroupSize );
return (k-1)/nGroupSize+1;
}
/**Function*************************************************************
Synopsis [Assigns a unique justifification ID for each PPI.]
Synopsis [Sort, make dup- and containment-free, and filter.]
Description []
......@@ -539,15 +658,31 @@ void Rf2_ManPrintVector( Vec_Int_t * p, int Num )
SeeAlso []
***********************************************************************/
void Rf2_ManAssignJustIds( Rf2_Man_t * p )
static inline void Rf2_ManPrintVectorSpecial( Rf2_Man_t * p, Vec_Int_t * vVec )
{
Gia_Obj_t * pObj;
int i, k = 0;
Vec_VecClear( p->vNod2Ppi );
Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI
Vec_VecPushInt( p->vNod2Ppi, k++, i );
printf( "Considering %d PPIs with unique justification IDs.\n", k );
int nPpis = Rf2_ManCountPpis( p );
int nGroupSize = (nPpis / 30) + (nPpis % 30 > 0);
int s, i, k, Entry, Counter;
Vec_IntForEachEntry( vVec, Entry, s )
{
k = 0;
Counter = 0;
Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
{
if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI
{
if ( (Entry >> (k++ / nGroupSize)) & 1 )
printf( "1" ), Counter++;
else
printf( "0" );
}
else
printf( "-" );
}
printf( " %3d \n", Counter );
}
}
/**Function*************************************************************
......@@ -581,7 +716,7 @@ Vec_Int_t * Rf2_ManPropagate( Rf2_Man_t * p, int Limit )
Vec_IntFill( Rf2_ObjVec(p, pObj), 1, 0 );
}
// assign justification sets for PPis
Vec_VecForEachLevelInt( p->vNod2Ppi, vVec, i )
Vec_VecForEachLevelInt( p->vGrp2Ppi, vVec, i )
Vec_IntForEachEntry( vVec, Entry, k )
{
assert( i < 31 );
......@@ -615,11 +750,11 @@ Vec_Int_t * Rf2_ManPropagate( Rf2_Man_t * p, int Limit )
continue;
}
assert( Gia_ObjIsAnd(pObj) );
vVec0 = Rf2_ObjVec(p, Gia_ObjFanin0(pObj));
vVec1 = Rf2_ObjVec(p, Gia_ObjFanin1(pObj));
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
if ( pObj->fMark0 == 1 )
{
vVec0 = Rf2_ObjVec(p, Gia_ObjFanin0(pObj));
vVec1 = Rf2_ObjVec(p, Gia_ObjFanin1(pObj));
Vec_IntForEachEntry( vVec0, Entry, k )
Vec_IntForEachEntry( vVec1, Entry2, j )
Vec_IntPush( vVec, Entry | Entry2 );
......@@ -645,6 +780,77 @@ Vec_Int_t * Rf2_ManPropagate( Rf2_Man_t * p, int Limit )
/**Function*************************************************************
Synopsis [Performs justification propagation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Rf2_ManBounds( Rf2_Man_t * p )
{
Gia_Obj_t * pObj;
int f, i, iBit = p->pCex->nRegs;
// init constant
pObj = Gia_ManConst0(p->pGia);
pObj->fMark0 = 0;
Rf2_ObjStart( p, pObj, Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) );
// iterate through the timeframes
for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis )
{
// initialize frontier values and init justification sets
Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
{
assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
pObj->fMark0 = Abc_InfoHasBit( p->pCex->pData, iBit + i );
Rf2_ObjStart( p, pObj, i );
}
// propagate internal nodes
Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i )
{
pObj->fMark0 = 0;
Rf2_ObjClear( p, pObj );
if ( Gia_ObjIsRo(p->pGia, pObj) )
{
if ( f == 0 )
{
Rf2_ObjStart( p, pObj, Vec_IntSize(p->vMap) + i );
continue;
}
pObj->fMark0 = Gia_ObjRoToRi(p->pGia, pObj)->fMark0;
Rf2_ObjCopy( p, pObj, Gia_ObjRoToRi(p->pGia, pObj) );
continue;
}
if ( Gia_ObjIsCo(pObj) )
{
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj));
Rf2_ObjCopy( p, pObj, Gia_ObjFanin0(pObj) );
continue;
}
assert( Gia_ObjIsAnd(pObj) );
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
if ( pObj->fMark0 == 1 )
Rf2_ObjDeriveAnd( p, pObj, 1 );
else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 )
Rf2_ObjDeriveAnd( p, pObj, 0 );
else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 )
Rf2_ObjCopy( p, pObj, Gia_ObjFanin0(pObj) );
else
Rf2_ObjCopy( p, pObj, Gia_ObjFanin1(pObj) );
}
}
assert( iBit == p->pCex->nBits );
if ( Gia_ManPo(p->pGia, 0)->fMark0 != 1 )
printf( "Output value is incorrect.\n" );
printf( "Bounds: \n" );
Rf2_ObjPrint( p, Gia_ManPo(p->pGia, 0) );
}
/**Function*************************************************************
Synopsis [Computes the refinement for a given counter-example.]
Description []
......@@ -657,8 +863,10 @@ Vec_Int_t * Rf2_ManPropagate( Rf2_Man_t * p, int Limit )
Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose )
{
Vec_Int_t * vJusts;
Vec_Int_t * vSelected = Vec_IntAlloc( 100 );
// Vec_Int_t * vSelected = Vec_IntAlloc( 100 );
Vec_Int_t * vSelected = NULL;
clock_t clk, clk2 = clock();
int nGroups;
p->nCalls++;
// initialize
p->pCex = pCex;
......@@ -670,15 +878,23 @@ Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
// collect reconvergence points
// Rf2_ManGatherFanins( p, 2 );
// propagate justification IDs
Rf2_ManAssignJustIds( p );
vJusts = Rf2_ManPropagate( p, 100 );
Rf2_ManPrintVector( vJusts, Rf2_ManCountPis(p) );
nGroups = Rf2_ManAssignJustIds( p );
vJusts = Rf2_ManPropagate( p, 32 );
// printf( "\n" );
// Rf2_ManPrintVector( vJusts, nGroups );
Rf2_ManPrintVectorSpecial( p, vJusts );
if ( Vec_IntSize(vJusts) == 0 )
{
printf( "Empty set of justifying subsets.\n" );
return NULL;
}
// p->nMapWords = Abc_BitWordNum( Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) + 1 ); // Map + Flops + Const
// Rf2_ManBounds( p );
// select the result
// Abc_PrintTime( 1, "Time", clock() - clk2 );
// verify (empty) refinement
clk = clock();
......@@ -687,7 +903,7 @@ Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
// Vec_IntReverseOrder( vSelected );
p->timeVer += clock() - clk;
p->timeTotal += clock() - clk2;
p->nRefines += Vec_IntSize(vSelected);
// p->nRefines += Vec_IntSize(vSelected);
return vSelected;
}
......
src/misc/vec/vecInt.h
......@@ -1170,23 +1170,25 @@ static inline void Vec_IntSort( Vec_Int_t * p, int fReverse )
Synopsis [Leaves only unique entries.]
Description []
Description [Returns the number of duplicated entried found.]
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntUniqify( Vec_Int_t * p )
static inline int Vec_IntUniqify( Vec_Int_t * p )
{
int i, k;
int i, k, RetValue;
if ( p->nSize < 2 )
return;
return 0;
Vec_IntSort( p, 0 );
for ( i = k = 1; i < p->nSize; i++ )
if ( p->pArray[i] != p->pArray[i-1] )
p->pArray[k++] = p->pArray[i];
RetValue = p->nSize - k;
p->nSize = k;
return RetValue;
}
/**Function*************************************************************
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment