diff options
Diffstat (limited to 'src/base/io/ioWriteCnf.c')
| -rw-r--r-- | src/base/io/ioWriteCnf.c | 65 |
1 files changed, 53 insertions, 12 deletions
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c index 09824f38..e1b2d956 100644 --- a/src/base/io/ioWriteCnf.c +++ b/src/base/io/ioWriteCnf.c @@ -19,13 +19,16 @@ ***********************************************************************/ #include "io.h" +#include "satSolver.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// + +static Abc_Ntk_t * s_pNtk = NULL; //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -39,33 +42,71 @@ SeeAlso [] ***********************************************************************/ -int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName ) +int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes ) { - solver * pSat; - if ( !Abc_NtkIsBddLogic(pNtk) ) + sat_solver * pSat; + if ( Abc_NtkIsStrash(pNtk) ) + printf( "Io_WriteCnf() warning: Generating CNF by applying heuristic AIG to CNF conversion.\n" ); + else + printf( "Io_WriteCnf() warning: Generating CNF by convering logic nodes into CNF clauses.\n" ); + if ( Abc_NtkPoNum(pNtk) != 1 ) { - fprintf( stdout, "Io_WriteCnf(): Currently can only process logic networks with BDDs.\n" ); + fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter (the network with one PO).\n" ); return 0; } - if ( Abc_NtkPoNum(pNtk) != 1 ) + if ( Abc_NtkLatchNum(pNtk) != 0 ) { - fprintf( stdout, "Io_WriteCnf(): Currently can only solve the miter (the network with one PO).\n" ); + fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter for combinational circuits.\n" ); return 0; } - if ( Abc_NtkLatchNum(pNtk) != 0 ) + if ( Abc_NtkNodeNum(pNtk) == 0 ) { - fprintf( stdout, "Io_WriteCnf(): Currently can only solve the miter for combinational circuits.\n" ); + fprintf( stdout, "The network has no logic nodes. No CNF file is generaled.\n" ); return 0; } + // convert to logic BDD network + if ( Abc_NtkIsLogic(pNtk) ) + Abc_NtkToBdd( pNtk ); // create solver with clauses - pSat = Abc_NtkMiterSatCreate( pNtk ); + pSat = Abc_NtkMiterSatCreate( pNtk, fAllPrimes ); + if ( pSat == NULL ) + { + fprintf( stdout, "The problem is trivially UNSAT. No CNF file is generated.\n" ); + return 1; + } // write the clauses - Asat_SolverWriteDimacs( pSat, pFileName ); + s_pNtk = pNtk; + Sat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 ); + s_pNtk = NULL; // free the solver - solver_delete( pSat ); + sat_solver_delete( pSat ); return 1; } +/**Function************************************************************* + + Synopsis [Output the mapping of PIs into variable numbers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteCnfOutputPiMapping( FILE * pFile, int incrementVars ) +{ + extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk ); + Abc_Ntk_t * pNtk = s_pNtk; + Vec_Int_t * vCiIds; + Abc_Obj_t * pObj; + int i; + vCiIds = Abc_NtkGetCiSatVarNums( pNtk ); + fprintf( pFile, "c PI variable numbers: <PI_name> <SAT_var_number>\n" ); + Abc_NtkForEachCi( pNtk, pObj, i ) + fprintf( pFile, "c %s %d\n", Abc_ObjName(pObj), Vec_IntEntry(vCiIds, i) + (int)(incrementVars > 0) ); + Vec_IntFree( vCiIds ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |