diff --git a/CMakeLists.txt b/CMakeLists.txt index a848fcda1..d73912a60 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -4,6 +4,13 @@ set(OPENSMT_VERSION_MAJOR 2) set(OPENSMT_VERSION_MINOR 8) set(OPENSMT_VERSION_PATCH 1) set(OPENSMT_VERSION ${OPENSMT_VERSION_MAJOR}.${OPENSMT_VERSION_MINOR}.${OPENSMT_VERSION_PATCH}) +execute_process( + COMMAND git describe --tags --dirty + WORKING_DIRECTORY ${CMAKE_CURRENT_LIST_DIR} + OUTPUT_VARIABLE OPENSMT_GIT_DESCRIPTION + OUTPUT_STRIP_TRAILING_WHITESPACE + ) + project(opensmt VERSION ${OPENSMT_VERSION} LANGUAGES CXX) set(CMAKE_CXX_STANDARD 20) @@ -66,7 +73,6 @@ find_package(GMP REQUIRED) set(THREADS_PREFER_PTHREAD_FLAG ON) find_package(Threads REQUIRED) - include_directories( ${CMAKE_SOURCE_DIR} ${GMP_INCLUDE_DIR} @@ -119,6 +125,12 @@ endif() add_subdirectory(${CMAKE_SOURCE_DIR}) + +target_compile_definitions(OpenSMT-bin PRIVATE + OPENSMT_GIT_DESCRIPTION="${OPENSMT_GIT_DESCRIPTION}" +) + + ################# TESTING ############################################# if(PACKAGE_TESTS) if (NOT BUILD_SHARED_LIBS) diff --git a/src/bin/opensmt.cc b/src/bin/opensmt.cc index 8e775073f..56305b81f 100644 --- a/src/bin/opensmt.cc +++ b/src/bin/opensmt.cc @@ -30,6 +30,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. #include #include #include +#include #include #include @@ -48,6 +49,10 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. namespace opensmt { +inline bool pipeExecution = false; + +SMTConfig parseCMDLineArgs(int argc, char * argv[ ]); + void catcher ( int ); /*****************************************************************************\ @@ -78,47 +83,13 @@ int main( int argc, char * argv[] ) // Accepts file from stdin if nothing specified FILE * fin = NULL; - int opt; - - SMTConfig c; - bool pipe = false; - while ((opt = getopt(argc, argv, "hdpir:v")) != -1) { - switch (opt) { - - case 'h': - // context.getConfig( ).printHelp( ); - break; - case 'd': - const char* msg; - c.setOption(SMTConfig::o_dryrun, SMTOption(true), msg); - break; - case 'r': - if (!c.setOption(SMTConfig::o_random_seed, SMTOption(atoi(optarg)), msg)) - fprintf(stderr, "Error setting random seed: %s\n", msg); - else - fprintf(stderr, "; Using random seed %d\n", atoi(optarg)); - break; - case 'i': - c.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); - break; - case 'v': - c.setOption(SMTConfig::o_verbosity, SMTOption(true), msg); - break; - case 'p': - pipe = true; - break; - default: /* '?' */ - fprintf(stderr, "Usage:\n\t%s [-d] [-h] [-r seed] filename [...]\n", - argv[0]); - return 0; - } - } + SMTConfig c = parseCMDLineArgs(argc,argv); Interpret interpreter(c); if (argc - optind == 0) { c.setInstanceName("stdin"); - if (pipe) { + if (pipeExecution) { interpreter.interpPipe(); } else { @@ -238,4 +209,81 @@ void catcher( int sig ) } } +void printVersion() { std::cerr << OPENSMT_GIT_DESCRIPTION << "\n"; } + + +void printHelp() +{ + const char help_string[] + = "Usage: opensmt [OPTION] \n" + "where OPTION can be\n" + " --help [-h] prints this help message and exits\n" + " --version prints opensmt version and exits\n" + " --dry-run [-d] executes dry run\n" + " --random-seed [-r] sets random seed to specific number\n" + " --produce-interpolants [-i] enables interpolant computation\n" + " --verbose [-v] verbose run of the solver\n" + " --pipe [-p] for execution within a pipe\n"; + std::cerr << help_string; +} + +SMTConfig parseCMDLineArgs( int argc, char * argv[ ] ) +{ + SMTConfig res; + int selectedLongOpt = 0; + constexpr int versionLongOpt = 1; + + struct option long_options[] = + { + {"help", no_argument, nullptr, 'h'}, + {"version", no_argument, &selectedLongOpt, versionLongOpt}, + {"verbose", no_argument, nullptr, 'v'}, + {"dry-run", no_argument, nullptr, 'd'}, + {"produce-interpolants", no_argument, nullptr, 'i'}, + {"pipe", no_argument, nullptr, 'p'}, + {"random-seed", required_argument, nullptr, 'r'}, + {0, 0, 0, 0} + }; + + while (true) { + int option_index = 0; + int c = getopt_long(argc, argv, "r:hdivp", long_options, &option_index); + if (c == -1) { break; } + + switch (c) { + case 0: + assert(*long_options[option_index].flag == versionLongOpt); + printVersion(); + exit(0); + case 'h': + printHelp(); + exit(0); + case 'd': + const char* msg; + res.setOption(SMTConfig::o_dryrun, SMTOption(true), msg); + break; + case 'r': + if (!res.setOption(SMTConfig::o_random_seed, SMTOption(atoi(optarg)), msg)) + fprintf(stderr, "Error setting random seed: %s\n", msg); + else + fprintf(stderr, "; Using random seed %d\n", atoi(optarg)); + break; + case 'i': + res.setOption(SMTConfig::o_produce_inter, SMTOption(true), msg); + break; + case 'v': + res.setOption(SMTConfig::o_verbosity, SMTOption(true), msg); + break; + case 'p': + pipeExecution = true; + break; + default: /* '?' */ + printHelp(); + exit(1); + } + } + + return res; +} + } // namespace opensmt diff --git a/src/options/SMTConfig.cc b/src/options/SMTConfig.cc index f1fd136c3..3388c7f1f 100644 --- a/src/options/SMTConfig.cc +++ b/src/options/SMTConfig.cc @@ -598,41 +598,4 @@ namespace opensmt { sat_theory_polarity_suggestion = 1; } - void - SMTConfig::parseCMDLine( int argc - , char * argv[ ] ) - { - for ( int i = 1 ; i < argc - 1 ; i ++ ) - { - const char * buf = argv[ i ]; - // Parsing of configuration options - // if ( sscanf( buf, "--config=%s", config_name ) == 1 ) - // { - // parseConfig( config_name ); - // break; - // } - if ( strcmp( buf, "--help" ) == 0 - || strcmp( buf, "-h" ) == 0 ) - { - printHelp( ); - exit( 1 ); - } - else - { - printHelp( ); - std::cerr << "unrecognized option" << buf << std::endl; - exit(1); - } - } - } - - void SMTConfig::printHelp( ) - { - const char help_string[] - = "Usage: ./opensmt [OPTION] filename\n" - "where OPTION can be\n" - " --help [-h] print this help\n" - " --config= use configuration file \n"; - std::cerr << help_string; - } } diff --git a/src/options/SMTConfig.h b/src/options/SMTConfig.h index b552687c6..91e98e1eb 100644 --- a/src/options/SMTConfig.h +++ b/src/options/SMTConfig.h @@ -387,11 +387,6 @@ namespace opensmt { // For standard executable // public: - SMTConfig(int argc, char* argv[]) : rocset(false), docset(false) { - initializeConfig( ); - // Parse command-line options - parseCMDLine( argc, argv ); - } // // For API // @@ -428,8 +423,6 @@ namespace opensmt { void initializeConfig ( ); void parseConfig ( char * ); - void parseCMDLine ( int argc, char * argv[ ] ); - void printHelp ( ); void printConfig ( std::ostream & out ); inline std::ostream & getStatsOut ( ) { assert( optionTable.has(o_produce_stats) ); return stats_out; }