diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 1c3aa4311a..aec9d39cac 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -715,6 +715,30 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fS return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates the AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Obj_t * Gia_MakeRandomChoice( Gia_Man_t * p, int iRepr ) +{ + int iTemp, Rand, Count = 0; + Gia_ClassForEachObj( p, iRepr, iTemp ) + Count++; + Rand = rand() % Count; + Count = 0; + Gia_ClassForEachObj( p, iRepr, iTemp ) + if ( Count++ == Rand ) + break; + return Gia_ManObj(p, iTemp); +} + /**Function************************************************************* Synopsis [Duplicates the AIG in the DFS order.] @@ -735,7 +759,7 @@ void Gia_ManEquivReduce2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, if ( fDiveIn && (pRepr = Gia_ManEquivRepr(p, pObj, 1, 0)) ) { int iTemp, iRepr = Gia_ObjId(p, pRepr); - Gia_Obj_t * pRepr2 = Gia_ManObj( p, Vec_IntEntry(vMap, iRepr) ); + Gia_Obj_t * pRepr2 = vMap ? Gia_ManObj( p, Vec_IntEntry(vMap, iRepr) ) : Gia_MakeRandomChoice(p, iRepr); Gia_ManEquivReduce2_rec( pNew, p, pRepr2, vMap, 0 ); Gia_ClassForEachObj( p, iRepr, iTemp ) { @@ -751,12 +775,13 @@ void Gia_ManEquivReduce2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Gia_ManEquivReduce2_rec( pNew, p, Gia_ObjFanin1(pObj), vMap, 1 ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); } -Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p ) +Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p, int fRandom ) { Vec_Int_t * vMap; Gia_Man_t * pNew; Gia_Obj_t * pObj; int i; + if ( fRandom ) srand(time(NULL)); if ( !p->pReprs && p->pSibls ) { int * pMap = ABC_FALLOC( int, Gia_ManObjNum(p) ); @@ -789,7 +814,7 @@ Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p ) break; if ( i == Gia_ManObjNum(p) ) return Gia_ManDup( p ); - vMap = Gia_ManChoiceMinLevel( p ); + vMap = fRandom ? NULL : Gia_ManChoiceMinLevel( p ); Gia_ManSetPhase( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); @@ -805,7 +830,7 @@ Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Gia_ManHashStop( pNew ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); - Vec_IntFree( vMap ); + Vec_IntFreeP( &vMap ); return pNew; } diff --git a/src/aig/gia/giaSupps.c b/src/aig/gia/giaSupps.c index 96721d66b9..894e26b7d0 100644 --- a/src/aig/gia/giaSupps.c +++ b/src/aig/gia/giaSupps.c @@ -572,6 +572,10 @@ int Supp_FindNextDiv( Supp_Man_t * p, int Pair ) iDiv1 = iDiv1 == -1 ? ABC_INFINITY : iDiv1; iDiv2 = iDiv2 == -1 ? ABC_INFINITY : iDiv2; iDiv = Abc_MinInt( iDiv1, iDiv2 ); + // return -1 if the pair cannot be distinguished by any divisor + // in this case the original resub problem has no solution + if ( iDiv == ABC_INFINITY ) + return -1; assert( iDiv >= 0 && iDiv < Vec_IntSize(p->vCands) ); return iDiv; } @@ -582,6 +586,8 @@ int Supp_ManRandomSolution( Supp_Man_t * p, int iSet, int fVerbose ) { int Pair = Supp_ComputePair( p, iSet ); int iDiv = Supp_FindNextDiv( p, Pair ); + if ( iDiv == -1 ) + return -1; iSet = Supp_ManSubsetAdd( p, iSet, iDiv, fVerbose ); if ( Supp_SetFuncNum(p, iSet) > 0 ) Vec_IntPush( p->vTempSets, iSet ); @@ -883,6 +889,10 @@ Vec_Int_t * Supp_ManCompute( Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * { Supp_ManAddPatternsFunc( p, i ); iSet = Supp_ManRandomSolution( p, 0, fVeryVerbose ); + if ( iSet == -1 ) { + Supp_ManDelete( p ); + return NULL; + } for ( r = 0; r < p->nRounds; r++ ) { if ( fVeryVerbose ) @@ -898,6 +908,10 @@ Vec_Int_t * Supp_ManCompute( Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t * iBest = iSet; } iSet = Supp_ManReconstruct( p, fVeryVerbose ); + if ( iSet == -1 ) { + Supp_ManDelete( p ); + return NULL; + } } if ( fVeryVerbose ) printf( "Matrix size %d.\n", Vec_PtrSize(p->vMatrix) ); diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 5cf7a0f593..58131f1856 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -841,7 +841,7 @@ extern ABC_DLL void Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t extern ABC_DLL void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode ); extern ABC_DLL void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames ); extern ABC_DLL void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames ); -extern ABC_DLL void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes, int fVerbose ); +extern ABC_DLL void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes, int fOutputs, int fVerbose ); extern ABC_DLL void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode ); extern ABC_DLL void Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll ); extern ABC_DLL void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 778e7f3190..7c3201a1ab 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -405,6 +405,7 @@ static int Abc_CommandAbc9Write ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9WriteLut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Ps ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9PFan ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Pms ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9PSig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Status ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9MuxProfile ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1183,6 +1184,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&wlut", Abc_CommandAbc9WriteLut, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&ps", Abc_CommandAbc9Ps, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&pfan", Abc_CommandAbc9PFan, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&pms", Abc_CommandAbc9Pms, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&psig", Abc_CommandAbc9PSig, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&status", Abc_CommandAbc9Status, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&profile", Abc_CommandAbc9MuxProfile, 0 ); @@ -2022,14 +2024,16 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int fListNodes; int fProfile; + int fOutputs; int fVerbose; // set defaults fListNodes = 0; fProfile = 1; + fOutputs = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "npvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "npovh" ) ) != EOF ) { switch ( c ) { @@ -2039,6 +2043,9 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'p': fProfile ^= 1; break; + case 'o': + fOutputs ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -2079,14 +2086,15 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } // process all COs - Abc_NtkPrintLevel( stdout, pNtk, fProfile, fListNodes, fVerbose ); + Abc_NtkPrintLevel( stdout, pNtk, fProfile, fListNodes, fOutputs, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: print_level [-npvh] \n" ); + Abc_Print( -2, "usage: print_level [-npovh] \n" ); Abc_Print( -2, "\t prints information about node level and cone size\n" ); Abc_Print( -2, "\t-n : toggles printing nodes by levels [default = %s]\n", fListNodes? "yes": "no" ); Abc_Print( -2, "\t-p : toggles printing level profile [default = %s]\n", fProfile? "yes": "no" ); + Abc_Print( -2, "\t-o : toggles printing output levels [default = %s]\n", fOutputs? "yes": "no" ); Abc_Print( -2, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\tnode : (optional) one node to consider\n"); @@ -9310,11 +9318,12 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Exa_ManExactSynthesis4( Bmc_EsPar_t * pPars ); extern void Exa_ManExactSynthesis5( Bmc_EsPar_t * pPars ); extern void Exa_ManExactSynthesis6( Bmc_EsPar_t * pPars, char * pFileName ); - int c, fKissat = 0, fKissat2 = 0; + extern void Exa_ManExactSynthesis7( Bmc_EsPar_t * pPars, int GateSize ); + int c, fKissat = 0, fKissat2 = 0, fUseNands = 0, GateSize = 0; Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INTadconugklvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INTGabdconugklvh" ) ) != EOF ) { switch ( c ) { @@ -9351,9 +9360,23 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->RuntimeLim < 0 ) goto usage; break; + case 'G': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + GateSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( GateSize < 0 ) + goto usage; + break; case 'a': pPars->fOnlyAnd ^= 1; break; + case 'b': + fUseNands ^= 1; + break; case 'd': pPars->fDynConstr ^= 1; break; @@ -9401,7 +9424,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Truth table should be given on the command line.\n" ); return 1; } - if ( (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) ) + if ( pPars->nVars >= 2 && (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) ) { Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (pPars->nVars-2)), strlen(pPars->pTtStr) ); return 1; @@ -9416,7 +9439,9 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Function should not have more than 10 inputs.\n" ); return 1; } - if ( fKissat ) + if ( fUseNands ) + Exa_ManExactSynthesis7( pPars, GateSize ); + else if ( fKissat ) Exa_ManExactSynthesis4( pPars ); else if ( fKissat2 ) Exa_ManExactSynthesis5( pPars ); @@ -9427,12 +9452,14 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: twoexact [-INT ] [-adconugklvh] \n" ); + Abc_Print( -2, "usage: twoexact [-INTG ] [-abdconugklvh] \n" ); Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" ); Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-N : the number of two-input nodes [default = %d]\n", pPars->nNodes ); Abc_Print( -2, "\t-T : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim ); + Abc_Print( -2, "\t-G : the largest allowed gate size (NANDs only) [default = %d]\n", GateSize ); Abc_Print( -2, "\t-a : toggle using only AND-gates (without XOR-gates) [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); + Abc_Print( -2, "\t-b : toggle using only NAND-gates [default = %s]\n", fUseNands ? "yes" : "no" ); Abc_Print( -2, "\t-d : toggle using dynamic constraint addition [default = %s]\n", pPars->fDynConstr ? "yes" : "no" ); Abc_Print( -2, "\t-c : toggle dumping CNF into a file [default = %s]\n", pPars->fDumpCnf ? "yes" : "no" ); Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" ); @@ -32499,6 +32526,57 @@ int Abc_CommandAbc9PFan( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Pms( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Gia_Obj_t * pObj; + int c, nSat = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9PFan(): There is no AIG.\n" ); + return 1; + } + printf( "Status of %d outputs of the miter: ", Gia_ManPoNum(pAbc->pGia) ); + Gia_ManForEachPo( pAbc->pGia, pObj, c ) + { + printf( "%d", c ); + if ( pAbc->pGia->vNamesOut ) + printf( "(%s)", (char *)Vec_PtrEntry(pAbc->pGia->vNamesOut, c) ); + printf( "=%s ", Gia_ObjFaninLit0p(pAbc->pGia, pObj) == 0 ? "unsat":"sat" ); + nSat += Gia_ObjFaninLit0p(pAbc->pGia, pObj) != 0; + } + printf( "\n" ); + printf( "Total sat = %d. Total unsat = %d.\n", nSat, Gia_ManPoNum(pAbc->pGia)-nSat ); + return 0; + +usage: + Abc_Print( -2, "usage: &pms [-h]\n" ); + Abc_Print( -2, "\t prints miter status after SAT sweeping\n" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -44038,14 +44116,14 @@ int Abc_CommandAbc9Era( Abc_Frame_t * pAbc, int argc, char ** argv ) ***********************************************************************/ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p ); + extern Gia_Man_t * Gia_ManEquivReduce2( Gia_Man_t * p, int fRandom ); Gia_Man_t * pTemp; Dch_Pars_t Pars, * pPars = &Pars; - int c, fMinLevel = 0, fEquiv = 0; + int c, fMinLevel = 0, fEquiv = 0, fRandom = 0; // set defaults Dch_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfremgcxyvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfremngcxyvh" ) ) != EOF ) { switch ( c ) { @@ -44103,6 +44181,9 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'm': fMinLevel ^= 1; break; + case 'n': + fRandom ^= 1; + break; case 'g': pPars->fUseGia ^= 1; break; @@ -44147,14 +44228,14 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) { pTemp = Gia_ManPerformDch( pAbc->pGia, pPars ); Abc_FrameUpdateGia( pAbc, pTemp ); - if ( fMinLevel ) - pTemp = Gia_ManEquivReduce2( pAbc->pGia ); + if ( fMinLevel || fRandom ) + pTemp = Gia_ManEquivReduce2( pAbc->pGia, fRandom ); } Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &dch [-WCS num] [-sptfremgcxyvh]\n" ); + Abc_Print( -2, "usage: &dch [-WCS num] [-sptfremngcxyvh]\n" ); Abc_Print( -2, "\t computes structural choices using a new approach\n" ); Abc_Print( -2, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); @@ -44165,7 +44246,8 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "\t-f : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" ); Abc_Print( -2, "\t-r : toggle skipping choices with redundant support [default = %s]\n", pPars->fSkipRedSupp? "yes": "no" ); Abc_Print( -2, "\t-e : toggle computing and merging equivalences [default = %s]\n", fEquiv? "yes": "no" ); - Abc_Print( -2, "\t-m : toggle minimizing logic level after merging equivalences [default = %s]\n", fMinLevel? "yes": "no" ); + Abc_Print( -2, "\t-m : toggle minimizing logic level after merging equivalences [default = %s]\n", fRandom? "yes": "no" ); + Abc_Print( -2, "\t-n : toggle selecting random choices while merging equivalences [default = %s]\n", fMinLevel? "yes": "no" ); Abc_Print( -2, "\t-g : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" ); Abc_Print( -2, "\t-c : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" ); Abc_Print( -2, "\t-x : toggle using new choice computation [default = %s]\n", pPars->fUseNew? "yes": "no" ); diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index e90159d2a9..6366652497 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -1228,11 +1228,19 @@ char * Abc_NodeGetPrintName( Abc_Obj_t * pObj ) } return Abc_ObjName(nPos == 1 ? pFanout : pObj); } -void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes, int fVerbose ) +void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes, int fOutputs, int fVerbose ) { Abc_Obj_t * pNode; int i, k, Length; - + if ( fOutputs ) + { + Abc_NtkLevel(pNtk); + printf( "Outputs by level: " ); + Abc_NtkForEachCo( pNtk, pNode, k ) + printf( "%d=%d ", k, Abc_ObjFanin0(pNode)->Level ); + printf( "\n" ); + return; + } if ( fListNodes ) { int nLevels; diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index d3a3ac18d7..40ecd4a5e5 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -3724,10 +3724,170 @@ void Exa_ManExactSynthesis6( Bmc_EsPar_t * pPars, char * pFileName ) if ( pMini ) Mini_AigStop( pMini ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Exa7_AddClause( FILE * pFile, int * pLits, int nLits ) +{ + int i, k = 0; + for ( i = 0; i < nLits; i++ ) { + if ( pLits[i] == 1 ) + return 0; + else if ( pLits[i] == 0 ) + continue; + else + pLits[k++] = pLits[i]; + } + nLits = k; + assert( nLits > 0 ); + if ( pFile ) + { + for ( i = 0; i < nLits; i++ ) + fprintf( pFile, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) ); + fprintf( pFile, "0\n" ); + } + if ( 0 ) + { + for ( i = 0; i < nLits; i++ ) + fprintf( stdout, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i])-1 ); + fprintf( stdout, "\n" ); + } + return 1; +} +static inline int Exa7_AddClause4( FILE * pFile, int Lit0, int Lit1, int Lit2, int Lit3 ) +{ + int pLits[4] = { Lit0, Lit1, Lit2, Lit3 }; + return Exa7_AddClause( pFile, pLits, 4 ); +} +int Exa7_GetVar( int n, int i, int j, int m ) +{ + return 1 + n*n*m + n*i + j; +} +int Exa7_ManGenCnf( char * pFileName, word * pTruth, int nVars, int nNodes, int GateSize ) +{ + int m, n, v, k, nV = nVars + nNodes, nMints = 1 << nVars, nClas = 0; + int pVars[32] = {0}; assert( nVars + nNodes + 1 < 32 ); + FILE * pFile = fopen( pFileName, "wb" ); + fputs( "p cnf \n", pFile ); + for ( m = 0; m < nMints; m++ ) + { + for ( v = 0; v < nVars; v++ ) + nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(Exa7_GetVar(nV, v, v, m), ((m >> v)&1)==0), 0, 0, 0 ); + nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(Exa7_GetVar(nV, nV-1, nV-1, m), ((pTruth[0] >> m)&1)==0), 0, 0, 0 ); + for ( n = nVars; n < nV; n++ ) + { + int iValNode = Exa7_GetVar(nV, n, n, m); + for ( v = 0; v < n; v++ ) + { + int iParVar = Exa7_GetVar(nV, v, n, 0); // v < n + int iFanVar = Exa7_GetVar(nV, n, v, m); + int iValFan = Exa7_GetVar(nV, v, v, m); + // iFanVar = ~iParVar | iValFan + nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iFanVar, 1), Abc_Var2Lit(iParVar, 1), Abc_Var2Lit(iValFan, 0), 0 ); + nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iFanVar, 0), Abc_Var2Lit(iParVar, 0), 0, 0 ); + nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iFanVar, 0), Abc_Var2Lit(iValFan, 1), 0, 0 ); + // iParVar & ~iValFan => iValNode + nClas += Exa7_AddClause4( pFile, Abc_Var2Lit(iParVar, 1), Abc_Var2Lit(iValFan, 0), Abc_Var2Lit(iValNode, 0), 0 ); + pVars[v] = Abc_Var2Lit(iFanVar, 1); + } + pVars[v] = Abc_Var2Lit(iValNode, 1); + // (iFanVar0 & iFanVar1 & iFanVar2) => ~iValNode + nClas += Exa7_AddClause( pFile, pVars, n+1 ); + } + } + for ( n = nVars; n < nV; n++ ) { + for ( v = 0; v < n; v++ ) + pVars[v] = Abc_Var2Lit(Exa7_GetVar(nV, v, n, 0), 0); // v < n + nClas += Exa7_AddClause( pFile, pVars, n ); + if ( GateSize ) { + int Total = 1 << n, Limit = GateSize + 1; + for ( m = 0; m < Total; m++ ) + { + if ( Abc_TtCountOnes((word)m) != Limit ) + continue; + for ( k = v = 0; v < n; v++ ) + if ( (m >> v) & 1 ) + pVars[k++] = Abc_Var2Lit(Exa7_GetVar(nV, v, n, 0), 1); + assert( k == Limit ); + nClas += Exa7_AddClause( pFile, pVars, Limit ); + } + } + } + rewind( pFile ); + fprintf( pFile, "p cnf %d %d", nMints * nV * nV, nClas ); + fclose( pFile ); + return nClas; +} +void Exa_ManDumpVerilog( Vec_Int_t * vValues, int nVars, int nNodes, int GateSize, word * pTruth ) +{ + FILE * pFile; + char Buffer[1000]; + char FileName[1100]; + int v, n, k, nV = nVars+nNodes; + Extra_PrintHexadecimalString( Buffer, (unsigned *)pTruth, nVars ); + sprintf( FileName, "func%s_%d_%d.v", Buffer, GateSize, nNodes ); + pFile = fopen( FileName, "wb" ); + fprintf( pFile, "// Realization of the %d-input function %s using %d NAND gates:\n", nVars, Buffer, nNodes ); + fprintf( pFile, "module func%s_%d_%d ( input", Buffer, GateSize, nNodes ); + for ( v = 0; v < nVars; v++ ) + fprintf( pFile, " %c,", 'a'+v ); + fprintf( pFile, " output out );\n" ); + for ( n = nVars; n < nV; n++ ) { + int nFans = 0; + for ( v = 0; v < n; v++ ) + nFans += Vec_IntEntry(vValues, Exa7_GetVar(nV, v, n, 0)); + fprintf( pFile, " wire %c = ~(", 'a'+n ); + for ( k = v = 0; v < n; v++ ) + if ( Vec_IntEntry(vValues, Exa7_GetVar(nV, v, n, 0)) ) + fprintf( pFile, "%c%s", 'a'+v, ++k < nFans ? " & ":"" ); + fprintf( pFile, ");\n" ); + } + fprintf( pFile, " assign out = %c;\n", 'a'+nV-1 ); + fprintf( pFile, "endmodule\n\n" ); + fclose( pFile ); + printf( "Solution was dumped into file \"%s\".\n", FileName ); +} +void Exa_ManExactSynthesis7( Bmc_EsPar_t * pPars, int GateSize ) +{ + abctime clkTotal = Abc_Clock(); + int v, n, nMints = 1 << pPars->nVars; + int nV = pPars->nVars + pPars->nNodes; + word pTruth[16]; Abc_TtReadHex( pTruth, pPars->pTtStr ); + Vec_Int_t * vValues = NULL; + char * pFileNameIn = "_temp_.cnf"; + char * pFileNameOut = "_temp_out.cnf"; + int nClas = Exa7_ManGenCnf( pFileNameIn, pTruth, pPars->nVars, pPars->nNodes, GateSize ); + if ( pPars->fVerbose ) + printf( "CNF with %d variables and %d clauses was dumped into file \"%s\".\n", nMints * nV * nV, nClas, pFileNameIn ); + vValues = Exa4_ManSolve( pFileNameIn, pFileNameOut, pPars->RuntimeLim, pPars->fVerbose ); + if ( pPars->fVerbose && vValues ) { + printf( " " ); + for ( n = 0; n < nV; n++ ) + printf( "%2d ", n ); + printf( "\n" ); + for ( n = pPars->nVars; n < nV; n++, printf("\n") ) { + printf( "%2d : ", n ); + for ( v = 0; v < n; v++ ) + printf( " %c ", Vec_IntEntry(vValues, Exa7_GetVar(nV, v, n, 0)) ? '1':'.' ); // v < n + } + } + if ( vValues ) + Exa_ManDumpVerilog( vValues, pPars->nVars, pPars->nNodes, GateSize, pTruth ); + Vec_IntFreeP( &vValues ); + Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - ABC_NAMESPACE_IMPL_END