From b25d9c482abeec3228d2fb79906f8180f6f7868b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 2 Aug 2024 18:30:09 -0700 Subject: [PATCH] Changing interface of &genrel. --- src/aig/gia/giaQbf.c | 203 +++++++++++++++++++++++++++++++++++++++++-- src/base/abci/abc.c | 55 +++++++----- 2 files changed, 228 insertions(+), 30 deletions(-) diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index f06836e87..1525e7d83 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -1027,17 +1027,13 @@ Vec_Int_t * Gia_ManGenCombs( Gia_Man_t * p, Vec_Int_t * vInsOuts, int nIns, int Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); return vRes; } -void Gia_ManGenRel( Gia_Man_t * pGia, Vec_Int_t * vInsOuts, int nIns, char * pFileName, int fVerbose ) +void Gia_ManGenWriteRel( Vec_Int_t * vRes, int nIns, int nOuts, char * pFileName ) { - Vec_Int_t * vRes = Gia_ManGenCombs( pGia, vInsOuts, nIns, fVerbose ); int i, k, Mask; - if ( vRes == NULL ) { - printf( "Enumerating solutions did not succeed.\n" ); - return; - } - Abc_RData_t * p2, * p = Abc_RDataStart( nIns, Vec_IntSize(vInsOuts)-nIns, Vec_IntSize(vRes) ); + int i, k, Mask, nVars = nIns + nOuts; + Abc_RData_t * p2, * p = Abc_RDataStart( nIns, nOuts, Vec_IntSize(vRes) ); Vec_IntForEachEntry( vRes, Mask, i ) { - for ( k = 0; k < Vec_IntSize(vInsOuts); k++ ) - if ( (Mask >> (Vec_IntSize(vInsOuts)-1-k)) & 1 ) { // the bit is 1 + for ( k = 0; k < nVars; k++ ) + if ( (Mask >> (nVars-1-k)) & 1 ) { // the bit is 1 if ( k < nIns ) Abc_RDataSetIn( p, k, i ); else @@ -1053,6 +1049,195 @@ void Gia_ManGenRel( Gia_Man_t * pGia, Vec_Int_t * vInsOuts, int nIns, char * pFi Abc_WritePla( p2, Extra_FileNameGenericAppend(pFileName, "_rel.pla"), 1 ); Abc_RDataStop( p2 ); Abc_RDataStop( p ); +} +void Gia_ManGenRel2( Gia_Man_t * pGia, Vec_Int_t * vInsOuts, int nIns, char * pFileName, int fVerbose ) +{ + Vec_Int_t * vRes = Gia_ManGenCombs( pGia, vInsOuts, nIns, fVerbose ); + if ( vRes == NULL ) { + printf( "Enumerating solutions did not succeed.\n" ); + return; + } + Gia_ManGenWriteRel( vRes, nIns, Vec_IntSize(vInsOuts)-nIns, pFileName ); + Vec_IntFree( vRes ); +} + +/**Function************************************************************* + + Synopsis [Derive the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManCollectNodeTfos( Gia_Man_t * p, int * pNodes, int nNodes ) +{ + Vec_Int_t * vTfo = Vec_IntAlloc( 100 ); + Gia_Obj_t * pObj; int i; + Gia_ManIncrementTravId( p ); + for ( i = 0; i < nNodes; i++ ) + Gia_ObjSetTravIdCurrentId( p, pNodes[i] ); + Gia_ManForEachAnd( p, pObj, i ) { + if ( Gia_ObjIsTravIdCurrentId(p, i) ) + continue; + if ( Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0(pObj, i)) || Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId1(pObj, i)) ) + Gia_ObjSetTravIdCurrentId( p, i ), Vec_IntPush( vTfo, i ); + } + Gia_ManForEachCo( p, pObj, i ) + if ( Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0p(p, pObj)) ) + Vec_IntPush( vTfo, Gia_ObjId(p, pObj) ); + return vTfo; +} +Vec_Int_t * Gia_ManCollectNodeTfis( Gia_Man_t * p, Vec_Int_t * vNodes ) +{ + Vec_Int_t * vTfi = Vec_IntAlloc( 100 ); + Gia_Obj_t * pObj; int i, Id; + Gia_ManIncrementTravId( p ); + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + if ( Gia_ObjIsCo(pObj) ) + Gia_ObjSetTravIdCurrentId( p, Gia_ObjFaninId0p(p, pObj) ); + Gia_ManForEachAndReverse( p, pObj, i ) { + if ( !Gia_ObjIsTravIdCurrentId(p, i) ) + continue; + Gia_ObjSetTravIdCurrentId(p, Gia_ObjFaninId0(pObj, i)); + Gia_ObjSetTravIdCurrentId(p, Gia_ObjFaninId1(pObj, i)); + } + Gia_ManForEachCiId( p, Id, i ) + if ( Gia_ObjIsTravIdCurrentId(p, Id) ) + Vec_IntPush( vTfi, Id ); + Gia_ManForEachAnd( p, pObj, i ) + if ( Gia_ObjIsTravIdCurrentId(p, i) ) + Vec_IntPush( vTfi, i ); + return vTfi; +} +Gia_Man_t * Gia_ManGenRelMiter( Gia_Man_t * pGia, Vec_Int_t * vInsOuts, int nIns ) +{ + Vec_Int_t * vTfo = Gia_ManCollectNodeTfos( pGia, Vec_IntEntryP(vInsOuts, nIns), Vec_IntSize(vInsOuts)-nIns ); + Vec_Int_t * vTfi = Gia_ManCollectNodeTfis( pGia, vTfo ); + Vec_Int_t * vInLits = Vec_IntAlloc( nIns ); + Vec_Int_t * vOutLits = Vec_IntAlloc( Vec_IntSize(vInsOuts) - nIns ); + Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; int i, iLit = 0; + Gia_ManFillValue( pGia ); + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( pGia->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManForEachObjVec( vTfi, pGia, pObj, i ) + if ( Gia_ObjIsCi(pObj) ) + pObj->Value = Gia_ManAppendCi(pNew); + for ( i = 0; i < Vec_IntSize(vInsOuts)-nIns; i++ ) + Vec_IntPush( vInLits, Gia_ManAppendCi(pNew) ); + Gia_ManForEachObjVec( vTfi, pGia, pObj, i ) + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachObjVec( vTfo, pGia, pObj, i ) + if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + Gia_ManForEachObjVec( vInsOuts, pGia, pObj, i ) + if ( i < nIns ) + Vec_IntPush( vOutLits, pObj->Value ); + else + pObj->Value = Vec_IntEntry( vInLits, i-nIns ); + Gia_ManForEachObjVec( vTfo, pGia, pObj, i ) + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachObjVec( vTfo, pGia, pObj, i ) + if ( Gia_ObjIsCo(pObj) ) + iLit = Gia_ManHashOr( pNew, iLit, Gia_ManHashXor(pNew, Gia_ObjFanin0Copy(pObj), pObj->Value) ); + Gia_ManAppendCo( pNew, iLit ); + Vec_IntForEachEntry( vOutLits, iLit, i ) + Gia_ManAppendCo( pNew, iLit ); + Vec_IntFree( vTfo ); + Vec_IntFree( vTfi ); + Vec_IntFree( vInLits ); + Vec_IntFree( vOutLits ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia) ); + return pNew; +} +void Gia_ManPrintRelMinterm( int Mint, int nIns, int nVars ) +{ + for ( int i = 0; i < nVars; i++ ) + printf( "%s%d", i == nIns ? " ":"", (Mint >> (nVars-1-i)) & 1 ); + printf( "\n" ); +} +Vec_Int_t * Gia_ManGenIoCombs( Gia_Man_t * pGia, Vec_Int_t * vInsOuts, int nIns, int fVerbose ) +{ + abctime clkStart = Abc_Clock(); + int nTimeOut = 600, nConfLimit = 1000000; + int i, iNode, iSatVar, Iter, Mask, nSolutions = 0, RetValue = 0; + Gia_Man_t * pMiter = Gia_ManGenRelMiter( pGia, vInsOuts, nIns ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t*)Mf_ManGenerateCnf( pMiter, 8, 0, 0, 0, 0 ); + sat_solver * pSat = (sat_solver*)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + int iLit = Abc_Var2Lit( 1, 0 ); // enumerating the care set (the miter output is 1) + int status = sat_solver_addclause( pSat, &iLit, &iLit + 1 ); assert( status ); + Vec_Int_t * vSatVars = Vec_IntAlloc( Vec_IntSize(vInsOuts) ); + Vec_IntForEachEntry( vInsOuts, iNode, i ) + Vec_IntPush( vSatVars, i < nIns ? 2+i : pCnf->nVars-Vec_IntSize(vInsOuts)+i ); + Vec_Int_t * vLits = Vec_IntAlloc( 100 ); + Vec_Int_t * vRes = Vec_IntAlloc( 1000 ); + for ( Iter = 0; Iter < 1000000; Iter++ ) + { + int status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 ); + if ( status == l_False ) { RetValue = 1; break; } + if ( status == l_Undef ) { RetValue = 0; break; } + nSolutions++; + // extract SAT assignment + Mask = 0; + Vec_IntClear( vLits ); + Vec_IntForEachEntry( vSatVars, iSatVar, i ) { + Vec_IntPush( vLits, Abc_Var2Lit(iSatVar, sat_solver_var_value(pSat, iSatVar)) ); + if ( sat_solver_var_value(pSat, iSatVar) ) + Mask |= 1 << (Vec_IntSize(vInsOuts)-1-i); + } + Vec_IntPush( vRes, Mask ); + if ( 0 ) { + printf( "%5d : ", Iter ); + Gia_ManPrintRelMinterm( Mask, nIns, Vec_IntSize(vSatVars) ); + } + // add clause + if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ) ) + { RetValue = 1; break; } + if ( nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= nTimeOut ) { RetValue = 0; break; } + } + // complement the set of input/output minterms + Vec_Int_t * vBits = Vec_IntStart( 1 << Vec_IntSize(vInsOuts) ); + Vec_IntForEachEntry( vRes, Mask, i ) + Vec_IntWriteEntry( vBits, Mask, 1 ); + Vec_IntClear( vRes ); + Vec_IntForEachEntry( vBits, Mask, i ) + if ( !Mask ) + Vec_IntPush( vRes, i ); + Vec_IntFree( vBits ); + // cleanup + Vec_IntFree( vLits ); + sat_solver_delete( pSat ); + Gia_ManStop( pMiter ); + Cnf_DataFree( pCnf ); + if ( RetValue == 0 ) + Vec_IntFreeP( &vRes ); + return vRes; +} +void Gia_ManGenRel( Gia_Man_t * pGia, Vec_Int_t * vInsOuts, int nIns, char * pFileName, int fVerbose ) +{ + abctime clkStart = Abc_Clock(); + Vec_Int_t * vRes = Gia_ManGenIoCombs( pGia, vInsOuts, nIns, fVerbose ); + if ( vRes == NULL ) { + printf( "Enumerating solutions did not succeed.\n" ); + return; + } + Gia_ManGenWriteRel( vRes, nIns, Vec_IntSize(vInsOuts)-nIns, pFileName ); + if ( fVerbose ) { + printf( "The resulting relation with %d input/output minterms is written into file \"%s\". ", Vec_IntSize(vRes), pFileName ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); + if ( 0 ) { + int i, Mint; + Vec_IntForEachEntry( vRes, Mint, i ) + Gia_ManPrintRelMinterm( Mint, nIns, Vec_IntSize(vInsOuts) ); + } + } Vec_IntFree( vRes ); } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index da6d06aa1..2b65d8c6f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -53482,23 +53482,30 @@ usage: int Abc_CommandAbc9GenRel( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Gia_ManGenRel( Gia_Man_t * pGia, Vec_Int_t * vInsOuts, int nIns, char * pFileName, int fVerbose ); - Vec_Int_t * vInsOuts = NULL; + Vec_Int_t * vInsOuts = NULL; char * pIns = NULL, * pOuts = NULL; int c, nIns = -1, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "IOvh" ) ) != EOF ) { switch ( c ) { case 'I': if ( globalUtilOptind >= argc ) { - Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); goto usage; } - nIns = atoi(argv[globalUtilOptind]); + pIns = argv[globalUtilOptind]; globalUtilOptind++; - if ( nIns < 0 ) + break; + case 'O': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" ); goto usage; + } + pOuts = argv[globalUtilOptind]; + globalUtilOptind++; break; case 'v': fVerbose ^= 1; @@ -53514,41 +53521,47 @@ int Abc_CommandAbc9GenRel( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9GenRel(): There is no AIG.\n" ); return 0; } - if ( nIns < 2 ) + if ( argc != globalUtilOptind+1 ) { - Abc_Print( -1, "Abc_CommandAbc9GenRel(): The number of inputs should be given on the command line.\n" ); + Abc_Print( -1, "Abc_CommandAbc9GenRel(): The output file name should be given as the last entry on the command line.\n" ); return 0; } - if ( argc == globalUtilOptind ) + if ( pIns == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9GenRel(): Node IDs should be given on the command line.\n" ); + Abc_Print( -1, "Abc_CommandAbc9GenRel(): A comma-separated list of window input node IDs should be given as \"-I list\" on the command line.\n" ); return 0; } - if ( argc-globalUtilOptind-nIns-1 < 1 ) + if ( pOuts == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9GenRel(): The relation should have at least one output.\n" ); + Abc_Print( -1, "Abc_CommandAbc9GenRel(): A comma-separated list of window output node IDs should be given as \"-O list\" on the command line.\n" ); return 0; } - vInsOuts = Vec_IntAlloc( 100 ); - for ( c = globalUtilOptind; c < argc-1; c++ ) - Vec_IntPush( vInsOuts, atoi(argv[c]) ); - if ( fVerbose ) - { + vInsOuts = Vec_IntAlloc( 16 ); + Vec_IntPush( vInsOuts, atoi(pIns) ); + for ( c = 0; pIns[c]; c++ ) + if ( pIns[c] == ',' ) + Vec_IntPush( vInsOuts, atoi(pIns+c+1) ); + nIns = Vec_IntSize(vInsOuts); + Vec_IntPush( vInsOuts, atoi(pOuts) ); + for ( c = 0; pOuts[c]; c++ ) + if ( pOuts[c] == ',' ) + Vec_IntPush( vInsOuts, atoi(pOuts+c+1) ); + if ( fVerbose ) { printf( "Deriving relation for %d inputs and %d outputs: ", nIns, Vec_IntSize(vInsOuts)-nIns ); Vec_IntPrint( vInsOuts ); } - Gia_ManGenRel( pAbc->pGia, vInsOuts, nIns, argv[argc-1], fVerbose ); + Gia_ManGenRel( pAbc->pGia, vInsOuts, nIns, argv[globalUtilOptind], fVerbose ); Vec_IntFree( vInsOuts ); return 0; usage: - Abc_Print( -2, "usage: &genrel [-I num] [-vh] ... \n" ); + Abc_Print( -2, "usage: &genrel [-I n1,n2,...nN] [-O m1,m2,...,mM] [-vh] \n" ); Abc_Print( -2, "\t generates Boolean relation for the given logic window\n" ); - Abc_Print( -2, "\t-I num : the number of inputs of the relation [default = undefined]\n" ); + Abc_Print( -2, "\t-I list : comma-separated list of window inputs [default = undefined]\n" ); + Abc_Print( -2, "\t-O list : comma-separated list of window outputs [default = undefined]\n" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %d]\n", fVerbose ? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); - Abc_Print( -2, "\t : the list of nodes for inputs and outputs\n"); - Abc_Print( -2, "\t : the output file name (extended PLA format)\n"); + Abc_Print( -2, "\t : the output file name (PLA format extended to represented Boolean relations)\n"); return 1; }