summaryrefslogtreecommitdiff
path: root/src/prop/cryptominisat/Solver/Main.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/cryptominisat/Solver/Main.cpp')
-rw-r--r--src/prop/cryptominisat/Solver/Main.cpp974
1 files changed, 974 insertions, 0 deletions
diff --git a/src/prop/cryptominisat/Solver/Main.cpp b/src/prop/cryptominisat/Solver/Main.cpp
new file mode 100644
index 000000000..111683ee8
--- /dev/null
+++ b/src/prop/cryptominisat/Solver/Main.cpp
@@ -0,0 +1,974 @@
+/*****************************************************************************
+MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+CryptoMiniSat -- Copyright (c) 2009 Mate Soos
+
+Original code by MiniSat authors are under an MIT licence.
+Modifications for CryptoMiniSat are under GPLv3 licence.
+******************************************************************************/
+
+/**
+@mainpage CryptoMiniSat
+@author Mate Soos, and collaborators
+
+CryptoMiniSat is an award-winning SAT solver based on MiniSat. It brings a
+number of benefits relative to MiniSat, among them XOR clauses, extensive
+failed literal probing, and better random search.
+
+The solver basically performs the following steps:
+
+1) parse CNF file into clause database
+
+2) run Conflict-Driven Clause-Learning DPLL on the clauses
+
+3) regularly run simplification passes on the clause-set
+
+4) display solution and if not used as a library, exit
+
+Here is a picture of of the above process in more detail:
+
+\image html "main_flowgraph.png"
+
+*/
+
+#include <ctime>
+#include <cstring>
+#include <errno.h>
+#include <string.h>
+#include <sstream>
+#include <iostream>
+#include <iomanip>
+#include <omp.h>
+#include <map>
+#include <set>
+#include "constants.h"
+
+#include <signal.h>
+
+#include "time_mem.h"
+#include "constants.h"
+#include "DimacsParser.h"
+
+#if defined(__linux__)
+#include <fpu_control.h>
+#endif
+
+#include "Main.h"
+
+using namespace CMSat;
+
+Main::Main(int _argc, char** _argv) :
+ numThreads(1)
+ , grouping(false)
+ , debugLib (false)
+ , debugNewVar (false)
+ , printResult (true)
+ , max_nr_of_solutions (1)
+ , fileNamePresent (false)
+ , twoFileNamesPresent (false)
+ , argc(_argc)
+ , argv(_argv)
+{
+}
+
+std::map<uint32_t, Solver*> solversToInterrupt;
+std::set<uint32_t> finished;
+
+void Main::readInAFile(const std::string& filename, Solver& solver)
+{
+ #pragma omp single
+ if (solver.conf.verbosity >= 1) {
+ std::cout << "c Reading file '" << filename << "'" << std::endl;
+ }
+ #ifdef DISABLE_ZLIB
+ FILE * in = fopen(filename.c_str(), "rb");
+ #else
+ gzFile in = gzopen(filename.c_str(), "rb");
+ #endif // DISABLE_ZLIB
+
+ #pragma omp single
+ if (in == NULL) {
+ std::cout << "ERROR! Could not open file '" << filename << "' for reading" << std::endl;
+ exit(1);
+ }
+
+ DimacsParser parser(&solver, debugLib, debugNewVar, grouping);
+ parser.parse_DIMACS(in);
+
+ #ifdef DISABLE_ZLIB
+ fclose(in);
+ #else
+ gzclose(in);
+ #endif // DISABLE_ZLIB
+}
+
+void Main::readInStandardInput(Solver& solver)
+{
+ if (solver.conf.verbosity >= 1) {
+ std::cout << "c Reading from standard input... Use '-h' or '--help' for help." << std::endl;
+ }
+ #ifdef DISABLE_ZLIB
+ FILE * in = stdin;
+ #else
+ gzFile in = gzdopen(fileno(stdin), "rb");
+ #endif // DISABLE_ZLIB
+
+ if (in == NULL) {
+ std::cout << "ERROR! Could not open standard input for reading" << std::endl;
+ exit(1);
+ }
+
+ DimacsParser parser(&solver, debugLib, debugNewVar, grouping);
+ parser.parse_DIMACS(in);
+
+ #ifndef DISABLE_ZLIB
+ gzclose(in);
+ #endif // DISABLE_ZLIB
+}
+
+
+
+void Main::parseInAllFiles(Solver& solver)
+{
+ double myTime = cpuTime();
+
+ //First read normal extra files
+ if ((debugLib || debugNewVar) && filesToRead.size() > 0) {
+ std::cout << "debugNewVar and debugLib must both be OFF to parse in extra files" << std::endl;
+ exit(-1);
+ }
+ for (uint32_t i = 0; i < filesToRead.size(); i++) {
+ readInAFile(filesToRead[i].c_str(), solver);
+ }
+
+ //Then read the main file or standard input
+ if (!fileNamePresent) {
+ readInStandardInput(solver);
+ } else {
+ string filename = argv[(twoFileNamesPresent ? argc-2 : argc-1)];
+ readInAFile(filename, solver);
+ }
+
+ if (solver.conf.verbosity >= 1) {
+ std::cout << "c Parsing time: "
+ << std::fixed << std::setw(5) << std::setprecision(2) << (cpuTime() - myTime)
+ << " s" << std::endl;
+ }
+}
+
+
+void Main::printUsage(char** argv)
+{
+#ifdef DISABLE_ZLIB
+ printf("USAGE: %s [options] <input-file> <result-output-file>\n\n where input is plain DIMACS.\n\n", argv[0]);
+#else
+ printf("USAGE: %s [options] <input-file> <result-output-file>\n\n where input may be either in plain or gzipped DIMACS.\n\n", argv[0]);
+#endif // DISABLE_ZLIB
+ printf("OPTIONS:\n\n");
+ printf(" --polarity-mode = {true,false,rnd,auto} [default: auto]. Selects the default\n");
+ printf(" polarity mode. Auto is the Jeroslow&Wang method\n");
+ //printf(" -decay = <num> [ 0 - 1 ]\n");
+ printf(" --rnd-freq = <num> [ 0 - 1 ]\n");
+ printf(" --verbosity = {0,1,2}\n");
+ printf(" --randomize = <seed> [0 - 2^32-1] Sets random seed, used for picking\n");
+ printf(" decision variables (default = 0)\n");
+ printf(" --restrict = <num> [1 - varnum] when picking random variables to branch\n");
+ printf(" on, pick one that in the 'num' most active vars useful\n");
+ printf(" for cryptographic problems, where the question is the key,\n");
+ printf(" which is usually small (e.g. 80 bits)\n");
+ printf(" --gaussuntil = <num> Depth until which Gaussian elimination is active.\n");
+ printf(" Giving 0 switches off Gaussian elimination\n");
+ printf(" --restarts = <num> [1 - 2^32-1] No more than the given number of\n");
+ printf(" restarts will be performed during search\n");
+ printf(" --nonormxorfind Don't find and collect >2-long xor-clauses from\n");
+ printf(" regular clauses\n");
+ printf(" --nobinxorfind Don't find and collect 2-long xor-clauses from\n");
+ printf(" regular clauses\n");
+ printf(" --noregbxorfind Don't regularly find and collect 2-long xor-clauses\n");
+ printf(" from regular clauses\n");
+ printf(" --doextendedscc Do strongly conn. comp. finding using non-exist. bins\n");
+ printf(" --noconglomerate Don't conglomerate 2 xor clauses when one var is dependent\n");
+ printf(" --nosimplify Don't do regular simplification rounds\n");
+ printf(" --greedyunbound Greedily unbound variables that are not needed for SAT\n");
+ printf(" --debuglib Solve at specific 'c Solver::solve()' points in the CNF\n");
+ printf(" file. Used to debug file generated by Solver's\n");
+ printf(" needLibraryCNFFile() function\n");
+ printf(" --debugnewvar Add new vars at specific 'c Solver::newVar()' points in \n");
+ printf(" the CNF file. Used to debug file generated by Solver's\n");
+ printf(" needLibraryCNFFile() function.\n");
+ printf(" --novarreplace Don't perform variable replacement. Needed for programmable\n");
+ printf(" solver feature\n");
+ printf(" --restart = {auto, static, dynamic} Which kind of restart strategy to\n");
+ printf(" follow. Default is auto\n");
+ printf(" --dumplearnts = <filename> If interrupted or reached restart limit, dump\n");
+ printf(" the learnt clauses to the specified file. Maximum size of\n");
+ printf(" dumped clauses can be specified with next option.\n");
+ printf(" --maxdumplearnts = [0 - 2^32-1] When dumping the learnts to file, what\n");
+ printf(" should be maximum length of the clause dumped. Useful\n");
+ printf(" to make the resulting file smaller. Default is 2^32-1\n");
+ printf(" note: 2-long XOR-s are always dumped.\n");
+ printf(" --dumporig = <filename> If interrupted or reached restart limit, dump\n");
+ printf(" the original problem instance, simplified to the\n");
+ printf(" current point.\n");
+ printf(" --alsoread = <filename> Also read this file in\n");
+ printf(" Can be used to re-read dumped learnts, for example\n");
+ printf(" --maxsolutions Search for given amount of solutions\n");
+ printf(" Can only be used in single-threaded more (\"--threads=1\")\n");
+ printf(" --pavgbranch Print average branch depth\n");
+ printf(" --nofailedlit Don't search for failed literals, and don't search for lits\n");
+ printf(" propagated both by 'varX' and '-varX'\n");
+ printf(" --noheuleprocess Don't try to minimise XORs by XOR-ing them together.\n");
+ printf(" Algo. as per global/local substitution in Heule's thesis\n");
+ printf(" --nosatelite Don't do clause subsumption, clause strengthening and\n");
+ printf(" variable elimination (implies -novarelim and -nosubsume1).\n");
+ printf(" --noxorsubs Don't try to subsume xor-clauses.\n");
+ printf(" --nosolprint Don't print the satisfying assignment if the solution\n");
+ printf(" is SAT\n");
+ printf(" --novarelim Don't perform variable elimination as per Een and Biere\n");
+ printf(" --nosubsume1 Don't perform clause contraction through resolution\n");
+#ifdef USE_GAUSS
+ printf(" --nomatrixfind Don't find distinct matrixes. Put all xors into one\n");
+ printf(" big matrix\n");
+ printf(" --noordercol Don't order variables in the columns of Gaussian\n");
+ printf(" elimination. Effectively disables iterative reduction\n");
+ printf(" of the matrix\n");
+ printf(" --noiterreduce Don't reduce iteratively the matrix that is updated\n");
+ printf(" --maxmatrixrows [0 - 2^32-1] Set maximum no. of rows for gaussian matrix.\n");
+ printf(" Too large matrixes should bee discarded for\n");
+ printf(" reasons of efficiency. Default: %d\n", gaussconfig.maxMatrixRows);
+ printf(" --minmatrixrows = [0 - 2^32-1] Set minimum no. of rows for gaussian matrix.\n");
+ printf(" Normally, too small matrixes are discarded for\n");
+ printf(" reasons of efficiency. Default: %d\n", gaussconfig.minMatrixRows);
+ printf(" --savematrix = [0 - 2^32-1] Save matrix every Nth decision level.\n");
+ printf(" Default: %d\n", gaussconfig.only_nth_gauss_save);
+ printf(" --maxnummatrixes = [0 - 2^32-1] Maximum number of matrixes to treat.\n");
+ printf(" Default: %d\n", gaussconfig.maxNumMatrixes);
+#endif //USE_GAUSS
+ //printf(" --addoldlearnts = Readd old learnts for failed variable searching.\n");
+ //printf(" These learnts are usually deleted, but may help\n");
+ printf(" --nohyperbinres Don't add binary clauses when doing failed lit probing.\n");
+ printf(" --noremovebins Don't remove useless binary clauses\n");
+ printf(" --noremlbins Don't remove useless learnt binary clauses\n");
+ printf(" --nosubswithbins Don't subsume with binary clauses\n");
+ printf(" --nosubswithnbins Don't subsume with non-existent binary clauses\n");
+ printf(" --noclausevivif Don't do perform clause vivification\n");
+ printf(" --nosortwatched Don't sort watches according to size: bin, tri, etc.\n");
+ printf(" --nolfminim Don't do on-the-fly self-subsuming resolution\n");
+ printf(" (called 'strong minimisation' in PrecoSat)\n");
+ printf(" --nocalcreach Don't calculate reachability and interfere with\n");
+ printf(" variable decisions accordingly\n");
+ printf(" --nobxor Don't find equivalent lits during failed lit search\n");
+ printf(" --norecotfssr Don't perform recursive/transitive OTF self-\n");
+ printf(" subsuming resolution\n");
+ printf(" --nocacheotfssr Don't cache 1-level equeue. Less memory used, but\n");
+ printf(" disables trans OTFSSR, adv. clause vivifier, etc.\n");
+ printf(" --nootfsubsume Don't do on-the-fly subsumption after conf. gen.\n");
+ #ifdef ENABLE_UNWIND_GLUE
+ printf(" --maxgluedel Automatically delete clauses over max glue. See '--maxglue'\n");
+ printf(" --maxglue = [0 - 2^%d-1] default: %d. Glue value above which we\n", MAX_GLUE_BITS, conf.maxGlue);
+ #endif //ENABLE_UNWIND_GLUE
+ printf(" throw the clause away on backtrack.\n");
+ printf(" --threads = Num threads (default is 1)\n");
+ printf(" --plain Get rid of all simplification algorithms\n");
+ printf(" --maxconfl = [0..2^63-1] Maximum number of conflicts to do\n");
+ printf("\n");
+}
+
+
+const char* Main::hasPrefix(const char* str, const char* prefix)
+{
+ int len = strlen(prefix);
+ if (strncmp(str, prefix, len) == 0)
+ return str + len;
+ else
+ return NULL;
+}
+
+void Main::printResultFunc(const Solver& S, const lbool ret, FILE* res)
+{
+ if (res != NULL) {
+ if (ret == l_True) {
+ std::cout << "c SAT" << std::endl;
+ fprintf(res, "SAT\n");
+ if (printResult) {
+ for (Var var = 0; var != S.nVars(); var++)
+ if (S.model[var] != l_Undef)
+ fprintf(res, "%s%d ", (S.model[var] == l_True)? "" : "-", var+1);
+ fprintf(res, "0\n");
+ }
+ } else if (ret == l_False) {
+ std::cout << "c UNSAT" << std::endl;
+ fprintf(res, "UNSAT\n");
+ } else {
+ std::cout << "c INCONCLUSIVE" << std::endl;
+ fprintf(res, "INCONCLUSIVE\n");
+ }
+ fclose(res);
+ } else {
+ if (ret == l_True) {
+ if (!printResult) std::cout << "c SATISFIABLE" << std::endl;
+ else std::cout << "s SATISFIABLE" << std::endl;
+ } else if (ret == l_False) {
+ if (!printResult) std::cout << "c UNSATISFIABLE" << std::endl;
+ else std::cout << "s UNSATISFIABLE" << std::endl;
+ }
+
+ if(ret == l_True && printResult) {
+ std::stringstream toPrint;
+ toPrint << "v ";
+ for (Var var = 0; var != S.nVars(); var++)
+ if (S.model[var] != l_Undef)
+ toPrint << ((S.model[var] == l_True)? "" : "-") << var+1 << " ";
+ toPrint << "0" << std::endl;
+ std::cout << toPrint.str();
+ }
+ }
+}
+
+void Main::parseCommandLine()
+{
+ const char* value;
+ char tmpFilename[201];
+ tmpFilename[0] = '\0';
+ uint32_t unparsedOptions = 0;
+ bool needTwoFileNames = false;
+ conf.verbosity = 2;
+
+ for (int i = 0; i < argc; i++) {
+ if ((value = hasPrefix(argv[i], "--polarity-mode="))) {
+ if (strcmp(value, "true") == 0)
+ conf.polarity_mode = polarity_true;
+ else if (strcmp(value, "false") == 0)
+ conf.polarity_mode = polarity_false;
+ else if (strcmp(value, "rnd") == 0)
+ conf.polarity_mode = polarity_rnd;
+ else if (strcmp(value, "auto") == 0)
+ conf.polarity_mode = polarity_auto;
+ else {
+ printf("ERROR! unknown polarity-mode %s\n", value);
+ exit(0);
+ }
+
+ } else if ((value = hasPrefix(argv[i], "--rnd-freq="))) {
+ double rnd;
+ if (sscanf(value, "%lf", &rnd) <= 0 || rnd < 0 || rnd > 1) {
+ printf("ERROR! illegal rnRSE ERROR!d-freq constant %s\n", value);
+ exit(0);
+ }
+ conf.random_var_freq = rnd;
+
+ /*} else if ((value = hasPrefix(argv[i], "--decay="))) {
+ double decay;
+ if (sscanf(value, "%lf", &decay) <= 0 || decay <= 0 || decay > 1) {
+ printf("ERROR! illegal decay constant %s\n", value);
+ exit(0);
+ }
+ conf.var_decay = 1 / decay;*/
+
+ } else if ((value = hasPrefix(argv[i], "--verbosity="))) {
+ int verbosity = (int)strtol(value, NULL, 10);
+ if (verbosity == EINVAL || verbosity == ERANGE) {
+ printf("ERROR! illegal verbosity level %s\n", value);
+ exit(0);
+ }
+ conf.verbosity = verbosity;
+ } else if ((value = hasPrefix(argv[i], "--randomize="))) {
+ int seed;
+ if (sscanf(value, "%d", &seed) < 0) {
+ printf("ERROR! illegal seed %s\n", value);
+ exit(0);
+ }
+ conf.origSeed = seed;
+ } else if ((value = hasPrefix(argv[i], "--restrict="))) {
+ int branchTo;
+ if (sscanf(value, "%d", &branchTo) < 0 || branchTo < 1) {
+ printf("ERROR! illegal restricted pick branch number %d\n", branchTo);
+ exit(0);
+ }
+ conf.restrictPickBranch = branchTo;
+ } else if ((value = hasPrefix(argv[i], "--gaussuntil="))) {
+ int until;
+ if (sscanf(value, "%d", &until) < 0) {
+ printf("ERROR! until %s\n", value);
+ exit(0);
+ }
+ gaussconfig.decision_until = until;
+ } else if ((value = hasPrefix(argv[i], "--restarts="))) {
+ int maxrest;
+ if (sscanf(value, "%d", &maxrest) < 0 || maxrest == 0) {
+ printf("ERROR! illegal maximum restart number %d\n", maxrest);
+ exit(0);
+ }
+ conf.maxRestarts = maxrest;
+ } else if ((value = hasPrefix(argv[i], "--dumplearnts="))) {
+ if (sscanf(value, "%200s", tmpFilename) < 0 || strlen(tmpFilename) == 0) {
+ printf("ERROR! wrong filename '%s'\n", tmpFilename);
+ exit(0);
+ }
+ conf.learntsFilename.assign(tmpFilename);
+ conf.needToDumpLearnts = true;
+ } else if ((value = hasPrefix(argv[i], "--dumporig="))) {
+ if (sscanf(value, "%200s", tmpFilename) < 0 || strlen(tmpFilename) == 0) {
+ printf("ERROR! wrong filename '%s'\n", tmpFilename);
+ exit(0);
+ }
+ conf.origFilename.assign(tmpFilename);
+ conf.needToDumpOrig = true;
+ } else if ((value = hasPrefix(argv[i], "--alsoread="))) {
+ if (sscanf(value, "%400s", tmpFilename) < 0 || strlen(tmpFilename) == 0) {
+ printf("ERROR! wrong filename '%s'\n", tmpFilename);
+ exit(0);
+ }
+ filesToRead.push_back(tmpFilename);
+ } else if ((value = hasPrefix(argv[i], "--maxdumplearnts="))) {
+ if (!conf.needToDumpLearnts) {
+ printf("ERROR! -dumplearnts=<filename> must be first activated before issuing -maxdumplearnts=<size>\n");
+ exit(0);
+ }
+ int tmp;
+ if (sscanf(value, "%d", &tmp) < 0 || tmp < 0) {
+ std::cout << "ERROR! wrong maximum dumped learnt clause size is illegal: " << tmp << std::endl;
+ exit(0);
+ }
+ conf.maxDumpLearntsSize = (uint32_t)tmp;
+ } else if ((value = hasPrefix(argv[i], "--maxsolutions="))) {
+ int tmp;
+ if (sscanf(value, "%d", &tmp) < 0 || tmp < 0) {
+ std::cout << "ERROR! wrong maximum number of solutions is illegal: " << tmp << std::endl;
+ exit(0);
+ }
+ max_nr_of_solutions = (uint32_t)tmp;
+
+ } else if ((value = hasPrefix(argv[i], "--pavgbranch"))) {
+ conf.doPrintAvgBranch = true;
+ } else if ((value = hasPrefix(argv[i], "--greedyunbound"))) {
+ conf.greedyUnbound = true;
+ } else if ((value = hasPrefix(argv[i], "--nonormxorfind"))) {
+ conf.doFindXors = false;
+ } else if ((value = hasPrefix(argv[i], "--nobinxorfind"))) {
+ conf.doFindEqLits = false;
+ } else if ((value = hasPrefix(argv[i], "--noregbxorfind"))) {
+ conf.doRegFindEqLits = false;
+ } else if ((value = hasPrefix(argv[i], "--doextendedscc"))) {
+ conf.doExtendedSCC = true;
+ } else if ((value = hasPrefix(argv[i], "--noconglomerate"))) {
+ conf.doConglXors = false;
+ } else if ((value = hasPrefix(argv[i], "--nosimplify"))) {
+ conf.doSchedSimp = false;
+ } else if ((value = hasPrefix(argv[i], "--debuglib"))) {
+ debugLib = true;
+ } else if ((value = hasPrefix(argv[i], "--debugnewvar"))) {
+ debugNewVar = true;
+ } else if ((value = hasPrefix(argv[i], "--novarreplace"))) {
+ conf.doReplace = false;
+ } else if ((value = hasPrefix(argv[i], "--nofailedlit"))) {
+ conf.doFailedLit = false;
+ } else if ((value = hasPrefix(argv[i], "--nodisablegauss"))) {
+ gaussconfig.dontDisable = true;
+ } else if ((value = hasPrefix(argv[i], "--maxnummatrixes="))) {
+ int maxNumMatrixes;
+ if (sscanf(value, "%d", &maxNumMatrixes) < 0) {
+ printf("ERROR! maxnummatrixes: %s\n", value);
+ exit(0);
+ }
+ gaussconfig.maxNumMatrixes = maxNumMatrixes;
+ } else if ((value = hasPrefix(argv[i], "--noheuleprocess"))) {
+ conf.doHeuleProcess = false;
+ } else if ((value = hasPrefix(argv[i], "--nosatelite"))) {
+ conf.doSatELite = false;
+ } else if ((value = hasPrefix(argv[i], "--noxorsubs"))) {
+ conf.doXorSubsumption = false;
+ } else if ((value = hasPrefix(argv[i], "--nohyperbinres"))) {
+ conf.doHyperBinRes = false;
+ } else if ((value = hasPrefix(argv[i], "--novarelim"))) {
+ conf.doVarElim = false;
+ } else if ((value = hasPrefix(argv[i], "--nosubsume1"))) {
+ conf.doSubsume1 = false;
+ } else if ((value = hasPrefix(argv[i], "--nomatrixfind"))) {
+ gaussconfig.noMatrixFind = true;
+ } else if ((value = hasPrefix(argv[i], "--noiterreduce"))) {
+ gaussconfig.iterativeReduce = false;
+ } else if ((value = hasPrefix(argv[i], "--noordercol"))) {
+ gaussconfig.orderCols = false;
+ } else if ((value = hasPrefix(argv[i], "--maxmatrixrows="))) {
+ int rows;
+ if (sscanf(value, "%d", &rows) < 0 || rows < 0) {
+ printf("ERROR! maxmatrixrows: %s\n", value);
+ exit(0);
+ }
+ gaussconfig.maxMatrixRows = (uint32_t)rows;
+ } else if ((value = hasPrefix(argv[i], "--minmatrixrows="))) {
+ int rows;
+ if (sscanf(value, "%d", &rows) < 0 || rows < 0) {
+ printf("ERROR! minmatrixrows: %s\n", value);
+ exit(0);
+ }
+ gaussconfig.minMatrixRows = rows;
+ } else if ((value = hasPrefix(argv[i], "--savematrix"))) {
+ int every;
+ if (sscanf(value, "%d", &every) < 0) {
+ printf("ERROR! savematrix: %s\n", value);
+ exit(0);
+ }
+ gaussconfig.only_nth_gauss_save = every;
+ } else if (strcmp(argv[i], "-h") == 0 || strcmp(argv[i], "-help") == 0 || strcmp(argv[i], "--help") == 0) {
+ printUsage(argv);
+ exit(0);
+ } else if ((value = hasPrefix(argv[i], "--restart="))) {
+ if (strcmp(value, "auto") == 0)
+ conf.fixRestartType = auto_restart;
+ else if (strcmp(value, "static") == 0)
+ conf.fixRestartType = static_restart;
+ else if (strcmp(value, "dynamic") == 0)
+ conf.fixRestartType = dynamic_restart;
+ else {
+ printf("ERROR! unknown restart type %s\n", value);
+ exit(0);
+ }
+ } else if ((value = hasPrefix(argv[i], "--nosolprint"))) {
+ printResult = false;
+ //} else if ((value = hasPrefix(argv[i], "--addoldlearnts"))) {
+ // conf.readdOldLearnts = true;
+ } else if ((value = hasPrefix(argv[i], "--nohyperbinres"))) {
+ conf.doHyperBinRes= false;
+ } else if ((value = hasPrefix(argv[i], "--noremovebins"))) {
+ conf.doRemUselessBins = false;
+ } else if ((value = hasPrefix(argv[i], "--nosubswithnbins"))) {
+ conf.doSubsWNonExistBins = false;
+ } else if ((value = hasPrefix(argv[i], "--nosubswithbins"))) {
+ conf.doSubsWBins = false;
+ } else if ((value = hasPrefix(argv[i], "--noclausevivif"))) {
+ conf.doClausVivif = false;
+ } else if ((value = hasPrefix(argv[i], "--nosortwatched"))) {
+ conf.doSortWatched = false;
+ } else if ((value = hasPrefix(argv[i], "--nolfminim"))) {
+ conf.doMinimLearntMore = false;
+ } else if ((value = hasPrefix(argv[i], "--nocalcreach"))) {
+ conf.doCalcReach = false;
+ } else if ((value = hasPrefix(argv[i], "--norecotfssr"))) {
+ conf.doMinimLMoreRecur = false;
+ } else if ((value = hasPrefix(argv[i], "--nocacheotfssr"))) {
+ conf.doCacheOTFSSRSet = false;
+ conf.doCacheOTFSSR = false;
+ } else if ((value = hasPrefix(argv[i], "--nootfsubsume"))) {
+ conf.doOTFSubsume = false;
+ } else if ((value = hasPrefix(argv[i], "--noremlbins"))) {
+ conf.doRemUselessLBins = false;
+ } else if ((value = hasPrefix(argv[i], "--maxconfl="))) {
+ int maxconfl = 0;
+ if (sscanf(value, "%d", &maxconfl) < 0 || maxconfl < 2) {
+ printf("ERROR! max confl: %s\n", value);
+ exit(0);
+ }
+ conf.maxConfl = maxconfl;
+ } else if ((value = hasPrefix(argv[i], "--plain"))) {
+ conf.isPlain = true;
+ conf.doOTFSubsume = false;
+ conf.doFindXors = false;
+ conf.doFindEqLits = false;
+ conf.doRegFindEqLits = false;
+ conf.doExtendedSCC = false;
+ conf.doConglXors = false;
+ conf.doSchedSimp = false;
+ conf.doReplace = false;
+ conf.doFailedLit = false;
+ conf.doHeuleProcess = false;
+ conf.doSatELite = false;
+ conf.doXorSubsumption = false;
+ printResult = false;
+ conf.doVarElim = false;
+ //nomatrixfind
+ gaussconfig.orderCols = false;
+ gaussconfig.iterativeReduce = false;
+ conf.doHyperBinRes = false;
+ conf.doRemUselessBins = false;
+ conf.doRemUselessLBins = false;
+ conf.doSubsWBins = false;
+ conf.doSubsWNonExistBins = false;
+ conf.doClausVivif = false;
+ conf.doCalcReach = false;
+ conf.doBXor = false;
+ conf.doMinimLMoreRecur = false;
+ conf.doMinimLearntMore = false;
+ conf.doCacheOTFSSR = false;
+ } else if ((value = hasPrefix(argv[i], "--nobxor"))) {
+ conf.doBXor = false;
+ #ifdef ENABLE_UNWIND_GLUE
+ } else if ((value = hasPrefix(argv[i], "--maxglue="))) {
+ int glue = 0;
+ if (sscanf(value, "%d", &glue) < 0 || glue < 2) {
+ printf("ERROR! maxGlue: %s\n", value);
+ exit(0);
+ }
+ if (glue >= (1<< MAX_GLUE_BITS)-1) {
+ std::cout << "Due to memory-packing limitations, max glue cannot be more than "
+ << ((1<< MAX_GLUE_BITS)-2) << std::endl;
+ exit(-1);
+ }
+ conf.maxGlue = (uint32_t)glue;
+ } else if ((value = hasPrefix(argv[i], "--maxgluedel"))) {
+ conf.doMaxGlueDel = true;
+ #endif //ENABLE_UNWIND_GLUE
+ } else if ((value = hasPrefix(argv[i], "--threads="))) {
+ numThreads = 0;
+ if (sscanf(value, "%d", &numThreads) < 0 || numThreads < 1) {
+ printf("ERROR! numThreads: %s\n", value);
+ exit(0);
+ }
+ } else if (strncmp(argv[i], "-", 1) == 0 || strncmp(argv[i], "--", 2) == 0) {
+ printf("ERROR! unknown flag %s\n", argv[i]);
+ exit(0);
+ } else {
+ //std::std::cout << "argc:" << argc << " i:" << i << ", value:" << argv[i] << std::endl;
+ unparsedOptions++;
+ if (unparsedOptions == 2) {
+ if (!(argc <= i+2)) {
+ std::cout << "You must give the input file as either:" << std::endl;
+ std::cout << " -- last option if you want the output to the console" << std::endl;
+ std::cout << " -- or one before the last option" << std::endl;
+ std::cout << "It appears that you did neither. Maybe you forgot the '--' from an option?" << std::endl;
+ exit(-1);
+ }
+ fileNamePresent = true;
+ if (argc == i+2) needTwoFileNames = true;
+ }
+ if (unparsedOptions == 3) {
+ if (!(argc <= i+1)) {
+ std::cout << "You must give the output file as the last option. Exiting" << std::endl;
+ exit(-1);
+ }
+ twoFileNamesPresent = true;
+ }
+ if (unparsedOptions == 4) {
+ std::cout << "You gave more than two filenames as parameters." << std::endl;
+ std::cout << "The first one is interpreted as the input, the second is the output." << std::endl;
+ std::cout << "However, the third one I cannot do anything with. EXITING" << std::endl;
+ exit(-1);
+ }
+ }
+ }
+ if (conf.verbosity >= 1) {
+ if (twoFileNamesPresent) {
+ std::cout << "c Outputting solution to file: " << argv[argc-1] << std::endl;
+ } else {
+ std::cout << "c Outputting solution to console" << std::endl;
+ }
+ }
+
+ if (unparsedOptions == 2 && needTwoFileNames == true) {
+ std::cout << "Command line wrong. You probably frogot to add "<< std::endl
+ << "the '--' in front of one of the options, or you started" << std::endl
+ << "your output file with a hyphen ('-'). Exiting." << std::endl;
+ exit(-1);
+ }
+ if (!debugLib) conf.libraryUsage = false;
+}
+
+FILE* Main::openOutputFile()
+{
+ FILE* res = NULL;
+ if (twoFileNamesPresent) {
+ char* filename = argv[argc-1];
+ res = fopen(filename, "wb");
+ if (res == NULL) {
+ int backup_errno = errno;
+ printf("Cannot open %s for writing. Problem: %s", filename, strerror(backup_errno));
+ exit(1);
+ }
+ }
+
+ return res;
+}
+
+void Main::setDoublePrecision(const uint32_t verbosity)
+{
+#if defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE)
+ fpu_control_t oldcw, newcw;
+ _FPU_GETCW(oldcw);
+ newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE;
+ _FPU_SETCW(newcw);
+ #pragma omp single
+ if (verbosity >= 1) {
+ printf("c WARNING: for repeatability, setting FPU to use double precision\n");
+ }
+#endif
+}
+
+void Main::printVersionInfo(const uint32_t verbosity)
+{
+#pragma omp single
+ if (verbosity >= 1) {
+ printf("c This is CryptoMiniSat %s\n", VERSION);
+ #ifdef __GNUC__
+ printf("c compiled with gcc version %s\n", __VERSION__);
+ #else
+ printf("c compiled with non-gcc compiler\n");
+ #endif
+ }
+}
+
+int Main::singleThreadSolve()
+{
+ Solver solver(conf, gaussconfig);
+ solversToInterrupt[0] = &solver;
+
+ printVersionInfo(conf.verbosity);
+ setDoublePrecision(conf.verbosity);
+
+ parseInAllFiles(solver);
+ FILE* res = openOutputFile();
+
+ unsigned long current_nr_of_solutions = 0;
+ lbool ret = l_True;
+ while(current_nr_of_solutions < max_nr_of_solutions && ret == l_True) {
+ ret = solver.solve();
+ current_nr_of_solutions++;
+
+ if (ret == l_True && current_nr_of_solutions < max_nr_of_solutions) {
+ if (conf.verbosity >= 1) std::cout << "c Prepare for next run..." << std::endl;
+ printResultFunc(solver, ret, res);
+
+ vec<Lit> lits;
+ for (Var var = 0; var != solver.nVars(); var++) {
+ if (solver.model[var] != l_Undef) {
+ lits.push( Lit(var, (solver.model[var] == l_True)? true : false) );
+ }
+ }
+ solver.addClause(lits);
+ }
+ }
+
+ if (conf.needToDumpLearnts) {
+ if (solver.dumpSortedLearnts(conf.learntsFilename, conf.maxDumpLearntsSize))
+ std::cout << "c Sorted learnt clauses dumped to file '" << conf.learntsFilename << "'" << std::endl;
+ else {
+ std::cout << "Error: Cannot open file '" << conf.learntsFilename << "' to write learnt clauses!" << std::endl;;
+ exit(-1);
+ }
+ }
+ if (conf.needToDumpOrig) {
+ if (ret == l_False && conf.origFilename == "stdout") {
+ std::cout << "p cnf 0 1" << std::endl;
+ std::cout << "0";
+ } else if (ret == l_True && conf.origFilename == "stdout") {
+ std::cout << "p cnf " << solver.model.size() << " " << solver.model.size() << std::endl;
+ for (uint32_t i = 0; i < solver.model.size(); i++) {
+ std::cout << (solver.model[i] == l_True ? "" : "-") << i+1 << " 0" << std::endl;
+ }
+ } else {
+ if (!solver.dumpOrigClauses(conf.origFilename)) {
+ std::cout << "Error: Cannot open file '" << conf.origFilename << "' to write learnt clauses!" << std::endl;
+ exit(-1);
+ }
+ if (conf.verbosity >= 1)
+ std::cout << "c Simplified original clauses dumped to file '"
+ << conf.origFilename << "'" << std::endl;
+ }
+ }
+ if (ret == l_Undef && conf.verbosity >= 1) {
+ std::cout << "c Not finished running -- signal caught or maximum restart reached" << std::endl;
+ }
+ if (conf.verbosity >= 1) solver.printStats();
+
+ printResultFunc(solver, ret, res);
+
+ return correctReturnValue(ret);
+}
+
+int Main::correctReturnValue(const lbool ret) const
+{
+ int retval = -1;
+ if (ret == l_True) retval = 10;
+ else if (ret == l_False) retval = 20;
+ else if (ret == l_Undef) retval = 15;
+ else {
+ std::cerr << "Something is very wrong, output is neither l_Undef, nor l_False, nor l_True" << std::endl;
+ exit(-1);
+ }
+
+ #ifdef NDEBUG
+ // (faster than "return", which will invoke the destructor for 'Solver')
+ exit(retval);
+ #endif
+ return retval;
+}
+
+int Main::oneThreadSolve()
+{
+ int numThreads = omp_get_num_threads();
+ SolverConf myConf = conf;
+ int num = omp_get_thread_num();
+ myConf.origSeed = num;
+ if (num > 0) {
+ if (num % 4 == 3) myConf.fixRestartType = dynamic_restart;
+ if (num % 4 == 2) myConf.doCalcReach = false;
+ //else myConf.fixRestartType = static_restart;
+ myConf.simpBurstSConf *= 1 + num;
+ myConf.simpStartMult *= 1.0 + 0.2*(double)num;
+ myConf.simpStartMMult *= 1.0 + 0.2*(double)num;
+ if (num == numThreads-1) {
+ //myConf.doVarElim = false;
+ myConf.doPerformPreSimp = false;
+ myConf.polarity_mode = polarity_false;
+ }
+ }
+ if (num != 0) myConf.verbosity = 0;
+
+ Solver solver(myConf, gaussconfig, &sharedData);
+ #pragma omp critical (solversToInterr)
+ {
+ solversToInterrupt[num] = &solver;
+ //std::cout << "Solver num " << num << " is to be interrupted " << std::endl;
+ }
+
+ printVersionInfo(myConf.verbosity);
+ setDoublePrecision(myConf.verbosity);
+
+ parseInAllFiles(solver);
+ lbool ret = solver.solve();
+ #pragma omp critical (finished)
+ {
+ finished.insert(num);
+ }
+
+ int retval = 0;
+ #pragma omp single
+ {
+ int numNeededInterrupt = 0;
+ while(numNeededInterrupt != numThreads-1) {
+ #pragma omp critical (solversToInterr)
+ {
+ for(int i = 0; i < numThreads; i++) {
+ if (i != num
+ && solversToInterrupt.find(i) != solversToInterrupt.end()
+ && solversToInterrupt[i]->needToInterrupt == false
+ ) {
+ solversToInterrupt[i]->needToInterrupt = true;
+ numNeededInterrupt++;
+ }
+ }
+ }
+ }
+ bool mustWait = true;
+ while (mustWait) {
+ #pragma omp critical (finished)
+ if (finished.size() == (unsigned)numThreads) mustWait = false;
+ }
+ if (conf.needToDumpLearnts) {
+ if (!solver.dumpSortedLearnts(conf.learntsFilename, conf.maxDumpLearntsSize)) {
+ std::cout << "Error: Cannot open file '" << conf.learntsFilename << "' to write learnt clauses!" << std::endl;;
+ exit(-1);
+ }
+ if (conf.verbosity >= 1) {
+ std::cout << "c Sorted learnt clauses dumped to file '"
+ << conf.learntsFilename << "'" << std::endl;
+ }
+ }
+ if (conf.needToDumpOrig) {
+ if (!solver.dumpOrigClauses(conf.origFilename)) {
+ std::cout << "Error: Cannot open file '" << conf.origFilename << "' to write learnt clauses!" << std::endl;
+ exit(-1);
+ }
+ if (conf.verbosity >= 1)
+ std::cout << "c Simplified original clauses dumped to file '"
+ << conf.origFilename << "'" << std::endl;
+ }
+
+ FILE* res = openOutputFile();
+ if (conf.verbosity >= 1) solver.printStats();
+ printResultFunc(solver, ret, res);
+
+ retval = correctReturnValue(ret);
+ exit(retval);
+ }
+ return retval;
+}
+
+int Main::multiThreadSolve()
+{
+ bool exitHere = false;
+ if (max_nr_of_solutions > 1) {
+ std::cerr << "ERROR: When multi-threading, only one solution can be found" << std::endl;
+ exitHere = true;
+ }
+ if (debugLib) {
+ std::cerr << "ERROR: When multi-threading, --debuglib cannot be used" << std::endl;
+ exitHere = true;
+ }
+ if (exitHere) {
+ std::cerr << "libarary in this version of CryptoMS is not multi-threaded :(" << std::endl;
+ std::cerr << "Please set option '--threads=1' on the command line." << std::endl;
+ exit(-1);
+ }
+
+ int finalRetVal;
+ if (numThreads != -1) {
+ assert(numThreads > 0);
+ omp_set_num_threads(numThreads);
+ }
+ #pragma omp parallel
+ {
+ #pragma omp single
+ {
+ if (conf.verbosity >= 1)
+ std::cout << "c Using " << omp_get_num_threads()
+ << " threads" << std::endl;
+ }
+ int retval = oneThreadSolve();
+
+ #pragma omp single
+ finalRetVal = retval;
+ }
+
+ return finalRetVal;
+}
+
+/**
+@brief For correctly and gracefully exiting
+
+It can happen that the user requests a dump of the learnt clauses. In this case,
+the program must wait until it gets to a state where the learnt clauses are in
+a correct state, then dump these and quit normally. This interrupt hander
+is used to achieve this
+*/
+void SIGINT_handler(int)
+{
+ #pragma omp critical
+ {
+ Solver& solver = *solversToInterrupt.begin()->second;
+ printf("\n");
+ std::cerr << "*** INTERRUPTED ***" << std::endl;
+ if (solver.conf.needToDumpLearnts || solver.conf.needToDumpOrig) {
+ solver.needToInterrupt = true;
+ std::cerr << "*** Please wait. We need to interrupt cleanly" << std::endl;
+ std::cerr << "*** This means we might need to finish some calculations" << std::endl;
+ } else {
+ if (solver.conf.verbosity >= 1) solver.printStats();
+ exit(1);
+ }
+ }
+}
+
+int main(int argc, char** argv)
+{
+ Main main(argc, argv);
+ main.parseCommandLine();
+ signal(SIGINT, SIGINT_handler);
+ //signal(SIGHUP,SIGINT_handler);
+
+ try {
+ if (main.numThreads == 1)
+ return main.singleThreadSolve();
+ else
+ return main.multiThreadSolve();
+ } catch (std::bad_alloc) {
+ std::cerr << "Memory manager cannot handle the load. Sorry. Exiting." << std::endl;
+ exit(-1);
+ } catch (std::out_of_range oor) {
+ std::cerr << oor.what() << std::endl;
+ exit(-1);
+ } catch (CMSat::DimacsParseError dpe) {
+ std::cerr << "PARSE ERROR!" << dpe.what() << std::endl;
+ exit(3);
+ }
+ return 0;
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback