From: Mathias Preiner Date: Thu, 11 Mar 2021 00:51:12 +0000 (-0800) Subject: Use CVC4_ASSERTIONS instead of NDEBUG. (#6099) X-Git-Tag: cvc5-1.0.0~2106 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a5ede7e253513ac0103c2521d7ac0c0452062b43;p=cvc5.git Use CVC4_ASSERTIONS instead of NDEBUG. (#6099) Ensures that all checks are performed in production builds with enabled assertions. --- diff --git a/src/prop/bvminisat/core/Main.cc b/src/prop/bvminisat/core/Main.cc deleted file mode 100644 index 307a4d7d9..000000000 --- a/src/prop/bvminisat/core/Main.cc +++ /dev/null @@ -1,198 +0,0 @@ -/*****************************************************************************************[Main.cc] -Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson -Copyright (c) 2007-2010, 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 - -#include -#include - -#include "prop/bvminisat/core/Dimacs.h" -#include "prop/bvminisat/core/Solver.h" -#include "prop/bvminisat/utils/Options.h" -#include "prop/bvminisat/utils/ParseUtils.h" -#include "prop/bvminisat/utils/System.h" - -namespace CVC4 { -namespace BVMinisat { - -//================================================================================================= - - -void printStats(Solver& solver) -{ - double cpu_time = cpuTime(); - double mem_used = memUsedPeak(); - printf("restarts : %"PRIu64"\n", solver.starts); - printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); - printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time); - printf("propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); - printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); - if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); - printf("CPU time : %g s\n", cpu_time); -} - - -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); } - -} /* CVC4::BVMinisat namespace */ -} /* CVC4 namespace */ - -//================================================================================================= -// Main: - - -int main(int argc, char** argv) -{ - using namespace CVC4; - using namespace CVC4::BVMinisat; - - try { - setUsageHelp("USAGE: %s [options] \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)); - 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)); - - parseOptions(argc, argv, true); - - Solver S; - double initial_time = cpuTime(); - - 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"); - - gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb"); - if (in == NULL) - printf("ERROR! Could not open file: %s\n", argc == 1 ? "" : 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); - printf("| |\n"); } - - // Change to signal-handlers that will only notify the solver and allow it to terminate - // voluntarily: - signal(SIGINT, SIGINT_interrupt); - signal(SIGXCPU,SIGINT_interrupt); - - if (!S.simplify()){ - if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res); - if (S.verbosity > 0){ - printf("===============================================================================\n"); - printf("Solved by unit propagation\n"); - printStats(S); - printf("\n"); } - printf("UNSATISFIABLE\n"); - exit(20); - } - - vec 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); - } -} diff --git a/src/prop/bvminisat/simp/Main.cc b/src/prop/bvminisat/simp/Main.cc deleted file mode 100644 index 481ed3f39..000000000 --- a/src/prop/bvminisat/simp/Main.cc +++ /dev/null @@ -1,217 +0,0 @@ -/*****************************************************************************************[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 - -#include -#include -#include - -#include "prop/bvminisat/core/Dimacs.h" -#include "prop/bvminisat/simp/SimpSolver.h" -#include "prop/bvminisat/utils/Options.h" -#include "prop/bvminisat/utils/ParseUtils.h" -#include "prop/bvminisat/utils/System.h" - -//================================================================================================= - - -namespace CVC4 { -namespace BVMinisat { - -void printStats(Solver& solver) -{ - double cpu_time = cpuTime(); - double mem_used = memUsedPeak(); - printf("restarts : %"PRIu64"\n", solver.starts); - printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); - printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time); - printf("propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); - printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); - if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); - printf("CPU time : %g s\n", cpu_time); -} - - -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); } - - -} /* CVC4::BVMinisat namespace */ -} /* CVC4 namespace */ - -//================================================================================================= -// Main: - -int main(int argc, char** argv) -{ - using namespace CVC4; - using namespace CVC4::BVMinisat; - try { - setUsageHelp("USAGE: %s [options] \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)); - - parseOptions(argc, argv, true); - - 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"); - - gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb"); - if (in == NULL) - printf("ERROR! Could not open file: %s\n", argc == 1 ? "" : 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 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); - } -} diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index dcf9ba89b..10f0aa03e 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -166,7 +166,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) bool SimpSolver::addClause_(vec& ps, ClauseId& id) { -#ifndef NDEBUG +#ifdef CVC4_ASSERTIONS for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i]))); #endif diff --git a/src/prop/minisat/core/Main.cc b/src/prop/minisat/core/Main.cc deleted file mode 100644 index 64a2a1c50..000000000 --- a/src/prop/minisat/core/Main.cc +++ /dev/null @@ -1,197 +0,0 @@ -/*****************************************************************************************[Main.cc] -Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson -Copyright (c) 2007-2010, 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 - -#include -#include - -#include "prop/minisat/utils/System.h" -#include "prop/minisat/utils/ParseUtils.h" -#include "prop/minisat/utils/Options.h" -#include "prop/minisat/core/Dimacs.h" -#include "prop/minisat/core/Solver.h" - -//================================================================================================= - - -namespace CVC4 { -namespace Minisat { -void printStats(Solver& solver) -{ - double cpu_time = cpuTime(); - double mem_used = memUsedPeak(); - printf("restarts : %"PRIu64"\n", solver.starts); - printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); - printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time); - printf("propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); - printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); - if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); - printf("CPU time : %g s\n", cpu_time); -} - - -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); } - -} /* CVC4::Minisat namespace */ -} /* CVC4 namespace */ - - -//================================================================================================= -// Main: - - -int main(int argc, char** argv) -{ - using namespace CVC4; - using namespace CVC4::Minisat; - try { - setUsageHelp("USAGE: %s [options] \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)); - 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)); - - parseOptions(argc, argv, true); - - Solver S; - double initial_time = cpuTime(); - - 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"); - - gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb"); - if (in == NULL) - printf("ERROR! Could not open file: %s\n", argc == 1 ? "" : 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); - printf("| |\n"); } - - // Change to signal-handlers that will only notify the solver and allow it to terminate - // voluntarily: - signal(SIGINT, SIGINT_interrupt); - signal(SIGXCPU,SIGINT_interrupt); - - if (!S.simplify()){ - if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res); - if (S.verbosity > 0){ - printf("===============================================================================\n"); - printf("Solved by unit propagation\n"); - printStats(S); - printf("\n"); } - printf("UNSATISFIABLE\n"); - exit(20); - } - - vec 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); - } -} diff --git a/src/prop/minisat/simp/Main.cc b/src/prop/minisat/simp/Main.cc deleted file mode 100644 index 675d0ed60..000000000 --- a/src/prop/minisat/simp/Main.cc +++ /dev/null @@ -1,218 +0,0 @@ -/*****************************************************************************************[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 - -#include -#include -#include - -#include "prop/minisat/utils/System.h" -#include "prop/minisat/utils/ParseUtils.h" -#include "prop/minisat/utils/Options.h" -#include "prop/minisat/core/Dimacs.h" -#include "prop/minisat/simp/SimpSolver.h" - -//================================================================================================= - - -namespace CVC4 { -namespace Minisat { - -void printStats(Solver& solver) -{ - double cpu_time = cpuTime(); - double mem_used = memUsedPeak(); - printf("restarts : %"PRIu64"\n", solver.starts); - printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); - printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time); - printf("propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); - printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); - if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); - printf("CPU time : %g s\n", cpu_time); -} - - - - -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); } - -} /* CVC4::Minisat namespace */ -} /* CVC4 namespace */ - -//================================================================================================= -// Main: - -int main(int argc, char** argv) -{ - using namespace CVC4; - using namespace CVC4::Minisat; - try { - setUsageHelp("USAGE: %s [options] \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)); - - parseOptions(argc, argv, true); - - 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"); - - gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb"); - if (in == NULL) - printf("ERROR! Could not open file: %s\n", argc == 1 ? "" : 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 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); - } -} diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index e925bad09..7051134eb 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -172,7 +172,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) bool SimpSolver::addClause_(vec& ps, bool removable, ClauseId& id) { -#ifndef NDEBUG +#ifdef CVC4_ASSERTIONS if (use_simplification) { for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i]))); } diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index ebd528616..0dd7cc070 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -451,7 +451,7 @@ Node lower_bound_as_node(const Node& var, poly::get_upper(poly::get_isolating_interval(alg))); int sl = poly::sign_at(get_defining_polynomial(alg), poly::get_lower(poly::get_isolating_interval(alg))); -#ifndef NDEBUG +#ifdef CVC4_ASSERTIONS int su = poly::sign_at(get_defining_polynomial(alg), poly::get_upper(poly::get_isolating_interval(alg))); Assert(sl != 0 && su != 0 && sl != su); @@ -507,7 +507,7 @@ Node upper_bound_as_node(const Node& var, poly::get_lower(poly::get_isolating_interval(alg))); Rational u = poly_utils::toRational( poly::get_upper(poly::get_isolating_interval(alg))); -#ifndef NDEBUG +#ifdef CVC4_ASSERTIONS int sl = poly::sign_at(get_defining_polynomial(alg), poly::get_lower(poly::get_isolating_interval(alg))); #endif diff --git a/src/util/real_algebraic_number_poly_imp.cpp b/src/util/real_algebraic_number_poly_imp.cpp index a7a55d63e..b4730c1b1 100644 --- a/src/util/real_algebraic_number_poly_imp.cpp +++ b/src/util/real_algebraic_number_poly_imp.cpp @@ -60,7 +60,7 @@ RealAlgebraicNumber::RealAlgebraicNumber(const std::vector& coefficients, long lower, long upper) { -#ifndef NDEBUG +#ifdef CVC4_ASSERTIONS for (long c : coefficients) { Assert(std::numeric_limits::min() <= c