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

Updated to arithmetic verification.

This commit is contained in:
Alan Mishchenko 2017-01-09 19:50:05 +07:00
parent ab6a87a4db
commit fbdf28e4c9
6 changed files with 527 additions and 65 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -3879,12 +3879,20 @@ Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p )
int i, iObj, iObj2, fFlip, Count1 = 0;
Vec_Int_t * vXors, * vPart[2], * vOrder;
Gia_Obj_t * pFan[2], * pObj = Gia_ManCo(p, 0);
assert( Gia_ManCoNum(p) == 1 );
vXors = Vec_IntAlloc( 100 );
if ( Gia_ObjFaninC0(pObj) )
Gia_ManCollectTopXors_rec( p, Gia_ObjFanin0(pObj), vXors );
if ( Gia_ManCoNum(p) == 1 )
{
if ( Gia_ObjFaninC0(pObj) )
Gia_ManCollectTopXors_rec( p, Gia_ObjFanin0(pObj), vXors );
else
Vec_IntPush( vXors, Gia_ObjId(p, Gia_ObjFanin0(pObj)) );
}
else
Vec_IntPush( vXors, Gia_ObjId(p, Gia_ObjFanin0(pObj)) );
{
Gia_ManForEachCo( p, pObj, i )
if ( Gia_ObjFaninId0p(p, pObj) > 0 )
Vec_IntPush( vXors, Gia_ObjFaninId0p(p, pObj) );
}
// order by support size
Gia_ManDupDemiterOrderXors( p, vXors );
//Vec_IntPrint( vXors );

146
src/base/abci/abc.c
View File

@ -40532,14 +40532,12 @@ usage:
int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pFile;
Cec_ParCec_t ParsCec, * pPars = &ParsCec;
Gia_Man_t * pSecond;
char * FileName, * pTemp;
Acec_ParCec_t ParsCec, * pPars = &ParsCec;
char ** pArgvNew;
int c, nArgcNew, fMiter = 0, fDualOutput = 0, fTwoOutput = 0;
Cec_ManCecSetDefaultParams( pPars );
int c, nArgcNew;
Acec_ManCecSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdtvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CTmdtvh" ) ) != EOF )
{
switch ( c )
{
@ -40565,17 +40563,14 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->TimeLimit < 0 )
goto usage;
break;
case 'n':
pPars->fNaive ^= 1;
break;
case 'm':
fMiter ^= 1;
pPars->fMiter ^= 1;
break;
case 'd':
fDualOutput ^= 1;
pPars->fDualOutput ^= 1;
break;
case 't':
fTwoOutput ^= 1;
pPars->fTwoOutput ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
@ -40586,15 +40581,20 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
if ( fMiter )
if ( pPars->fMiter )
{
Gia_Man_t * pGia0, * pGia1, * pDual;
if ( argc != globalUtilOptind )
{
Abc_Print( -1, "Abc_CommandAbc9Acec(): If the input is a miter, it cannot be given on the command line.\n" );
return 1;
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Acec(): There is no AIG.\n" );
return 1;
}
if ( fDualOutput )
if ( pPars->fDualOutput )
{
if ( Gia_ManPoNum(pAbc->pGia) & 1 )
{
@ -40604,28 +40604,28 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( !pPars->fSilent )
Abc_Print( 1, "Assuming the current network is a double-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
Gia_ManDemiterDual( pAbc->pGia, &pGia0, &pGia1 );
pAbc->Status = Gia_PolynCec( pGia0, pGia1, pPars );
pAbc->Status = Acec_Solve( pGia0, pGia1, pPars );
}
else if ( fTwoOutput )
else if ( pPars->fTwoOutput )
{
if ( Gia_ManPoNum(pAbc->pGia) & 1 )
{
Abc_Print( -1, "The dual-output miter should have an even number of outputs.\n" );
Abc_Print( -1, "The two-output miter should have an even number of outputs.\n" );
return 1;
}
if ( !pPars->fSilent )
Abc_Print( 1, "Assuming the current network is a two-word miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
Gia_ManDemiterTwoWords( pAbc->pGia, &pGia0, &pGia1 );
pAbc->Status = Gia_PolynCec( pGia0, pGia1, pPars );
pAbc->Status = Acec_Solve( pGia0, pGia1, pPars );
}
else
else // regular single- or multi-output miter
{
if ( !pPars->fSilent )
Abc_Print( 1, "Assuming the current network is a single-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
Abc_Print( 1, "Assuming the current network is a regular single- or multi-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
pDual = Gia_ManDemiterToDual( pAbc->pGia );
Gia_ManDemiterDual( pDual, &pGia0, &pGia1 );
Gia_ManStop( pDual );
pAbc->Status = Gia_PolynCec( pGia0, pGia1, pPars );
pAbc->Status = Acec_Solve( pGia0, pGia1, pPars );
}
Abc_FrameReplaceCex( pAbc, &pGia0->pCexComb );
Gia_ManStop( pGia0 );
@ -40635,52 +40635,96 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
pArgvNew = argv + globalUtilOptind;
nArgcNew = argc - globalUtilOptind;
if ( nArgcNew != 1 )
if ( nArgcNew == 0 || nArgcNew == 1 )
{
if ( pAbc->pGia->pSpec == NULL )
Gia_Man_t * pSecond;
char * pTemp, * FileName = NULL;
if ( nArgcNew == 0 )
{
Abc_Print( -1, "File name is not given on the command line.\n" );
return 1;
FileName = pAbc->pGia->pSpec;
if ( FileName == NULL )
{
Abc_Print( -1, "File name is not given on the command line.\n" );
return 1;
}
}
FileName = pAbc->pGia->pSpec;
else // if ( nArgcNew == 1 )
{
FileName = pArgvNew[0];
// fix the wrong symbol
for ( pTemp = FileName; *pTemp; pTemp++ )
if ( *pTemp == '>' )
*pTemp = '\\';
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) )
Abc_Print( 1, "Did you mean \"%s\"?", FileName );
Abc_Print( 1, "\n" );
return 1;
}
fclose( pFile );
}
pSecond = Gia_AigerRead( FileName, 0, 0, 0 );
if ( pSecond == NULL )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );
return 0;
}
pAbc->Status = Acec_Solve( pAbc->pGia, pSecond, pPars );
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
Gia_ManStop( pSecond );
}
else if ( nArgcNew == 2 )
{
Gia_Man_t * pGias[2] = {NULL}; int i;
char * pTemp, * FileName[2] = { pArgvNew[0], pArgvNew[1] };
for ( i = 0; i < 2; i++ )
{
// fix the wrong symbol
for ( pTemp = FileName[i]; *pTemp; pTemp++ )
if ( *pTemp == '>' )
*pTemp = '\\';
if ( (pFile = fopen( FileName[i], "r" )) == NULL )
{
Abc_Print( -1, "Cannot open input file \"%s\". ", FileName[i] );
if ( (FileName[i] = Extra_FileGetSimilarName( FileName[i], ".aig", NULL, NULL, NULL, NULL )) )
Abc_Print( 1, "Did you mean \"%s\"?", FileName[i] );
Abc_Print( 1, "\n" );
return 1;
}
fclose( pFile );
pGias[i] = Gia_AigerRead( FileName[i], 0, 0, 0 );
if ( pGias[i] == NULL )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );
return 0;
}
}
pAbc->Status = Acec_Solve( pGias[0], pGias[1], pPars );
Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb );
Gia_ManStop( pGias[0] );
Gia_ManStop( pGias[1] );
}
else
FileName = pArgvNew[0];
// fix the wrong symbol
for ( pTemp = FileName; *pTemp; pTemp++ )
if ( *pTemp == '>' )
*pTemp = '\\';
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) )
Abc_Print( 1, "Did you mean \"%s\"?", FileName );
Abc_Print( 1, "\n" );
Abc_Print( -1, "Too many command-line arguments.\n" );
return 1;
}
fclose( pFile );
pSecond = Gia_AigerRead( FileName, 0, 0, 0 );
if ( pSecond == NULL )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );
return 0;
}
pAbc->Status = Gia_PolynCec( pAbc->pGia, pSecond, pPars );
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
Gia_ManStop( pSecond );
return 0;
usage:
Abc_Print( -2, "usage: &acec [-CT num] [-nmdtvh]\n" );
Abc_Print( -2, "usage: &acec [-CT num] [-mdtvh] <file1> <file2>\n" );
Abc_Print( -2, "\t combinational equivalence checking for arithmetic circuits\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
Abc_Print( -2, "\t-n : toggle using naive SAT-based checking [default = %s]\n", pPars->fNaive? "yes":"no");
Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits");
Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no");
Abc_Print( -2, "\t-t : toggle using two-word miter [default = %s]\n", fTwoOutput? "yes":"no");
Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", pPars->fMiter? "miter":"two circuits");
Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", pPars->fDualOutput? "yes":"no");
Abc_Print( -2, "\t-t : toggle using two-word miter [default = %s]\n", pPars->fTwoOutput? "yes":"no");
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\tfile1 : (optional) the file with the first network\n");
Abc_Print( -2, "\tfile2 : (optional) the file with the second network\n");
return 1;
}

