diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-10-01 08:01:00 -0700 |
commit | 4812c90424dfc40d26725244723887a2d16ddfd9 (patch) | |
tree | b32ace96e7e2d84d586e09ba605463b6f49c3271 /src/base/io/ioWriteCnf.c | |
parent | e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (diff) | |
download | abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.gz abc-4812c90424dfc40d26725244723887a2d16ddfd9.tar.bz2 abc-4812c90424dfc40d26725244723887a2d16ddfd9.zip |
Version abc71001
Diffstat (limited to 'src/base/io/ioWriteCnf.c')
-rw-r--r-- | src/base/io/ioWriteCnf.c | 115 |
1 files changed, 115 insertions, 0 deletions
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c new file mode 100644 index 00000000..e1b2d956 --- /dev/null +++ b/src/base/io/ioWriteCnf.c @@ -0,0 +1,115 @@ +/**CFile**************************************************************** + + FileName [ioWriteCnf.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Command processing package.] + + Synopsis [Procedures to output CNF of the miter cone.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: ioWriteCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "io.h" +#include "satSolver.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Abc_Ntk_t * s_pNtk = NULL; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Write the miter cone into a CNF file for the SAT solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes ) +{ + 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 the miter (the network with one PO).\n" ); + return 0; + } + if ( Abc_NtkLatchNum(pNtk) != 0 ) + { + fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter for combinational circuits.\n" ); + return 0; + } + if ( Abc_NtkNodeNum(pNtk) == 0 ) + { + 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, fAllPrimes ); + if ( pSat == NULL ) + { + fprintf( stdout, "The problem is trivially UNSAT. No CNF file is generated.\n" ); + return 1; + } + // write the clauses + s_pNtk = pNtk; + Sat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 ); + s_pNtk = NULL; + // free the solver + 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 /// +//////////////////////////////////////////////////////////////////////// + + |