diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index dd189c6dfc..56b6dda38f 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -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 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 085bb0f0e9..04851b0bd8 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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(); @@ -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 ) { @@ -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: @@ -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; @@ -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; @@ -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 ) { @@ -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: @@ -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; } diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c index 2cfb46bb0d..3c46e30a23 100644 --- a/src/base/abci/abcFraig.c +++ b/src/base/abci/abcFraig.c @@ -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 ); @@ -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) ); @@ -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; diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 5dc125d065..6d8144e456 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -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 ); diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c index 03722926ff..2cd08abefc 100644 --- a/src/base/abci/abcProve.c +++ b/src/base/abci/abcProve.c @@ -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 ) @@ -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; } diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c index 02f7b83843..bc9669c416 100644 --- a/src/base/abci/abcQuant.c +++ b/src/base/abci/abcQuant.c @@ -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 ); diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c index 0b0881a6c2..2a31661efe 100644 --- a/src/base/abci/abcRewrite.c +++ b/src/base/abci/abcRewrite.c @@ -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; @@ -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 diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c index e970ac387b..dcdaba543e 100644 --- a/src/base/abci/abcSweep.c +++ b/src/base/abci/abcSweep.c @@ -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) ); } diff --git a/src/map/scl/sclBufSize.c b/src/map/scl/sclBufSize.c index be9cc3bd1b..4aae3184c2 100644 --- a/src/map/scl/sclBufSize.c +++ b/src/map/scl/sclBufSize.c @@ -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 ); diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h index b688fc09e7..7ec825ae70 100644 --- a/src/opt/rwr/rwr.h +++ b/src/opt/rwr/rwr.h @@ -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 ========================================================*/ diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c index 1856f7b74b..0233bf4293 100644 --- a/src/opt/rwr/rwrEva.c +++ b/src/opt/rwr/rwrEva.c @@ -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; @@ -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 diff --git a/src/proof/fraig/fraig.h b/src/proof/fraig/fraig.h index 0c021feb0b..2c0484d9ac 100644 --- a/src/proof/fraig/fraig.h +++ b/src/proof/fraig/fraig.h @@ -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 }; @@ -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 ); diff --git a/src/proof/fraig/fraigApi.c b/src/proof/fraig/fraigApi.c index b0b47075cd..38057f14f2 100644 --- a/src/proof/fraig/fraigApi.c +++ b/src/proof/fraig/fraigApi.c @@ -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************************************************************* @@ -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************************************************************* @@ -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 ); diff --git a/src/proof/fraig/fraigCanon.c b/src/proof/fraig/fraigCanon.c index 47539db254..0e29b974c6 100644 --- a/src/proof/fraig/fraigCanon.c +++ b/src/proof/fraig/fraigCanon.c @@ -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; @@ -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 diff --git a/src/proof/fraig/fraigChoice.c b/src/proof/fraig/fraigChoice.c index 4e6a225b12..e9fe772605 100644 --- a/src/proof/fraig/fraigChoice.c +++ b/src/proof/fraig/fraigChoice.c @@ -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) ); } @@ -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) ); } diff --git a/src/proof/fraig/fraigInt.h b/src/proof/fraig/fraigInt.h index 37f007205c..90b87913a7 100644 --- a/src/proof/fraig/fraigInt.h +++ b/src/proof/fraig/fraigInt.h @@ -354,7 +354,7 @@ extern unsigned Aig_ManRandom( int fReset ); //////////////////////////////////////////////////////////////////////// /*=== fraigCanon.c =============================================================*/ -extern Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2 ); +extern Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2, int enable_approximation ); /*=== fraigFanout.c =============================================================*/ extern void Fraig_NodeAddFaninFanout( Fraig_Node_t * pFanin, Fraig_Node_t * pFanout ); extern void Fraig_NodeRemoveFaninFanout( Fraig_Node_t * pFanin, Fraig_Node_t * pFanoutToRemove );