Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Update sclBufSize.c #45

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open

Update sclBufSize.c #45

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
698251a
Update sclBufSize.c
marina-neseem Jun 16, 2019
cfb370a
disable SAT checking in fraig
marina-neseem Dec 14, 2019
dff0580
add -x flag to fraig command to enable approcimation
marina-neseem Dec 15, 2019
b47a2b7
modify the approximation condition
marina-neseem Dec 16, 2019
8b61091
Add approximate rewriting
marina-neseem Dec 16, 2019
aab7612
fix bug in argument passing
marina-neseem Dec 16, 2019
f527012
fix a bug in approximate rewrite
marina-neseem Dec 17, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/base/abc/abc.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -877,7 +877,7 @@ extern ABC_DLL int Abc_NodeRef_rec( Abc_Obj_t * pNode );
/*=== abcRefactor.c ==========================================================*/
extern ABC_DLL int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose );
/*=== abcRewrite.c ==========================================================*/
extern ABC_DLL int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable );
extern ABC_DLL int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable, int fApproximationEnable );
/*=== abcSat.c ==========================================================*/
extern ABC_DLL int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fVerbose, ABC_INT64_T * pNumConfs, ABC_INT64_T * pNumInspects );
extern ABC_DLL void * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes );
Expand Down
24 changes: 21 additions & 3 deletions src/base/abci/abc.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7036,6 +7036,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
int fVerbose;
int fVeryVerbose;
int fPlaceEnable;
int fApproximationEnable;
// external functions
extern void Rwr_Precompute();

Expand All @@ -7046,8 +7047,9 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
fVerbose = 0;
fVeryVerbose = 0;
fPlaceEnable = 0;
fApproximationEnable = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "lxzvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "lxzvwha" ) ) != EOF )
{
switch ( c )
{
Expand All @@ -7069,6 +7071,15 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'p':
fPlaceEnable ^= 1;
break;
case 'a':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-a\" should be followed by an integer.\n" );
goto usage;
}
fApproximationEnable = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'h':
goto usage;
default:
Expand Down Expand Up @@ -7099,7 +7110,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
}

// modify the current network
if ( !Abc_NtkRewrite( pNtk, fUpdateLevel, fUseZeros, fVerbose, fVeryVerbose, fPlaceEnable ) )
if ( !Abc_NtkRewrite( pNtk, fUpdateLevel, fUseZeros, fVerbose, fVeryVerbose, fPlaceEnable, fApproximationEnable ) )
{
Abc_Print( -1, "Rewriting has failed.\n" );
return 1;
Expand All @@ -7113,6 +7124,8 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -2, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printout subgraph statistics [default = %s]\n", fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-a : toggle how many bits are neglected to do approximation while rewriting [default = %d] [max = 3]\n", fApproximationEnable);

