luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

out-side box matching

This commit is contained in:
Allen Ho 2023-10-30 15:09:01 -07:00
parent 31ad17fa1a
commit ba64d6118b
3 changed files with 155 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Makefile
View File

@ -33,7 +33,8 @@ MODULES := \
src/proof/pdr src/proof/abs src/proof/live src/proof/ssc src/proof/int \
src/proof/cec src/proof/acec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \
src/aig/aig src/aig/saig src/aig/gia src/aig/ioa src/aig/ivy src/aig/hop \
src/aig/miniaig
src/aig/miniaig \
src/sat/bsat2
all: $(PROG)
default: $(PROG)

96
src/aig/gia/giaDup.c
View File

@ -30,6 +30,8 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
Vec_Int_t* vLitBmiter;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -5699,13 +5701,107 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose )
Gia_ManConst0(p2)->Value = 0;
Gia_ManForEachCi( p1, pObj, i )
pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew );
// TODO: record the corresponding impl node of each lit
vLitBmiter = Vec_IntAlloc( Gia_ManObjNum(p2) );
Vec_IntFill( vLitBmiter, Gia_ManObjNum(p2) + Gia_ManObjNum(p1), 0 );
Gia_ManForEachAnd( p2, pObj, i )
{
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 3 );
}
// TODO: find nodes in spec
Vec_Int_t * vTypeSpec = Vec_IntAlloc( 16 );
Vec_IntFill( vTypeSpec, Gia_ManObjNum(p1), 0 );
int n = Gia_ManBufNum(p1) / 2;
Gia_ManStaticFanoutStart( p1 );
Vec_Ptr_t * vQ = Vec_PtrAlloc(16);
Gia_Obj_t * pObj2;
int c1 = 0;
int c2 = 0;
int count;
Gia_ManForEachBuf( p1, pObj, i )
{
if ( count < n )
{
Vec_IntSetEntry( vTypeSpec, Gia_ObjId( p1, pObj ), 1 );
c1++;
count ++;
Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) );
Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) );
while ( Vec_PtrSize(vQ) != 0 )
{
pObj2 = Vec_PtrPop(vQ);
if ( Vec_IntEntry( vTypeSpec, Gia_ObjId(p1, pObj2) ) != 0 ) continue;
c1 ++;
Vec_IntSetEntry( vTypeSpec, Gia_ObjId(p1, pObj2), 1 );
if ( Gia_ObjFaninNum(p1, pObj2) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj2) );
if ( Gia_ObjFaninNum(p1, pObj2) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj2) );
}
}
else
{
Vec_IntSetEntry( vTypeSpec, Gia_ObjId( p1, pObj ), 2 );
c2 ++;
int j;
// pObj = Gia_ObjFanin0(pObj);
Gia_ObjForEachFanoutStatic(p1, pObj, pObj2, j)
{
Vec_PtrPush( vQ, pObj2 );
}
while ( Vec_PtrSize(vQ) != 0 )
{
pObj2 = Vec_PtrPop(vQ);
if ( Vec_IntEntry( vTypeSpec, Gia_ObjId(p1, pObj2) ) != 0 ) continue;
Vec_IntSetEntry( vTypeSpec, Gia_ObjId(p1, pObj2), 2 );
c2 ++;
for( int j = 0; j < Gia_ObjFanoutNum(p1, pObj2); j++ )
{
Vec_PtrPush( vQ, Gia_ObjFanout(p1, pObj2, j) );
}
}
}
}
Gia_ManStaticFanoutStop( p1 );
printf( "category %d %d %d\n", c1, c2, Gia_ManObjNum(p1) );
// TODO: record hashed equivalent nodes
Gia_ManForEachAnd( p1, pObj, i ) {
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) > 0 )
{
if ( Vec_IntGetEntry( vLitBmiter, pObj->Value ) == 3 ) // eq node in impl
{
Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 3 + Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) );
}
else
{
Vec_IntUpdateEntry( vLitBmiter, pObj->Value, Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) );
}
}
if ( Gia_ObjIsBuf(pObj) )
Vec_IntPush( vLits, pObj->Value );
}
// int e;
// Vec_IntForEachEntry( vLitBmiter, e, i )
// {
// printf( "%d ", e );
// }
// printf("\n");
Gia_ManForEachCo( p2, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
//Gia_ManForEachCo( p1, pObj, i )

57
src/proof/cec/cecSatG2.c
View File

@ -143,6 +143,9 @@ static inline int Cec4_ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj )
static inline int Cec4_ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Cec4_ObjSatId(p, pObj) == -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), Num); Vec_IntPush(&p->vSuppVars, Gia_ObjId(p, pObj)); if ( Gia_ObjIsCi(pObj) ) Vec_IntPushTwo(&p->vCopiesTwo, Gia_ObjId(p, pObj), Num); assert(Vec_IntSize(&p->vVarMap) == Num); Vec_IntPush(&p->vVarMap, Gia_ObjId(p, pObj)); return Num; }
static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Cec4_ObjSatId(p, pObj) != -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), -1); }
extern Vec_Int_t* vLitBmiter;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -1887,7 +1890,43 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
continue;
}
if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) )
{
if ( Vec_IntEntry( vLitBmiter, pRepr->Value ) == 3 )
{
switch ( Vec_IntEntry( vLitBmiter, pObj -> Value ) )
{
case 1:
case 4:
Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 5 );
break;
default:
break;
}
}
else
{
if ( Vec_IntEntry(vLitBmiter, pObj->Value ) == 3 )
switch ( Vec_IntEntry( vLitBmiter, pRepr -> Value ) )
{
case 1:
case 4:
Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 4 );
break;
case 2:
case 5:
Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 5 );
break;
default:
break;
}
}
pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase );
}
}
if ( p->iPatsPi > 0 )
{
@ -1933,10 +1972,28 @@ finalize:
Gia_ManRemoveWrongChoices( p );
return p->pCexSeq ? 0 : 1;
}
extern Vec_Int_t * vLitBmiter;
Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
{
Gia_Man_t * pNew = NULL;
Cec4_ManPerformSweeping( p, pPars, &pNew, 0 );
int e, i, c1=0, c2=0, c3=0, c4=0, c5=0;
Vec_IntForEachEntry( vLitBmiter, e, i )
{
if ( i%2 ) continue;
switch (e)
{
case 1: c1++; break;
case 2: c2++; break;
case 3: c3++; break;
case 4: c4++; break;
case 5: c5++; break;
default:
break;
}
}
printf("category %d %d %d %d %d\n", c1, c2, c3+c4+c5, c4, c5);
return pNew;
}
void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose )