diff options
Diffstat (limited to 'src/base/io/ioWriteCnf.c')
| -rw-r--r-- | src/base/io/ioWriteCnf.c | 65 |
1 files changed, 12 insertions, 53 deletions
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c index e1b2d956..09824f38 100644 --- a/src/base/io/ioWriteCnf.c +++ b/src/base/io/ioWriteCnf.c @@ -19,16 +19,13 @@ ***********************************************************************/ #include "io.h" -#include "satSolver.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// - -static Abc_Ntk_t * s_pNtk = NULL; //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// +/// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -42,71 +39,33 @@ static Abc_Ntk_t * s_pNtk = NULL; SeeAlso [] ***********************************************************************/ -int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes ) +int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName ) { - 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 ) + solver * pSat; + if ( !Abc_NtkIsBddLogic(pNtk) ) { - fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter (the network with one PO).\n" ); + fprintf( stdout, "Io_WriteCnf(): Currently can only process logic networks with BDDs.\n" ); return 0; } - if ( Abc_NtkLatchNum(pNtk) != 0 ) + if ( Abc_NtkPoNum(pNtk) != 1 ) { - fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter for combinational circuits.\n" ); + fprintf( stdout, "Io_WriteCnf(): Currently can only solve the miter (the network with one PO).\n" ); return 0; } - if ( Abc_NtkNodeNum(pNtk) == 0 ) + if ( Abc_NtkLatchNum(pNtk) != 0 ) { - fprintf( stdout, "The network has no logic nodes. No CNF file is generaled.\n" ); + fprintf( stdout, "Io_WriteCnf(): Currently can only solve the miter for combinational circuits.\n" ); return 0; } - // convert to logic BDD network - if ( Abc_NtkIsLogic(pNtk) ) - Abc_NtkToBdd( pNtk ); // create solver with clauses - pSat = Abc_NtkMiterSatCreate( pNtk, fAllPrimes ); - if ( pSat == NULL ) - { - fprintf( stdout, "The problem is trivially UNSAT. No CNF file is generated.\n" ); - return 1; - } + pSat = Abc_NtkMiterSatCreate( pNtk ); // write the clauses - s_pNtk = pNtk; - Sat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 ); - s_pNtk = NULL; + Asat_SolverWriteDimacs( pSat, pFileName ); // free the solver - sat_solver_delete( pSat ); + 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 /// |