diff options
Diffstat (limited to 'src/base/acb/acbFunc.c')
| -rw-r--r-- | src/base/acb/acbFunc.c | 2496 |
1 files changed, 2494 insertions, 2 deletions
diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c index 40f37dfd..7d36a1ff 100644 --- a/src/base/acb/acbFunc.c +++ b/src/base/acb/acbFunc.c @@ -19,14 +19,87 @@ ***********************************************************************/ #include "acb.h" +#include "aig/miniaig/ndr.h" +#include "sat/cnf/cnf.h" +#include "sat/bsat/satStore.h" +#include "sat/satoko/satoko.h" +#include "map/mio/mio.h" +#include "misc/util/utilTruth.h" +#include "aig/gia/giaAig.h" ABC_NAMESPACE_IMPL_START - //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define ACB_LAST_NAME_ID 14 + +typedef enum { + ACB_NONE = 0, // 0: unused + ACB_MODULE, // 1: "module" + ACB_ENDMODULE, // 2: "endmodule" + ACB_INPUT, // 3: "input" + ACB_OUTPUT, // 4: "output" + ACB_WIRE, // 5: "wire" + ACB_BUF, // 6: "buf" + ACB_NOT, // 7: "not" + ACB_AND, // 8: "and" + ACB_NAND, // 9: "nand" + ACB_OR, // 10: "or" + ACB_NOR, // 11: "nor" + ACB_XOR, // 12: "xor" + ACB_XNOR, // 13: "xnor" + ACB_UNUSED // 14: unused +} Acb_KeyWords_t; + +static inline char * Acb_Num2Name( int i ) +{ + if ( i == 1 ) return "module"; + if ( i == 2 ) return "endmodule"; + if ( i == 3 ) return "input"; + if ( i == 4 ) return "output"; + if ( i == 5 ) return "wire"; + if ( i == 6 ) return "buf"; + if ( i == 7 ) return "not"; + if ( i == 8 ) return "and"; + if ( i == 9 ) return "nand"; + if ( i == 10 ) return "or"; + if ( i == 11 ) return "nor"; + if ( i == 12 ) return "xor"; + if ( i == 13 ) return "xnor"; + return NULL; +} + +static inline int Acb_Type2Oper( int i ) +{ + if ( i == 6 ) return ABC_OPER_BIT_BUF; + if ( i == 7 ) return ABC_OPER_BIT_INV; + if ( i == 8 ) return ABC_OPER_BIT_AND; + if ( i == 9 ) return ABC_OPER_BIT_NAND; + if ( i == 10 ) return ABC_OPER_BIT_OR; + if ( i == 11 ) return ABC_OPER_BIT_NOR; + if ( i == 12 ) return ABC_OPER_BIT_XOR; + if ( i == 13 ) return ABC_OPER_BIT_NXOR; + assert( 0 ); + return -1; +} + +static inline char * Acb_Oper2Name( int i ) +{ + if ( i == ABC_OPER_CONST_F ) return "const0"; + if ( i == ABC_OPER_CONST_T ) return "const1"; + if ( i == ABC_OPER_BIT_BUF ) return "buf"; + if ( i == ABC_OPER_BIT_INV ) return "not"; + if ( i == ABC_OPER_BIT_AND ) return "and"; + if ( i == ABC_OPER_BIT_NAND ) return "nand"; + if ( i == ABC_OPER_BIT_OR ) return "or"; + if ( i == ABC_OPER_BIT_NOR ) return "nor"; + if ( i == ABC_OPER_BIT_XOR ) return "xor"; + if ( i == ABC_OPER_BIT_NXOR ) return "xnor"; + assert( 0 ); + return NULL; +} //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -34,6 +107,662 @@ ABC_NAMESPACE_IMPL_START /**Function************************************************************* + Synopsis [Installs the required standard cell library.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * pLibStr[25] = { + "GATE buf 1 O=a; PIN * INV 1 999 1.0 0.0 1.0 0.0\n" + "GATE inv 1 O=!a; PIN * INV 1 999 1.0 0.0 1.0 0.0\n" + "GATE and2 1 O=a*b; PIN * INV 1 999 1.0 0.0 1.0 0.0\n" + "GATE and3 1 O=a*b*c; PIN * INV 1 999 1.0 0.0 1.0 0.0\n" + "GATE and4 1 O=a*b*c*d; PIN * INV 1 999 1.0 0.0 1.0 0.0\n" + "GATE or2 1 O=a+b; PIN * INV 1 999 1.0 0.0 1.0 0.0\n" + "GATE or3 1 O=a+b+c; PIN * INV 1 999 1.0 0.0 1.0 0.0\n" + "GATE or4 1 O=a+b+c+d; PIN * INV 1 999 1.0 0.0 1.0 0.0\n" + "GATE nand2 1 O=!(a*b); PIN * INV 1 999 1.0 0.0 1.0 0.0\n" + "GATE nand3 1 O=!(a*b*c); PIN * INV 1 999 1.0 0.0 1.0 0.0\n" + "GATE nand4 1 O=!(a*b*c*d); PIN * INV 1 999 1.0 0.0 1.0 0.0\n" + "GATE nor2 1 O=!(a+b); PIN * INV 1 999 1.0 0.0 1.0 0.0\n" + "GATE nor3 1 O=!(a+b+c); PIN * INV 1 999 1.0 0.0 1.0 0.0\n" + "GATE nor4 1 O=!(a+b+c+d); PIN * INV 1 999 1.0 0.0 1.0 0.0\n" + "GATE xor 1 O=!a*b+a*!b; PIN * INV 1 999 1.0 0.0 1.0 0.0\n" + "GATE xnor 1 O=a*b+!a*!b; PIN * INV 1 999 1.0 0.0 1.0 0.0\n" + "GATE zero 0 O=CONST0;\n" + "GATE one 0 O=CONST1;\n" +}; +void Acb_IntallLibrary() +{ + extern Mio_Library_t * Mio_LibraryReadBuffer( char * pBuffer, int fExtendedFormat, st__table * tExcludeGate, int fVerbose ); + Mio_Library_t * pLib; + int i; + // create library string + Vec_Str_t * vLibStr = Vec_StrAlloc( 1000 ); + for ( i = 0; pLibStr[i]; i++ ) + Vec_StrAppend( vLibStr, pLibStr[i] ); + Vec_StrPush( vLibStr, '\0' ); + // create library + pLib = Mio_LibraryReadBuffer( Vec_StrArray(vLibStr), 0, NULL, 0 ); + Mio_LibrarySetName( pLib, Abc_UtilStrsav("iccad17.genlib") ); + Mio_UpdateGenlib( pLib ); + Vec_StrFree( vLibStr ); +} + +/**Function************************************************************* + + Synopsis [Parse Verilog file into an intermediate representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Nam_t * Acb_VerilogStartNames() +{ + Abc_Nam_t * pNames = Abc_NamStart( 100, 16 ); + int i, NameId, fFound; + for ( i = 1; i < ACB_UNUSED; i++ ) + { + NameId = Abc_NamStrFindOrAdd( pNames, Acb_Num2Name(i), &fFound ); + assert( i == NameId && !fFound ); + } + return pNames; +} +Vec_Int_t * Acb_VerilogSimpleLex( char * pFileName, Abc_Nam_t * pNames ) +{ + Vec_Int_t * vBuffer = Vec_IntAlloc( 1000 ); + char * pBuffer = Extra_FileReadContents( pFileName ); + char * pToken; + if ( pBuffer == NULL ) + return NULL; + pToken = strtok( pBuffer, " \n\r()," ); + while ( pToken ) + { + Vec_IntPush( vBuffer, Abc_NamStrFindOrAdd(pNames, pToken, NULL) ); + pToken = strtok( NULL, " \n\r(),;" ); + } + ABC_FREE( pBuffer ); + return vBuffer; +} +int Acb_WireIsTarget( int Token, Abc_Nam_t * pNames ) +{ + char * pStr = Abc_NamStr(pNames, Token); + return pStr[0] == 't' && pStr[1] == '_'; +} +void * Acb_VerilogSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames ) +{ + void * pDesign = NULL; + Vec_Int_t * vInputs = Vec_IntAlloc(100); + Vec_Int_t * vOutputs = Vec_IntAlloc(100); + Vec_Int_t * vWires = Vec_IntAlloc(100); + Vec_Int_t * vTypes = Vec_IntAlloc(100); + Vec_Int_t * vFanins = Vec_IntAlloc(100); + Vec_Int_t * vCur = NULL; + int i, ModuleID, Token, Size, Count = 0; + assert( Vec_IntEntry(vBuffer, 0) == ACB_MODULE ); + Vec_IntForEachEntryStart( vBuffer, Token, i, 2 ) + { + if ( vCur == NULL && Token >= ACB_UNUSED ) + continue; + if ( Token == ACB_ENDMODULE ) + break; + if ( Token == ACB_INPUT ) + vCur = vInputs; + else if ( Token == ACB_OUTPUT ) + vCur = vOutputs; + else if ( Token == ACB_WIRE ) + vCur = vWires; + else if ( Token >= ACB_BUF && Token <= ACB_XNOR ) + { + Vec_IntPush( vTypes, Token ); + Vec_IntPush( vTypes, Vec_IntSize(vFanins) ); + vCur = vFanins; + } + else + Vec_IntPush( vCur, Token ); + } + Vec_IntPush( vTypes, -1 ); + Vec_IntPush( vTypes, Vec_IntSize(vFanins) ); + // create design + pDesign = Ndr_Create( Vec_IntEntry(vBuffer, 1) ); + ModuleID = Ndr_AddModule( pDesign, Vec_IntEntry(vBuffer, 1) ); + // create inputs + Ndr_DataResize( pDesign, Vec_IntSize(vInputs) ); + Vec_IntForEachEntry( vInputs, Token, i ) + Ndr_DataPush( pDesign, NDR_INPUT, Token ); + Ndr_DataAddTo( pDesign, ModuleID-256, Vec_IntSize(vInputs) ); + Ndr_DataAddTo( pDesign, 0, Vec_IntSize(vInputs) ); + // create outputs + Ndr_DataResize( pDesign, Vec_IntSize(vOutputs) ); + Vec_IntForEachEntry( vOutputs, Token, i ) + Ndr_DataPush( pDesign, NDR_OUTPUT, Token ); + Ndr_DataAddTo( pDesign, ModuleID-256, Vec_IntSize(vOutputs) ); + Ndr_DataAddTo( pDesign, 0, Vec_IntSize(vOutputs) ); + // create targets + Ndr_DataResize( pDesign, Vec_IntSize(vWires) ); + Vec_IntForEachEntry( vWires, Token, i ) + if ( Acb_WireIsTarget(Token, pNames) ) + Ndr_DataPush( pDesign, NDR_TARGET, Token ), Count++; + Ndr_DataAddTo( pDesign, ModuleID-256, Count ); + Ndr_DataAddTo( pDesign, 0, Count ); + // create nodes + Vec_IntForEachEntry( vInputs, Token, i ) + Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CI, 0, 0, 0, 0, 0, NULL, 1, &Token, NULL ); // no fanins + if ( (Token = Abc_NamStrFind(pNames, "1\'b0")) ) + Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CONST_F, 0, 0, 0, 0, 0, NULL, 1, &Token, NULL ); // no fanins + if ( (Token = Abc_NamStrFind(pNames, "1\'b1")) ) + Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CONST_T, 0, 0, 0, 0, 0, NULL, 1, &Token, NULL ); // no fanins + Vec_IntForEachEntryDouble( vTypes, Token, Size, i ) + if ( Token > 0 ) + { + int Output = Vec_IntEntry(vFanins, Size); + int nFanins = Vec_IntEntry(vTypes, i+3) - Size - 1; + int * pFanins = Vec_IntEntryP(vFanins, Size+1); + Ndr_AddObject( pDesign, ModuleID, Acb_Type2Oper(Token), 0, 0, 0, 0, nFanins, pFanins, 1, &Output, NULL ); // many fanins + } + Vec_IntForEachEntry( vOutputs, Token, i ) + Ndr_AddObject( pDesign, ModuleID, ABC_OPER_CO, 0, 0, 0, 0, 1, &Token, 1, &Token, NULL ); // one fanin + // cleanup + Vec_IntFree( vInputs ); + Vec_IntFree( vOutputs ); + Vec_IntFree( vWires ); + Vec_IntFree( vTypes ); + Vec_IntFree( vFanins ); + return pDesign; +} + +/**Function************************************************************* + + Synopsis [Read weights of nodes from the weight file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Acb_ReadWeightMap( char * pFileName, Abc_Nam_t * pNames ) +{ + Vec_Int_t * vWeights = Vec_IntStartFull( Abc_NamObjNumMax(pNames) ); + char * pBuffer = Extra_FileReadContents( pFileName ); + char * pToken, * pNum; + if ( pBuffer == NULL ) + return NULL; + pToken = strtok( pBuffer, " \n\r()," ); + pNum = strtok( NULL, " \n\r()," ); + while ( pToken ) + { + int NameId = Abc_NamStrFind(pNames, pToken); + int Number = atoi(pNum); + if ( NameId <= 0 ) + { + printf( "Cannot find name \"%s\" among node names of this network.\n", pToken ); + continue; + } + Vec_IntWriteEntry( vWeights, NameId, Number ); + pToken = strtok( NULL, " \n\r(),;" ); + pNum = strtok( NULL, " \n\r(),;" ); + } + ABC_FREE( pBuffer ); + return vWeights; +} + +/**Function************************************************************* + + Synopsis [Create network from the intermediate representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Acb_Ntk_t * Acb_VerilogSimpleRead( char * pFileName, char * pFileNameW ) +{ + extern Acb_Ntk_t * Acb_NtkFromNdr( char * pFileName, void * pModule, Abc_Nam_t * pNames, Vec_Int_t * vWeights, int nNameIdMax ); + Acb_Ntk_t * pNtk; + Abc_Nam_t * pNames = Acb_VerilogStartNames(); + Vec_Int_t * vBuffer = Acb_VerilogSimpleLex( pFileName, pNames ); + void * pModule = vBuffer ? Acb_VerilogSimpleParse( vBuffer, pNames ) : NULL; + Vec_Int_t * vWeights = pFileNameW ? Acb_ReadWeightMap( pFileNameW, pNames ) : NULL; + if ( pFileName && pModule == NULL ) + { + printf( "Cannot read input file \"%s\".\n", pFileName ); + return NULL; + } + if ( pFileNameW && vWeights == NULL ) + { + printf( "Cannot read weight file \"%s\".\n", pFileNameW ); + return NULL; + } +// Ndr_ModuleWriteVerilog( "iccad17/unit1/test.v", pModule, pNameStrs ); + pNtk = Acb_NtkFromNdr( pFileName, pModule, pNames, vWeights, Abc_NamObjNumMax(pNames) ); + Ndr_Delete( pModule ); + Vec_IntFree( vBuffer ); + Vec_IntFreeP( &vWeights ); + Abc_NamDeref( pNames ); + return pNtk; +} + +/**Function************************************************************* + + Synopsis [Write Verilog for sanity checking.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_VerilogSimpleWrite( Acb_Ntk_t * p, char * pFileName ) +{ + int i, iObj, fFirst = 1; + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for writing.\n", pFileName ); return; } + + fprintf( pFile, "\nmodule %s (\n ", Acb_NtkName(p) ); + + Acb_NtkForEachPi( p, iObj, i ) + fprintf( pFile, "%s, ", Acb_ObjNameStr(p, iObj) ); + fprintf( pFile, "\n " ); + + Acb_NtkForEachPo( p, iObj, i ) + fprintf( pFile, "%s%s", fFirst ? "":", ", Acb_ObjNameStr(p, iObj) ), fFirst = 0; + fprintf( pFile, "\n);\n\n" ); + + Acb_NtkForEachPi( p, iObj, i ) + fprintf( pFile, " input %s;\n", Acb_ObjNameStr(p, iObj) ); + fprintf( pFile, "\n" ); + + Acb_NtkForEachPo( p, iObj, i ) + fprintf( pFile, " output %s;\n", Acb_ObjNameStr(p, iObj) ); + fprintf( pFile, "\n" ); + + Acb_NtkForEachNode( p, iObj ) + if ( Acb_ObjFaninNum(p, iObj) > 0 ) + fprintf( pFile, " wire %s;\n", Acb_ObjNameStr(p, iObj) ); + fprintf( pFile, "\n" ); + + Acb_NtkForEachNode( p, iObj ) + if ( Acb_ObjFaninNum(p, iObj) > 0 ) + { + int * pFanin, iFanin, k, start = ftell(pFile)+55; + fprintf( pFile, " %s (", Acb_Oper2Name( Acb_ObjType(p, iObj) ) ); + fprintf( pFile, " %s", Acb_ObjNameStr(p, iObj) ); + Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, k ) + //if ( iFanin == 0 ) fprintf( pFile, ", <zero>" ); else + fprintf( pFile, ", %s", Acb_ObjNameStr(p, iFanin) ); + fprintf( pFile, " );" ); + if ( Acb_NtkHasObjWeights(p) && Acb_ObjWeight(p, iObj) > 0 ) + fprintf( pFile, " %*s // weight = %d", (int)(start-ftell(pFile)), "", Acb_ObjWeight(p, iObj) ); + fprintf( pFile, "\n" ); + } + else // constant nodes + { + assert( Acb_ObjType(p, iObj) == ABC_OPER_CONST_F || Acb_ObjType(p, iObj) == ABC_OPER_CONST_T ); + fprintf( pFile, " %s (", Acb_Oper2Name( ABC_OPER_BIT_BUF ) ); + fprintf( pFile, " 1\'b%d", Acb_ObjType(p, iObj) == ABC_OPER_CONST_T ); + fprintf( pFile, " );" ); + } + + fprintf( pFile, "\nendmodule\n\n" ); + fclose( pFile ); +} + + + + + + + +/**Function************************************************************* + + Synopsis [Compute roots (PO nodes in the TFO of the targets in F).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Acb_NtkFindRoots_rec( Acb_Ntk_t * p, int iObj, Vec_Bit_t * vBlock ) +{ + int * pFanin, iFanin, i, Res = 0; + if ( Acb_ObjIsTravIdPrev(p, iObj) ) + return 1; + if ( Acb_ObjSetTravIdCur(p, iObj) ) + return 0; + assert( !Acb_ObjIsCi(p, iObj) ); + Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, i ) + Res |= Acb_NtkFindRoots_rec( p, iFanin, vBlock ); + if ( Res ) Acb_ObjSetTravIdPrev( p, iObj ); + if ( Res ) Vec_BitWriteEntry( vBlock, iObj, 1 ); + return Res; +} +Vec_Int_t * Acb_NtkFindRoots( Acb_Ntk_t * p, Vec_Int_t * vTargets, Vec_Bit_t ** pvBlock ) +{ + int i, iObj; + Vec_Int_t * vRoots = Vec_IntAlloc( 1000 ); + Vec_Bit_t * vBlock = Vec_BitStart( Acb_NtkObjNum(p) ); + *pvBlock = vBlock; + // mark targets + Acb_NtkIncTravId( p ); + assert( Vec_IntSize(vTargets) > 0 ); + Vec_IntForEachEntry( vTargets, iObj, i ) + { + Acb_ObjSetTravIdCur( p, iObj ); + Vec_BitWriteEntry( vBlock, iObj, 1 ); + } + // mark inputs + Acb_NtkIncTravId( p ); + Acb_NtkForEachCi( p, iObj, i ) + Acb_ObjSetTravIdCur( p, iObj ); + // collect outputs reachable from targets + Acb_NtkForEachCoDriver( p, iObj, i ) + if ( Acb_NtkFindRoots_rec(p, iObj, vBlock) ) + Vec_IntPush( vRoots, i ); + //Vec_IntPrint( vRoots ); + return vRoots; +} + +/**Function************************************************************* + + Synopsis [Compute support in the TFI of the roots.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_NtkFindSupp_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vSupp ) +{ + int * pFanin, iFanin, i; + if ( Acb_ObjSetTravIdCur(p, iObj) ) + return; + if ( Acb_ObjIsCi(p, iObj) ) + Vec_IntPush( vSupp, Acb_ObjCioId(p, iObj) ); + else + Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, i ) + Acb_NtkFindSupp_rec( p, iFanin, vSupp ); +} +Vec_Int_t * Acb_NtkFindSupp( Acb_Ntk_t * p, Vec_Int_t * vRoots ) +{ + int i, iObj; + Vec_Int_t * vSupp = Vec_IntAlloc( 1000 ); + Acb_NtkIncTravId( p ); + Acb_NtkForEachCoDriverVec( vRoots, p, iObj, i ) + Acb_NtkFindSupp_rec( p, iObj, vSupp ); + Vec_IntSort( vSupp, 0 ); + //Vec_IntPrint( vSupp ); + return vSupp; +} + +/**Function************************************************************* + + Synopsis [Collect divisors whose support is completely contained in vSupp.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Acb_NtkFindDivs_rec( Acb_Ntk_t * p, int iObj ) +{ + int * pFanin, iFanin, i, Res = 1; + if ( Acb_ObjIsTravIdPrev(p, iObj) ) + return 1; + if ( Acb_ObjSetTravIdCur(p, iObj) ) + return 0; + if ( Acb_ObjIsCi(p, iObj) ) + return 0; + Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, i ) + Res &= Acb_NtkFindDivs_rec( p, iFanin ); + if ( Res ) Acb_ObjSetTravIdPrev( p, iObj ); + return Res; +} +Vec_Int_t * Acb_NtkFindDivsCis( Acb_Ntk_t * p, Vec_Int_t * vSupp ) +{ + int i, iObj; + Vec_Int_t * vDivs = Vec_IntAlloc( Vec_IntSize(vSupp) ); + Acb_NtkForEachCiVec( vSupp, p, iObj, i ) + { + assert( Acb_ObjWeight(p, iObj) > 0 ); + Vec_IntPush( vDivs, iObj ); + } + printf( "Divisors are %d support variables (CIs in the TFO of the targets).\n", Vec_IntSize(vSupp) ); + return vDivs; +} +Vec_Int_t * Acb_NtkFindDivs( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Bit_t * vBlock ) +{ + int fPrintWeights = 0; + int nDivLimit = 3000; + int i, iObj; + Vec_Int_t * vDivs = Vec_IntAlloc( 1000 ); + // mark inputs + Acb_NtkIncTravId( p ); + Acb_NtkForEachCiVec( vSupp, p, iObj, i ) + { + Acb_ObjSetTravIdCur( p, iObj ); + if ( Acb_ObjWeight(p, iObj) > 0 ) + Vec_IntPush( vDivs, iObj ); + } + // collect nodes whose support is contained in vSupp + Acb_NtkIncTravId( p ); + Acb_NtkForEachNode( p, iObj ) + if ( !Vec_BitEntry(vBlock, iObj) && Acb_ObjWeight(p, iObj) > 0 && Acb_NtkFindDivs_rec(p, iObj) ) + Vec_IntPush( vDivs, iObj ); + // sort divisors by cost (first cheap ones; later expensive ones) + Vec_IntSelectSortCost( Vec_IntArray(vDivs), Vec_IntSize(vDivs), &p->vObjWeight ); + //Vec_IntPrint( vDivs ); + nDivLimit = Abc_MinInt( Vec_IntSize(vDivs), nDivLimit ); + if ( fPrintWeights ) + { +// Vec_IntForEachEntryStop( vDivs, iObj, i, nDivLimit ) +// printf( "%d:%d (w=%d) ", i, iObj, Vec_IntEntry(&p->vObjWeight, iObj) ); +// printf( "\n" ); + + printf( " : " ); + Vec_IntForEachEntryStop( vDivs, iObj, i, nDivLimit ) + printf( "%d", (Vec_IntEntry(&p->vObjWeight, iObj) / 100) % 10 ); + printf( "\n" ); + printf( " : " ); + Vec_IntForEachEntryStop( vDivs, iObj, i, nDivLimit ) + printf( "%d", (Vec_IntEntry(&p->vObjWeight, iObj) / 10) % 10 ); + printf( "\n" ); + printf( " : " ); + Vec_IntForEachEntryStop( vDivs, iObj, i, nDivLimit ) + printf( "%d", (Vec_IntEntry(&p->vObjWeight, iObj) / 1) % 10 ); + printf( "\n" ); + } + printf( "Reducing divisor set from %d to ", Vec_IntSize(vDivs) ); + Vec_IntShrink( vDivs, nDivLimit ); + printf( "%d.\n", Vec_IntSize(vDivs) ); + return vDivs; +} + +/**Function************************************************************* + + Synopsis [Compute support and internal nodes in the TFI of the roots.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_NtkFindNodes_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vNodes ) +{ + int * pFanin, iFanin, i; + if ( Acb_ObjSetTravIdCur(p, iObj) ) + return; + if ( Acb_ObjIsCi(p, iObj) ) + return; + Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, i ) + Acb_NtkFindNodes_rec( p, iFanin, vNodes ); + assert( !Acb_ObjIsCo(p, iObj) ); + Vec_IntPush( vNodes, iObj ); +} +Vec_Int_t * Acb_NtkFindNodes( Acb_Ntk_t * p, Vec_Int_t * vRoots, Vec_Int_t * vDivs ) +{ + int i, iObj; + Vec_Int_t * vNodes = Vec_IntAlloc( 1000 ); + Acb_NtkIncTravId( p ); + Acb_NtkForEachCoDriverVec( vRoots, p, iObj, i ) + Acb_NtkFindNodes_rec( p, iObj, vNodes ); + if ( vDivs ) + Vec_IntForEachEntry( vDivs, iObj, i ) + Acb_NtkFindNodes_rec( p, iObj, vNodes ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Derive AIG for one network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Acb_ObjToGia( Gia_Man_t * pNew, Acb_Ntk_t * p, int iObj, Vec_Int_t * vTemp ) +{ + int * pFanin, iFanin, k, Type, Res; + assert( !Acb_ObjIsCio(p, iObj) ); + Vec_IntClear( vTemp ); + Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, k ) + Vec_IntPush( vTemp, Acb_ObjCopy(p, iFanin) ); + Type = Acb_ObjType( p, iObj ); + if ( Type == ABC_OPER_CONST_F ) + return 0; + if ( Type == ABC_OPER_CONST_T ) + return 1; + if ( Type == ABC_OPER_BIT_BUF ) + return Vec_IntEntry(vTemp, 0); + if ( Type == ABC_OPER_BIT_INV ) + return Abc_LitNot( Vec_IntEntry(vTemp, 0) ); + if ( Type == ABC_OPER_BIT_AND || Type == ABC_OPER_BIT_NAND ) + { + Res = 1; + Vec_IntForEachEntry( vTemp, iFanin, k ) + Res = Gia_ManHashAnd( pNew, Res, iFanin ); + return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NAND ); + } + if ( Type == ABC_OPER_BIT_OR || Type == ABC_OPER_BIT_NOR ) + { + Res = 0; + Vec_IntForEachEntry( vTemp, iFanin, k ) + Res = Gia_ManHashOr( pNew, Res, iFanin ); + return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NOR ); + } + if ( Type == ABC_OPER_BIT_XOR || Type == ABC_OPER_BIT_NXOR ) + { + Res = 0; + Vec_IntForEachEntry( vTemp, iFanin, k ) + Res = Gia_ManHashXor( pNew, Res, iFanin ); + return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NXOR ); + } + assert( 0 ); + return -1; +} +Gia_Man_t * Acb_NtkToGia( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Int_t * vNodes, Vec_Int_t * vRoots, Vec_Int_t * vDivs, Vec_Int_t * vTargets ) +{ + Gia_Man_t * pNew, * pOne; + Vec_Int_t * vFanins; + int i, iObj; + pNew = Gia_ManStart( 2 * Acb_NtkObjNum(p) + 1000 ); + Gia_ManHashAlloc( pNew ); + Acb_NtkCleanObjCopies( p ); + // create primary inputs + Acb_NtkForEachCiVec( vSupp, p, iObj, i ) + Acb_ObjSetCopy( p, iObj, Gia_ManAppendCi(pNew) ); + // add targets as primary inputs + if ( vTargets ) + Vec_IntForEachEntry( vTargets, iObj, i ) + Acb_ObjSetCopy( p, iObj, Gia_ManAppendCi(pNew) ); + // bit-blast internal nodes + vFanins = Vec_IntAlloc( 4 ); + Vec_IntForEachEntry( vNodes, iObj, i ) + if ( Acb_ObjCopy(p, iObj) == -1 ) // skip targets assigned above + Acb_ObjSetCopy( p, iObj, Acb_ObjToGia(pNew, p, iObj, vFanins) ); + Vec_IntFree( vFanins ); + // create primary outputs + Acb_NtkForEachCoDriverVec( vRoots, p, iObj, i ) + Gia_ManAppendCo( pNew, Acb_ObjCopy(p, iObj) ); + // add divisor as primary outputs (if the divisors are not primary inputs) + if ( vDivs && Vec_IntSize(vDivs) > Vec_IntSize(vSupp) ) + Vec_IntForEachEntry( vDivs, iObj, i ) + Gia_ManAppendCo( pNew, Acb_ObjCopy(p, iObj) ); + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pOne = pNew ); + Gia_ManStop( pOne ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Derive miter of two AIGs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Acb_CreateMiter( Gia_Man_t * pF, Gia_Man_t * pG ) +{ + Gia_Man_t * pNew, * pOne; + Gia_Obj_t * pObj; + int i, iMiter = 0, iXor; + Gia_ManFillValue( pF ); + Gia_ManFillValue( pG ); + pNew = Gia_ManStart( Gia_ManObjNum(pF) + Gia_ManObjNum(pF) + 1000 ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(pF)->Value = 0; + Gia_ManConst0(pG)->Value = 0; + Gia_ManForEachCi( pF, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachCi( pG, pObj, i ) + pObj->Value = Gia_ManCi(pF, i)->Value; + Gia_ManForEachAnd( pF, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachAnd( pG, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( pG, pObj, i ) + { + iXor = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(pF, i)) ); + iMiter = Gia_ManHashOr( pNew, iMiter, iXor ); + } + Gia_ManAppendCo( pNew, iMiter ); + Gia_ManForEachCo( pF, pObj, i ) + if ( i >= Gia_ManCoNum(pG) ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pOne = pNew ); + Gia_ManStop( pOne ); + return pNew; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -43,8 +772,1771 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -void Acb_NtkTestRun( char * pFileNames[3], int fVerbose ) +#define NWORDS 64 + +void Vec_IntPermute( Vec_Int_t * p ) +{ + int i, nSize = Vec_IntSize( p ); + int * pArray = Vec_IntArray( p ); + srand( time(NULL) ); + for ( i = 0; i < nSize; i++ ) + { + int j = rand()%nSize; + ABC_SWAP( int, pArray[i], pArray[j] ); + } +} + +void Acb_PrintPatterns( Vec_Wrd_t * vPats, int nPats, Vec_Int_t * vWeights ) +{ + int i, k, Entry, nDivs = Vec_IntSize(vWeights); + printf( " : " ); + Vec_IntForEachEntry( vWeights, Entry, i ) + printf( "%d", (Entry / 100) % 10 ); + printf( "\n" ); + printf( " : " ); + Vec_IntForEachEntry( vWeights, Entry, i ) + printf( "%d", (Entry / 10) % 10 ); + printf( "\n" ); + printf( " : " ); + Vec_IntForEachEntry( vWeights, Entry, i ) + printf( "%d", (Entry / 1) % 10 ); + printf( "\n" ); + printf( "\n" ); + + printf( " : " ); + for ( i = 0; i < nDivs; i++ ) + printf( "%d", (i / 100) % 10 ); + printf( "\n" ); + printf( " : " ); + for ( i = 0; i < nDivs; i++ ) + printf( "%d", (i / 10) % 10 ); + printf( "\n" ); + printf( " : " ); + for ( i = 0; i < nDivs; i++ ) + printf( "%d", i % 10 ); + printf( "\n" ); + printf( "\n" ); + + for ( k = 0; k < nPats; k++ ) + { + printf( "%3d : ", k ); + for ( i = 0; i < nDivs; i++ ) + printf( "%c", Abc_TtGetBit(Vec_WrdEntryP(vPats, NWORDS*i), k) ? '*' : '|' ); + printf( "\n" ); + } + printf( "\n" ); +} + +Vec_Int_t * Acb_DeriveWeights( Vec_Int_t * vDivs, Acb_Ntk_t * pNtkF ) +{ + int i, iDiv; + Vec_Int_t * vWeights = Vec_IntAlloc( Vec_IntSize(vDivs) ); + Vec_IntForEachEntry( vDivs, iDiv, i ) + Vec_IntPush( vWeights, Vec_IntEntry(&pNtkF->vObjWeight, iDiv) ); + return vWeights; +} +int Acb_ComputeSuppCost( Vec_Int_t * vSupp, Vec_Int_t * vWeights, int iFirstDiv ) +{ + int i, Entry, Cost = 0; + Vec_IntForEachEntry( vSupp, Entry, i ) + Cost += Vec_IntEntry( vWeights, Abc_Lit2Var(Entry) - iFirstDiv ); + return Cost; +} +Vec_Int_t * Acb_FindSupportStart( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeights, Vec_Wrd_t ** pvPats, int * piPats ) +{ + int i, status, nDivs = Vec_IntSize(vWeights); + Vec_Int_t * vSupp = Vec_IntAlloc( 100 ); + Vec_Wrd_t * vPats = Vec_WrdStart( NWORDS * nDivs ); + int iPat = 0; + while ( 1 ) + { + int fFound = 0; + // try one run + status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 ); + if ( status == l_False ) + break; + assert( status == l_True ); + // collect pattern + for ( i = 0; i < nDivs; i++ ) + { + if ( sat_solver_var_value(pSat, iFirstDiv+i) == 0 ) + continue; + Abc_TtSetBit( Vec_WrdEntryP(vPats, NWORDS*i), iPat ); + if ( fFound ) + continue; + // process new divisor + Vec_IntPush( vSupp, Abc_Var2Lit(iFirstDiv+i, 1) ); + //printf( "Selecting divisor %d with weight %d\n", i, Vec_IntEntry(vWeights, i) ); + fFound = 1; + } + assert( fFound ); + iPat++; + } + *piPats = iPat; + *pvPats = vPats; + Vec_IntSort( vSupp, 0 ); + return vSupp; +} +int Acb_FindArgMaxUnderMask( Vec_Wrd_t * vPats, word Mask[NWORDS], Vec_Int_t * vWeights, int nPats ) +{ + int nDivs = Vec_WrdSize(vPats)/NWORDS; + int nWords = Abc_Bit6WordNum(nPats); + int i, iBest = -1; + int Cost, CostBest = -1; + for ( i = 0; i < nDivs; i++ ) + { + word * pPat = Vec_WrdEntryP(vPats, NWORDS*i); + Cost = Abc_TtCountOnesVecMask(Mask, pPat, nWords, 0); + if ( CostBest < Cost ) +// if ( CostBest == -1 || (float)CostBest/Cost < 0.6*(float)Vec_IntEntry(vWeights, iBest)/Vec_IntEntry(vWeights, i) ) +// if ( CostBest == -1 || (float)CostBest/Cost < 0.67*(float)Vec_IntEntry(vWeights, iBest)/Vec_IntEntry(vWeights, i) ) + { + CostBest = Cost; + iBest = i; + } + } + return iBest; +} +int Acb_FindArgMaxUnderMask2( Vec_Wrd_t * vPats, word Mask[NWORDS], Vec_Int_t * vWeights, int nPats ) +{ + int nDivs = Vec_WrdSize(vPats)/NWORDS; + int i, b, iBest = -1; + int Cost, CostBest = -1; + // count how many times each of them appears + Vec_Int_t * vCounts = Vec_IntStart(nPats); + for ( i = 0; i < nDivs; i++ ) + { + word * pPat = Vec_WrdEntryP(vPats, NWORDS*i); + for ( b = 0; b < nPats; b++ ) + if ( Abc_TtGetBit(pPat, b) ) + Vec_IntAddToEntry( vCounts, b, 1 ); + } + for ( i = 0; i < nDivs; i++ ) + { + word * pPat = Vec_WrdEntryP(vPats, NWORDS*i); +// Cost = Abc_TtCountOnesVecMask(Mask, pPat, NWORDS, 0); + Cost = 0; + for ( b = 0; b < nPats; b++ ) + if ( Abc_TtGetBit(pPat, b) && Abc_TtGetBit(Mask, b) ) + Cost += 1000000/Vec_IntEntry(vCounts, b); + if ( CostBest < Cost ) + { + CostBest = Cost; + iBest = i; + } + } + Vec_IntFree( vCounts ); + return iBest; +} + +Vec_Int_t * Acb_FindSupportNext( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeights, Vec_Wrd_t * vPats, int * pnPats ) { + int i, status, nDivs = Vec_IntSize(vWeights); + Vec_Int_t * vSupp = Vec_IntAlloc( 100 ); + word * pMask, Mask[NWORDS]; Abc_TtConst( Mask, NWORDS, 1 ); + while ( 1 ) + { + int iDivBest = Acb_FindArgMaxUnderMask( vPats, Mask, vWeights, *pnPats ); + Vec_IntPush( vSupp, Abc_Var2Lit(iFirstDiv+iDivBest, 1) ); + //printf( "Selecting divisor %d with weight %d\n", iDivBest, Vec_IntEntry(vWeights, iDivBest) ); +// Mask &= ~Vec_WrdEntry( vPats, iDivBest ); + pMask = Vec_WrdEntryP( vPats, NWORDS*iDivBest ); + Abc_TtAndSharp( Mask, Mask, pMask, NWORDS, 1 ); + + // try one run + status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 ); + if ( status == l_False ) + break; + assert( status == l_True ); + // collect pattern + for ( i = 0; i < nDivs; i++ ) + { + if ( sat_solver_var_value(pSat, iFirstDiv+i) == 0 ) + continue; + Abc_TtSetBit( Vec_WrdEntryP(vPats, NWORDS*i), *pnPats ); + } + (*pnPats)++; + if ( *pnPats == NWORDS*64 ) + { + Vec_IntFreeP( &vSupp ); + return NULL; + } + assert( *pnPats < NWORDS*64 ); + //Acb_PrintPatterns( vPats, *pnPats, vWeights ); + //i = i; + } + Vec_IntSort( vSupp, 0 ); + return vSupp; +} +Vec_Int_t * Acb_FindSupportMinOne( sat_solver * pSat, int iFirstDiv, Vec_Wrd_t * vPats, int * pnPats, Vec_Int_t * vSupp, int iVar ) +{ + int i, iLit, status; + int nDivs = Vec_WrdSize(vPats)/NWORDS; + Vec_Int_t * vLits = Vec_IntAlloc( Vec_IntSize(vSupp) ); + Vec_IntForEachEntry( vSupp, iLit, i ) + if ( i != iVar ) + Vec_IntPush( vLits, iLit ); + // try one run + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), 0, 0, 0, 0 ); + if ( status == l_False ) + return vLits; + Vec_IntFree( vLits ); + assert( status == l_True ); + // collect pattern + for ( i = 0; i < nDivs; i++ ) + { + if ( sat_solver_var_value(pSat, iFirstDiv+i) == 0 ) + continue; + Abc_TtSetBit( Vec_WrdEntryP(vPats, NWORDS*i), *pnPats ); + } + (*pnPats)++; + if ( *pnPats == NWORDS*64 ) + return NULL; + return vSupp; +} +Vec_Int_t * Acb_FindSupportMin( sat_solver * pSat, int iFirstDiv, Vec_Wrd_t * vPats, int * pnPats, Vec_Int_t * vSuppStart ) +{ + Vec_Int_t * vTemp, * vSupp = Vec_IntDup( vSuppStart ); int i; + for ( i = Vec_IntSize(vSupp)-1; i >= 0; i-- ) + { + vSupp = Acb_FindSupportMinOne( pSat, iFirstDiv, vPats, pnPats, vTemp = vSupp, i ); + if ( vTemp != vSupp ) + Vec_IntFree( vTemp ); + if ( vSupp == NULL ) + return NULL; + } + return vSupp; +} +void Acb_FindReplace( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeights, Vec_Wrd_t * vPats, int nPats, Vec_Int_t * vSupp ) +{ + int i, k, iLit, iLit2, status, nWords = Abc_Bit6WordNum(nPats); + word Covered[NWORDS], Both[NWORDS], Mask[NWORDS], * pMask; + assert( nWords <= NWORDS ); + // prepare constant pattern + Abc_TtConst( Mask, nWords, 0 ); + for ( i = 0; i < nPats; i++ ) + Abc_TtSetBit( Mask, i ); + // try to replace each by a cheaper one + Vec_IntForEachEntry( vSupp, iLit, i ) + { + int iDiv = Abc_Lit2Var(iLit) - iFirstDiv; + // collect covered except by this one + Abc_TtConst( Covered, nWords, 0 ); + Vec_IntForEachEntry( vSupp, iLit2, k ) + { + if ( iLit2 == iLit ) + continue; + pMask = Vec_WrdEntryP( vPats, NWORDS*(Abc_Lit2Var(iLit2) - iFirstDiv) ); + Abc_TtOr( Covered, Covered, pMask, nWords ); + } + // consider any cheaper ones that this one + for ( k = 0; k < iDiv; k++ ) + { + if ( Vec_IntEntry(vWeights, k) == Vec_IntEntry(vWeights, iDiv) ) + continue; + assert( Vec_IntEntry(vWeights, k) < Vec_IntEntry(vWeights, iDiv) ); + pMask = Vec_WrdEntryP( vPats, NWORDS*k ); + // check if it covers the remaining ones + Abc_TtOr( Both, Covered, pMask, nWords ); + if ( !Abc_TtEqual(Both, Mask, nWords) ) + continue; + // try this one + Vec_IntWriteEntry( vSupp, i, Abc_Var2Lit(iFirstDiv+k, 1) ); + status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 ); + if ( status == l_False ) // success + { + //printf( "Replacing %d(%d) by %d(%d) with const difference %d.\n", + // iDiv, Vec_IntEntry(vWeights, iDiv), k, Vec_IntEntry(vWeights, k), + // Vec_IntEntry(vWeights, iDiv) - Vec_IntEntry(vWeights, k) ); + break; + } + Vec_IntWriteEntry( vSupp, i, iLit ); + } + } +} + +Vec_Int_t * Acb_FindSupport( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeights, Vec_Int_t * vSuppStart, int TimeOut ) +{ + abctime clkLimit = TimeOut * CLOCKS_PER_SEC + Abc_Clock(); + Vec_Wrd_t * vPats = NULL; + int nPats = 0; + Vec_Int_t * vSuppBest, * vSupp;//, * vTemp; + int CostBest, Cost; + int Iter; + + // find initial best + CostBest = Acb_ComputeSuppCost( vSuppStart, vWeights, iFirstDiv ); + vSuppBest = Vec_IntDup( vSuppStart ); + printf( "Starting cost = %d.\n", CostBest ); + + // interatively find the one with the most ones in the uncovered rows + for ( Iter = 0; Iter < 200; Iter++ ) + { + if ( Abc_Clock() > clkLimit ) + { + Vec_IntFree( vSuppBest ); + Vec_WrdFree( vPats ); + return NULL; + } + if ( Iter == 0 ) + vSupp = Acb_FindSupportStart( pSat, iFirstDiv, vWeights, &vPats, &nPats ); + else + vSupp = Acb_FindSupportNext( pSat, iFirstDiv, vWeights, vPats, &nPats ); + if ( vSupp == NULL ) + break; + //vSupp = Acb_FindSupportMin( pSat, iFirstDiv, vPats, &nPats, vTemp = vSupp ); + //Vec_IntFree( vTemp ); + if ( vSupp == NULL ) + break; + Cost = Acb_ComputeSuppCost( vSupp, vWeights, iFirstDiv ); + //Acb_PrintPatterns( vPats, nPats, vWeights ); + if ( CostBest > Cost ) + { + CostBest = Cost; + ABC_SWAP( Vec_Int_t *, vSuppBest, vSupp ); + printf( "Iter %4d: Next cost = %d. ", Iter, Cost ); + printf( "Updating best solution.\n" ); + } + Vec_IntFree( vSupp ); + } + Acb_FindReplace( pSat, iFirstDiv, vWeights, vPats, nPats, vSuppBest ); + + //printf( "Number of patterns = %d.\n", nPats ); + Vec_WrdFree( vPats ); + return vSuppBest; +} + +/**Function************************************************************* + + Synopsis [Compute the best support of the targets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Acb_DerivePatchSupport( Cnf_Dat_t * pCnf, int iTar, int nTargets, int nCoDivs, Vec_Int_t * vDivs, Acb_Ntk_t * pNtkF, Vec_Int_t * vSuppOld, int TimeOut ) +{ + Vec_Int_t * vSupp = Vec_IntAlloc( 100 ); + int i, Lit; + int iCoVarBeg = 1; + int iCiVarBeg = pCnf->nVars - nTargets; + sat_solver * pSat = sat_solver_new(); + sat_solver_setnvars( pSat, 2 * pCnf->nVars + nCoDivs ); + // add clauses + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + return NULL; + // add output clause + Lit = Abc_Var2Lit( iCoVarBeg, 0 ); + if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) + return NULL; + // add clauses + pCnf->pMan = NULL; + Cnf_DataLift( pCnf, pCnf->nVars ); + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + return NULL; + Cnf_DataLift( pCnf, -pCnf->nVars ); + // add output clause + Lit = Abc_Var2Lit( iCoVarBeg+pCnf->nVars, 0 ); + if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) + return NULL; + // create XORs for targets + // add negative literal + Lit = Abc_Var2Lit( iCiVarBeg + iTar, 1 ); + if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) + return NULL; + // add positive literal + Lit = Abc_Var2Lit( iCiVarBeg+pCnf->nVars + iTar, 0 ); + if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) + return NULL; + // create XORs for divisors + if ( nCoDivs > 0 ) + { + abctime clk = Abc_Clock(); + int fUseMinAssump = 1; + int iLit, nSuppNew, status; + int iDivVar = 2 * pCnf->nVars; + int pLits[2]; + int j = 0, iDivOld; + Vec_IntClear( vSupp ); + if ( vSuppOld ) + { + // start with predefined support + Vec_IntForEachEntry( vSuppOld, iDivOld, j ) + { + int iVar0 = iCoVarBeg+1+iDivOld; + int iVar1 = iCoVarBeg+1+iDivOld+pCnf->nVars; + //printf( "Selecting predefined divisor %d with weight %d\n", + // iDivOld, Vec_IntEntry(&pNtkF->vObjWeight, Vec_IntEntry(vDivs, iDivOld)) ); + // add equality clauses + pLits[0] = Abc_Var2Lit( iVar0, 0 ); + pLits[1] = Abc_Var2Lit( iVar1, 1 ); + if ( !sat_solver_addclause( pSat, pLits, pLits+2 ) ) + { + printf( "Unsat is detected earlier.\n" ); + status = l_False; + break; + } + pLits[0] = Abc_Var2Lit( iVar0, 1 ); + pLits[1] = Abc_Var2Lit( iVar1, 0 ); + if ( !sat_solver_addclause( pSat, pLits, pLits+2 ) ) + { + printf( "Unsat is detected earlier.\n" ); + status = l_False; + break; + } + } + } + if ( vSuppOld == NULL || j == Vec_IntSize(vSuppOld) ) + { + for ( i = 0; i < nCoDivs; i++ ) + { + sat_solver_add_xor( pSat, iDivVar+i, iCoVarBeg+1+i, iCoVarBeg+1+i+pCnf->nVars, 0 ); + Vec_IntPush( vSupp, Abc_Var2Lit(iDivVar+i, 1) ); + } + // try one run + if ( TimeOut ) sat_solver_set_runtime_limit( pSat, TimeOut * CLOCKS_PER_SEC + Abc_Clock() ); + status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 ); + if ( TimeOut ) sat_solver_set_runtime_limit( pSat, 0 ); + if ( status != l_False ) + { + printf( "Support computation timed out after %d sec.\n", TimeOut ); + sat_solver_delete( pSat ); + Vec_IntFree( vSupp ); + return NULL; + } + assert( status == l_False ); + printf( "Proved that the problem has a solution. " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + // find minimum subset + if ( fUseMinAssump ) + { + // solve in a standard way + abctime clk = Abc_Clock(); + nSuppNew = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 ); + Vec_IntShrink( vSupp, nSuppNew ); + Vec_IntSort( vSupp, 0 ); + printf( "Found one feasible set of %d divisors. ", Vec_IntSize(vSupp) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + + // perform minimization + if ( Vec_IntSize(vSupp) > 0 ) + { + abctime clk = Abc_Clock(); + Vec_Int_t * vTemp, * vWeights = Acb_DeriveWeights( vDivs, pNtkF ); + vSupp = Acb_FindSupport( pSat, iDivVar, vWeights, vTemp = vSupp, TimeOut ); + Vec_IntFree( vWeights ); + Vec_IntFree( vTemp ); + if ( vSupp == NULL ) + { + printf( "Support minimization timed out after %d sec.\n", TimeOut ); + sat_solver_delete( pSat ); + return NULL; + } + printf( "Minimized support to %d supp vars. ", Vec_IntSize(vSupp) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + } + else + { + int * pFinal, nFinal = sat_solver_final( pSat, &pFinal ); + printf( "AnalyzeFinal returned %d (out of %d).\n", nFinal, Vec_IntSize(vSupp) ); + Vec_IntClear( vSupp ); + for ( i = 0; i < nFinal; i++ ) + Vec_IntPush( vSupp, Abc_LitNot(pFinal[i]) ); + // try one run + status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 ); + assert( status == l_False ); + // try again + nFinal = sat_solver_final( pSat, &pFinal ); + printf( "AnalyzeFinal returned %d (out of %d).\n", nFinal, Vec_IntSize(vSupp) ); + } + // remap them into numbers + Vec_IntForEachEntry( vSupp, iLit, i ) + Vec_IntWriteEntry( vSupp, i, Abc_Lit2Var(iLit)-iDivVar ); + Vec_IntSort( vSupp, 0 ); + } + } + sat_solver_delete( pSat ); + if ( vSupp ) Vec_IntSort( vSupp, 0 ); + return vSupp; +} + +static inline int satoko_add_xor( satoko_t * pSat, int iVarA, int iVarB, int iVarC, int fCompl ) +{ + int Lits[3]; + int Cid; + assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 ); + + Lits[0] = toLitCond( iVarA, !fCompl ); + Lits[1] = toLitCond( iVarB, 1 ); + Lits[2] = toLitCond( iVarC, 1 ); + Cid = satoko_add_clause( pSat, Lits, 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarA, !fCompl ); + Lits[1] = toLitCond( iVarB, 0 ); + Lits[2] = toLitCond( iVarC, 0 ); + Cid = satoko_add_clause( pSat, Lits, 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarA, fCompl ); + Lits[1] = toLitCond( iVarB, 1 ); + Lits[2] = toLitCond( iVarC, 0 ); + Cid = satoko_add_clause( pSat, Lits, 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarA, fCompl ); + Lits[1] = toLitCond( iVarB, 0 ); + Lits[2] = toLitCond( iVarC, 1 ); + Cid = satoko_add_clause( pSat, Lits, 3 ); + assert( Cid ); + return 4; +} +Vec_Int_t * Acb_DerivePatchSupportS( Cnf_Dat_t * pCnf, int nCiTars, int nCoDivs, Vec_Int_t * vDivs, Acb_Ntk_t * pNtkF, Vec_Int_t * vSuppOld, int TimeOut ) +{ + Vec_Int_t * vSupp = Vec_IntAlloc( 100 ); + int i, Lit; + int iCoVarBeg = 1; + int iCiVarBeg = pCnf->nVars - nCiTars; + satoko_t * pSat = satoko_create(); + satoko_setnvars( pSat, 2 * pCnf->nVars + nCiTars + nCoDivs ); + satoko_options(pSat)->no_simplify = 1; + // add clauses + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !satoko_add_clause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) + return NULL; + // add output clause + Lit = Abc_Var2Lit( iCoVarBeg, 0 ); + if ( !satoko_add_clause( pSat, &Lit, 1 ) ) + return NULL; + // add clauses + pCnf->pMan = NULL; + Cnf_DataLift( pCnf, pCnf->nVars ); + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !satoko_add_clause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) + return NULL; + Cnf_DataLift( pCnf, -pCnf->nVars ); + // add output clause + Lit = Abc_Var2Lit( iCoVarBeg+pCnf->nVars, 0 ); + if ( !satoko_add_clause( pSat, &Lit, 1 ) ) + return NULL; + // create XORs for targets + if ( nCiTars > 0 ) + { +/* + int iXorVar = 2 * pCnf->nVars; + int Lit; + Vec_IntClear( vSupp ); + for ( i = 0; i < nCiTars; i++ ) + { + satoko_add_xor( pSat, iXorVar+i, iCiVarBeg+i, iCiVarBeg+i+pCnf->nVars, 0 ); + Vec_IntPush( vSupp, Abc_Var2Lit(iXorVar+i, 0) ); + } + if ( !satoko_add_clause( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp) ) ) + return NULL; +*/ + // add negative literal + Lit = Abc_Var2Lit( iCiVarBeg, 1 ); + if ( !satoko_add_clause( pSat, &Lit, 1 ) ) + return NULL; + // add positive literal + Lit = Abc_Var2Lit( iCiVarBeg+pCnf->nVars, 0 ); + if ( !satoko_add_clause( pSat, &Lit, 1 ) ) + return NULL; + } + // create XORs for divisors + if ( nCoDivs > 0 ) + { + abctime clk = Abc_Clock(); + int fUseMinAssump = 1; + int iLit, status, nSuppNew; + int iDivVar = 2 * pCnf->nVars + nCiTars; + Vec_IntClear( vSupp ); + for ( i = 0; i < nCoDivs; i++ ) + { + satoko_add_xor( pSat, iDivVar+i, iCoVarBeg+1+i, iCoVarBeg+1+i+pCnf->nVars, 0 ); + Vec_IntPush( vSupp, Abc_Var2Lit(iDivVar+i, 1) ); +/* + pLits[0] = Abc_Var2Lit(iCoVarBeg+1+i, 1); + pLits[1] = Abc_Var2Lit(iCoVarBeg+1+i+pCnf->nVars, 0); + pLits[2] = Abc_Var2Lit(iDivVar+i, 1); + if ( !satoko_add_clause( pSat, pLits, 3 ) ) + assert( 0 ); + + pLits[0] = Abc_Var2Lit(iCoVarBeg+1+i, 0); + pLits[1] = Abc_Var2Lit(iCoVarBeg+1+i+pCnf->nVars, 1); + pLits[2] = Abc_Var2Lit(iDivVar+i, 1); + if ( !satoko_add_clause( pSat, pLits, 3 ) ) + assert( 0 ); + + Vec_IntPush( vSupp, Abc_Var2Lit(iDivVar+i, 0) ); +*/ + } + + // try one run + status = satoko_solve_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp) ); + if ( status != l_False ) + { + printf( "Demonstrated that the problem has NO solution. " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + satoko_destroy( pSat ); + Vec_IntFree( vSupp ); + return NULL; + } + assert( status == l_False ); + printf( "Proved that the problem has a solution. " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + + // find minimum subset + if ( fUseMinAssump ) + { + abctime clk = Abc_Clock(); + nSuppNew = satoko_minimize_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 ); + Vec_IntShrink( vSupp, nSuppNew ); + printf( "Solved the problem with %d supp vars. ", Vec_IntSize(vSupp) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + else + { + int * pFinal, nFinal = satoko_final_conflict( pSat, &pFinal ); + printf( "AnalyzeFinal returned %d (out of %d).\n", nFinal, Vec_IntSize(vSupp) ); + Vec_IntClear( vSupp ); + for ( i = 0; i < nFinal; i++ ) + Vec_IntPush( vSupp, Abc_LitNot(pFinal[i]) ); + // try one run + status = satoko_solve_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp) ); + assert( status == l_False ); + // try again + nFinal = satoko_final_conflict( pSat, &pFinal ); + printf( "AnalyzeFinal returned %d (out of %d).\n", nFinal, Vec_IntSize(vSupp) ); + } + + // remap them into numbers + Vec_IntForEachEntry( vSupp, iLit, i ) + Vec_IntWriteEntry( vSupp, i, Abc_Lit2Var(iLit)-iDivVar ); + Vec_IntSort( vSupp, 0 ); + //Vec_IntPrint( vSupp ); + } + satoko_destroy( pSat ); + Vec_IntSort( vSupp, 0 ); + return vSupp; +} + + +/**Function************************************************************* + + Synopsis [Compute functions of the targets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Acb_EnumerateSatAssigns( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vTempLits, Vec_Str_t * vTempSop ) +{ + int fCreatePrime = 1; + int status, i, iMint, iVar, iLit, nFinal, * pFinal, pLits[2]; + Vec_Int_t * vTemp, * vLits; + assert( FreeVar < sat_solver_nvars(pSat) ); + pLits[0] = Abc_Var2Lit( PivotVar, 1 ); // F = 1 + pLits[1] = Abc_Var2Lit( FreeVar, 0 ); // iNewLit + Vec_StrClear( vTempSop ); + Vec_StrGrow( vTempSop, 8 * (Vec_IntSize(vDivVars) + 3) + 1 ); + // check constant 0 + status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 ); + if ( status == l_False ) + { + Vec_StrPush( vTempSop, ' ' ); + Vec_StrPush( vTempSop, '0' ); + Vec_StrPush( vTempSop, '\n' ); + Vec_StrPush( vTempSop, '\0' ); + return Vec_StrReleaseArray(vTempSop); + } + // check constant 1 + pLits[0] = Abc_LitNot(pLits[0]); + status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 ); + pLits[0] = Abc_LitNot(pLits[0]); + if ( status == l_False || Vec_IntSize(vDivVars) == 0 ) + { + Vec_StrPush( vTempSop, ' ' ); + Vec_StrPush( vTempSop, '1' ); + Vec_StrPush( vTempSop, '\n' ); + Vec_StrPush( vTempSop, '\0' ); + return Vec_StrReleaseArray(vTempSop); + } + //Vec_IntPrint( vDivVars ); + vTemp = Vec_IntAlloc( 100 ); + vLits = Vec_IntAlloc( 100 ); + for ( iMint = 0; ; iMint++ ) + { + if ( iMint == 1000 ) + { + printf( "Reached the limit on the number of cubes (1000).\n" ); + Vec_IntFree( vTemp ); + Vec_IntFree( vLits ); + return NULL; + } + //int Offset = Vec_StrSize(vTempSop); + // find onset minterm + status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 ); + if ( status == l_False ) + { + printf( "Finished enumerating %d cubes.\n", iMint ); + Vec_IntFree( vTemp ); + Vec_IntFree( vLits ); + Vec_StrPush( vTempSop, '\0' ); + return Vec_StrReleaseArray(vTempSop); + } + assert( status == l_True ); + // collect divisor literals + Vec_IntClear( vTempLits ); + Vec_IntPush( vTempLits, Abc_LitNot(pLits[0]) ); // F = 0 + //printf( "%8d %3d ", 0, 0 ); +// Vec_IntForEachEntry( vDivVars, iVar, i ) + Vec_IntForEachEntryReverse( vDivVars, iVar, i ) + { + Vec_IntPush( vTempLits, sat_solver_var_literal(pSat, iVar) ); + //printf( "%c", '0' + sat_solver_var_value(pSat, iVar) ); + } + //printf( "\n" ); + // create new cube + for ( i = 0; i < Vec_IntSize(vDivVars); i++ ) + Vec_StrPush( vTempSop, '-' ); + if ( fCreatePrime ) + { + // expand against offset + status = sat_solver_push(pSat, Vec_IntEntry(vTempLits, 0)); + assert( status == 1 ); + nFinal = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vTempLits)+1, Vec_IntSize(vTempLits)-1, 0 ); + Vec_IntShrink( vTempLits, nFinal+1 ); + sat_solver_pop(pSat); + // compute cube and add clause + Vec_IntWriteEntry( vTempLits, 0, Abc_LitNot(pLits[1]) ); // NOT(iNewLit) + Vec_IntForEachEntryStart( vTempLits, iLit, i, 1 ) + { + Vec_IntWriteEntry( vTempLits, i, Abc_LitNot(iLit) ); + iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(iLit) ); assert( iVar >= 0 ); + //uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar]; + Vec_StrWriteEntry( vTempSop, Vec_StrSize(vTempSop) - Vec_IntSize(vDivVars) + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) ); + } + } + else + { + // expand against offset + status = sat_solver_solve( pSat, Vec_IntArray(vTempLits), Vec_IntLimit(vTempLits), 0, 0, 0, 0 ); + if ( status != l_False ) + printf( "Selected onset minterm number %d belongs to the offset (this is a bug).\n", iMint ); + assert( status == l_False ); + + // compute cube and add clause + nFinal = sat_solver_final( pSat, &pFinal ); + Vec_IntSelectSort( pFinal, nFinal ); +/* + // pretend that this is final + veci_resize(&pSat->conf_final,0); + Vec_IntForEachEntry( vTempLits, iLit, i ) + veci_push(&pSat->conf_final, lit_neg(iLit)); + pFinal = pSat->conf_final.ptr; + nFinal = Vec_IntSize(vTempLits); +*/ + //////////////////////////////////////////////////////// + // create new cube + Vec_IntClear( vTemp ); + Vec_IntPush( vTemp, Abc_LitNot(pLits[0]) ); // F = 0 + for ( i = 0; i < nFinal; i++ ) + { + if ( pFinal[i] == pLits[0] ) + continue; + Vec_IntPush( vTemp, Abc_LitNot(pFinal[i]) ); + } + + //Vec_IntPrint( vTemp ); + // try removing each one starting with the last one + //printf( "Started with %d lits ", nFinal-1 ); + for ( i = nFinal - 1; i > 0; i-- ) + { + int iLit = Vec_IntEntry( vTemp, i ); + Vec_IntDrop( vTemp, i ); + // try SAT + status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), 0, 0, 0, 0 ); + if ( status == l_False ) + { + // printf( "U" ); + continue; + } + //if ( status == l_True ) + // printf( "S" ); + //else if ( status == l_Undef ) + // printf( "T" ); + Vec_IntInsert( vTemp, i, iLit ); + } + //printf( " Ended up with %d lits\n", Vec_IntSize(vTemp)-1 ); + //Vec_IntPrint( vTemp ); + + Vec_IntForEachEntry( vTemp, iLit, i ) + pFinal[i] = Abc_LitNot(iLit); + nFinal = Vec_IntSize(vTemp); + //////////////////////////////////////////////////////// + + + Vec_IntClear( vTempLits ); + Vec_IntPush( vTempLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit) + for ( i = 0; i < nFinal; i++ ) + { + if ( pFinal[i] == pLits[0] ) + continue; + Vec_IntPush( vTempLits, pFinal[i] ); + iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 ); + //uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar]; + Vec_StrWriteEntry( vTempSop, Vec_StrSize(vTempSop) - Vec_IntSize(vDivVars) + iVar, (char)('0' + Abc_LitIsCompl(pFinal[i])) ); + } + } + //printf( "%6d : %8d %3d ", iMint, (int)pSat->stats.conflicts, Vec_IntSize(vTempLits)-1 ); + + Vec_StrAppend( vTempSop, " 1\n" ); + status = sat_solver_addclause( pSat, Vec_IntArray(vTempLits), Vec_IntLimit(vTempLits) ); + assert( status ); + + //Vec_StrPush( vTempSop, '\0' ); + //printf( "%s", Vec_StrEntryP(vTempSop, Offset) ); + //Vec_StrPop( vTempSop ); + } + assert( 0 ); + return NULL; +} +char * Acb_DeriveOnePatchFunction( Cnf_Dat_t * pCnf, int iTar, int nTargets, int nCoDivs, Vec_Int_t * vUsed, int fCisOnly ) +{ + char * pSop = NULL; + Vec_Int_t * vTempLits = Vec_IntAlloc( Vec_IntSize(vUsed)+1 ); + Vec_Str_t * vTempSop = Vec_StrAlloc(0); + int i, Lit; + int iCiVarBeg = pCnf->nVars - nTargets - Vec_IntSize(vUsed); + int iCoVarBeg = 1, Index; + sat_solver * pSat = sat_solver_new(); + sat_solver_setnvars( pSat, pCnf->nVars + 1 ); + // add clauses + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + return NULL; + // add output clause + Lit = Abc_Var2Lit( iCoVarBeg, 0 ); + if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) + return NULL; + // remap vUsed to be in terms of divisor variables + if ( fCisOnly ) + { + Vec_IntForEachEntry( vUsed, Index, i ) + Vec_IntWriteEntry( vUsed, i, iCiVarBeg + Index ); + } + else + { + Vec_IntForEachEntry( vUsed, Index, i ) + Vec_IntWriteEntry( vUsed, i, iCoVarBeg + 1 + Index ); + } + // enumerate assignments for each target in terms of used divisors + pSop = Acb_EnumerateSatAssigns( pSat, pCnf->nVars - nTargets + iTar, pCnf->nVars, vUsed, vTempLits, vTempSop ); + Vec_IntFree( vTempLits ); + Vec_StrFree( vTempSop ); + sat_solver_delete( pSat ); + if ( pSop == NULL ) + return NULL; + //printf( "Function %d:\n%s", i, pSop ); + // remap vUsed to be in terms of original divisors + if ( fCisOnly ) + { + Vec_IntForEachEntry( vUsed, Index, i ) + Vec_IntWriteEntry( vUsed, i, Index - iCiVarBeg ); + } + else + { + Vec_IntForEachEntry( vUsed, Index, i ) + Vec_IntWriteEntry( vUsed, i, Index - (iCoVarBeg + 1) ); + } + return pSop; +} +int Acb_CheckMiter( Cnf_Dat_t * pCnf ) +{ + int iCoVarBeg = 1, i, Lit, status; + sat_solver * pSat = sat_solver_new(); + sat_solver_setnvars( pSat, pCnf->nVars ); + // add clauses + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + return 1; + // add output clause + Lit = Abc_Var2Lit( iCoVarBeg, 0 ); + if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) + return 1; + status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 ); + sat_solver_delete( pSat ); + return status == l_False; +} + + +/**Function************************************************************* + + Synopsis [Update miter by substituting the last target by a given function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_CollectIntNodes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + assert( Gia_ObjIsAnd(pObj) ); + Acb_CollectIntNodes_rec( p, Gia_ObjFanin0(pObj), vNodes ); + Acb_CollectIntNodes_rec( p, Gia_ObjFanin1(pObj), vNodes ); + Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); +} +void Acb_CollectIntNodes( Gia_Man_t * p, Vec_Int_t * vNodes0, Vec_Int_t * vNodes1 ) +{ + Gia_Obj_t * pObj; int i; + Vec_IntClear( vNodes0 ); + Vec_IntClear( vNodes1 ); + Gia_ManIncrementTravId( p ); + Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); + Gia_ManForEachCi( p, pObj, i ) + Gia_ObjSetTravIdCurrent( p, pObj ); + Gia_ManForEachCo( p, pObj, i ) + if ( i > 0 ) + Acb_CollectIntNodes_rec( p, Gia_ObjFanin0(pObj), vNodes1 ); + Gia_ManForEachCo( p, pObj, i ) + if ( i == 0 ) + Acb_CollectIntNodes_rec( p, Gia_ObjFanin0(pObj), vNodes0 ); +} +Gia_Man_t * Acb_UpdateMiter( Gia_Man_t * pM, Gia_Man_t * pOne, int iTar, int nTargets, Vec_Int_t * vUsed, int fCisOnly ) +{ + Gia_Man_t * pRes, * pTemp; + Gia_Obj_t * pObj; int i; + Vec_Int_t * vNodes0 = Vec_IntAlloc( Gia_ManAndNum(pM) ); + Vec_Int_t * vNodes1 = Vec_IntAlloc( Gia_ManAndNum(pM) ); + Acb_CollectIntNodes( pM, vNodes0, vNodes1 ); + Gia_ManFillValue( pM ); + Gia_ManFillValue( pOne ); + // create new + pRes = Gia_ManStart( Gia_ManObjNum(pM) + Gia_ManObjNum(pOne) ); + Gia_ManHashAlloc( pRes ); + Gia_ManConst0(pM)->Value = 0; + Gia_ManConst0(pOne)->Value = 0; + // copy first part of the miter + Gia_ManForEachCi( pM, pObj, i ) +// if ( i < Gia_ManCiNum(pM) - 1 ) + pObj->Value = Gia_ManAppendCi( pRes ); + Gia_ManForEachObjVec( vNodes1, pM, pObj, i ) + pObj->Value = Gia_ManHashAnd( pRes, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( pM, pObj, i ) + if ( i > 0 ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + // transfer to New + //assert( Gia_ManCiNum(pOne) <= Vec_IntSize(vUsed) ); + assert( Gia_ManCoNum(pOne) == 1 ); + if ( fCisOnly ) + { + Gia_ManForEachCi( pOne, pObj, i ) + if ( i < Vec_IntSize(vUsed) ) + pObj->Value = Gia_ManCi(pM, Vec_IntEntry(vUsed, i))->Value; + } + else + { + Gia_ManForEachCi( pOne, pObj, i ) + pObj->Value = Gia_ManCo(pM, 1+Vec_IntEntry(vUsed, i))->Value; + } + Gia_ManForEachAnd( pOne, pObj, i ) + pObj->Value = Gia_ManHashAnd( pRes, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + // transfer to miter + pObj = Gia_ManCi( pM, Gia_ManCiNum(pM) - nTargets + iTar ); + pObj->Value = Gia_ObjFanin0Copy( Gia_ManCo(pOne, 0) ); + Gia_ManForEachObjVec( vNodes0, pM, pObj, i ) + pObj->Value = Gia_ManHashAnd( pRes, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( pM, pObj, i ) + Gia_ManAppendCo( pRes, Gia_ObjFanin0Copy(pObj) ); + // cleanup + Vec_IntFree( vNodes0 ); + Vec_IntFree( vNodes1 ); + Gia_ManHashStop( pRes ); + pRes = Gia_ManCleanup( pTemp = pRes ); + Gia_ManStop( pTemp ); + assert( Gia_ManCiNum(pRes) == Gia_ManCiNum(pM) ); + assert( Gia_ManCoNum(pRes) == Gia_ManCoNum(pM) ); + return pRes; +} + +/**Function************************************************************* + + Synopsis [Generate strings representing instance and the patch.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Str_t * Acb_GenerateInstance( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUsed, Vec_Int_t * vTars ) +{ + int i, iObj; + Vec_Str_t * vStr = Vec_StrAlloc( 100 ); + Vec_StrAppend( vStr, "patch p0 (" ); + Vec_IntForEachEntry( vTars, iObj, i ) + Vec_StrPrintF( vStr, "%s .%s(%s)", i ? ",":"", Acb_ObjNameStr(p, iObj), Acb_ObjNameStr(p, iObj) ); + Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i ) + Vec_StrPrintF( vStr, ", .%s(%s)", Acb_ObjNameStr(p, iObj), Acb_ObjNameStr(p, iObj) ); + Vec_StrAppend( vStr, " );\n" ); + Vec_StrPush( vStr, '\0' ); + return vStr; +} +Vec_Ptr_t * Acb_GenerateSignalNames( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUsed, int nNodes, Vec_Int_t * vTars, Vec_Wec_t * vGates ) +{ + Vec_Ptr_t * vRes = Vec_PtrStart( Vec_IntSize(vUsed) + nNodes ); + Vec_Str_t * vStr = Vec_StrAlloc(1000); int i, iObj, nWires = 1; + // create input names + Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i ) + Vec_PtrWriteEntry( vRes, i, Abc_UtilStrsav(Acb_ObjNameStr(p, iObj)) ); + // create names for nodes driving outputs + assert( Vec_WecSize(vGates) == Vec_IntSize(vUsed) + nNodes + Vec_IntSize(vTars) ); + Vec_IntForEachEntry( vTars, iObj, i ) + { + Vec_Int_t * vGate = Vec_WecEntry( vGates, Vec_IntSize(vUsed) + nNodes + i ); + assert( Vec_IntEntry(vGate, 0) == ABC_OPER_BIT_BUF ); + Vec_PtrWriteEntry( vRes, Vec_IntEntry(vGate, 1), Abc_UtilStrsav(Acb_ObjNameStr(p, iObj)) ); + } + for ( i = Vec_IntSize(vUsed); i < Vec_IntSize(vUsed) + nNodes; i++ ) + if ( Vec_PtrEntry(vRes, i) == NULL ) + { + Vec_StrPrintF( vStr, "ww%d", nWires++ ); + Vec_StrPush( vStr, '\0' ); + Vec_PtrWriteEntry( vRes, i, Vec_StrReleaseArray(vStr) ); + } + Vec_StrFree( vStr ); + return vRes; +} +Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUsed, Vec_Ptr_t * vSops, Vec_Ptr_t * vGias, Vec_Int_t * vTars ) +{ + extern Vec_Wec_t * Abc_SopSynthesize( Vec_Ptr_t * vSops ); + extern Vec_Wec_t * Abc_GiaSynthesize( Vec_Ptr_t * vGias ); + Vec_Wec_t * vGates = vGias ? Abc_GiaSynthesize(vGias) : Abc_SopSynthesize(vSops); Vec_Int_t * vGate; + int nOuts = vGias ? Vec_PtrSize(vGias) : Vec_PtrSize(vSops); + int i, k, iObj, nWires = Vec_WecSize(vGates) - Vec_IntSize(vUsed) - nOuts, fFirst = 1; + Vec_Ptr_t * vNames = Acb_GenerateSignalNames( p, vDivs, vUsed, nWires, vTars, vGates ); + + Vec_Str_t * vStr = Vec_StrAlloc( 100 ); + Vec_StrAppend( vStr, "module patch (" ); + + assert( Vec_IntSize(vTars) == nOuts ); + Vec_IntForEachEntry( vTars, iObj, i ) + Vec_StrPrintF( vStr, "%s %s", i ? ",":"", Acb_ObjNameStr(p, iObj) ); + Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i ) + Vec_StrPrintF( vStr, ", %s", Acb_ObjNameStr(p, iObj) ); + Vec_StrAppend( vStr, " );\n\n" ); + + Vec_StrAppend( vStr, " output" ); + Vec_IntForEachEntry( vTars, iObj, i ) + Vec_StrPrintF( vStr, "%s %s", i ? ",":"", Acb_ObjNameStr(p, iObj) ); + Vec_StrAppend( vStr, ";\n" ); + + Vec_StrAppend( vStr, " input" ); + Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i ) + Vec_StrPrintF( vStr, "%s %s", i ? ",":"", Acb_ObjNameStr(p, iObj) ); + Vec_StrAppend( vStr, ";\n" ); + + if ( nWires > nOuts ) + { + Vec_StrAppend( vStr, " wire" ); + for ( i = 0; i < nWires; i++ ) + { + char * pName = (char *)Vec_PtrEntry( vNames, Vec_IntSize(vUsed)+i ); + if ( !strncmp(pName, "ww", 2) ) + Vec_StrPrintF( vStr, "%s %s", fFirst ? "":",", pName ), fFirst = 0; + } + Vec_StrAppend( vStr, ";\n\n" ); + } + + // create internal nodes + Vec_WecForEachLevelStartStop( vGates, vGate, i, Vec_IntSize(vUsed), Vec_IntSize(vUsed)+nWires ) + { + if ( Vec_IntSize(vGate) > 2 ) + { + Vec_StrPrintF( vStr, " %s (", Acb_Oper2Name(Vec_IntEntry(vGate, 0)) ); + Vec_IntForEachEntryStart( vGate, iObj, k, 1 ) + Vec_StrPrintF( vStr, "%s %s", k > 1 ? ",":"", (char *)Vec_PtrEntry(vNames, iObj) ); + Vec_StrAppend( vStr, " );\n" ); + } + else + { + assert( Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_F || Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T ); + Vec_StrPrintF( vStr, " %s (", Acb_Oper2Name( ABC_OPER_BIT_BUF ) ); + Vec_StrPrintF( vStr, " %s, ", (char *)Vec_PtrEntry(vNames, Vec_IntEntry(vGate, 1)) ); + Vec_StrPrintF( vStr, " 1\'b%d", Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T ); + Vec_StrPrintF( vStr, " );" ); + } + } + Vec_StrAppend( vStr, "\nendmodule\n\n" ); + Vec_StrPush( vStr, '\0' ); + Vec_PtrFreeFree( vNames ); + Vec_WecFree( vGates ); + + printf( "Synthesized patch with %d inputs, %d outputs and %d gates.\n", Vec_IntSize(vUsed), nOuts, nWires ); + return vStr; +} + +/**Function************************************************************* + + Synopsis [Produce output files.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_GenerateFilePatch( Vec_Str_t * p, char * pFileNamePatch ) +{ + FILE * pFile = fopen( pFileNamePatch, "wb" ); + if ( !pFile ) + return; + fprintf( pFile, "%s", Vec_StrArray(p) ); + fclose( pFile ); +} +void Acb_GenerateFileOut( Vec_Str_t * vPatchLine, char * pFileNameF, char * pFileNameOut, Vec_Str_t * vPatch ) +{ + char * pBuffer = ABC_ALLOC( char, 10000 ); + FILE * pFileIn, * pFileOut; + // input file + pFileIn = fopen( pFileNameF, "rb" ); + if ( !pFileIn ) + return; + // output file + pFileOut = fopen( pFileNameOut, "wb" ); + if ( !pFileOut ) + return; + // copy line by line + while ( fgets(pBuffer, 10000, pFileIn) ) + { + if ( strstr(pBuffer, "endmodule") ) + fprintf( pFileOut, "\n%s", Vec_StrArray(vPatchLine) ); + fputs( pBuffer, pFileOut ); + } + if ( vPatch ) + fprintf( pFileOut, "\n\n%s\n", Vec_StrArray(vPatch) ); + fclose( pFileIn ); + fclose( pFileOut ); + ABC_FREE( pBuffer ); +} + +/**Function************************************************************* + + Synopsis [Print parameters of the patch.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_PrintPatch( Acb_Ntk_t * pNtkF, Vec_Int_t * vDivs, Vec_Int_t * vUsed, abctime clk ) +{ + int i, iObj, Weight = 0; + printf( "Patch has %d inputs: ", Vec_IntSize(vUsed) ); + Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i ) + { + printf( "%d=%s(w=%d) ", Vec_IntEntry(vUsed, i), Acb_ObjNameStr(pNtkF, iObj), Acb_ObjWeight(pNtkF, iObj) ); + Weight += Acb_ObjWeight(pNtkF, iObj); + } + printf( "\nTotal weight = %d ", Weight ); + Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clk ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Quantifies targets 0 up to iTar (out of nTars).] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Acb_NtkEcoSynthesize( Gia_Man_t * p ) +{ + int Iter, fVerbose = 0; + Gia_Man_t * pNew = Gia_ManDup( p ); + + if ( fVerbose ) printf( "M_quo: " ); + if ( fVerbose ) Gia_ManPrintStats( pNew, NULL ); + + pNew = Gia_ManAreaBalance( p = pNew, 0, 0, 0, 0 ); + Gia_ManStop( p ); + + if ( fVerbose ) printf( "M_bal: " ); + if ( fVerbose ) Gia_ManPrintStats( pNew, NULL ); + + for ( Iter = 0; Iter < 2; Iter++ ) + { + pNew = Gia_ManCompress2( p = pNew, 1, 0 ); + Gia_ManStop( p ); + + if ( fVerbose ) printf( "M_dc2: " ); + if ( fVerbose ) Gia_ManPrintStats( pNew, NULL ); + } + + pNew = Gia_ManAigSyn2( p = pNew, 0, 1, 0, 100, 0, 0, 0 ); + Gia_ManStop( p ); + + if ( fVerbose ) printf( "M_sn2: " ); + if ( fVerbose ) Gia_ManPrintStats( pNew, NULL ); + + for ( Iter = 0; Iter < 2; Iter++ ) + { + pNew = Gia_ManCompress2( p = pNew, 1, 0 ); + Gia_ManStop( p ); + + if ( fVerbose ) printf( "M_dc2: " ); + if ( fVerbose ) Gia_ManPrintStats( pNew, NULL ); + } + return pNew; +} +Cnf_Dat_t * Acb_NtkEcoCompute( Gia_Man_t * p, int iTar, int nTars ) +{ + Gia_Man_t * pCof = Gia_ManDup( p ); + Cnf_Dat_t * pCnf; int v, fVerbose = 1; + for ( v = 0; v < iTar; v++ ) + { + pCof = Gia_ManDupUniv( p = pCof, Gia_ManCiNum(pCof) - nTars + v ); + assert( Gia_ManCiNum(pCof) == Gia_ManCiNum(p) ); + Gia_ManStop( p ); + } + if ( fVerbose ) printf( "M_quo: " ); + if ( fVerbose ) Gia_ManPrintStats( pCof, NULL ); + pCof = Acb_NtkEcoSynthesize( p = pCof ); + Gia_ManStop( p ); + if ( fVerbose ) printf( "M_syn: " ); + if ( fVerbose ) Gia_ManPrintStats( pCof, NULL ); + if ( 0 && iTar < nTars ) + { + Gia_Man_t * pCof0 = Gia_ManDupCofactorVar( pCof, Gia_ManCiNum(pCof) - nTars + iTar, 0 ); + Gia_Man_t * pCof1 = Gia_ManDupCofactorVar( pCof, Gia_ManCiNum(pCof) - nTars + iTar, 1 ); + pCof0 = Acb_NtkEcoSynthesize( p = pCof0 ); + Gia_ManStop( p ); + pCof1 = Acb_NtkEcoSynthesize( p = pCof1 ); + Gia_ManStop( p ); + Gia_AigerWrite( pCof0, "eco_qbf0.aig", 0, 0 ); + Gia_AigerWrite( pCof1, "eco_qbf1.aig", 0, 0 ); + Gia_ManStop( pCof0 ); + Gia_ManStop( pCof1 ); + printf( "Dumped cof0 into file \"%s\".\n", "eco_qbf0.aig" ); + printf( "Dumped cof1 into file \"%s\".\n", "eco_qbf1.aig" ); + } +// Gia_AigerWrite( pCof, "eco_qbf.aig", 0, 0 ); +// printf( "Dumped the result of quantification into file \"%s\".\n", "eco_qbf.aig" ); + pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCof, 8, 0, 0, 0, 0 ); + Gia_ManStop( pCof ); + return pCnf; +} +Gia_Man_t * Gia_ManInterOneInt( Gia_Man_t * pCof1, Gia_Man_t * pCof0, int Depth ) +{ + extern Gia_Man_t * Gia_ManInterOne( Gia_Man_t * pNtkOn, Gia_Man_t * pNtkOff, int fVerbose ); + extern Gia_Man_t * Abc_GiaSynthesizeInter( Gia_Man_t * p ); + Gia_Man_t * pGia[2] = { pCof0, pCof1 }; + Gia_Man_t * pCof[2][2] = {{0}}, * pTemp; + Gia_Man_t * pInter[2], * pFinal; + Gia_Obj_t * pObj; + int i, n, m, Count, CountBest = 0, iVarBest = -1; + // find PIs with the highest fanout + Vec_Int_t * vFanCount; + if ( Gia_ManAndNum(pCof1) == 0 || Gia_ManAndNum(pCof0) == 0 ) + return Gia_ManDup(pCof1); + vFanCount = Vec_IntStart( Gia_ManCiNum(pCof0) ); + for ( n = 0; n < 2; n++ ) + { + Gia_ManForEachAnd( pGia[n], pObj, i ) + { + if ( Gia_ObjIsCi(Gia_ObjFanin0(pObj)) ) + Vec_IntAddToEntry( vFanCount, Gia_ObjCioId(Gia_ObjFanin0(pObj)), 1 ); + if ( Gia_ObjIsCi(Gia_ObjFanin1(pObj)) ) + Vec_IntAddToEntry( vFanCount, Gia_ObjCioId(Gia_ObjFanin1(pObj)), 1 ); + } + } + Vec_IntForEachEntry( vFanCount, Count, i ) + if ( CountBest < Count ) + { + CountBest = Count; + iVarBest = i; + } + Vec_IntFree( vFanCount ); + // Gia_Man_t * Gia_ManDupCofactorVar( Gia_Man_t * p, int iVar, int Value ) + for ( n = 0; n < 2; n++ ) + for ( m = 0; m < 2; m++ ) + { + pCof[n][m] = Gia_ManDupCofactorVar( pGia[n], iVarBest, m ); + pCof[n][m] = Acb_NtkEcoSynthesize( pTemp = pCof[n][m] ); + Gia_ManStop( pTemp ); + printf( "%*sCof%d%d : ", 8-Depth, "", n, m ); + Gia_ManPrintStats( pCof[n][m], NULL ); + } + for ( m = 0; m < 2; m++ ) + { + if ( Gia_ManAndNum(pCof[1][m]) == 0 || Gia_ManAndNum(pCof[0][m]) == 0 ) + pInter[m] = Gia_ManDup( pCof[1][m] ); + else if ( Depth == 1 ) + pInter[m] = Gia_ManInterOne( pCof[1][m], pCof[0][m], 1 ); + else + pInter[m] = Gia_ManInterOneInt( pCof[1][m], pCof[0][m], Depth-1 ); + printf( "%*sInter%d : ", 8-Depth, "", m ); + Gia_ManPrintStats( pInter[m], NULL ); + pInter[m] = Abc_GiaSynthesizeInter( pTemp = pInter[m] ); + Gia_ManStop( pTemp ); + printf( "%*sInter%d : ", 8-Depth, "", m ); + Gia_ManPrintStats( pInter[m], NULL ); + } + for ( n = 0; n < 2; n++ ) + for ( m = 0; m < 2; m++ ) + Gia_ManStop( pCof[n][m] ); + pFinal = Gia_ManDupMux( iVarBest, pInter[1], pInter[0] ); + for ( m = 0; m < 2; m++ ) + Gia_ManStop( pInter[m] ); + return pFinal; +} +Gia_Man_t * Acb_NtkEcoComputeInter2( Gia_Man_t * p, int iTar, int nTars ) +{ +// extern Gia_Man_t * Gia_ManInterOne( Gia_Man_t * pNtkOn, Gia_Man_t * pNtkOff, int fVerbose ); + extern Gia_Man_t * Abc_GiaSynthesizeInter( Gia_Man_t * p ); + Gia_Man_t * pInter, * pCof0, * pCof1, * pCof = Gia_ManDup( p ); int v; + for ( v = 0; v < iTar; v++ ) + { + pCof = Gia_ManDupUniv( p = pCof, Gia_ManCiNum(pCof) - nTars + v ); + assert( Gia_ManCiNum(pCof) == Gia_ManCiNum(p) ); + Gia_ManStop( p ); + + pCof = Acb_NtkEcoSynthesize( p = pCof ); + Gia_ManStop( p ); + } + pCof0 = Gia_ManDupCofactorVar( pCof, Gia_ManCiNum(pCof) - nTars + iTar, 1 ); + pCof1 = Gia_ManDupCofactorVar( pCof, Gia_ManCiNum(pCof) - nTars + iTar, 0 ); + Gia_ManStop( pCof ); + pCof0 = Acb_NtkEcoSynthesize( p = pCof0 ); + Gia_ManStop( p ); + pCof1 = Acb_NtkEcoSynthesize( p = pCof1 ); + Gia_ManStop( p ); + + printf( "Cof0 : " ); + Gia_ManPrintStats( pCof0, NULL ); + printf( "Cof1 : " ); + Gia_ManPrintStats( pCof1, NULL ); + + if ( Gia_ManAndNum(pCof1) == 0 || Gia_ManAndNum(pCof0) == 0 ) + pInter = Gia_ManDup(pCof1); + else + pInter = Gia_ManInterOneInt( pCof1, pCof0, 7 ); + Gia_ManStop( pCof0 ); + Gia_ManStop( pCof1 ); + pInter = Abc_GiaSynthesizeInter( p = pInter ); + Gia_ManStop( p ); + //Gia_ManPrintStats( pInter, NULL ); + pInter = Gia_ManDupRemovePis( p = pInter, nTars ); + Gia_ManStop( p ); + //Gia_ManPrintStats( pInter, NULL ); + return pInter; +} +Gia_Man_t * Acb_NtkEcoComputeInter( Gia_Man_t * p, int iTar, int nTars ) +{ + Gia_Man_t * pCof1, * pCof = Gia_ManDup( p ); int v; + for ( v = 0; v < iTar; v++ ) + { + pCof = Gia_ManDupUniv( p = pCof, Gia_ManCiNum(pCof) - nTars + v ); + assert( Gia_ManCiNum(pCof) == Gia_ManCiNum(p) ); + Gia_ManStop( p ); + + pCof = Acb_NtkEcoSynthesize( p = pCof ); + Gia_ManStop( p ); + } + pCof1 = Gia_ManDupCofactorVar( pCof, Gia_ManCiNum(pCof) - nTars + iTar, 0 ); + Gia_ManStop( pCof ); + + pCof1 = Acb_NtkEcoSynthesize( p = pCof1 ); + Gia_ManStop( p ); + + pCof1 = Gia_ManDupRemovePis( p = pCof1, nTars ); + Gia_ManStop( p ); + return pCof1; +} + +/**Function************************************************************* + + Synopsis [Transform patch functions to have common support.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Acb_RemapOneFunction( char * pStr, Vec_Int_t * vSupp, Vec_Int_t * vMap, int nVars ) +{ + Vec_Str_t * vTempSop = Vec_StrAlloc( 100 ); + char * pToken = strtok( pStr, "\n" ); int i; + while ( pToken != NULL ) + { + for ( i = 0; i < nVars; i++ ) + Vec_StrPush( vTempSop, '-' ); + for ( i = 0; pToken[i] != ' '; i++ ) + if ( pToken[i] != '-' ) + { + int iVar = Vec_IntEntry( vMap, Vec_IntEntry(vSupp, i) ); + assert( iVar >= 0 && iVar < nVars ); + Vec_StrWriteEntry( vTempSop, Vec_StrSize(vTempSop) - nVars + iVar, pToken[i] ); + } + Vec_StrPrintF( vTempSop, " %d\n", pToken[i+1] - '0' ); + pToken = strtok( NULL, "\n" ); + } + Vec_StrPush( vTempSop, '\0' ); + pToken = Vec_StrReleaseArray(vTempSop); + Vec_StrFree( vTempSop ); + return pToken; +} +Vec_Ptr_t * Acb_TransformPatchFunctions( Vec_Ptr_t * vSops, Vec_Wec_t * vSupps, Vec_Int_t ** pvUsed, int nDivs ) +{ + Vec_Ptr_t * vFuncs = Vec_PtrAlloc( Vec_PtrSize(vSops) ); + Vec_Int_t * vUsed = Vec_IntAlloc( 100 ); + Vec_Int_t * vMap = Vec_IntStartFull( nDivs ); + Vec_Int_t * vPres = Vec_IntStart( nDivs ); + Vec_Int_t * vLevel; + int i, k, iVar; + // check what divisors are used + Vec_WecForEachLevel( vSupps, vLevel, i ) + { + char * pSop = (char *)Vec_PtrEntry( vSops, i ); + char * pStrCopy = Abc_UtilStrsav( pSop ); + char * pToken = strtok( pStrCopy, "\n" ); + while ( pToken != NULL ) + { + for ( k = 0; pToken[k] != ' '; k++ ) + if ( pToken[k] != '-' ) + Vec_IntWriteEntry( vPres, Vec_IntEntry(vLevel, k), 1 ); + pToken = strtok( NULL, "\n" ); + } + ABC_FREE( pStrCopy ); + } + // create common order + Vec_WecForEachLevel( vSupps, vLevel, i ) + Vec_IntForEachEntry( vLevel, iVar, k ) + { + if ( !Vec_IntEntry(vPres, iVar) ) + continue; + if ( Vec_IntEntry(vMap, iVar) >= 0 ) + continue; + Vec_IntWriteEntry( vMap, iVar, Vec_IntSize(vUsed) ); + Vec_IntPush( vUsed, iVar ); + } + printf( "The number of used variables %d (out of %d).\n", Vec_IntSum(vPres), Vec_IntSize(vPres) ); + // remap SOPs + Vec_WecForEachLevel( vSupps, vLevel, i ) + { + char * pSop = (char *)Vec_PtrEntry( vSops, i ); + pSop = Acb_RemapOneFunction( pSop, vLevel, vMap, Vec_IntSize(vUsed) ); + //printf( "Function %d\n%s", i, pSop ); + Vec_PtrPush( vFuncs, pSop ); + } + Vec_IntFree( vPres ); + Vec_IntFree( vMap ); + *pvUsed = vUsed; + return vFuncs; +} + +/**Function************************************************************* + + Synopsis [Performs ECO for two networks.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF, int fCisOnly ) +{ + extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop ); + + abctime clk = Abc_Clock(); + int nTargets = Vec_IntSize(&pNtkF->vTargets); + int TimeOut = fCisOnly ? 0 : 60; // 60 seconds + int RetValue = 1; + + // compute various sets of nodes + Vec_Bit_t * vBlock; + Vec_Int_t * vRoots = Acb_NtkFindRoots( pNtkF, &pNtkF->vTargets, &vBlock ); + Vec_Int_t * vSuppF = Acb_NtkFindSupp( pNtkF, vRoots ); + Vec_Int_t * vSuppG = Acb_NtkFindSupp( pNtkG, vRoots ); + Vec_Int_t * vSupp = Vec_IntTwoMerge( vSuppF, vSuppG ); + Vec_Int_t * vDivs = fCisOnly ? Acb_NtkFindDivsCis( pNtkF, vSupp ) : Acb_NtkFindDivs( pNtkF, vSupp, vBlock ); + Vec_Int_t * vNodesF = Acb_NtkFindNodes( pNtkF, vRoots, vDivs ); + Vec_Int_t * vNodesG = Acb_NtkFindNodes( pNtkG, vRoots, NULL ); + + // create AIGs + Gia_Man_t * pGiaF = Acb_NtkToGia( pNtkF, vSupp, vNodesF, vRoots, vDivs, &pNtkF->vTargets ); + Gia_Man_t * pGiaG = Acb_NtkToGia( pNtkG, vSupp, vNodesG, vRoots, NULL, NULL ); + Gia_Man_t * pGiaM = Acb_CreateMiter( pGiaF, pGiaG ); + + Cnf_Dat_t * pCnf; + Gia_Man_t * pTemp, * pOne; + Vec_Ptr_t * vSops = Vec_PtrAlloc( nTargets ); + Vec_Wec_t * vSupps = Vec_WecAlloc( nTargets ); + Vec_Int_t * vSuppOld = Vec_IntAlloc( 100 ); + + Vec_Int_t * vUsed = NULL; + Vec_Ptr_t * vFuncs = NULL; + Vec_Ptr_t * vGias = fCisOnly ? Vec_PtrAlloc(nTargets) : NULL; + Vec_Str_t * vInst = NULL, * vPatch = NULL; + + char * pSop = NULL; + int i, Res; + + printf( "The number of targets = %d.\n", nTargets ); + + printf( "NtkF: " ); + Gia_ManPrintStats( pGiaF, NULL ); + printf( "NtkG: " ); + Gia_ManPrintStats( pGiaG, NULL ); + printf( "Miter: " ); + Gia_ManPrintStats( pGiaM, NULL ); + + // check that the problem has a solution + if ( 0 )//fCisOnly ) + { + int Lit, status; + sat_solver * pSat; + pCnf = Acb_NtkEcoCompute( pGiaM, nTargets, nTargets ); + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + Cnf_DataFree( pCnf ); + // add output clause + Lit = Abc_Var2Lit( 1, 0 ); + status = sat_solver_addclause( pSat, &Lit, &Lit+1 ); + status = status == 0 ? l_False : sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 ); + sat_solver_delete( pSat ); + printf( "The ECO problem has %s solution. ", status == l_False ? "a" : "NO" ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + if ( status != l_False ) + { + RetValue = 0; + goto cleanup; + } + } + + for ( i = nTargets-1; i >= 0; i-- ) + { + Vec_Int_t * vSupp = NULL; + printf( "\nConsidering target %d (out of %d)...\n", i, nTargets ); + // compute support of this target + if ( fCisOnly ) + { + vSupp = Vec_IntStartNatural( Vec_IntSize(vDivs) ); + printf( "Target %d has support with %d variables.\n", i, Vec_IntSize(vSupp) ); + + pOne = Acb_NtkEcoComputeInter( pGiaM, i, nTargets ); + printf( "Tar%02d: ", i ); + Gia_ManPrintStats( pOne, NULL ); + + // update miter + pGiaM = Acb_UpdateMiter( pTemp = pGiaM, pOne, i, nTargets, vSupp, fCisOnly ); + Gia_ManStop( pTemp ); + + // add to functions + Vec_PtrPush( vGias, pOne ); + } + else + { + pCnf = Acb_NtkEcoCompute( pGiaM, i, nTargets ); +// vSupp = Acb_DerivePatchSupportS( pCnf, i, nTargets, Vec_IntSize(vDivs), vDivs, pNtkF, NULL, TimeOut ); + vSupp = Acb_DerivePatchSupport( pCnf, i, nTargets, Vec_IntSize(vDivs), vDivs, pNtkF, vSuppOld, TimeOut ); + if ( vSupp == NULL ) + { + Vec_IntFree( vSuppOld ); + Cnf_DataFree( pCnf ); + RetValue = 0; + goto cleanup; + } + Vec_IntAppend( vSuppOld, vSupp ); + Vec_IntClear( vSupp ); + Vec_IntAppend( vSupp, vSuppOld ); + //Vec_IntClear( vSuppOld ); + + // derive function of this target + pSop = Acb_DeriveOnePatchFunction( pCnf, i, nTargets, Vec_IntSize(vDivs), vSupp, fCisOnly ); + Cnf_DataFree( pCnf ); + if ( pSop == NULL ) + { + Vec_IntFree( vSuppOld ); + RetValue = 0; + goto cleanup; + } + + // add new function to the miter + pOne = Abc_SopSynthesizeOne( pSop ); + printf( "Tar%02d: ", i ); + Gia_ManPrintStats( pOne, NULL ); + + // update miter + pGiaM = Acb_UpdateMiter( pTemp = pGiaM, pOne, i, nTargets, vSupp, fCisOnly ); + Gia_ManStop( pTemp ); + Gia_ManStop( pOne ); + + // add to functions + Vec_PtrPush( vSops, pSop ); + } + // add to supports + Vec_IntAppend( Vec_WecPushLevel(vSupps), vSupp ); + Vec_IntFree( vSupp ); + } + Vec_IntFree( vSuppOld ); + + // make sure the function is UNSAT + printf( "\n" ); + if ( !fCisOnly ) + { + abctime clk = Abc_Clock(); + pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGiaM, 8, 0, 0, 0, 0 ); + Res = Acb_CheckMiter( pCnf ); + Cnf_DataFree( pCnf ); + if ( Res == 1 ) + printf( "The ECO solution was verified successfully. " ); + else + printf( "The ECO solution verification FAILED. " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + + // derive new patch functions + if ( fCisOnly ) + { + vUsed = Vec_IntStartNatural( Vec_IntSize(vDivs) ); + Vec_PtrReverseOrder( vGias ); + } + else + { + vFuncs = Acb_TransformPatchFunctions( vSops, vSupps, &vUsed, Vec_IntSize(vDivs) ); + Vec_PtrReverseOrder( vFuncs ); + } + + // generate instance and patch + vInst = Acb_GenerateInstance( pNtkF, vDivs, vUsed, &pNtkF->vTargets ); + vPatch = Acb_GeneratePatch( pNtkF, vDivs, vUsed, vFuncs, vGias, &pNtkF->vTargets ); + + // print the results + //printf( "%s", Vec_StrArray(vPatch) ); + Acb_PrintPatch( pNtkF, vDivs, vUsed, clk ); + + // generate output files + Acb_GenerateFilePatch( vPatch, "patch.v" ); + Acb_GenerateFileOut( vInst, pFileNameF, "out.v", vPatch ); + //Gia_AigerWrite( pGiaG, "test.aig", 0, 0 ); +cleanup: + // cleanup + if ( vGias ) + { + Gia_Man_t * pTemp; int i; + Vec_PtrForEachEntry( Gia_Man_t *, vGias, pTemp, i ) + Gia_ManStop( pTemp ); + Vec_PtrFree( vGias ); + } + Vec_StrFreeP( &vPatch ); + Vec_StrFreeP( &vInst ); + + Vec_PtrFreeFree( vSops ); + Vec_WecFree( vSupps ); + + if ( vFuncs ) Vec_PtrFreeFree( vFuncs ); + Vec_IntFreeP( &vUsed ); + + Gia_ManStop( pGiaF ); + Gia_ManStop( pGiaG ); + Gia_ManStop( pGiaM ); + + Vec_IntFreeP( &vSuppF ); + Vec_IntFreeP( &vSuppG ); + Vec_IntFreeP( &vSupp ); + Vec_IntFreeP( &vNodesF ); + Vec_IntFreeP( &vNodesG ); + Vec_IntFreeP( &vRoots ); + Vec_IntFreeP( &vDivs ); + Vec_BitFreeP( &vBlock ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Read/write test.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_NtkTestRun2( char * pFileNames[3], int fVerbose ) +{ + char * pFileNameOut = Extra_FileNameGenericAppend( pFileNames[0], "_w.v" ); + Acb_Ntk_t * pNtk = Acb_VerilogSimpleRead( pFileNames[0], pFileNames[2] ); + Acb_VerilogSimpleWrite( pNtk, pFileNameOut ); + Acb_ManFree( pNtk->pDesign ); + Acb_IntallLibrary(); +} + + +/**Function************************************************************* + + Synopsis [Top level procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_NtkRunEco( char * pFileNames[3], int fVerbose ) +{ + Acb_Ntk_t * pNtkF = Acb_VerilogSimpleRead( pFileNames[0], pFileNames[2] ); + Acb_Ntk_t * pNtkG = Acb_VerilogSimpleRead( pFileNames[1], NULL ); + if ( !pNtkF || !pNtkG ) + return; + //int * pArray = Vec_IntArray( &pNtkF->vTargets ); + //ABC_SWAP( int, pArray[7], pArray[4] ); + //Vec_IntReverseOrder( &pNtkF->vTargets ); + //Vec_IntPermute( &pNtkF->vTargets ); + //Vec_IntPrint( &pNtkF->vTargets ); + + assert( Acb_NtkCiNum(pNtkF) == Acb_NtkCiNum(pNtkG) ); + assert( Acb_NtkCoNum(pNtkF) == Acb_NtkCoNum(pNtkG) ); + + Acb_IntallLibrary(); + + if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames[0], 0 ) ) + { + printf( "General ECO computation timed out. Trying inputs only.\n\n" ); + if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames[0], 1 ) ) + printf( "Input-only ECO computation also timed out.\n\n" ); + } + + Acb_ManFree( pNtkF->pDesign ); + Acb_ManFree( pNtkG->pDesign ); } //////////////////////////////////////////////////////////////////////// |