diff options
Diffstat (limited to 'src/prop/cryptominisat/Solver/Main.cpp')
-rw-r--r-- | src/prop/cryptominisat/Solver/Main.cpp | 974 |
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; +} |