diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-01-23 08:01:00 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-01-23 08:01:00 -0800 |
| commit | b1a913fb5e85ba04646632f3d771ad79bfd8a720 (patch) | |
| tree | 672fd9d1e3f52bf9be192cb91355e2eee6b14302 /src/base/io | |
| parent | 2167d6c148191f7aa65381bb0618b64050bf4de3 (diff) | |
| download | abc-b1a913fb5e85ba04646632f3d771ad79bfd8a720.tar.gz abc-b1a913fb5e85ba04646632f3d771ad79bfd8a720.tar.bz2 abc-b1a913fb5e85ba04646632f3d771ad79bfd8a720.zip | |
Version abc70123
Diffstat (limited to 'src/base/io')
| -rw-r--r-- | src/base/io/ioWriteCnf.c | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c index f12a1297..88695668 100644 --- a/src/base/io/ioWriteCnf.c +++ b/src/base/io/ioWriteCnf.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "io.h" +#include "satSolver.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -43,7 +44,7 @@ static Abc_Ntk_t * s_pNtk = NULL; ***********************************************************************/ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes ) { - solver * pSat; + sat_solver * pSat; if ( Abc_NtkIsStrash(pNtk) ) printf( "Io_WriteCnf() warning: Generating CNF by applying heuristic AIG to CNF conversion.\n" ); else @@ -67,7 +68,7 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes ) if ( Abc_NtkIsLogic(pNtk) ) Abc_NtkLogicToBdd( pNtk ); // create solver with clauses - pSat = Abc_NtkMiterSatCreate( pNtk, 0, fAllPrimes ); + pSat = Abc_NtkMiterSatCreate( pNtk, fAllPrimes ); if ( pSat == NULL ) { fprintf( stdout, "The problem is trivially UNSAT. No CNF file is generated.\n" ); @@ -75,10 +76,10 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes ) } // write the clauses s_pNtk = pNtk; - Asat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 ); + Sat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 ); s_pNtk = NULL; // free the solver - solver_delete( pSat ); + sat_solver_delete( pSat ); return 1; } |