Skip to content

Commit

Permalink
Merge branch 'dev'
Browse files Browse the repository at this point in the history
  • Loading branch information
@marekpiotrow
marekpiotrow committed Apr 28, 2024
2 parents 721c505 + ec368c4 commit 5a4c82c
Show file tree
Hide file tree
Showing 12 changed files with 216 additions and 58 deletions.
4 changes: 2 additions & 2 deletions ADTs/File.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ class File {
#endif
if (pos == File_BufSize){
ssize_t wrote = write(fd, buf, File_BufSize);
if (wrote != File_BufSize) printf("ERROR! Write failed.\n"), exit(1);
if (wrote != File_BufSize) printf("ERROR! Write failed.\n"), exit(0);
pos = 0; }
return buf[pos++] = (uchar)chr; }

Expand All @@ -129,7 +129,7 @@ class File {
void flush(void) {
assert(mode == WRITE);
ssize_t wrote = write(fd, buf, pos);
if (wrote != pos) printf("ERROR! Write failed.\n"), exit(1);
if (wrote != pos) printf("ERROR! Write failed.\n"), exit(0);
pos = 0; }

void seek(int64 pos, int whence = SEEK_SET);
Expand Down
4 changes: 2 additions & 2 deletions ADTs/Global.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,7 @@ template<class T> macro T* xmalloc(size_t size) {
T* tmp = (T*)malloc(size * sizeof(T));
assert(size == 0 || tmp != NULL);
if (size != 0 && tmp == NULL) { // M. Piotrow 11.10.2017
exit(1);
exit(0);
//std::bad_alloc exc; throw exc;
}
return tmp; }
Expand All @@ -129,7 +129,7 @@ template<class T> macro T* xrealloc(T* ptr, size_t size) {
T* tmp = (T*)realloc((void*)ptr, size * sizeof(T));
assert(size == 0 || tmp != NULL);
if (size != 0 && tmp == NULL) { // M. Piotrow 11.10.2017
exit(1);
exit(0);
//std::bad_alloc exc; throw exc;
}
return tmp; }
Expand Down
2 changes: 1 addition & 1 deletion Main.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -159,5 +159,5 @@ int main(int argc, char** argv)
if (opt_scip_parallel)
std::this_thread::sleep_for(std::chrono::milliseconds(10));
#endif
std::_Exit(0); // (faster than "return", which will invoke the destructor for 'PbSolver')
std::_Exit(exit_code); // (faster than "return", which will invoke the destructor for 'PbSolver')
}
38 changes: 23 additions & 15 deletions Main_utils.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,6 +87,7 @@ bool opt_maxsat_prepr = true;
bool opt_use_maxpre = false;
bool opt_reuse_sorters = true;
uint64_t opt_unsat_conflicts = 5000000;
int exit_code = 0;
#ifdef MAXPRE
char opt_maxpre_str[80]= "[uvsrgc]";
int opt_maxpre_time = 0;
Expand All @@ -97,9 +98,12 @@ maxPreprocessor::PreprocessorInterface *maxpre_ptr = NULL;
#ifdef USE_SCIP
bool opt_use_scip_slvr = true;
double opt_scip_cpu = 0;
double opt_scip_cpu_default = 400;
double opt_scip_cpu_default = 600;
double opt_scip_cpu_add = 400;
bool opt_scip_parallel = true;
time_t wall_clock_time;
bool opt_force_scip = false;
double opt_scip_delay = 0;
#endif

char* opt_input = NULL;
Expand Down Expand Up @@ -159,18 +163,18 @@ void outputResult(const PbSolver& S, bool optimum)

if (opt_output_top < 0) {
if (optimum){
if (S.best_goalvalue == Int_MAX) printf("s UNSATISFIABLE\n");
if (S.best_goalvalue == Int_MAX) printf("s UNSATISFIABLE\n"), exit_code = 20;
else {
if (!opt_satisfiable_out) {
char* tmp = toString(S.best_goalvalue);
printf("o %s\n", tmp);
xfree(tmp);
}
printf("s OPTIMUM FOUND\n");
printf("s OPTIMUM FOUND\n"), exit_code = 30;
}
}else{
if (S.best_goalvalue == Int_MAX) printf("s UNKNOWN\n");
else printf("%c SATISFIABLE\n", (opt_satisfiable_out ? 's' : 'c'));
if (S.best_goalvalue == Int_MAX) printf("s UNKNOWN\n"), exit_code = 0;
else printf("%c SATISFIABLE\n", (opt_satisfiable_out ? 's' : 'c')), exit_code = 10;
}
resultsPrinted = true;
} else if (opt_output_top == 1) resultsPrinted = true;
Expand Down Expand Up @@ -313,12 +317,12 @@ void handlerOutputResult(const PbSolver& S, bool optimum = true)
}
const char *out = NULL;
if (optimum){
if (S.best_goalvalue == Int_MAX) out = "s UNSATISFIABLE\n";
else out = "s OPTIMUM FOUND\n";
if (S.best_goalvalue == Int_MAX) out = "s UNSATISFIABLE\n", exit_code = 20;
else out = "s OPTIMUM FOUND\n", exit_code = 30;
}else{
if (S.best_goalvalue == Int_MAX) out = "s UNKNOWN\n";
else if (opt_satisfiable_out) out = "s SATISFIABLE\n";
else out = "c SATISFIABLE\n";
if (S.best_goalvalue == Int_MAX) out = "s UNKNOWN\n", exit_code = 0;
else if (opt_satisfiable_out) out = "s SATISFIABLE\n", exit_code = 10;
else out = "c SATISFIABLE\n", exit_code = 10;
}
if (out != NULL) strcpy(buf + lst, out), lst += strlen(out);
lst = write(1, buf, lst); lst = 0;
Expand All @@ -331,7 +335,7 @@ void SIGINT_handler(int /*signum*/) {
reportf("*** INTERRUPTED ***\n");
//SatELite::deleteTmpFiles();
fflush(stdout);
std::_Exit(0); }
std::_Exit(exit_code); }


