From f68bd519c69dabfe0c507810d84d3289e082947e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 6 Sep 2017 17:57:44 -0700 Subject: Integrating Glucose into &bmcs -g. --- src/sat/glucose/AbcGlucoseCmd.cpp | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) (limited to 'src/sat/glucose/AbcGlucoseCmd.cpp') diff --git a/src/sat/glucose/AbcGlucoseCmd.cpp b/src/sat/glucose/AbcGlucoseCmd.cpp index 80fdb77f..8dbe3790 100644 --- a/src/sat/glucose/AbcGlucoseCmd.cpp +++ b/src/sat/glucose/AbcGlucoseCmd.cpp @@ -72,15 +72,12 @@ void Glucose_End( Abc_Frame_t * pAbc ) ***********************************************************************/ 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 c = 0; + int pre = 1; + int verb = 0; int nConfls = 0; - ExtSat_Pars pPars; + Glucose_Pars pPars; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "Cpvh" ) ) != EOF ) { @@ -110,7 +107,7 @@ int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - pPars = ExtSat_CreatePars(pre,verb,0,nConfls); + pPars = Glucose_CreatePars(pre,verb,0,nConfls); if ( argc == globalUtilOptind + 1 ) { -- cgit v1.2.3