// Abc_Print( -2, "\t-p : toggle placement-aware rewriting [default = %s]\n", fPlaceEnable? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
Expand Down Expand Up @@ -15969,8 +15982,9 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
pParams->fTryProve = 0; // tries to solve the final miter
pParams->fVerbose = 0; // the verbosiness flag
pParams->fVerboseP = 0; // the verbosiness flag
pParams->approximate= 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscptvaeh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscptvaehx" ) ) != EOF )
{
switch ( c )
{
Expand Down Expand Up @@ -16032,6 +16046,9 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'e':
fExdc ^= 1;
break;
case 'x':
pParams->approximate ^= 1;
break;
case 'h':
goto usage;
default:
Expand Down Expand Up @@ -16107,6 +16124,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -2, "\t-e : toggle functional sweeping using EXDC [default = %s]\n", fExdc? "yes": "no" );
Abc_Print( -2, "\t-a : toggle between all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "dfs" );
Abc_Print( -2, "\t-t : toggle using partitioned representation [default = %s]\n", fPartition? "yes": "no" );
Abc_Print( -2, "\t-x : toggle doing approximations [default = %s]\n", pParams->approximate? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
Expand Down
6 changes: 3 additions & 3 deletions src/base/abci/abcFraig.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -133,7 +133,7 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExd
Extra_ProgressBarUpdate( pProgress, i, NULL );
pNode->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan,
Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, (int)Abc_ObjFaninC0(pNode) ),
Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, (int)Abc_ObjFaninC1(pNode) ) );
Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, (int)Abc_ObjFaninC1(pNode) ), ((Fraig_Params_t *)pParams)->approximate );
}
if ( pProgress )
Extra_ProgressBarStop( pProgress );
Expand Down Expand Up @@ -189,7 +189,7 @@ Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc
Abc_AigForEachAnd( pNtkStrash, pObj, i )
pObj->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan,
Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFaninC0(pObj) ),
Fraig_NotCond( Abc_ObjFanin1(pObj)->pCopy, (int)Abc_ObjFaninC1(pObj) ) );
Fraig_NotCond( Abc_ObjFanin1(pObj)->pCopy, (int)Abc_ObjFaninC1(pObj) ),0 );
// get the EXDC to be returned
pObj = Abc_NtkPo( pNtkStrash, 0 );
gResult = Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFaninC0(pObj) );
Expand Down Expand Up @@ -234,7 +234,7 @@ void Abc_NtkFraigRemapUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
Abc_NtkForEachNode( pNtk, pNode, i )
if ( pNode->pCopy )
{
gNodeNew = Fraig_NodeAnd( pMan, (Fraig_Node_t *)pNode->pCopy, Fraig_Not(gNodeExdc) );
gNodeNew = Fraig_NodeAnd( pMan, (Fraig_Node_t *)pNode->pCopy, Fraig_Not(gNodeExdc) ,0);
if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(gNodeNew), (char ***)&ppSlot ) )
*ppSlot = NULL;
pNode->pNext = *ppSlot;
Expand Down
4 changes: 2 additions & 2 deletions src/base/abci/abcIvy.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -552,10 +552,10 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
pParams->fUseRewriting = 0;
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0, 0 );
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
//printf( "After rwsat = %d. ", Abc_NtkNodeNum(pNtk) );
//ABC_PRT( "Time", Abc_Clock() - clk );
Expand Down
6 changes: 3 additions & 3 deletions src/base/abci/abcProve.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -146,7 +146,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
if ( --Counter == 0 )
break;
*/
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0, 0 );
if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
break;
if ( --Counter == 0 )
Expand Down Expand Up @@ -337,9 +337,9 @@ void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, abctime clk, int fVerb
Abc_Ntk_t * Abc_NtkMiterRwsat( Abc_Ntk_t * pNtk )
{
Abc_Ntk_t * pNtkTemp;
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0, 0 );
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp );
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
return pNtk;
}
Expand Down
4 changes: 2 additions & 2 deletions src/base/abci/abcQuant.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,14 +50,14 @@ void Abc_NtkSynthesize( Abc_Ntk_t ** ppNtk, int fMoreEffort )

pNtk = *ppNtk;

Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );

if ( fMoreEffort )
{
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );
Expand Down
4 changes: 2 additions & 2 deletions src/base/abci/abcRewrite.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ extern void Abc_PlaceUpdate( Vec_Ptr_t * vAddedCells, Vec_Ptr_t * vUpdatedNets
SeeAlso []

***********************************************************************/
int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable )
int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable, int fApproximationEnable )
{
extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
ProgressBar * pProgress;
Expand Down Expand Up @@ -122,7 +122,7 @@ Rwr_ManAddTimeCuts( pManRwr, Abc_Clock() - clk );
continue;

// for each cut, try to resynthesize it
nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUpdateLevel, fUseZeros, fPlaceEnable );
nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUpdateLevel, fUseZeros, fPlaceEnable, fApproximationEnable );
if ( !(nGain > 0 || (nGain == 0 && fUseZeros)) )
continue;
// if we end up here, a rewriting step is accepted
Expand Down
2 changes: 1 addition & 1 deletion src/base/abci/abcSweep.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,7 @@ void Abc_NtkFraigSweepUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
// get the FRAIG node
gNode = Fraig_NotCond( Abc_ObjRegular(pNodeAig)->pCopy, (int)Abc_ObjIsComplement(pNodeAig) );
// perform ANDing with EXDC
gNodeRes = Fraig_NodeAnd( pMan, gNode, Fraig_Not(gNodeExdc) );
gNodeRes = Fraig_NodeAnd( pMan, gNode, Fraig_Not(gNodeExdc),0 );
// write the node back
Abc_ObjRegular(pNodeAig)->pCopy = (Abc_Obj_t *)Fraig_NotCond( gNodeRes, (int)Abc_ObjIsComplement(pNodeAig) );
}
Expand Down
3 changes: 2 additions & 1 deletion src/map/scl/sclBufSize.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -406,7 +406,8 @@ void Abc_SclBufSize( Bus_Man_t * p, float Gain )
Abc_NtkForEachObjReverse( p->pNtk, pObj, i )
{
if ( !((Abc_ObjIsNode(pObj) && Abc_ObjFaninNum(pObj) > 0) || (Abc_ObjIsCi(pObj) && p->pPiDrive)) )
continue;
if(!(Abc_ObjIsPi(pObj) && p->pPars->fBufPis) )
continue;
if ( 2 * nObjsOld < Abc_NtkObjNumMax(p->pNtk) )
{
printf( "Buffering could not be completed because the gain value (%d) is too low.\n", p->pPars->GainRatio );
Expand Down
2 changes: 1 addition & 1 deletion src/opt/rwr/rwr.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,7 @@ static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c ) { return (Rwr_N
/*=== rwrDec.c ========================================================*/
extern void Rwr_ManPreprocess( Rwr_Man_t * p );
/*=== rwrEva.c ========================================================*/
extern int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUpdateLevel, int fUseZeros, int fPlaceEnable );
extern int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUpdateLevel, int fUseZeros, int fPlaceEnableint, int fApproximationEnable );
extern void Rwr_ScoresClean( Rwr_Man_t * p );
extern void Rwr_ScoresReport( Rwr_Man_t * p );
/*=== rwrLib.c ========================================================*/
Expand Down
12 changes: 10 additions & 2 deletions src/opt/rwr/rwrEva.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ static int Rwr_NodeGetDepth_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves );
SeeAlso []

***********************************************************************/
int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUpdateLevel, int fUseZeros, int fPlaceEnable )
int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUpdateLevel, int fUseZeros, int fPlaceEnable, int fApproximationEnable )
{
int fVeryVerbose = 0;
Dec_Graph_t * pGraph;
Expand Down Expand Up @@ -98,7 +98,15 @@ clk = Abc_Clock();
// Cut_CutPrint( pCut, 0 ), printf( "\n" );

// get the fanin permutation
uTruth = 0xFFFF & *Cut_CutReadTruth(pCut);
if (fApproximationEnable == 0)
uTruth = 0xFFFF & *Cut_CutReadTruth(pCut);
else if (fApproximationEnable == 1)
uTruth = 0xFFFE & *Cut_CutReadTruth(pCut);
else if (fApproximationEnable == 2)
uTruth = 0xFFFC & *Cut_CutReadTruth(pCut);
else
uTruth = 0xFFF8 & *Cut_CutReadTruth(pCut);

pPerm = p->pPerms4[ (int)p->pPerms[uTruth] ];
uPhase = p->pPhases[uTruth];
// collect fanins with the corresponding permutation/phase
Expand Down
3 changes: 2 additions & 1 deletion src/proof/fraig/fraig.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,7 @@ struct Fraig_ParamsStruct_t_
int fVerboseP; // the verbosiness flag (for proof reporting)
int fInternal; // is set to 1 for internal fraig calls
int nConfLimit; // the limit on the number of conflicts
int approximate; // if set to 1, run approximate fraig
ABC_INT64_T nInspLimit; // the limit on the number of inspections
};

Expand Down Expand Up @@ -181,7 +182,7 @@ extern int Fraig_NodeIsAnd( Fraig_Node_t * p );
extern int Fraig_NodeComparePhase( Fraig_Node_t * p1, Fraig_Node_t * p2 );