18
src/proof/acec/acec.h
View File

@ -38,6 +38,21 @@ ABC_NAMESPACE_HEADER_START
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
// combinational equivalence checking parameters
typedef struct Acec_ParCec_t_ Acec_ParCec_t;
struct Acec_ParCec_t_
{
int nBTLimit; // conflict limit at a node
int TimeLimit; // the runtime limit in seconds
int fMiter; // input circuit is a miter
int fDualOutput; // dual-output miter
int fTwoOutput; // two-output miter
int fSilent; // print no messages
int fVeryVerbose; // verbose stats
int fVerbose; // verbose stats
int iOutFail; // the number of failed output
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -51,7 +66,8 @@ ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/*=== acecCore.c ========================================================*/
extern int Gia_PolynCec( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Cec_ParCec_t * pPars );
extern void Acec_ManCecSetDefaultParams( Acec_ParCec_t * p );
extern int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars );
/*=== acecFadds.c ========================================================*/
extern Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose, Vec_Int_t ** vCutsXor2 );
extern Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose );

383
src/proof/acec/acecCore.c
View File

@ -19,6 +19,7 @@
***********************************************************************/
#include "acecInt.h"
#include "proof/cec/cec.h"
ABC_NAMESPACE_IMPL_START
@ -31,6 +32,31 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [This procedure sets default parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acec_ManCecSetDefaultParams( Acec_ParCec_t * p )
{
memset( p, 0, sizeof(Acec_ParCec_t) );
p->nBTLimit = 1000; // conflict limit at a node
p->TimeLimit = 0; // the runtime limit in seconds
p->fMiter = 0; // input circuit is a miter
p->fDualOutput = 0; // dual-output miter
p->fTwoOutput = 0; // two-output miter
p->fSilent = 0; // print no messages
p->fVeryVerbose = 0; // verbose stats
p->fVerbose = 0; // verbose stats
p->iOutFail = -1; // the number of failed output
}
/**Function*************************************************************
Synopsis []
@ -42,15 +68,356 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
int Gia_PolynCec( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Cec_ParCec_t * pPars )
void Acec_BoxFree( Acec_Box_t * pBox )
{
Vec_Int_t * vOrder0 = Gia_PolynReorder( pGia0, pPars->fVerbose, pPars->fVeryVerbose );
Vec_Int_t * vOrder1 = Gia_PolynReorder( pGia1, pPars->fVerbose, pPars->fVeryVerbose );
Gia_PolynBuild( pGia0, vOrder0, 0, pPars->fVerbose, pPars->fVeryVerbose );
Gia_PolynBuild( pGia1, vOrder1, 0, pPars->fVerbose, pPars->fVeryVerbose );
Vec_IntFree( vOrder0 );
Vec_IntFree( vOrder1 );
return 1;
Vec_WecFree( pBox->vUnique );
Vec_WecFree( pBox->vShared );
Vec_WecFree( pBox->vLeafLits );
Vec_WecFree( pBox->vRootLits );
ABC_FREE( pBox );
}
void Acec_BoxFreeP( Acec_Box_t ** ppBox )
{
if ( *ppBox )
Acec_BoxFree( *ppBox );
*ppBox = NULL;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acec_InsertHadd( Gia_Man_t * pNew, int In[2], int Out[2] )
{
int And, Or;
Out[1] = Gia_ManAppendAnd2( pNew, In[0], In[1] );
And = Gia_ManAppendAnd2( pNew, Abc_LitNot(In[0]), Abc_LitNot(In[1]) );
Or = Gia_ManAppendOr2( pNew, Out[1], And );
Out[0] = Abc_LitNot( Or );
}
void Acec_InsertFadd( Gia_Man_t * pNew, int In[3], int Out[2] )
{
int In2[2], Out1[2], Out2[2];
Acec_InsertHadd( pNew, In, Out1 );
In2[0] = Out1[0];
In2[1] = In[2];
Acec_InsertHadd( pNew, In2, Out2 );
Out[0] = Out2[0];
Out[1] = Gia_ManAppendOr2( pNew, Out1[1], Out2[1] );
}
Vec_Int_t * Acec_InsertTree( Gia_Man_t * pNew, Vec_Wec_t * vLeafMap )
{
Vec_Int_t * vRootRanks = Vec_IntAlloc( Vec_WecSize(vLeafMap) + 5 );
Vec_Int_t * vLevel;
int i, In[3], Out[2];
Vec_WecForEachLevel( vLeafMap, vLevel, i )
{
if ( Vec_IntSize(vLevel) == 0 )
{
Vec_IntPush( vRootRanks, 0 );
continue;
}
while ( Vec_IntSize(vLevel) > 1 )
{
if ( Vec_IntSize(vLevel) == 2 )
Vec_IntPush( vLevel, 0 );
In[0] = Vec_IntPop( vLevel );
In[1] = Vec_IntPop( vLevel );
In[2] = Vec_IntPop( vLevel );
Acec_InsertFadd( pNew, In, Out );
Vec_IntPush( vLevel, Out[0] );
if ( i-1 < Vec_WecSize(vLeafMap) )
vLevel = Vec_WecEntry(vLeafMap, i+1);
else
vLevel = Vec_WecPushLevel(vLeafMap);
Vec_IntPush( vLevel, Out[1] );
}
assert( Vec_IntSize(vLevel) == 1 );
Vec_IntPush( vRootRanks, Vec_IntEntry(vLevel, 0) );
}
return vRootRanks;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Acec_FindEquivs( Gia_Man_t * pBase, Gia_Man_t * pAdd )
{
Gia_Obj_t * pObj;
int i;
Gia_ManFillValue( pAdd );
Gia_ManConst0(pAdd)->Value = 0;
if ( pBase == NULL )
{
pBase = Gia_ManStart( Gia_ManObjNum(pAdd) );
pBase->pName = Abc_UtilStrsav( pAdd->pName );
pBase->pSpec = Abc_UtilStrsav( pAdd->pSpec );
Gia_ManForEachCi( pAdd, pObj, i )
pObj->Value = Gia_ManAppendCi(pBase);
Gia_ManHashAlloc( pBase );
}
else
{
assert( Gia_ManCiNum(pBase) == Gia_ManCiNum(pAdd) );
Gia_ManForEachCi( pAdd, pObj, i )
pObj->Value = Gia_Obj2Lit( pBase, Gia_ManCi(pBase, i) );
}
Gia_ManForEachAnd( pAdd, pObj, i )
pObj->Value = Gia_ManHashAnd( pBase, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
return pBase;
}
Vec_Int_t * Acec_CountRemap( Gia_Man_t * pAdd )
{
Gia_Obj_t * pObj; int i;
Vec_Int_t * vMapNew = Vec_IntStartFull( Gia_ManObjNum(pAdd) );
Gia_ManForEachCand( pAdd, pObj, i )
Vec_IntWriteEntry( vMapNew, i, Abc_Lit2Var(pObj->Value) );
return vMapNew;
}
void Acec_ComputeEquivClasses( Gia_Man_t * pOne, Gia_Man_t * pTwo, Vec_Int_t ** pvMap1, Vec_Int_t ** pvMap2 )
{
Gia_Man_t * pBase;
pBase = Acec_FindEquivs( NULL, pOne );
pBase = Acec_FindEquivs( pBase, pTwo );
*pvMap1 = Acec_CountRemap( pOne );
*pvMap2 = Acec_CountRemap( pTwo );
Gia_ManStop( pBase );
}
static inline void Acec_MatchBoxesSort( int * pArray, int nSize, int * pCosts )
{
int i, j, best_i;
for ( i = 0; i < nSize-1; i++ )
{
best_i = i;
for ( j = i+1; j < nSize; j++ )
if ( pCosts[Abc_Lit2Var(pArray[j])] > pCosts[Abc_Lit2Var(pArray[best_i])] )
best_i = j;
ABC_SWAP( int, pArray[i], pArray[best_i] );
}
}
int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
{
Vec_Int_t * vMap0, * vMap1, * vLevel;
int i, nSize, nTotal;
Acec_ComputeEquivClasses( pBox0->pGia, pBox1->pGia, &vMap0, &vMap1 );
// sort nodes in the classes by their equivalences
Vec_WecForEachLevel( pBox0->vLeafLits, vLevel, i )
Acec_MatchBoxesSort( Vec_IntArray(vLevel), Vec_IntSize(vLevel), Vec_IntArray(vMap0) );
Vec_WecForEachLevel( pBox1->vLeafLits, vLevel, i )
Acec_MatchBoxesSort( Vec_IntArray(vLevel), Vec_IntSize(vLevel), Vec_IntArray(vMap1) );
// reorder nodes to have the same order
assert( pBox0->vShared == NULL );
assert( pBox1->vShared == NULL );
pBox0->vShared = Vec_WecStart( Vec_WecSize(pBox0->vLeafLits) );
pBox1->vShared = Vec_WecStart( Vec_WecSize(pBox1->vLeafLits) );
pBox0->vUnique = Vec_WecStart( Vec_WecSize(pBox0->vLeafLits) );
pBox1->vUnique = Vec_WecStart( Vec_WecSize(pBox1->vLeafLits) );
nSize = Abc_MinInt( Vec_WecSize(pBox0->vLeafLits), Vec_WecSize(pBox1->vLeafLits) );
Vec_WecForEachLevelStart( pBox0->vLeafLits, vLevel, i, nSize )
Vec_IntAppend( Vec_WecEntry(pBox0->vUnique, i), vLevel );
Vec_WecForEachLevelStart( pBox1->vLeafLits, vLevel, i, nSize )
Vec_IntAppend( Vec_WecEntry(pBox1->vUnique, i), vLevel );
for ( i = 0; i < nSize; i++ )
{
Vec_Int_t * vShared0 = Vec_WecEntry( pBox0->vShared, i );
Vec_Int_t * vShared1 = Vec_WecEntry( pBox1->vShared, i );
Vec_Int_t * vUnique0 = Vec_WecEntry( pBox0->vUnique, i );
Vec_Int_t * vUnique1 = Vec_WecEntry( pBox1->vUnique, i );
Vec_Int_t * vLevel0 = Vec_WecEntry( pBox0->vLeafLits, i );
Vec_Int_t * vLevel1 = Vec_WecEntry( pBox1->vLeafLits, i );
int * pBeg0 = Vec_IntArray(vLevel0);
int * pBeg1 = Vec_IntArray(vLevel1);
int * pEnd0 = Vec_IntLimit(vLevel0);
int * pEnd1 = Vec_IntLimit(vLevel1);
while ( pBeg0 < pEnd0 && pBeg1 < pEnd1 )
{
if ( *pBeg0 == *pBeg1 )
{
Vec_IntPush( vShared0, *pBeg0++ );
Vec_IntPush( vShared1, *pBeg1++ );
}
else if ( *pBeg0 > *pBeg1 )
Vec_IntPush( vUnique0, *pBeg0++ );
else
Vec_IntPush( vUnique1, *pBeg1++ );
}
while ( pBeg0 < pEnd0 )
Vec_IntPush( vUnique0, *pBeg0++ );
while ( pBeg1 < pEnd1 )
Vec_IntPush( vUnique1, *pBeg1++ );
assert( Vec_IntSize(vShared0) == Vec_IntSize(vShared1) );
assert( Vec_IntSize(vShared0) + Vec_IntSize(vUnique0) == Vec_IntSize(vLevel0) );
assert( Vec_IntSize(vShared1) + Vec_IntSize(vUnique1) == Vec_IntSize(vLevel1) );
}
nTotal = Vec_WecSizeSize(pBox0->vShared);
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) );
return nTotal;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Acec_InsertBox_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( ~pObj->Value )
return pObj->Value;
assert( Gia_ObjIsAnd(pObj) );
Acec_InsertBox_rec( pNew, p, Gia_ObjFanin0(pObj) );
Acec_InsertBox_rec( pNew, p, Gia_ObjFanin1(pObj) );
return (pObj->Value = Gia_ManAppendAnd( 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_Wec_t * vLeafMap = Vec_WecStart( Vec_WecSize(vLeafLits) );
Vec_Int_t * vLevel, * vRootRanks;
int i, k, iLit, iLitNew;
Vec_WecForEachLevel( vLeafLits, vLevel, i )
Vec_IntForEachEntry( vLevel, iLit, k )
{
Gia_Obj_t * pObj = Gia_ManObj( p, Abc_Lit2Var(iLit) );
iLitNew = Acec_InsertBox_rec( pNew, p, pObj );
iLitNew = Abc_LitNotCond( iLitNew, Abc_LitIsCompl(iLit) );
Vec_WecPush( vLeafMap, i, iLitNew );
}
// construct map of root literals
vRootRanks = Acec_InsertTree( pNew, vLeafMap );
Vec_WecFree( vLeafMap );
return vRootRanks;
}
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;
int i, k, iLit, iLitNew;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
// implement tree
if ( fAll )
vRootRanks = Acec_BuildTree( pNew, p, pBox->vLeafLits );
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 );
}
// update polarity of literals
Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
Vec_IntForEachEntry( vLevel, iLit, k )
{
pObj = Gia_ManObj( p, Abc_Lit2Var(iLit) );
iLitNew = k ? 0 : Vec_IntEntry( vRootRanks, k );
pObj->Value = Abc_LitNotCond( iLitNew, Abc_LitIsCompl(iLit) );
}
Vec_IntFree( vRootRanks );
// construct the outputs
Gia_ManForEachCo( p, pObj, i )
Acec_InsertBox_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachCo( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
{
int status = -1;
Gia_Man_t * pMiter;
Gia_Man_t * pGia0n = pGia0, * pGia1n = pGia1;
Cec_ParCec_t ParsCec, * pCecPars = &ParsCec;
Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0 );
Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1 );
if ( pBox0 == NULL || pBox1 == NULL ) // cannot match
printf( "Cannot find arithmetic boxes in both LHS and RHS. Trying regular CEC.\n" );
else if ( !Acec_MatchBoxes( pBox0, pBox1 ) ) // cannot find matching
printf( "Cannot match arithmetic boxes in LHS and RHS. Trying regular CEC.\n" );
else
{
pGia0n = Acec_InsertBox( pBox0, 1 );
pGia1n = Acec_InsertBox( pBox1, 1 );
printf( "Found, matched, and normalized arithmetic boxes in LHS and RHS. Solving resulting CEC.\n" );
}
// solve regular CEC problem
Cec_ManCecSetDefaultParams( pCecPars );
pCecPars->nBTLimit = pPars->nBTLimit;
pMiter = Gia_ManMiter( pGia0n, pGia1n, 0, 1, 0, 0, pPars->fVerbose );
if ( pMiter )
{
int fDumpMiter = 1;
if ( fDumpMiter )
{
Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "acec_miter.aig" );
Gia_AigerWrite( pMiter, "acec_miter.aig", 0, 0 );
}
status = Cec_ManVerify( pMiter, pCecPars );
ABC_SWAP( Abc_Cex_t *, pGia0->pCexComb, pMiter->pCexComb );
Gia_ManStop( pMiter );
}
else
printf( "Miter computation has failed.\n" );
if ( pGia0n != pGia0 )
Gia_ManStop( pGia0n );
if ( pGia1n != pGia1 )
Gia_ManStop( pGia1n );
Acec_BoxFreeP( &pBox0 );
Acec_BoxFreeP( &pBox1 );
return status;
}
////////////////////////////////////////////////////////////////////////

13
src/proof/acec/acecInt.h
View File

@ -27,7 +27,6 @@
////////////////////////////////////////////////////////////////////////
#include "aig/gia/gia.h"
#include "proof/cec/cec.h"
#include "acec.h"
////////////////////////////////////////////////////////////////////////
@ -38,6 +37,16 @@
ABC_NAMESPACE_HEADER_START
typedef struct Acec_Box_t_ Acec_Box_t;
struct Acec_Box_t_
{
Gia_Man_t * pGia; // AIG manager
Vec_Wec_t * vLeafLits; // leaf literals by rank
Vec_Wec_t * vRootLits; // root literals by rank
Vec_Wec_t * vShared; // shared leaves
Vec_Wec_t * vUnique; // unique leaves
};
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
@ -54,6 +63,8 @@ ABC_NAMESPACE_HEADER_START
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== acecPa.c ========================================================*/
extern Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p );
/*=== acecUtil.c ========================================================*/
extern void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose );
extern Vec_Int_t * Gia_PolynCollectLastXor( Gia_Man_t * pGia, int fVerbose );

16
src/proof/acec/acecPa.c
View File

@ -273,6 +273,22 @@ void Pas_ManComputeCutsTest( Gia_Man_t * p )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p )
{
return NULL;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////