--- /dev/null
+
+#include "solver_interface.h"
+#include <errno.h>
+
+#include <signal.h>
+#include <zlib.h>
+#include <sys/resource.h>
+
+#include "utils/System.h"
+#include "utils/ParseUtils.h"
+#include "utils/Options.h"
+#include "core/Dimacs.h"
+#include "simp/SimpSolver.h"
+
+using namespace Glucose;
+
+
+static const char* _certified = "CORE -- CERTIFIED UNSAT";
+
+void printStats(Solver& solver)
+{
+ double cpu_time = cpuTime();
+ double mem_used = 0;//memUsedPeak();
+ printf("c restarts : %" PRIu64" (%" PRIu64" conflicts in avg)\n", solver.starts,(solver.starts>0 ?solver.conflicts/solver.starts : 0));
+ printf("c blocked restarts : %" PRIu64" (multiple: %" PRIu64") \n", solver.nbstopsrestarts,solver.nbstopsrestartssame);
+ printf("c last block at restart : %" PRIu64"\n",solver.lastblockatrestart);
+ printf("c nb ReduceDB : %" PRIu64"\n", solver.nbReduceDB);
+ printf("c nb removed Clauses : %" PRIu64"\n",solver.nbRemovedClauses);
+ printf("c nb learnts DL2 : %" PRIu64"\n", solver.nbDL2);
+ printf("c nb learnts size 2 : %" PRIu64"\n", solver.nbBin);
+ printf("c nb learnts size 1 : %" PRIu64"\n", solver.nbUn);
+
+ printf("c conflicts : %-12" PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time);
+ printf("c decisions : %-12" PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time);
+ printf("c propagations : %-12" PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
+ printf("c conflict literals : %-12" PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
+ printf("c nb reduced Clauses : %" PRIu64"\n",solver.nbReducedClauses);
+
+ if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
+ printf("c 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); }
+
+
+int *buffer;
+int length;
+int offset;
+
+int *outbuffer;
+int outoffset;
+
+int getInt() {
+ if (offset>=length) {
+ ssize_t ptr;
+ offset = 0;
+ do {
+ ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE);
+ if (ptr == -1)
+ exit(-1);
+ } while(ptr==0);
+ ssize_t bytestoread=(4-(ptr & 3)) & 3;
+ while(bytestoread != 0) {
+ ssize_t p=read(0, &((char *)buffer)[ptr], bytestoread);
+ if (p == -1)
+ exit(-1);
+ bytestoread -= p;
+ ptr += p;
+ }
+ length = ptr / 4;
+ offset = 0;
+ }
+
+ return buffer[offset++];
+}
+
+void flushInts() {
+ ssize_t bytestowrite=sizeof(int)*outoffset;
+ ssize_t byteswritten=0;
+ do {
+ ssize_t n=write(IS_OUT_FD, &((char *)outbuffer)[byteswritten], bytestowrite);
+ if (n == -1) {
+ fprintf(stderr, "Write failure\n");
+ exit(-1);
+ }
+ bytestowrite -= n;
+ byteswritten += n;
+ } while(bytestowrite != 0);
+ outoffset = 0;
+}
+
+void putInt(int value) {
+ if (outoffset>=IS_BUFFERSIZE) {
+ flushInts();
+ }
+ outbuffer[outoffset++]=value;
+}
+
+void readClauses(Solver *solver) {
+ vec<Lit> clause;
+ int numvars = solver->nVars();
+ bool haveClause = false;
+ while(true) {
+ int lit=getInt();
+ if (lit!=0) {
+ int var = abs(lit) - 1;
+ while (var >= numvars) {
+ numvars++;
+ solver->newVar();
+ }
+ clause.push( (lit>0) ? mkLit(var) : ~mkLit(var));
+ haveClause = true;
+ } else {
+ if (haveClause) {
+ solver->addClause_(clause);
+ haveClause = false;
+ clause.clear();
+ } else {
+ //done with clauses
+ return;
+ }
+ }
+ }
+}
+
+void processCommands(SimpSolver *solver) {
+ while(true) {
+ int command=getInt();
+ switch(command) {
+ case IS_FREEZE: {
+ int var=getInt()-1;
+ solver->setFrozen(var, true);
+ break;
+ }
+ case IS_RUNSOLVER: {
+ vec<Lit> dummy;
+ lbool ret = solver->solveLimited(dummy);
+ if (ret == l_True) {
+ putInt(IS_SAT);
+ putInt(solver->nVars());
+ for(int i=0;i<solver->nVars();i++) {
+ putInt(solver->model[i]==l_True);
+ }
+ } else if (ret == l_False) {
+ putInt(IS_UNSAT);
+ } else {
+ putInt(IS_INDETER);
+ }
+ flushInts();
+ return;
+ }
+ default:
+ fprintf(stderr, "Unreconized command\n");
+ exit(-1);
+ }
+ }
+}
+
+void processSAT(SimpSolver *solver) {
+ buffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
+ offset=0;
+ length=0;
+ outbuffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE);
+ outoffset=0;
+
+ while(true) {
+ double initial_time = cpuTime();
+ readClauses(solver);
+ double parse_time = cpuTime();
+ processCommands(solver);
+ double finish_time = cpuTime();
+ printf("Parse time: %12.2f s Solve time:%12.2f s\n", parse_time-initial_time, finish_time-parse_time);
+ }
+}
+
+
+
+//=================================================================================================
+// Main:
+
+int main(int argc, char** argv) {
+ try {
+ printf("c\nc This is glucose 4.0 -- based on MiniSAT (Many thanks to MiniSAT team)\nc\n");
+
+
+ setUsageHelp("c USAGE: %s [options] <input-file> <result-output-file>\n\n where input may be either in plain or gzipped DIMACS.\n");
+
+
+#if defined(__linux__)
+ fpu_control_t oldcw, newcw;
+ _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
+ //printf("c 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 mod ("MAIN", "model", "show model.", false);
+ IntOption vv ("MAIN", "vv", "Verbosity every vv conflicts", 10000, IntRange(1,INT32_MAX));
+ 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));
+
+ BoolOption opt_certified (_certified, "certified", "Certified UNSAT using DRUP format", false);
+ StringOption opt_certified_file (_certified, "certified-output", "Certified UNSAT output file", "NULL");
+
+ parseOptions(argc, argv, true);
+
+ SimpSolver S;
+ S.parsing = 1;
+ S.verbosity = verb;
+ S.verbEveryConflicts = vv;
+ S.showModel = mod;
+ 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("c 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("c WARNING! Could not set resource limit: Virtual memory.\n");
+ } }
+
+ //do solver stuff here
+ processSAT(&S);
+
+ printf("c | Number of variables: %12d |\n", S.nVars());
+ printf("c | Number of clauses: %12d |\n", S.nClauses());
+
+
+ // 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.parsing = 0;
+
+#ifdef NDEBUG
+ exit(0);
+#else
+ return (0);
+#endif
+ } catch (OutOfMemoryException&){
+ printf("c =========================================================================================================\n");
+ printf("INDETERMINATE\n");
+ exit(0);
+ }
+}
--- /dev/null
+
+#include "solver_interface.h"
+#include <errno.h>
+
+#include <signal.h>
+#include <zlib.h>
+#include <sys/resource.h>
+
+#include "utils/System.h"
+#include "utils/ParseUtils.h"
+#include "utils/Options.h"
+#include "core/Dimacs.h"
+#include "simp/SimpSolver.h"
+
+using namespace Glucose;
+
+
+static const char* _certified = "CORE -- CERTIFIED UNSAT";
+
+void printStats(Solver& solver)
+{
+ double cpu_time = cpuTime();
+ double mem_used = 0;//memUsedPeak();
+ printf("c restarts : %" PRIu64" (%" PRIu64" conflicts in avg)\n", solver.starts,(solver.starts>0 ?solver.conflicts/solver.starts : 0));
+ printf("c blocked restarts : %" PRIu64" (multiple: %" PRIu64") \n", solver.nbstopsrestarts,solver.nbstopsrestartssame);
+ printf("c last block at restart : %" PRIu64"\n",solver.lastblockatrestart);
+ printf("c nb ReduceDB : %" PRIu64"\n", solver.nbReduceDB);
+ printf("c nb removed Clauses : %" PRIu64"\n",solver.nbRemovedClauses);
+ printf("c nb learnts DL2 : %" PRIu64"\n", solver.nbDL2);
+ printf("c nb learnts size 2 : %" PRIu64"\n", solver.nbBin);
+ printf("c nb learnts size 1 : %" PRIu64"\n", solver.nbUn);
+
+ printf("c conflicts : %-12" PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time);
+ printf("c decisions : %-12" PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time);
+ printf("c propagations : %-12" PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
+ printf("c conflict literals : %-12" PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
+ printf("c nb reduced Clauses : %" PRIu64"\n",solver.nbReducedClauses);
+
+ if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
+ printf("c 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); }
+
+
+int *buffer;
+int length;
+int offset;
+
+int getInt() {
+ if (offset>=length) {
+ ssize_t ptr;
+ offset = 0;
+ do {
+ ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE);
+ if (ptr == -1)
+ exit(-1);
+ } while(ptr==0);
+ ssize bytestoread=(4-(ptr & 3)) & 3;
+ while(bytestoread != 0) {
+ ssize_t p=read(0, &((char *)buffer)[ptr], bytestoread);
+ if (p == -1)
+ exit(-1);
+ bytestoread -= p;
+ ptr += p;
+ }
+ length = ptr / 4;
+ offset = 0;
+ }
+
+ return buffer[offset++];
+}
+
+void putInt(int value) {
+}
+
+void readClauses(Solver *solver) {
+ vec<Lit> clause;
+ int numvars = solver->nVars();
+ bool haveClause = false;
+ while(true) {
+ int lit=getInt();
+ if (lit!=0) {
+ int var = abs(lit) - 1;
+ while (var >= numvars) {
+ numvars++;
+ solver->newVar();
+ }
+ clause.push( (lit>0) ? mkLit(var) : ~mkLit(var));
+ haveClause = true;
+ } else {
+ if (haveClause) {
+ solver->addClause_(clause);
+ haveClause = false;
+ clause.clear();
+ } else {
+ //done with clauses
+ return;
+ }
+ }
+ }
+}
+
+void processCommands(Solver *solver) {
+ while(true) {
+ int command=getInt();
+ switch(command) {
+ case IS_FREEZE:
+ int var=getInt();
+ solver->setFrozen(var, true);
+ break;
+ case IS_RUNSOLVER: {
+ vec<Lit> dummy;
+ lbool ret = solver->solveLimited(dummy);
+ if (ret == l_True) {
+ putInt(IS_SAT);
+ putInt(solver->nVars());
+ for(int i=0;i<solver->nVars();i++) {
+ putInt(solver->model[i]==l_True);
+ }
+ } else if (ret == l_False) {
+ putInt(IS_UNSAT);
+ } else {
+ putInt(IS_INDETER);
+ }
+ flushInts();
+ return;
+ }
+ default:
+ fprintf(stderr, "Unreconized command\n");
+ exit(-1);
+ }
+ }
+}
+
+void processSAT(Solver *solver) {
+ buffer=(int *) malloc(sizeof(int)*BUFFERSIZE);
+ offset=0;
+ length=0;
+
+ while(true) {
+ double initial_time = cpuTime();
+ readClauses(solver);
+ double parse_time = cpuTime();
+ processCommands(solver);
+ double finish_time = cpuTime();
+
+ }
+}
+
+
+
+//=================================================================================================
+// Main:
+
+int main(int argc, char** argv) {
+ try {
+ printf("c\nc This is glucose 4.0 -- based on MiniSAT (Many thanks to MiniSAT team)\nc\n");
+
+
+ setUsageHelp("c USAGE: %s [options] <input-file> <result-output-file>\n\n where input may be either in plain or gzipped DIMACS.\n");
+
+
+#if defined(__linux__)
+ fpu_control_t oldcw, newcw;
+ _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
+ //printf("c 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 mod ("MAIN", "model", "show model.", false);
+ IntOption vv ("MAIN", "vv", "Verbosity every vv conflicts", 10000, IntRange(1,INT32_MAX));
+ 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));
+
+ BoolOption opt_certified (_certified, "certified", "Certified UNSAT using DRUP format", false);
+ StringOption opt_certified_file (_certified, "certified-output", "Certified UNSAT output file", "NULL");
+
+ parseOptions(argc, argv, true);
+
+ SimpSolver S;
+ S.parsing = 1;
+ S.verbosity = verb;
+ S.verbEveryConflicts = vv;
+ S.showModel = mod;
+ 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("c 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("c WARNING! Could not set resource limit: Virtual memory.\n");
+ } }
+
+ //do solver stuff here
+ processSAT(&S);
+
+ printf("c | Number of variables: %12d |\n", S.nVars());
+ printf("c | Number of clauses: %12d |\n", S.nClauses());
+
+ double parsed_time = cpuTime();
+ if (S.verbosity > 0){
+ printf("c | Parse time: %12.2f s |\n", parsed_time - initial_time);
+ printf("c | |\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);
+
+ S.parsing = 0;
+
+#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("c =========================================================================================================\n");
+ printf("INDETERMINATE\n");
+ exit(0);
+ }
+}
--- /dev/null
+EXEC = glucose
+DEPDIR = mtl utils core
+MROOT = $(PWD)/..
+CFLAGS = -I ../..
+include $(MROOT)/mtl/template.mk
--- /dev/null
+EXEC = glucose
+DEPDIR = mtl utils core
+MROOT = $(PWD)/..
+
+include $(MROOT)/mtl/template.mk
--- /dev/null
+/***************************************************************************************[SimpSolver.cc]
+ Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon
+ CRIL - Univ. Artois, France
+ LRI - Univ. Paris Sud, France (2009-2013)
+ Labri - Univ. Bordeaux, France
+
+ Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
+ CRIL - Univ. Artois, France
+ Labri - Univ. Bordeaux, France
+
+Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
+Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it
+is based on. (see below).
+
+Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel
+version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software
+without restriction, including the rights to use, copy, modify, merge, publish, distribute,
+sublicence, 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 and below copyrights notices and this permission notice shall be included in all
+copies or substantial portions of the Software;
+- The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot
+be used in any competitive event (sat competitions/evaluations) without the express permission of
+the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event
+using Glucose Parallel as an embedded SAT engine (single core or not).
+
+
+--------------- Original Minisat Copyrights
+
+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 "mtl/Sort.h"
+#include "simp/SimpSolver.h"
+#include "utils/System.h"
+
+using namespace Glucose;
+
+//=================================================================================================
+// Options:
+
+
+static const char* _cat = "SIMP";
+
+static BoolOption opt_use_asymm (_cat, "asymm", "Shrink clauses by asymmetric branching.", false);
+static BoolOption opt_use_rcheck (_cat, "rcheck", "Check if a clause is already implied. (costly)", false);
+static BoolOption opt_use_elim (_cat, "elim", "Perform variable elimination.", true);
+static IntOption opt_grow (_cat, "grow", "Allow a variable elimination step to grow by a number of clauses.", 0);
+static IntOption opt_clause_lim (_cat, "cl-lim", "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20, IntRange(-1, INT32_MAX));
+static IntOption opt_subsumption_lim (_cat, "sub-lim", "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX));
+static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered during simplification.", 0.5, DoubleRange(0, false, HUGE_VAL, false));
+
+
+//=================================================================================================
+// Constructor/Destructor:
+
+
+SimpSolver::SimpSolver() :
+ Solver()
+ , grow (opt_grow)
+ , clause_lim (opt_clause_lim)
+ , subsumption_lim (opt_subsumption_lim)
+ , simp_garbage_frac (opt_simp_garbage_frac)
+ , use_asymm (opt_use_asymm)
+ , use_rcheck (opt_use_rcheck)
+ , use_elim (opt_use_elim)
+ , merges (0)
+ , asymm_lits (0)
+ , eliminated_vars (0)
+ , elimorder (1)
+ , use_simplification (true)
+ , occurs (ClauseDeleted(ca))
+ , elim_heap (ElimLt(n_occ))
+ , bwdsub_assigns (0)
+ , n_touched (0)
+{
+ vec<Lit> dummy(1,lit_Undef);
+ ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
+ bwdsub_tmpunit = ca.alloc(dummy);
+ remove_satisfied = false;
+}
+
+
+SimpSolver::~SimpSolver()
+{
+}
+
+
+
+SimpSolver::SimpSolver(const SimpSolver &s) : Solver(s)
+ , grow (s.grow)
+ , clause_lim (s.clause_lim)
+ , subsumption_lim (s.subsumption_lim)
+ , simp_garbage_frac (s.simp_garbage_frac)
+ , use_asymm (s.use_asymm)
+ , use_rcheck (s.use_rcheck)
+ , use_elim (s.use_elim)
+ , merges (s.merges)
+ , asymm_lits (s.asymm_lits)
+ , eliminated_vars (s.eliminated_vars)
+ , elimorder (s.elimorder)
+ , use_simplification (s.use_simplification)
+ , occurs (ClauseDeleted(ca))
+ , elim_heap (ElimLt(n_occ))
+ , bwdsub_assigns (s.bwdsub_assigns)
+ , n_touched (s.n_touched)
+{
+ // TODO: Copy dummy... what is it???
+ vec<Lit> dummy(1,lit_Undef);
+ ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
+ bwdsub_tmpunit = ca.alloc(dummy);
+ remove_satisfied = false;
+ //End TODO
+
+
+ s.elimclauses.memCopyTo(elimclauses);
+ s.touched.memCopyTo(touched);
+ s.occurs.copyTo(occurs);
+ s.n_occ.memCopyTo(n_occ);
+ s.elim_heap.copyTo(elim_heap);
+ s.subsumption_queue.copyTo(subsumption_queue);
+ s.frozen.memCopyTo(frozen);
+ s.eliminated.memCopyTo(eliminated);
+
+ use_simplification = s.use_simplification;
+ bwdsub_assigns = s.bwdsub_assigns;
+ n_touched = s.n_touched;
+ bwdsub_tmpunit = s.bwdsub_tmpunit;
+ qhead = s.qhead;
+ ok = s.ok;
+}
+
+
+
+Var SimpSolver::newVar(bool sign, bool dvar) {
+ Var v = Solver::newVar(sign, dvar);
+ frozen .push((char)false);
+ eliminated.push((char)false);
+
+ if (use_simplification){
+ n_occ .push(0);
+ n_occ .push(0);
+ occurs .init(v);
+ touched .push(0);
+ elim_heap .insert(v);
+ }
+ return v; }
+
+lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
+{
+ vec<Var> extra_frozen;
+ lbool result = l_True;
+ do_simp &= use_simplification;
+
+ if (do_simp){
+ // Assumptions must be temporarily frozen to run variable elimination:
+ for (int i = 0; i < assumptions.size(); i++){
+ Var v = var(assumptions[i]);
+
+ // If an assumption has been eliminated, remember it.
+ assert(!isEliminated(v));
+
+ if (!frozen[v]){
+ // Freeze and store.
+ setFrozen(v, true);
+ extra_frozen.push(v);
+ } }
+
+ result = lbool(eliminate(turn_off_simp));
+ }
+
+ if (result == l_True)
+ result = Solver::solve_();
+ else if (verbosity >= 1)
+ printf("===============================================================================\n");
+
+ if (result == l_True)
+ extendModel();
+
+ if (do_simp)
+ // Unfreeze the assumptions that were frozen:
+ for (int i = 0; i < extra_frozen.size(); i++)
+ setFrozen(extra_frozen[i], false);
+
+
+ return result;
+}
+
+
+
+bool SimpSolver::addClause_(vec<Lit>& ps)
+{
+#ifndef NDEBUG
+ for (int i = 0; i < ps.size(); i++)
+ assert(!isEliminated(var(ps[i])));
+#endif
+ int nclauses = clauses.size();
+
+ if (use_rcheck && implied(ps))
+ return true;
+
+ if (!Solver::addClause_(ps))
+ return false;
+
+ if(!parsing && certifiedUNSAT) {
+ for (int i = 0; i < ps.size(); i++)
+ fprintf(certifiedOutput, "%i " , (var(ps[i]) + 1) * (-2 * sign(ps[i]) + 1) );
+ fprintf(certifiedOutput, "0\n");
+ }
+
+ if (use_simplification && clauses.size() == nclauses + 1){
+ CRef cr = clauses.last();
+ const Clause& c = ca[cr];
+
+ // NOTE: the clause is added to the queue immediately and then
+ // again during 'gatherTouchedClauses()'. If nothing happens
+ // in between, it will only be checked once. Otherwise, it may
+ // be checked twice unnecessarily. This is an unfortunate
+ // consequence of how backward subsumption is used to mimic
+ // forward subsumption.
+ subsumption_queue.insert(cr);
+ for (int i = 0; i < c.size(); i++){
+ occurs[var(c[i])].push(cr);
+ n_occ[toInt(c[i])]++;
+ touched[var(c[i])] = 1;
+ n_touched++;
+ if (elim_heap.inHeap(var(c[i])))
+ elim_heap.increase(var(c[i]));
+ }
+ }
+
+ return true;
+}
+
+
+
+void SimpSolver::removeClause(CRef cr,bool inPurgatory)
+{
+ const Clause& c = ca[cr];
+
+ if (use_simplification)
+ for (int i = 0; i < c.size(); i++){
+ n_occ[toInt(c[i])]--;
+ updateElimHeap(var(c[i]));
+ occurs.smudge(var(c[i]));
+ }
+
+ Solver::removeClause(cr,inPurgatory);
+}
+
+
+bool SimpSolver::strengthenClause(CRef cr, Lit l)
+{
+ Clause& c = ca[cr];
+ assert(decisionLevel() == 0);
+ assert(use_simplification);
+
+ // FIX: this is too inefficient but would be nice to have (properly implemented)
+ // if (!find(subsumption_queue, &c))
+ subsumption_queue.insert(cr);
+
+ if (certifiedUNSAT) {
+ for (int i = 0; i < c.size(); i++)
+ if (c[i] != l) fprintf(certifiedOutput, "%i " , (var(c[i]) + 1) * (-2 * sign(c[i]) + 1) );
+ fprintf(certifiedOutput, "0\n");
+ }
+
+ if (c.size() == 2){
+ removeClause(cr);
+ c.strengthen(l);
+ }else{
+ if (certifiedUNSAT) {
+ fprintf(certifiedOutput, "d ");
+ for (int i = 0; i < c.size(); i++)
+ fprintf(certifiedOutput, "%i " , (var(c[i]) + 1) * (-2 * sign(c[i]) + 1) );
+ fprintf(certifiedOutput, "0\n");
+ }
+
+ detachClause(cr, true);
+ c.strengthen(l);
+ attachClause(cr);
+ remove(occurs[var(l)], cr);
+ n_occ[toInt(l)]--;
+ updateElimHeap(var(l));
+ }
+
+ return c.size() == 1 ? enqueue(c[0]) && propagate() == CRef_Undef : true;
+}
+
+
+// Returns FALSE if clause is always satisfied ('out_clause' should not be used).
+bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
+{
+ merges++;
+ out_clause.clear();
+
+ bool ps_smallest = _ps.size() < _qs.size();
+ const Clause& ps = ps_smallest ? _qs : _ps;
+ const Clause& qs = ps_smallest ? _ps : _qs;
+
+ for (int i = 0; i < qs.size(); i++){
+ if (var(qs[i]) != v){
+ for (int j = 0; j < ps.size(); j++)
+ if (var(ps[j]) == var(qs[i]))
+ if (ps[j] == ~qs[i])
+ return false;
+ else
+ goto next;
+ out_clause.push(qs[i]);
+ }
+ next:;
+ }
+
+ for (int i = 0; i < ps.size(); i++)
+ if (var(ps[i]) != v)
+ out_clause.push(ps[i]);
+
+ return true;
+}
+
+
+// Returns FALSE if clause is always satisfied.
+bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
+{
+ merges++;
+
+ bool ps_smallest = _ps.size() < _qs.size();
+ const Clause& ps = ps_smallest ? _qs : _ps;
+ const Clause& qs = ps_smallest ? _ps : _qs;
+ const Lit* __ps = (const Lit*)ps;
+ const Lit* __qs = (const Lit*)qs;
+
+ size = ps.size()-1;
+
+ for (int i = 0; i < qs.size(); i++){
+ if (var(__qs[i]) != v){
+ for (int j = 0; j < ps.size(); j++)
+ if (var(__ps[j]) == var(__qs[i]))
+ if (__ps[j] == ~__qs[i])
+ return false;
+ else
+ goto next;
+ size++;
+ }
+ next:;
+ }
+
+ return true;
+}
+
+
+void SimpSolver::gatherTouchedClauses()
+{
+ if (n_touched == 0) return;
+
+ int i,j;
+ for (i = j = 0; i < subsumption_queue.size(); i++)
+ if (ca[subsumption_queue[i]].mark() == 0)
+ ca[subsumption_queue[i]].mark(2);
+
+ for (i = 0; i < touched.size(); i++)
+ if (touched[i]){
+ const vec<CRef>& cs = occurs.lookup(i);
+ for (j = 0; j < cs.size(); j++)
+ if (ca[cs[j]].mark() == 0){
+ subsumption_queue.insert(cs[j]);
+ ca[cs[j]].mark(2);
+ }
+ touched[i] = 0;
+ }
+
+ for (i = 0; i < subsumption_queue.size(); i++)
+ if (ca[subsumption_queue[i]].mark() == 2)
+ ca[subsumption_queue[i]].mark(0);
+
+ n_touched = 0;
+}
+
+
+bool SimpSolver::implied(const vec<Lit>& c)
+{
+ assert(decisionLevel() == 0);
+
+ trail_lim.push(trail.size());
+ for (int i = 0; i < c.size(); i++)
+ if (value(c[i]) == l_True){
+ cancelUntil(0);
+ return false;
+ }else if (value(c[i]) != l_False){
+ assert(value(c[i]) == l_Undef);
+ uncheckedEnqueue(~c[i]);
+ }
+
+ bool result = propagate() != CRef_Undef;
+ cancelUntil(0);
+ return result;
+}
+
+
+// Backward subsumption + backward subsumption resolution
+bool SimpSolver::backwardSubsumptionCheck(bool verbose)
+{
+ int cnt = 0;
+ int subsumed = 0;
+ int deleted_literals = 0;
+ assert(decisionLevel() == 0);
+
+ while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
+
+ // Empty subsumption queue and return immediately on user-interrupt:
+ if (asynch_interrupt){
+ subsumption_queue.clear();
+ bwdsub_assigns = trail.size();
+ break; }
+
+ // Check top-level assignments by creating a dummy clause and placing it in the queue:
+ if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
+ Lit l = trail[bwdsub_assigns++];
+ ca[bwdsub_tmpunit][0] = l;
+ ca[bwdsub_tmpunit].calcAbstraction();
+ subsumption_queue.insert(bwdsub_tmpunit); }
+
+ CRef cr = subsumption_queue.peek(); subsumption_queue.pop();
+ Clause& c = ca[cr];
+
+ if (c.mark()) continue;
+
+ if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
+ printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
+
+ assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated before this point.
+
+ // Find best variable to scan:
+ Var best = var(c[0]);
+ for (int i = 1; i < c.size(); i++)
+ if (occurs[var(c[i])].size() < occurs[best].size())
+ best = var(c[i]);
+
+ // Search all candidates:
+ vec<CRef>& _cs = occurs.lookup(best);
+ CRef* cs = (CRef*)_cs;
+
+ for (int j = 0; j < _cs.size(); j++)
+ if (c.mark())
+ break;
+ else if (!ca[cs[j]].mark() && cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){
+ Lit l = c.subsumes(ca[cs[j]]);
+
+ if (l == lit_Undef)
+ subsumed++, removeClause(cs[j]);
+ else if (l != lit_Error){
+ deleted_literals++;
+
+ if (!strengthenClause(cs[j], ~l))
+ return false;
+
+ // Did current candidate get deleted from cs? Then check candidate at index j again:
+ if (var(l) == best)
+ j--;
+ }
+ }
+ }
+
+ return true;
+}
+
+
+bool SimpSolver::asymm(Var v, CRef cr)
+{
+ Clause& c = ca[cr];
+ assert(decisionLevel() == 0);
+
+ if (c.mark() || satisfied(c)) return true;
+
+ trail_lim.push(trail.size());
+ Lit l = lit_Undef;
+ for (int i = 0; i < c.size(); i++)
+ if (var(c[i]) != v && value(c[i]) != l_False)
+ uncheckedEnqueue(~c[i]);
+ else
+ l = c[i];
+
+ if (propagate() != CRef_Undef){
+ cancelUntil(0);
+ asymm_lits++;
+ if (!strengthenClause(cr, l))
+ return false;
+ }else
+ cancelUntil(0);
+
+ return true;
+}
+
+
+bool SimpSolver::asymmVar(Var v)
+{
+ assert(use_simplification);
+
+ const vec<CRef>& cls = occurs.lookup(v);
+
+ if (value(v) != l_Undef || cls.size() == 0)
+ return true;
+
+ for (int i = 0; i < cls.size(); i++)
+ if (!asymm(v, cls[i]))
+ return false;
+
+ return backwardSubsumptionCheck();
+}
+
+
+static void mkElimClause(vec<uint32_t>& elimclauses, Lit x)
+{
+ elimclauses.push(toInt(x));
+ elimclauses.push(1);
+}
+
+
+static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)
+{
+ int first = elimclauses.size();
+ int v_pos = -1;
+
+ // Copy clause to elimclauses-vector. Remember position where the
+ // variable 'v' occurs:
+ for (int i = 0; i < c.size(); i++){
+ elimclauses.push(toInt(c[i]));
+ if (var(c[i]) == v)
+ v_pos = i + first;
+ }
+ assert(v_pos != -1);
+
+ // Swap the first literal with the 'v' literal, so that the literal
+ // containing 'v' will occur first in the clause:
+ uint32_t tmp = elimclauses[v_pos];
+ elimclauses[v_pos] = elimclauses[first];
+ elimclauses[first] = tmp;
+
+ // Store the length of the clause last:
+ elimclauses.push(c.size());
+}
+
+
+
+bool SimpSolver::eliminateVar(Var v)
+{
+ assert(!frozen[v]);
+ assert(!isEliminated(v));
+ assert(value(v) == l_Undef);
+
+ // Split the occurrences into positive and negative:
+ //
+ const vec<CRef>& cls = occurs.lookup(v);
+ vec<CRef> pos, neg;
+ for (int i = 0; i < cls.size(); i++)
+ (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
+
+ // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
+ // clause must exceed the limit on the maximal clause size (if it is set):
+ //
+ int cnt = 0;
+ int clause_size = 0;
+
+ for (int i = 0; i < pos.size(); i++)
+ for (int j = 0; j < neg.size(); j++)
+ if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) &&
+ (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
+ return true;
+
+ // Delete and store old clauses:
+ eliminated[v] = true;
+ setDecisionVar(v, false);
+ eliminated_vars++;
+
+ if (pos.size() > neg.size()){
+ for (int i = 0; i < neg.size(); i++)
+ mkElimClause(elimclauses, v, ca[neg[i]]);
+ mkElimClause(elimclauses, mkLit(v));
+ }else{
+ for (int i = 0; i < pos.size(); i++)
+ mkElimClause(elimclauses, v, ca[pos[i]]);
+ mkElimClause(elimclauses, ~mkLit(v));
+ }
+
+
+ // Produce clauses in cross product:
+ vec<Lit>& resolvent = add_tmp;
+ for (int i = 0; i < pos.size(); i++)
+ for (int j = 0; j < neg.size(); j++)
+ if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent))
+ return false;
+
+ for (int i = 0; i < cls.size(); i++)
+ removeClause(cls[i]);
+
+ // Free occurs list for this variable:
+ occurs[v].clear(true);
+
+ // Free watchers lists for this variable, if possible:
+ if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
+ if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
+
+ return backwardSubsumptionCheck();
+}
+
+
+bool SimpSolver::substitute(Var v, Lit x)
+{
+ assert(!frozen[v]);
+ assert(!isEliminated(v));
+ assert(value(v) == l_Undef);
+
+ if (!ok) return false;
+
+ eliminated[v] = true;
+ setDecisionVar(v, false);
+ const vec<CRef>& cls = occurs.lookup(v);
+
+ vec<Lit>& subst_clause = add_tmp;
+ for (int i = 0; i < cls.size(); i++){
+ Clause& c = ca[cls[i]];
+
+ subst_clause.clear();
+ for (int j = 0; j < c.size(); j++){
+ Lit p = c[j];
+ subst_clause.push(var(p) == v ? x ^ sign(p) : p);
+ }
+
+
+ if (!addClause_(subst_clause))
+ return ok = false;
+
+ removeClause(cls[i]);
+
+ }
+
+ return true;
+}
+
+
+void SimpSolver::extendModel()
+{
+ int i, j;
+ Lit x;
+
+ if(model.size()==0) model.growTo(nVars());
+
+ for (i = elimclauses.size()-1; i > 0; i -= j){
+ for (j = elimclauses[i--]; j > 1; j--, i--)
+ if (modelValue(toLit(elimclauses[i])) != l_False)
+ goto next;
+
+ x = toLit(elimclauses[i]);
+ model[var(x)] = lbool(!sign(x));
+ next:;
+ }
+}
+
+
+bool SimpSolver::eliminate(bool turn_off_elim)
+{
+ if (!simplify()) {
+ ok = false;
+ return false;
+ }
+ else if (!use_simplification)
+ return true;
+
+ // Main simplification loop:
+ //
+
+ int toPerform = clauses.size()<=4800000;
+
+ if(!toPerform) {
+ printf("c Too many clauses... No preprocessing\n");
+ }
+
+ while (toPerform && (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0)){
+
+ gatherTouchedClauses();
+ // printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
+ if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) &&
+ !backwardSubsumptionCheck(true)){
+ ok = false; goto cleanup; }
+
+ // Empty elim_heap and return immediately on user-interrupt:
+ if (asynch_interrupt){
+ assert(bwdsub_assigns == trail.size());
+ assert(subsumption_queue.size() == 0);
+ assert(n_touched == 0);
+ elim_heap.clear();
+ goto cleanup; }
+
+ // printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
+ for (int cnt = 0; !elim_heap.empty(); cnt++){
+ Var elim = elim_heap.removeMin();
+
+ if (asynch_interrupt) break;
+
+ if (isEliminated(elim) || value(elim) != l_Undef) continue;
+
+ if (verbosity >= 2 && cnt % 100 == 0)
+ printf("elimination left: %10d\r", elim_heap.size());
+
+ if (use_asymm){
+ // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
+ bool was_frozen = frozen[elim];
+ frozen[elim] = true;
+ if (!asymmVar(elim)){
+ ok = false; goto cleanup; }
+ frozen[elim] = was_frozen; }
+
+ // At this point, the variable may have been set by assymetric branching, so check it
+ // again. Also, don't eliminate frozen variables:
+ if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){
+ ok = false; goto cleanup; }
+
+ checkGarbage(simp_garbage_frac);
+ }
+
+ assert(subsumption_queue.size() == 0);
+ }
+ cleanup:
+
+ // If no more simplification is needed, free all simplification-related data structures:
+ if (turn_off_elim){
+ touched .clear(true);
+ occurs .clear(true);
+ n_occ .clear(true);
+ elim_heap.clear(true);
+ subsumption_queue.clear(true);
+
+ use_simplification = false;
+ remove_satisfied = true;
+ ca.extra_clause_field = false;
+
+ // Force full cleanup (this is safe and desirable since it only happens once):
+ rebuildOrderHeap();
+ garbageCollect();
+ }else{
+ // Cheaper cleanup:
+ cleanUpClauses(); // TODO: can we make 'cleanUpClauses()' not be linear in the problem size somehow?
+ checkGarbage();
+ }
+
+ if (verbosity >= 0 && elimclauses.size() > 0)
+ printf("c | Eliminated clauses: %10.2f Mb |\n",
+ double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
+
+
+ return ok;
+
+
+}
+
+
+void SimpSolver::cleanUpClauses()
+{
+ occurs.cleanAll();
+ int i,j;
+ for (i = j = 0; i < clauses.size(); i++)
+ if (ca[clauses[i]].mark() == 0)
+ clauses[j++] = clauses[i];
+ clauses.shrink(i - j);
+}
+
+
+//=================================================================================================
+// Garbage Collection methods:
+
+
+void SimpSolver::relocAll(ClauseAllocator& to)
+{
+ if (!use_simplification) return;
+
+ // All occurs lists:
+ //
+ for (int i = 0; i < nVars(); i++){
+ vec<CRef>& cs = occurs[i];
+ for (int j = 0; j < cs.size(); j++)
+ ca.reloc(cs[j], to);
+ }
+
+ // Subsumption queue:
+ //
+ for (int i = 0; i < subsumption_queue.size(); i++)
+ ca.reloc(subsumption_queue[i], to);
+
+ // Temporary clause:
+ //
+ ca.reloc(bwdsub_tmpunit, to);
+}
+
+
+void SimpSolver::garbageCollect()
+{
+ // Initialize the next region to a size corresponding to the estimated utilization degree. This
+ // is not precise but should avoid some unnecessary reallocations for the new region:
+ ClauseAllocator to(ca.size() - ca.wasted());
+
+ cleanUpClauses();
+ to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
+ relocAll(to);
+ Solver::relocAll(to);
+ if (verbosity >= 2)
+ printf("| Garbage collection: %12d bytes => %12d bytes |\n",
+ ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
+ to.moveTo(ca);
+}
--- /dev/null
+/***************************************************************************************[SimpSolver.h]
+ Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon
+ CRIL - Univ. Artois, France
+ LRI - Univ. Paris Sud, France (2009-2013)
+ Labri - Univ. Bordeaux, France
+
+ Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
+ CRIL - Univ. Artois, France
+ Labri - Univ. Bordeaux, France
+
+Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
+Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it
+is based on. (see below).
+
+Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel
+version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software
+without restriction, including the rights to use, copy, modify, merge, publish, distribute,
+sublicence, 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 and below copyrights notices and this permission notice shall be included in all
+copies or substantial portions of the Software;
+- The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot
+be used in any competitive event (sat competitions/evaluations) without the express permission of
+the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event
+using Glucose Parallel as an embedded SAT engine (single core or not).
+
+
+--------------- Original Minisat Copyrights
+
+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.
+ **************************************************************************************************/
+
+#ifndef Glucose_SimpSolver_h
+#define Glucose_SimpSolver_h
+
+#include "mtl/Queue.h"
+#include "core/Solver.h"
+#include "mtl/Clone.h"
+
+namespace Glucose {
+
+//=================================================================================================
+
+
+class SimpSolver : public Solver {
+ public:
+ // Constructor/Destructor:
+ //
+ SimpSolver();
+ ~SimpSolver();
+
+ SimpSolver(const SimpSolver &s);
+
+
+ /**
+ * Clone function
+ */
+ virtual Clone* clone() const {
+ return new SimpSolver(*this);
+ }
+
+
+ // Problem specification:
+ //
+ virtual Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
+ bool addClause (const vec<Lit>& ps);
+ bool addEmptyClause(); // Add the empty clause to the solver.
+ bool addClause (Lit p); // Add a unit clause to the solver.
+ bool addClause (Lit p, Lit q); // Add a binary clause to the solver.
+ bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver.
+ virtual bool addClause_( vec<Lit>& ps);
+ bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction).
+
+ // Variable mode:
+ //
+ void setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.
+ bool isEliminated(Var v) const;
+
+ // Solving:
+ //
+ bool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
+ lbool solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
+ bool solve ( bool do_simp = true, bool turn_off_simp = false);
+ bool solve (Lit p , bool do_simp = true, bool turn_off_simp = false);
+ bool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false);
+ bool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
+ bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification.
+
+ // Memory managment:
+ //
+ virtual void garbageCollect();
+
+
+ // Generate a (possibly simplified) DIMACS file:
+ //
+#if 0
+ void toDimacs (const char* file, const vec<Lit>& assumps);
+ void toDimacs (const char* file);
+ void toDimacs (const char* file, Lit p);
+ void toDimacs (const char* file, Lit p, Lit q);
+ void toDimacs (const char* file, Lit p, Lit q, Lit r);
+#endif
+
+ // Mode of operation:
+ //
+ int parsing;
+ int grow; // Allow a variable elimination step to grow by a number of clauses (default to zero).
+ int clause_lim; // Variables are not eliminated if it produces a resolvent with a length above this limit.
+ // -1 means no limit.
+ int subsumption_lim; // Do not check if subsumption against a clause larger than this. -1 means no limit.
+ double simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac').
+
+ bool use_asymm; // Shrink clauses by asymmetric branching.
+ bool use_rcheck; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
+ bool use_elim; // Perform variable elimination.
+ // Statistics:
+ //
+ int merges;
+ int asymm_lits;
+ int eliminated_vars;
+
+ protected:
+
+ // Helper structures:
+ //
+ struct ElimLt {
+ const vec<int>& n_occ;
+ explicit ElimLt(const vec<int>& no) : n_occ(no) {}
+
+ // TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating
+ // 32-bit implementation instead then, but this will have to do for now.
+ uint64_t cost (Var x) const { return (uint64_t)n_occ[toInt(mkLit(x))] * (uint64_t)n_occ[toInt(~mkLit(x))]; }
+ bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
+
+ // TODO: investigate this order alternative more.
+ // bool operator()(Var x, Var y) const {
+ // int c_x = cost(x);
+ // int c_y = cost(y);
+ // return c_x < c_y || c_x == c_y && x < y; }
+ };
+
+ struct ClauseDeleted {
+ const ClauseAllocator& ca;
+ explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
+ bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } };
+
+ // Solver state:
+ //
+ int elimorder;
+ bool use_simplification;
+ vec<uint32_t> elimclauses;
+ vec<char> touched;
+ OccLists<Var, vec<CRef>, ClauseDeleted>
+ occurs;
+ vec<int> n_occ;
+ Heap<ElimLt> elim_heap;
+ Queue<CRef> subsumption_queue;
+ vec<char> frozen;
+ vec<char> eliminated;
+ int bwdsub_assigns;
+ int n_touched;
+
+ // Temporaries:
+ //
+ CRef bwdsub_tmpunit;
+
+ // Main internal methods:
+ //
+ virtual lbool solve_ (bool do_simp = true, bool turn_off_simp = false);
+ bool asymm (Var v, CRef cr);
+ bool asymmVar (Var v);
+ void updateElimHeap (Var v);
+ void gatherTouchedClauses ();
+ bool merge (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
+ bool merge (const Clause& _ps, const Clause& _qs, Var v, int& size);
+ bool backwardSubsumptionCheck (bool verbose = false);
+ bool eliminateVar (Var v);
+ void extendModel ();
+
+ void removeClause (CRef cr,bool inPurgatory=false);
+ bool strengthenClause (CRef cr, Lit l);
+ void cleanUpClauses ();
+ bool implied (const vec<Lit>& c);
+ virtual void relocAll (ClauseAllocator& to);
+};
+
+
+//=================================================================================================
+// Implementation of inline methods:
+
+
+inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; }
+inline void SimpSolver::updateElimHeap(Var v) {
+ assert(use_simplification);
+ // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
+ if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
+ elim_heap.update(v); }
+
+
+inline bool SimpSolver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); }
+inline bool SimpSolver::addEmptyClause() { add_tmp.clear(); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
+inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
+
+inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
+ budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; }
+
+inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
+ assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
+
+//=================================================================================================
+}
+
+#endif
--- /dev/null
+/Users/briandemsky/research/model/sat/glucose-syrup/incremental/Main.o /Users/briandemsky/research/model/sat/glucose-syrup/incremental/Main.or /Users/briandemsky/research/model/sat/glucose-syrup/incremental/Main.od /Users/briandemsky/research/model/sat/glucose-syrup/incremental/Main.op: \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/Main.cc \
+ ../../solver_interface.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../utils/System.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/IntTypes.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../utils/ParseUtils.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../utils/Options.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Vec.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/XAlloc.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/Dimacs.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/SolverTypes.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Alg.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Map.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Alloc.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../simp/SimpSolver.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Queue.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/Solver.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Heap.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/BoundedQueue.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/Constants.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Clone.h
+/Users/briandemsky/research/model/sat/glucose-syrup/incremental/SimpSolver.o /Users/briandemsky/research/model/sat/glucose-syrup/incremental/SimpSolver.or /Users/briandemsky/research/model/sat/glucose-syrup/incremental/SimpSolver.od /Users/briandemsky/research/model/sat/glucose-syrup/incremental/SimpSolver.op: \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/SimpSolver.cc \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Sort.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Vec.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/IntTypes.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/XAlloc.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../simp/SimpSolver.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Queue.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/Solver.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Heap.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Alg.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../utils/Options.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../utils/ParseUtils.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/SolverTypes.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Map.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Alloc.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/BoundedQueue.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/Constants.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Clone.h \
+ /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../utils/System.h
projects / satlib.git / commitdiff