diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
| -rw-r--r-- | src/aig/gia/giaJf.c | 30 | ||||
| -rw-r--r-- | src/base/io/io.c | 66 |
3 files changed, 95 insertions, 2 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index b2cc1a8f..c6ace8db 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -254,6 +254,7 @@ struct Jf_Par_t_ int fFuncDsd; int fGenCnf; int fCnfObjIds; + int fAddOrCla; int fPureAig; int fVerbose; int fVeryVerbose; diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c index 8ba81c4c..0e737adc 100644 --- a/src/aig/gia/giaJf.c +++ b/src/aig/gia/giaJf.c @@ -159,11 +159,17 @@ void Jf_ManGenCnf( word uTruth, int iLitOut, Vec_Int_t * vLeaves, Vec_Int_t * vL } } } -Cnf_Dat_t * Jf_ManCreateCnfRemap( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas ) +Cnf_Dat_t * Jf_ManCreateCnfRemap( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas, int fAddOrCla ) { Cnf_Dat_t * pCnf; Gia_Obj_t * pObj; int i, Entry, * pMap, nVars = 0; + if ( fAddOrCla ) + { + Vec_IntPush( vClas, Vec_IntSize(vLits) ); + Gia_ManForEachPo( p, pObj, i ) + Vec_IntPush( vLits, Abc_Var2Lit(Gia_ObjId(p, pObj), 0) ); + } // label nodes present in the mapping Vec_IntForEachEntry( vLits, Entry, i ) Gia_ManObj(p, Abc_Lit2Var(Entry))->fMark0 = 1; @@ -1543,7 +1549,7 @@ Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p ) if ( p->pPars->fCnfObjIds ) pNew->pData = Jf_ManCreateCnf( pNew, vLits, vClas ); else - pNew->pData = Jf_ManCreateCnfRemap( pNew, vLits, vClas ); + pNew->pData = Jf_ManCreateCnfRemap( pNew, vLits, vClas, p->pPars->fAddOrCla ); } Vec_IntFreeP( &vLits ); Vec_IntFreeP( &vClas ); @@ -1760,6 +1766,26 @@ Gia_Man_t * Jf_ManDeriveCnf( Gia_Man_t * p, int fCnfObjIds ) pPars->fCnfObjIds = fCnfObjIds; return Jf_ManPerformMapping( p, pPars ); } +Gia_Man_t * Jf_ManDeriveCnfMiter( Gia_Man_t * p ) +{ + Jf_Par_t Pars, * pPars = &Pars; + Jf_ManSetDefaultPars( pPars ); + pPars->fGenCnf = 1; + pPars->fCnfObjIds = 0; + pPars->fAddOrCla = 1; + return Jf_ManPerformMapping( p, pPars ); +} +void Jf_ManDumpCnf( Gia_Man_t * p, char * pFileName ) +{ + Gia_Man_t * pNew; + Cnf_Dat_t * pCnf; + pNew = Jf_ManDeriveCnfMiter( p ); + pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL; + Cnf_DataWriteIntoFile( pCnf, pFileName, 0, NULL, NULL ); + Gia_ManStop( pNew ); + Cnf_DataFree(pCnf); +} + void Jf_ManTestCnf( Gia_Man_t * p ) { Gia_Man_t * pNew; diff --git a/src/base/io/io.c b/src/base/io/io.c index 14646894..fa97ea1e 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -59,6 +59,7 @@ static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBook ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteCnf ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandWriteCnf2 ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteDot ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteEqn ( Abc_Frame_t * pAbc, int argc, char **argv ); @@ -125,6 +126,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "write_cellnet", IoCommandWriteCellNet, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_counter", IoCommandWriteCounter, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_cnf", IoCommandWriteCnf, 0 ); + Cmd_CommandAdd( pAbc, "I/O", "&write_cnf", IoCommandWriteCnf2, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_dot", IoCommandWriteDot, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_eqn", IoCommandWriteEqn, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_gml", IoCommandWriteGml, 0 ); @@ -2031,6 +2033,70 @@ usage: SeeAlso [] ***********************************************************************/ +int IoCommandWriteCnf2( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + extern void Jf_ManDumpCnf( Gia_Man_t * p, char * pFileName ); + FILE * pFile; + char * pFileName; + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "IoCommandWriteCnf2(): There is no AIG.\n" ); + return 1; + } + if ( Gia_ManRegNum(pAbc->pGia) > 0 ) + { + Abc_Print( -1, "IoCommandWriteCnf2(): Works only for combinational miters.\n" ); + return 0; + } + if ( argc != globalUtilOptind + 1 ) + goto usage; + // get the input file name + pFileName = argv[globalUtilOptind]; + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + return 0; + } + Jf_ManDumpCnf( pAbc->pGia, pFileName ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: &write_cnf [-vh] <file>\n" ); + fprintf( pAbc->Err, "\t writes CNF produced by new DSD-based generator\n" ); + fprintf( pAbc->Err, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes" : "no" ); + fprintf( pAbc->Err, "\t-h : print the help massage\n" ); + fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); + return 1; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv ) { char * pFileName; |