Skip to content

Commit

Permalink
Changing interface of &genrel.
Browse files Browse the repository at this point in the history
  • Loading branch information
@alanminko
alanminko committed Aug 3, 2024
1 parent 7d88bf2 commit b25d9c4
Show file tree
Hide file tree
Showing 2 changed files with 228 additions and 30 deletions.
203 changes: 194 additions & 9 deletions src/aig/gia/giaQbf.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 );
}

Expand Down
55 changes: 34 additions & 21 deletions src/base/abci/abc.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53482,23 +53482,30 @@ int Abc_CommandAbc9Odc( Abc_Frame_t * pAbc, int argc, char ** argv )
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;
Expand All @@ -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] <node1> <node2> ... <nodeN> <filename>\n" );
Abc_Print( -2, "usage: &genrel [-I n1,n2,...nN] [-O m1,m2,...,mM] [-vh] <filename>\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<nodes> : the list of nodes for inputs and outputs\n");
Abc_Print( -2, "\t<file> : the output file name (extended PLA format)\n");
Abc_Print( -2, "\t<file> : the output file name (PLA format extended to represented Boolean relations)\n");
return 1;
}

Expand Down

0 comments on commit b25d9c4

Please sign in to comment.