diff options
Diffstat (limited to 'src/sat/bsat2/MainSimp.cpp')
| -rw-r--r-- | src/sat/bsat2/MainSimp.cpp | 206 |
1 files changed, 206 insertions, 0 deletions
diff --git a/src/sat/bsat2/MainSimp.cpp b/src/sat/bsat2/MainSimp.cpp new file mode 100644 index 00000000..4a890921 --- /dev/null +++ b/src/sat/bsat2/MainSimp.cpp @@ -0,0 +1,206 @@ +/*****************************************************************************************[Main.cc] +Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +Copyright (c) 2007, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#include <errno.h> + +#include <signal.h> +#include "misc/zlib/zlib.h" + +#ifndef _WIN32 +#include <sys/resource.h> +#endif + +#include "System.h" +#include "ParseUtils.h" +#include "Options.h" +#include "Dimacs.h" +#include "SimpSolver.h" + +using namespace Minisat; + +//================================================================================================= + +extern void printStats(Solver& solver); + +static Solver* solver; +// Terminate by notifying the solver and back out gracefully. This is mainly to have a test-case +// for this feature of the Solver as it may take longer than an immediate call to '_exit()'. +static void SIGINT_interrupt(int signum) { solver->interrupt(); } + +// Note that '_exit()' rather than 'exit()' has to be used. The reason is that 'exit()' calls +// destructors and may cause deadlocks if a malloc/free function happens to be running (these +// functions are guarded by locks for multithreaded use). +static void SIGINT_exit(int signum) { + printf("\n"); printf("*** INTERRUPTED ***\n"); + if (solver->verbosity > 0){ + printStats(*solver); + printf("\n"); printf("*** INTERRUPTED ***\n"); } + _exit(1); } + + +//================================================================================================= +// Main: + +extern "C" int MainSimp(int argc, char** argv) +{ + try { + setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n where input may be either in plain or gzipped DIMACS.\n"); + // printf("This is MiniSat 2.0 beta\n"); + +#if defined(__linux__) + fpu_control_t oldcw, newcw; + _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw); + printf("WARNING: for repeatability, setting FPU to use double precision\n"); +#endif + // Extra options: + // + IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2)); + BoolOption pre ("MAIN", "pre", "Completely turn on/off any preprocessing.", true); + StringOption dimacs ("MAIN", "dimacs", "If given, stop after preprocessing and write the result to this file."); + IntOption cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", INT32_MAX, IntRange(0, INT32_MAX)); + IntOption mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", INT32_MAX, IntRange(0, INT32_MAX)); + + if ( !parseOptions(argc, argv, true) ) + return 1; + + SimpSolver S; + double initial_time = cpuTime(); + + if (!pre) S.eliminate(true); + + S.verbosity = verb; + + solver = &S; +/* + // Use signal handlers that forcibly quit until the solver will be able to respond to + // interrupts: + signal(SIGINT, SIGINT_exit); + signal(SIGXCPU,SIGINT_exit); + + // Set limit on CPU-time: + if (cpu_lim != INT32_MAX){ + rlimit rl; + getrlimit(RLIMIT_CPU, &rl); + if (rl.rlim_max == RLIM_INFINITY || (rlim_t)cpu_lim < rl.rlim_max){ + rl.rlim_cur = cpu_lim; + if (setrlimit(RLIMIT_CPU, &rl) == -1) + printf("WARNING! Could not set resource limit: CPU-time.\n"); + } } + + // Set limit on virtual memory: + if (mem_lim != INT32_MAX){ + rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024; + rlimit rl; + getrlimit(RLIMIT_AS, &rl); + if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){ + rl.rlim_cur = new_mem_lim; + if (setrlimit(RLIMIT_AS, &rl) == -1) + printf("WARNING! Could not set resource limit: Virtual memory.\n"); + } } +*/ + if (argc == 1) + { + printf("Reading from standard input... Use '--help' for help.\n"); + return 1; + } + + gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb"); + if (in == NULL) + printf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1); + + if (S.verbosity > 0){ + printf("============================[ Problem Statistics ]=============================\n"); + printf("| |\n"); } + + parse_DIMACS(in, S); + gzclose(in); + FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL; + + if (S.verbosity > 0){ + printf("| Number of variables: %12d |\n", S.nVars()); + printf("| Number of clauses: %12d |\n", S.nClauses()); } + + double parsed_time = cpuTime(); + if (S.verbosity > 0) + printf("| Parse time: %12.2f s |\n", parsed_time - initial_time); + + // Change to signal-handlers that will only notify the solver and allow it to terminate + // voluntarily: +// signal(SIGINT, SIGINT_interrupt); +// signal(SIGXCPU,SIGINT_interrupt); + + S.eliminate(true); + double simplified_time = cpuTime(); + if (S.verbosity > 0){ + printf("| Simplification time: %12.2f s |\n", simplified_time - parsed_time); + printf("| |\n"); } + + if (!S.okay()){ + if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res); + if (S.verbosity > 0){ + printf("===============================================================================\n"); + printf("Solved by simplification\n"); + printStats(S); + printf("\n"); } + printf("UNSATISFIABLE\n"); + exit(20); + } + + if (dimacs){ + if (S.verbosity > 0) + printf("==============================[ Writing DIMACS ]===============================\n"); + S.toDimacs((const char*)dimacs); + if (S.verbosity > 0) + printStats(S); + exit(0); + } + + vec<Lit> dummy; + lbool ret = S.solveLimited(dummy); + + if (S.verbosity > 0){ + printStats(S); + printf("\n"); } + printf(ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n"); + if (res != NULL){ + if (ret == l_True){ + fprintf(res, "SAT\n"); + for (int i = 0; i < S.nVars(); i++) + if (S.model[i] != l_Undef) + fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); + fprintf(res, " 0\n"); + }else if (ret == l_False) + fprintf(res, "UNSAT\n"); + else + fprintf(res, "INDET\n"); + fclose(res); + } + +//#ifdef NDEBUG +// exit(ret == l_True ? 10 : ret == l_False ? 20 : 0); // (faster than "return", which will invoke the destructor for 'Solver') +//#else + return (ret == l_True ? 10 : ret == l_False ? 20 : 0); +//#endif + } catch (OutOfMemoryException&){ + printf("===============================================================================\n"); + printf("INDETERMINATE\n"); + exit(0); + } +} |