/**CFile**************************************************************** FileName [AbcGlucoseCmd.cpp] SystemName [ABC: Logic synthesis and verification system.] PackageName [SAT solver Glucose 3.0.] Synopsis [Interface to Glucose.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - September 6, 2017.] Revision [$Id: AbcGlucoseCmd.cpp,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "aig/gia/gia.h" #include "base/main/mainInt.h" #include "sat/glucose/AbcGlucose.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// static int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ extern "C" { void Glucose_Init(Abc_Frame_t *pAbc) { Cmd_CommandAdd( pAbc, "ABC9", "&glucose", Abc_CommandGlucose, 0 ); } void Glucose_End( Abc_Frame_t * pAbc ) { } } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Glucose_SolveCnf( char * pFilename, ExtSat_Pars * pPars ); extern int Glucose_SolveAig( Gia_Man_t * p, ExtSat_Pars * pPars ); int c = 0; int pre = 1; int verb = 0; int nConfls = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "Cpvh" ) ) != EOF ) { switch ( c ) { case 'C': if ( globalUtilOptind >= argc ) { Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); goto usage; } nConfls = atoi(argv[globalUtilOptind]); globalUtilOptind++; if ( nConfls < 0 ) goto usage; break; case 'p': pre ^= 1; break; case 'v': verb ^= 1; break; case 'h': goto usage; default: goto usage; } } ExtSat_Pars pPars = ExtSat_CreatePars(pre,verb,0,nConfls); if ( argc == globalUtilOptind + 1 ) { Glucose_SolveCnf( argv[globalUtilOptind], &pPars ); return 0; } if ( pAbc->pGia == NULL ) { Abc_Print( -1, "Abc_CommandGlucose(): There is no AIG.\n" ); return 1; } if ( Glucose_SolveAig( pAbc->pGia, &pPars ) == 10 ) Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb ); return 0; usage: Abc_Print( -2, "usage: &glucose [-C num] [-pvh] \n" ); Abc_Print( -2, "\t run glucose\n" ); Abc_Print( -2, "\t-C num : conflict limit [default = %d]\n", nConfls ); Abc_Print( -2, "\t-p : enable preprocessing [default = %d]\n",pre); Abc_Print( -2, "\t-v : verbosity [default = %d]\n",verb); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t : (optional) CNF file to solve\n"); return 1; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END