diff --git a/Main_utils.cc b/Main_utils.cc index 882d754..4096255 100644 --- a/Main_utils.cc +++ b/Main_utils.cc @@ -35,6 +35,7 @@ Read a DIMACS file and apply the SAT-solver to it. #include "MsSolver.h" #include "PbParser.h" #include "FEnv.h" +#include "Main_utils.h" #ifdef MAXPRE #include "preprocessorinterface.hpp" @@ -388,7 +389,7 @@ PbSolver::solve_Command convert(Command cmd) { static cchar* doc = "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\n" - "UWrMaxSat 1.5 -- University of Wrocław MaxSAT solver by Marek Piotrów (2019-2024)\n" + "UWrMaxSat %s -- University of Wrocław MaxSAT solver by Marek Piotrów (2019-2024)\n" "and PB solver by Marek Piotrów and Michał Karpiński (2018) -- an extension of\n" "MiniSat+ 1.1, based on MiniSat 2.2.0 -- (C) Niklas Een, Niklas Sorensson (2012)\n" "with COMiniSatPS by Chanseok Oh (2016) as the SAT solver\n" @@ -494,7 +495,7 @@ static void parseOptions(int argc, char** argv, bool check_files) char* arg = argv[i]; if (arg[0] == '-'){ if (oneof(arg,"h,help")) - fprintf(stderr, doc, opt_bdd_thres, opt_sort_thres, opt_goal_bias, opt_base_max, + fprintf(stderr, doc, UWR_VERSION, opt_bdd_thres, opt_sort_thres, opt_goal_bias, opt_base_max, opt_base_max, opt_unsat_conflicts #ifdef MAXPRE , opt_maxpre_str @@ -596,7 +597,7 @@ static void parseOptions(int argc, char** argv, bool check_files) } if (args.size() == 0 && check_files) - fprintf(stderr, doc, opt_bdd_thres, opt_sort_thres, opt_goal_bias, opt_base_max, + fprintf(stderr, doc, UWR_VERSION, opt_bdd_thres, opt_sort_thres, opt_goal_bias, opt_base_max, opt_base_max, opt_unsat_conflicts #ifdef MAXPRE , opt_maxpre_str diff --git a/Main_utils.h b/Main_utils.h index 2841a93..f1ae1f0 100644 --- a/Main_utils.h +++ b/Main_utils.h @@ -21,6 +21,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef MAIN_UTILS_H #define MAIN_UTILS_H +#ifndef UWR_VERSION +#define UWR_VERSION "1.6.0" +#endif + extern bool opt_model_out; extern bool opt_bin_model_out; extern bool opt_satisfiable_out; @@ -32,7 +36,7 @@ extern bool opt_use_maxpre; extern int exit_code; #ifdef MAXPRE -extern char *opt_maxpre_str; +extern char opt_maxpre_str[]; extern int opt_maxpre_time; extern int opt_maxpre_skip; #endif diff --git a/ipamir.cc b/ipamir.cc index 99fd32b..384435d 100644 --- a/ipamir.cc +++ b/ipamir.cc @@ -21,11 +21,6 @@ FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. ***********************************************/ -/** - * Return the name and the version of the incremental SAT - * solving library. - */ - #include "MsSolver.h" #include "FEnv.h" #include "Main_utils.h" @@ -72,7 +67,7 @@ extern "C" { */ IPAMIR_API const char * ipamir_signature () { - static char tmp[200] = "UWrMaxSat"; + static char tmp[200] = "UWrMaxSat" UWR_VERSION; return tmp; }