extern Fraig_Node_t * Fraig_NodeOr( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
extern Fraig_Node_t * Fraig_NodeAnd( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
extern Fraig_Node_t * Fraig_NodeAnd( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2, int enable_approximation );
extern Fraig_Node_t * Fraig_NodeOr( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
extern Fraig_Node_t * Fraig_NodeExor( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
extern Fraig_Node_t * Fraig_NodeMux( Fraig_Man_t * p, Fraig_Node_t * pNode, Fraig_Node_t * pNodeT, Fraig_Node_t * pNodeE );
Expand Down
10 changes: 5 additions & 5 deletions src/proof/fraig/fraigApi.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -209,9 +209,9 @@ void Fraig_ManSetPo( Fraig_Man_t * p, Fraig_Node_t * pNode )
SeeAlso []

***********************************************************************/
Fraig_Node_t * Fraig_NodeAnd( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 )
Fraig_Node_t * Fraig_NodeAnd( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2, int enable_approximation )
{
return Fraig_NodeAndCanon( p, p1, p2 );
return Fraig_NodeAndCanon( p, p1, p2, enable_approximation );
}

/**Function*************************************************************
Expand All @@ -227,7 +227,7 @@ Fraig_Node_t * Fraig_NodeAnd( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t *
***********************************************************************/
Fraig_Node_t * Fraig_NodeOr( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 )
{
return Fraig_Not( Fraig_NodeAndCanon( p, Fraig_Not(p1), Fraig_Not(p2) ) );
return Fraig_Not( Fraig_NodeAndCanon( p, Fraig_Not(p1), Fraig_Not(p2), 0 ) );
}

/**Function*************************************************************
Expand Down Expand Up @@ -260,8 +260,8 @@ Fraig_Node_t * Fraig_NodeExor( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t
Fraig_Node_t * Fraig_NodeMux( Fraig_Man_t * p, Fraig_Node_t * pC, Fraig_Node_t * pT, Fraig_Node_t * pE )
{
Fraig_Node_t * pAnd1, * pAnd2, * pRes;
pAnd1 = Fraig_NodeAndCanon( p, pC, pT ); Fraig_Ref( pAnd1 );
pAnd2 = Fraig_NodeAndCanon( p, Fraig_Not(pC), pE ); Fraig_Ref( pAnd2 );
pAnd1 = Fraig_NodeAndCanon( p, pC, pT, 0 ); Fraig_Ref( pAnd1 );
pAnd2 = Fraig_NodeAndCanon( p, Fraig_Not(pC), pE, 0 ); Fraig_Ref( pAnd2 );
pRes = Fraig_NodeOr( p, pAnd1, pAnd2 );
Fraig_RecursiveDeref( p, pAnd1 );
Fraig_RecursiveDeref( p, pAnd2 );
Expand Down
6 changes: 4 additions & 2 deletions src/proof/fraig/fraigCanon.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []

***********************************************************************/
Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2 )
Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2, int enable_approximation )
{
Fraig_Node_t * pNodeNew, * pNodeOld, * pNodeRepr;
int fUseSatCheck;
Expand Down Expand Up @@ -165,8 +165,10 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
// check the simulation hash table
pNodeOld = Fraig_HashTableLookupF( pMan, pNodeNew );
if ( pNodeOld == NULL ) // the node is unique
return pNodeNew;
return pNodeNew;
}
if ( enable_approximation == 1 )
return pNodeNew;
assert( pNodeOld->pRepr == 0 );
// there is another node which looks the same according to simulation

Expand Down
24 changes: 12 additions & 12 deletions src/proof/fraig/fraigChoice.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,29 +122,29 @@ Fraig_ManCheckConsistency( pMan );

if (fShortCut)
{
pT = Fraig_NodeAnd(pMan, pB, pC);
pT = Fraig_NodeAnd(pMan, pB, pC, 0);
if ( !pT->pRepr )
{
pN = Fraig_NodeAnd(pMan, pA, pT);
pN = Fraig_NodeAnd(pMan, pA, pT, 0);
// Fraig_NodeAddChoice( pMan, pNode, pN );
}
}
else
pN = Fraig_NodeAnd(pMan, pA, Fraig_NodeAnd(pMan, pB, pC));
pN = Fraig_NodeAnd(pMan, pA, Fraig_NodeAnd(pMan, pB, pC, 0), 0);
// assert ( Fraig_NodesEqual(pN, pNode) );


if (fShortCut)
{
pT = Fraig_NodeAnd(pMan, pA, pC);
pT = Fraig_NodeAnd(pMan, pA, pC, 0);
if ( !pT->pRepr )
{
pN = Fraig_NodeAnd(pMan, pB, pT);
pN = Fraig_NodeAnd(pMan, pB, pT, 0);
// Fraig_NodeAddChoice( pMan, pNode, pN );
}
}
else
pN = Fraig_NodeAnd(pMan, pB, Fraig_NodeAnd(pMan, pA, pC));
pN = Fraig_NodeAnd(pMan, pB, Fraig_NodeAnd(pMan, pA, pC, 0), 0);
// assert ( Fraig_NodesEqual(pN, pNode) );
}

Expand All @@ -163,28 +163,28 @@ Fraig_ManCheckConsistency( pMan );

if (fShortCut)
{
pT = Fraig_NodeAnd(pMan, pA, pB);
pT = Fraig_NodeAnd(pMan, pA, pB, 0);
if ( !pT->pRepr )
{
pN = Fraig_NodeAnd(pMan, pC, pT);
pN = Fraig_NodeAnd(pMan, pC, pT, 0);
// Fraig_NodeAddChoice( pMan, pNode, pN );
}
}
else
pN = Fraig_NodeAnd(pMan, Fraig_NodeAnd(pMan, pA, pB), pC);
pN = Fraig_NodeAnd(pMan, Fraig_NodeAnd(pMan, pA, pB, 0), pC, 0);
// assert ( Fraig_NodesEqual(pN, pNode) );

if (fShortCut)
{
pT = Fraig_NodeAnd(pMan, pA, pC);
pT = Fraig_NodeAnd(pMan, pA, pC, 0);
if ( !pT->pRepr )
{
pN = Fraig_NodeAnd(pMan, pB, pT);
pN = Fraig_NodeAnd(pMan, pB, pT, 0);
// Fraig_NodeAddChoice( pMan, pNode, pN );
}
}
else
pN = Fraig_NodeAnd(pMan, Fraig_NodeAnd(pMan, pA, pC), pB);
pN = Fraig_NodeAnd(pMan, Fraig_NodeAnd(pMan, pA, pC, 0), pB, 0);
// assert ( Fraig_NodesEqual(pN, pNode) );
}

Expand Down
Loading