void SIGTERM_handler(int signum) {
Expand All @@ -345,7 +349,7 @@ void SIGTERM_handler(int signum) {
handlerOutputResult(*pb_solver, false);
//SatELite::deleteTmpFiles();
//fflush(stdout);
std::_Exit(0);
std::_Exit(exit_code);
}

void increase_stack_size(int new_size) // M. Piotrow 16.10.2017
Expand Down Expand Up @@ -452,6 +456,8 @@ static cchar* doc =
" -no-scip Do not use SCIP solver. (The default setting is to use it for small instances.)\n"
" -scip-cpu= Timeout in seconds for SCIP solver. Zero - no limit (default).\n"
" -no-par Do not run SCIP solver in a separate thread. Timeout is changed to %gs if not set by user. \n"
" -force-scip Force to run SCIP solver. (The default setting is to use it for small instances.)\n"
" -scip-delay= Time in seconds to delay SCIP start if it has to use the same thread. Zero - no delay (default)\n"
#endif
"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\n"
;
Expand Down Expand Up @@ -548,7 +554,9 @@ static void parseOptions(int argc, char** argv, bool check_files)
#endif
#ifdef USE_SCIP
else if (oneof(arg, "no-scip" )) opt_use_scip_slvr = false;
else if (oneof(arg, "force-scip")) opt_force_scip = true;
else if (strncmp(arg, "-scip-cpu=", 10) == 0) opt_scip_cpu = atoi(arg+10);
else if (strncmp(arg, "-scip-delay=", 12) == 0) opt_scip_delay = atoi(arg+12);
else if (oneof(arg, "no-par" )) opt_scip_parallel = false, opt_scip_cpu = (opt_scip_cpu == 0 ? opt_scip_cpu_default : opt_scip_cpu);
#endif
else if (oneof(arg, "s,satlive" )) opt_satlive = false;
Expand All @@ -572,13 +580,13 @@ static void parseOptions(int argc, char** argv, bool check_files)
opt_use_maxpre = true, opt_maxpre_time = atoi(arg+13);
#else
else if (strncmp(arg, "-maxpre", 7)==0 || strncmp(arg, "-maxpre-skip", 12)==0 || strncmp(arg, "-maxpre-time", 12)==0)
fprintf(stderr, "ERROR! MaxPre is not available: invalid command line option: %s\n", argv[i]), exit(1);
fprintf(stderr, "ERROR! MaxPre is not available: invalid command line option: %s\n", argv[i]), exit(0);
#endif
else if (strncmp(arg, "-top=", 5) == 0)
opt_minimization = 1, opt_maxsat_msu = true, opt_to_bin_search = false,
opt_output_top = atoi(arg+5);
else
fprintf(stderr, "ERROR! Invalid command line option: %s\n", argv[i]), exit(1);
fprintf(stderr, "ERROR! Invalid command line option: %s\n", argv[i]), exit(0);

}else
args.push(arg);
Expand All @@ -600,7 +608,7 @@ static void parseOptions(int argc, char** argv, bool check_files)
opt_result = args[1];
else if (args.size() > 2)
fprintf(stderr, "ERROR! Too many files specified on commandline.\n"),
exit(1);
exit(0);
}

void setOptions(int argc, char *argv[], bool check_files)
Expand Down
4 changes: 4 additions & 0 deletions Main_utils.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ extern bool opt_preprocess;
extern bool opt_old_format;
extern int opt_mem_lim;
extern bool opt_use_maxpre;
extern int exit_code;

#ifdef MAXPRE
extern char *opt_maxpre_str;
Expand All @@ -18,8 +19,11 @@ extern int opt_maxpre_skip;
extern bool opt_use_scip_slvr;
extern double opt_scip_cpu;
extern double opt_scip_cpu_default;
extern double opt_scip_cpu_add;
extern bool opt_scip_parallel;
extern time_t wall_clock_time;
extern bool opt_force_scip;
extern double opt_scip_delay;
#endif

extern MsSolver *pb_solver;
Expand Down
Loading

0 comments on commit 5a4c82c

Please sign in to comment.