From 94ab17c39e847a2326138068fadfe52c3675f70b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 2 Jun 2022 07:47:33 -0700 Subject: Supporting new resub problem format. --- src/aig/gia/giaUtil.c | 50 +++++++++++++++++++++++++++++- src/base/io/io.c | 53 ++++++++++++++++++++++++++++++++ src/base/main/mainUtils.c | 2 +- src/misc/util/utilTruth.h | 18 +++++++++++ src/misc/vec/vecInt.h | 2 ++ src/proof/acec/acecBo.c | 77 +++++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 200 insertions(+), 2 deletions(-) diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 431be5b7..d8130550 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -3080,7 +3080,55 @@ Gia_Man_t * Gia_ManTransformCond( Gia_Man_t * p ) Abc_PrintTime( 0, "Time", Abc_Clock() - clk ); return NULL; } - +void Gia_ManWriteSol( Gia_Man_t * p, char * pFileName ) +{ + char * pBasicName = Extra_FileNameGeneric( pFileName ); + char * pFileName2 = Abc_UtilStrsavTwo( pBasicName, ".sol" ); + FILE * pFile = fopen( pFileName2, "wb" ); + ABC_FREE( pBasicName ); + if ( pFile == NULL ) + printf( "Cannot open output file \"%s\".\n", pFileName2 ); + else + { + Gia_Obj_t * pObj; int i; + Gia_ManForEachAnd( p, pObj, i ) + fprintf( pFile, "%d %d ", Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i) ); + Gia_ManForEachCo( p, pObj, i ) + fprintf( pFile, "%d %d ", Gia_ObjFaninLit0p(p, pObj), Gia_ObjFaninLit0p(p, pObj) ); + fclose( pFile ); + printf( "Finished writing solution file \"%s\".\n", pFileName2 ); + } + ABC_FREE( pFileName2 ); +} +void Gia_ManWriteResub( Gia_Man_t * p, char * pFileName ) +{ + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + printf( "Cannot open output file \"%s\".\n", pFileName ); + else + { + Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) ); + Vec_Wrd_t * vSimsPo = Gia_ManSimPatSimOut( p, vSimsPi, 1 ); + int i, k, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p); + word * pTemp = ABC_ALLOC( word, nWords ); + fprintf( pFile, "%d %d %d %d\n", Gia_ManCiNum(p), 0, Gia_ManCoNum(p), 1 << Gia_ManCiNum(p) ); + for ( i = 0; i < Gia_ManCiNum(p); i++ ) + Abc_TtPrintBinary1( pFile, Vec_WrdEntryP(vSimsPi, i*nWords), Gia_ManCiNum(p) ), fprintf(pFile, "\n"); + for ( i = 0; i < (1 << Gia_ManCoNum(p)); i++ ) + { + Abc_TtFill( pTemp, nWords ); + for ( k = 0; k < Gia_ManCoNum(p); k++ ) + Abc_TtAndCompl( pTemp, pTemp, 0, Vec_WrdEntryP(vSimsPo, k*nWords), !((i>>k)&1), nWords ); + Abc_TtPrintBinary1( pFile, pTemp, Gia_ManCiNum(p) ), fprintf(pFile, "\n"); + } + ABC_FREE( pTemp ); + fclose( pFile ); + Vec_WrdFree( vSimsPi ); + Vec_WrdFree( vSimsPo ); + printf( "Finished writing resub file \"%s\".\n", pFileName ); + Gia_ManWriteSol( p, pFileName ); + } +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/io/io.c b/src/base/io/io.c index 26bfb1f4..9b3d288a 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -84,6 +84,7 @@ static int IoCommandWriteTruths ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteStatus ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteSmv ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteJson ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandWriteResub ( Abc_Frame_t * pAbc, int argc, char **argv ); extern void Abc_FrameCopyLTLDataBase( Abc_Frame_t *pAbc, Abc_Ntk_t * pNtk ); @@ -155,6 +156,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "write_status", IoCommandWriteStatus, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_smv", IoCommandWriteSmv, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_json", IoCommandWriteJson, 0 ); + Cmd_CommandAdd( pAbc, "I/O", "&write_resub", IoCommandWriteResub, 0 ); } /**Function************************************************************* @@ -3480,6 +3482,57 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IoCommandWriteResub( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + extern void Gia_ManWriteResub( Gia_Man_t * p, char * pFileName ); + char * pFileName; + int c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc != globalUtilOptind + 1 ) + goto usage; + pFileName = argv[globalUtilOptind]; + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "IoCommandWriteResub(): There is no AIG.\n" ); + return 1; + } + if ( Gia_ManCiNum(pAbc->pGia) > 20 ) + { + Abc_Print( -1, "IoCommandWriteResub(): The number of inputs is wrong.\n" ); + return 1; + } + Gia_ManWriteResub( pAbc->pGia, pFileName ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: &write_resub [-ch] \n" ); + fprintf( pAbc->Err, "\t write the network in resub format\n" ); + fprintf( pAbc->Err, "\t-h : print the help message\n" ); + fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .json)\n" ); + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c index bb6d0a31..377299fd 100644 --- a/src/base/main/mainUtils.c +++ b/src/base/main/mainUtils.c @@ -160,7 +160,7 @@ void Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName ) void Abc_UtilsSource( Abc_Frame_t * pAbc ) { #ifdef WIN32 - if ( Cmd_CommandExecute(pAbc, "source -s abc.rc") ) + if ( Cmd_CommandExecute(pAbc, "source abc.rc") ) { if ( Cmd_CommandExecute(pAbc, "source ..\\abc.rc") == 0 ) printf( "Loaded \"abc.rc\" from the parent directory.\n" ); diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index d9efa55f..bc8ac3f0 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -1471,6 +1471,24 @@ static inline void Abc_TtPrintBinary( word * pTruth, int nVars ) printf( "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) ); printf( "\n" ); } +static inline void Abc_TtPrintBinary1( FILE * pFile, word * pTruth, int nVars ) +{ + word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars); + int k, Limit = Abc_MinInt( 64, (1 << nVars) ); + assert( nVars >= 2 ); + for ( pThis = pTruth; pThis < pLimit; pThis++ ) + for ( k = 0; k < Limit; k++ ) + fprintf( pFile, "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) ); +} +static inline void Abc_TtPrintBinary2( FILE * pFile, word * pTruth, int nVars ) +{ + word * pThis; + int k, Limit = Abc_MinInt( 64, (1 << nVars) ); + assert( nVars >= 2 ); + for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- ) + for ( k = Limit-1; k >= 0; k-- ) + fprintf( pFile, "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) ); +} /**Function************************************************************* diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index c15369d2..e4ea6cfe 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -61,6 +61,8 @@ struct Vec_Int_t_ for ( i = Start; (i < Stop) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ ) #define Vec_IntForEachEntryReverse( vVec, pEntry, i ) \ for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && (((pEntry) = Vec_IntEntry(vVec, i)), 1); i-- ) +#define Vec_IntForEachEntryReverseStart( vVec, pEntry, i, Start ) \ + for ( i = Start; (i >= 0) && (((pEntry) = Vec_IntEntry(vVec, i)), 1); i-- ) #define Vec_IntForEachEntryTwo( vVec1, vVec2, Entry1, Entry2, i ) \ for ( i = 0; (i < Vec_IntSize(vVec1)) && (((Entry1) = Vec_IntEntry(vVec1, i)), 1) && (((Entry2) = Vec_IntEntry(vVec2, i)), 1); i++ ) #define Vec_IntForEachEntryTwoStart( vVec1, vVec2, Entry1, Entry2, i, Start ) \ diff --git a/src/proof/acec/acecBo.c b/src/proof/acec/acecBo.c index 9cddcd13..51af0214 100644 --- a/src/proof/acec/acecBo.c +++ b/src/proof/acec/acecBo.c @@ -21,6 +21,7 @@ #include "acecInt.h" #include "misc/vec/vecWec.h" #include "misc/extra/extra.h" +#include "misc/util/utilTruth.h" ABC_NAMESPACE_IMPL_START @@ -207,6 +208,82 @@ void Acec_DetectBoothTest( Gia_Man_t * p ) } } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManResubTest4() +{ + Vec_Int_t * vRes = Vec_IntAlloc( 100 ); + unsigned T = 0xF335ACC0; + int a, b, c; + int i, k, f, y; + int Count = 0; + for ( a = 0; a < 2; a++ ) + { + unsigned A = s_Truths5[a]; + for ( b = 0; b < 3; b++ ) + { + unsigned B = s_Truths5[2+b]; + for ( c = 0; c < 3; c++ ) if ( c != b ) + { + unsigned C = s_Truths5[2+c]; + Vec_IntPush( vRes, A & B & C ); + Vec_IntPush( vRes, A & B & ~C ); + } + } + } + printf( "Size = %d.\n", Vec_IntSize(vRes) ); + for ( i = 0; i < (1 << Vec_IntSize(vRes)); i++ ) + { + unsigned F[7] = {0}; + unsigned Y[3] = {0}; + if ( Abc_TtCountOnes( (word)i ) >= 8 ) + continue; + for ( f = k = 0; k < Vec_IntSize(vRes); k++ ) + if ( ((i >> k) & 1) ) + F[f++] = Vec_IntEntry(vRes, k); + { + unsigned S1 = (F[0] & F[1]) | (F[0] & F[2]) | (F[1] & F[2]); + unsigned C1 = F[0] ^ F[1] ^ F[2]; + unsigned S2 = (F[3] & F[4]) | (F[3] & F[5]) | (F[4] & F[5]); + unsigned C2 = F[3] ^ F[4] ^ F[5]; + unsigned S3 = (F[6] & S1) | (F[6] & S2) | (S1 & S2); + unsigned C3 = F[6] ^ S1 ^ S2; + unsigned S4 = (C1 & C2) | (C1 & C3) | (C2 & C3); + unsigned C4 = C1 ^ C2 ^ C3; + Y[0] = S3; + Y[1] = S4; + Y[2] = C4; + } + for ( y = 0; y < 3; y++ ) + if ( Y[y] == T ) + printf( "Found!\n" ); + Count++; + } + printf( "Tried = %d.\n", Count ); + Vec_IntFree( vRes ); +} +void Gia_ManResubTest5() +{ + unsigned T = 0xF335ACC0; + int i; + for ( i = 0; i < 4; i++ ) + { + unsigned x = i%2 ? Abc_Tt5Cofactor1(T, 0) : Abc_Tt5Cofactor0(T, 0); + unsigned y = i/2 ? Abc_Tt5Cofactor1(x, 1) : Abc_Tt5Cofactor0(x, 1); + word F = y; + F |= F << 32; + //Dau_DsdPrintFromTruth2( &F, 6 ); printf( "\n" ); + } +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3