From 6ad6539c0f460735168cbe4a0d52729b01c45645 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 14 May 2024 22:35:43 -0700 Subject: [PATCH] New command &genrel to generate relations for windows in the AIG. --- src/aig/gia/giaQbf.c | 94 +++++++++++++++++++++++++++++++++++++++++++ src/base/abci/abc.c | 85 ++++++++++++++++++++++++++++++++++++++ src/base/io/ioResub.h | 6 +++ 3 files changed, 185 insertions(+) diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index 6ccbe4605..2c2dbde36 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -24,6 +24,7 @@ #include "misc/extra/extra.h" #include "sat/glucose/AbcGlucose.h" #include "misc/util/utilTruth.h" +#include "base/io/ioResub.h" ABC_NAMESPACE_IMPL_START @@ -945,6 +946,99 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i return RetValue; } +/**Function************************************************************* + + Synopsis [Performs QBF solving using an improved algorithm.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManGenCombs( Gia_Man_t * p, Vec_Int_t * vInsOuts, int fVerbose ) +{ + int nTimeOut = 600, nConfLimit = 1000000; + int i, iObj, iSatVar, Iter, Mask, nSolutions = 0, RetValue = 0; + abctime clkStart = Abc_Clock(); + Gia_Man_t * pCopy = Gia_ManDup(p); + Vec_IntForEachEntry( vInsOuts, iObj, i ) + Gia_ManAppendCo( pCopy, Abc_Var2Lit(iObj, 0) ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCopy, 8, 0, 0, 0, 0 ); + sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + Vec_Int_t * vLits = Vec_IntAlloc( 100 ); + Vec_Int_t * vRes = Vec_IntAlloc( 1000 ); + //Gia_ManForEachCoId( pCopy, iObj, i ) + // printf( "%d=%d ", i, pCnf->pVarNums[iObj] ); + //printf( "\n" ); + Cnf_DataFree( pCnf ); + 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 ); + for ( i = 0; i < Vec_IntSize(vInsOuts); i++ ) { + iSatVar = i + 1+Gia_ManCoNum(p); + 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 ( fVerbose ) + { + printf( "%5d : ", Iter ); + for ( i = Vec_IntSize(vInsOuts)-1; i >= 0; i-- ) + printf( "%d", (Mask >> i) & 1 ); + printf( "\n" ); + } + // 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; } + } + Vec_IntSort( vRes, 0 ); + Gia_ManStop( pCopy ); + Vec_IntFree( vLits ); + sat_solver_delete( pSat ); + if ( RetValue == 0 ) + Vec_IntFreeP( &vRes ); + if ( fVerbose ) + 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 ) +{ + Vec_Int_t * vRes = Gia_ManGenCombs( pGia, vInsOuts, fVerbose ); int i, k, Mask; + if ( vRes == NULL ) { + printf( "Enumerating solutions did not succeed.\n" ); + return; + } + Abc_RData_t * p = Abc_RDataStart( nIns, Vec_IntSize(vInsOuts)-nIns, 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 + if ( k < nIns ) + Abc_RDataSetIn( p, k, i ); + else + Abc_RDataSetOut( p, 2*(k-nIns)+1, i ); + } + else { // the bit is zero + if ( k >= nIns ) + Abc_RDataSetOut( p, 2*(k-nIns), i ); + } + } + Abc_WritePla( p, pFileName, 0 ); + Abc_RDataStop( p ); + Vec_IntFree( vRes ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index e6e78bb42..49c88ef5e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -607,6 +607,7 @@ static int Abc_CommandAbc9BRecover ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9StrEco ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GenCex ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Odc ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9GenRel ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1396,6 +1397,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&str_eco", Abc_CommandAbc9StrEco, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gencex", Abc_CommandAbc9GenCex, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&odc", Abc_CommandAbc9Odc, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&genrel", Abc_CommandAbc9GenRel, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); { @@ -53026,6 +53028,89 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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; + int c, nIns = -1, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF ) + { + switch ( c ) + { + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nIns = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nIns < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9GenRel(): There is no AIG.\n" ); + return 0; + } + if ( nIns < 2 ) + { + Abc_Print( -1, "Abc_CommandAbc9GenRel(): The number of inputs should be given on the command line.\n" ); + return 0; + } + if ( argc == globalUtilOptind ) + { + Abc_Print( -1, "Abc_CommandAbc9GenRel(): Node IDs should be given on the command line.\n" ); + return 0; + } + if ( argc-globalUtilOptind-nIns-1 < 1 ) + { + Abc_Print( -1, "Abc_CommandAbc9GenRel(): The relation should have at least one output.\n" ); + return 0; + } + vInsOuts = Vec_IntAlloc( 100 ); + for ( c = globalUtilOptind; c < argc-1; c++ ) + Vec_IntPush( vInsOuts, atoi(argv[c]) ); + 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 ); + Vec_IntFree( vInsOuts ); + return 0; + +usage: + Abc_Print( -2, "usage: &genrel [-I num] [-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-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"); + return 1; +} /**Function************************************************************* Synopsis [] diff --git a/src/base/io/ioResub.h b/src/base/io/ioResub.h index 06c3d24ba..f78d6f8cd 100644 --- a/src/base/io/ioResub.h +++ b/src/base/io/ioResub.h @@ -52,6 +52,12 @@ struct Abc_RData_t_ /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +static inline int Abc_RDataGetIn ( Abc_RData_t * p, int i, int b ) { return Abc_InfoHasBit((unsigned *)Vec_WrdEntryP(p->vSimsIn, i*p->nSimWords), b); } +static inline int Abc_RDataGetOut( Abc_RData_t * p, int i, int b ) { return Abc_InfoHasBit((unsigned *)Vec_WrdEntryP(p->vSimsOut, i*p->nSimWords), b); } + +static inline void Abc_RDataSetIn ( Abc_RData_t * p, int i, int b ) { Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(p->vSimsIn, i*p->nSimWords), b); } +static inline void Abc_RDataSetOut( Abc_RData_t * p, int i, int b ) { Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(p->vSimsOut, i*p->nSimWords), b); } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// ////////////////////////////////////////////////////////////////////////