Skip to content

Commit

Permalink
Versioning: added version command and reintroduced help message
Browse files Browse the repository at this point in the history 
Versioning: version command and automatic generation of version.h

Versioning: updated version production to macros in CMake and changed SMTConfig

Versioning: rework of the parameters for opensmt

Versioning: fix of Martin's comments

Versioning: fix of Tomas' comments

Versioning: code cleaning

Versioning: removed pipe and slight renaming
  • Loading branch information
@BritikovKI
BritikovKI committed Nov 13, 2024
1 parent fd98482 commit c267e01
Show file tree
Hide file tree
Showing 4 changed files with 97 additions and 81 deletions.
14 changes: 13 additions & 1 deletion CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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}
Expand Down Expand Up @@ -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)
Expand Down
120 changes: 84 additions & 36 deletions src/bin/opensmt.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
#include <cstdlib>
#include <cstdio>
#include <csignal>
#include <getopt.h>
#include <iostream>
#include <unistd.h>

Expand All @@ -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 );

/*****************************************************************************\
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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] <filename>\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] <seed> 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
37 changes: 0 additions & 37 deletions src/options/SMTConfig.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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=<filename> use configuration file <filename>\n";
std::cerr << help_string;
}
}
7 changes: 0 additions & 7 deletions src/options/SMTConfig.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
//
Expand Down Expand Up @@ -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; }
Expand Down

0 comments on commit c267e01

Please sign in to comment.