Skip to content

A
abc
Commit b193ef05 by Alan Mishchenko
Options

Updates to arithmetic verification.

parent 7457b8a6
Showing with 90 additions and 24 deletions
src/proof/acec/acecCore.c
......@@ -307,6 +307,50 @@ int Acec_MatchCountCommon( Vec_Wec_t * vLits1, Vec_Wec_t * vLits2, int Shift )
Vec_IntFree( vRes );
return nCommon;
}
void Vec_IntInsertOrder( Vec_Int_t * vLits, Vec_Int_t * vClasses, int Lit, int Class )
{
int i;
for ( i = Vec_IntSize(vClasses)-1; i >= 0; i-- )
if ( Vec_IntEntry(vClasses,i) >= Class )
break;
Vec_IntInsert( vLits, i+1, Lit );
Vec_IntInsert( vClasses, i+1, Class );
}
void Acec_MoveDuplicates( Vec_Wec_t * vLits, Vec_Wec_t * vClasses )
{
Vec_Int_t * vLevel1, * vLevel2;
int i, k, Prev, This, Entry;
Vec_WecForEachLevel( vLits, vLevel1, i )
{
if ( i == Vec_WecSize(vLits) - 1 )
break;
vLevel2 = Vec_WecEntry(vClasses, i);
assert( Vec_IntSize(vLevel1) == Vec_IntSize(vLevel2) );
Prev = -1;
Vec_IntForEachEntry( vLevel2, This, k )
{
if ( Prev != This )
{
Prev = This;
continue;
}
Prev = -1;
Entry = Vec_IntEntry( vLevel1, k );
Vec_IntDrop( vLevel1, k );
Vec_IntDrop( vLevel2, k-- );
Vec_IntDrop( vLevel1, k );
Vec_IntDrop( vLevel2, k-- );
Vec_IntInsertOrder( Vec_WecEntry(vLits, i+1), Vec_WecEntry(vClasses, i+1), Entry, This );
assert( Vec_IntSize(vLevel1) == Vec_IntSize(vLevel2) );
assert( Vec_IntSize(Vec_WecEntry(vLits, i+1)) == Vec_IntSize(Vec_WecEntry(vClasses, i+1)) );
}
}
}
void Acec_MatchCheckShift( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Vec_Wec_t * vLits0, Vec_Wec_t * vLits1, Vec_Int_t * vMap0, Vec_Int_t * vMap1, Vec_Wec_t * vRoots0, Vec_Wec_t * vRoots1 )
{
Vec_Wec_t * vRes0 = Acec_MatchCopy( vLits0, vMap0 );
......@@ -318,14 +362,20 @@ void Acec_MatchCheckShift( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Vec_Wec_t * vLi
{
Vec_WecInsertLevel( vLits0, 0 );
Vec_WecInsertLevel( vRoots0, 0 );
Vec_WecInsertLevel( vRes0, 0 );
printf( "Shifted one level up.\n" );
}
else if ( nCommonMinus > nCommonPlus && nCommonMinus > nCommon )
{
Vec_WecInsertLevel( vLits1, 0 );
Vec_WecInsertLevel( vRoots1, 0 );
Vec_WecInsertLevel( vRes1, 0 );
printf( "Shifted one level down.\n" );
}
Acec_MoveDuplicates( vLits0, vRes0 );
Acec_MoveDuplicates( vLits1, vRes1 );
//Vec_WecPrintLits( vLits1 );
//printf( "Input literals:\n" );
//Vec_WecPrintLits( vLits0 );
//printf( "Equiv classes:\n" );
......@@ -410,6 +460,10 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
printf( "Box0: Matched %d entries out of %d.\n", nTotal, Vec_WecSizeSize(pBox0->vLeafLits) );
printf( "Box1: Matched %d entries out of %d.\n", nTotal, Vec_WecSizeSize(pBox1->vLeafLits) );
//Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vShared, Vec_IntArray(vMap0), 0 );
//Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vShared, Vec_IntArray(vMap1), 0 );
//printf( "\n" );
//Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vUnique, Vec_IntArray(vMap0), 0 );
//Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vUnique, Vec_IntArray(vMap1), 0 );
......@@ -448,8 +502,8 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
printf( "Cannot match arithmetic boxes in LHS and RHS. Trying regular CEC.\n" );
else
{
pGia0n = Acec_InsertBox( pBox0, 1 );
pGia1n = Acec_InsertBox( pBox1, 1 );
pGia0n = Acec_InsertBox( pBox0, 0 );
pGia1n = Acec_InsertBox( pBox1, 0 );
printf( "Matching of adder trees in LHS and RHS succeeded. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// remove the last output
......
src/proof/acec/acecNorm.c
......@@ -76,9 +76,19 @@ Vec_Int_t * Acec_InsertTree( Gia_Man_t * pNew, Vec_Wec_t * vLeafMap )
{
if ( Vec_IntSize(vLevel) == 2 )
Vec_IntPush( vLevel, 0 );
In[2] = Vec_IntPop( vLevel );
In[1] = Vec_IntPop( vLevel );
In[0] = Vec_IntPop( vLevel );
//In[2] = Vec_IntPop( vLevel );
//In[1] = Vec_IntPop( vLevel );
//In[0] = Vec_IntPop( vLevel );
In[0] = Vec_IntEntry( vLevel, 0 );
Vec_IntDrop( vLevel, 0 );
In[1] = Vec_IntEntry( vLevel, 0 );
Vec_IntDrop( vLevel, 0 );
In[2] = Vec_IntEntry( vLevel, 0 );
Vec_IntDrop( vLevel, 0 );
Acec_InsertFadd( pNew, In, Out );
Vec_IntPush( vLevel, Out[0] );
if ( i+1 < Vec_WecSize(vLeafMap) )
......@@ -114,11 +124,22 @@ int Acec_InsertBox_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
Acec_InsertBox_rec( pNew, p, Gia_ObjFanin1(pObj) );
return (pObj->Value = Gia_ManAppendAnd2( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ));
}
Vec_Int_t * Acec_BuildTree( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Wec_t * vLeafLits )
Vec_Int_t * Acec_BuildTree( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Int_t * vRootLits )
{
Vec_Wec_t * vLeafMap = Vec_WecStart( Vec_WecSize(vLeafLits) );
Vec_Int_t * vLevel, * vRootRanks;
int i, k, iLit, iLitNew;
// add roo literals
if ( vRootLits )
Vec_IntForEachEntry( vRootLits, iLit, i )
{
if ( i < Vec_WecSize(vLeafMap) )
vLevel = Vec_WecEntry(vLeafMap, i);
else
vLevel = Vec_WecPushLevel(vLeafMap);
Vec_IntPush( vLevel, iLit );
}
// add other literals
Vec_WecForEachLevel( vLeafLits, vLevel, i )
Vec_IntForEachEntry( vLevel, iLit, k )
{
......@@ -137,7 +158,7 @@ Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll )
Gia_Man_t * p = pBox->pGia;
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
Vec_Int_t * vRootRanks, * vLevel;
Vec_Int_t * vRootRanks, * vLevel, * vTemp;
int i, k, iLit, iLitNew;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
......@@ -148,26 +169,14 @@ Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll )
pObj->Value = Gia_ManAppendCi( pNew );
// implement tree
if ( fAll )
vRootRanks = Acec_BuildTree( pNew, p, pBox->vLeafLits );
vRootRanks = Acec_BuildTree( pNew, p, pBox->vLeafLits, NULL );
else
{
Vec_Wec_t * vLeafLits;
assert( pBox->vShared != NULL );
assert( pBox->vUnique != NULL );
vRootRanks = Acec_BuildTree( p, p, pBox->vShared );
// add these roots to the unique ones
vLeafLits = Vec_WecDup( pBox->vUnique );
Vec_IntForEachEntry( vRootRanks, iLit, i )
{
if ( i < Vec_WecSize(vLeafLits) )
vLevel = Vec_WecEntry(vLeafLits, i);
else
vLevel = Vec_WecPushLevel(vLeafLits);
Vec_IntPush( vLevel, iLit );
}
Vec_IntFree( vRootRanks );
vRootRanks = Acec_BuildTree( pNew, p, vLeafLits );
Vec_WecFree( vLeafLits );
vRootRanks = Acec_BuildTree( pNew, p, pBox->vShared, NULL );
vRootRanks = Acec_BuildTree( pNew, p, pBox->vUnique, vTemp = vRootRanks );
Vec_IntFree( vTemp );
}
// update polarity of literals
Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
......
src/proof/acec/acecTree.c
......@@ -207,6 +207,9 @@ void Acec_TreeFilterOne2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree )
Gia_ManForEachAnd( p, pObj, i )
if ( Vec_BitEntry(vIsLeaf, i) )
Acec_TreeMarkTFI_rec( p, i, vMarked );
// additional one
//if ( 10942 < Gia_ManObjNum(p) )
// Acec_TreeMarkTFI_rec( p, 10942, vMarked );
// remove those that overlap with the marked TFI
Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
{
......@@ -419,7 +422,7 @@ Vec_Int_t * Acec_TreeFindPoints( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * v
int i;
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
{
if ( vIgnore && (Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+3)) && Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+4))) )
if ( vIgnore && (Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+3)) || Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+4))) )
continue;
Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+0), i, 0 );
Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+1), i, 0 );
......
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