From 79d1fc95de8ff4b79b1460fd050656075f90ff34 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Jan 23 2012 16:18:37 +0000 Subject: New upstream version. Man page is now upstream. All patches have been applied upstream. Tests have been removed from the source distribution. --- diff --git a/.gitignore b/.gitignore index 1006ba7..fc103b7 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1 @@ -/cryptominisat-2.9.1.tar.gz +/cryptominisat-2.9.2.tar.gz diff --git a/cryptominisat-exit.patch b/cryptominisat-exit.patch deleted file mode 100644 index 3446992..0000000 --- a/cryptominisat-exit.patch +++ /dev/null @@ -1,556 +0,0 @@ ---- ./Solver/DimacsParser.h.orig 2011-05-25 05:44:48.000000000 -0600 -+++ ./Solver/DimacsParser.h 2011-12-07 10:40:07.775736369 -0700 -@@ -9,6 +9,7 @@ Modifications for CryptoMiniSat are unde - #ifndef DIMACSPARSER_H - #define DIMACSPARSER_H - -+#include - #include - #include "SolverTypes.h" - #include "constants.h" -@@ -29,6 +30,13 @@ namespace CMSat { - - class Solver; - -+class DimacsParseError : public std::runtime_error -+{ -+ public: -+ explicit DimacsParseError(const std::string& arg); -+ virtual ~DimacsParseError() throw(); -+}; -+ - /** - @brief Parses up a DIMACS file that my be zipped - */ -@@ -45,16 +53,16 @@ class DimacsParser - void skipWhitespace(StreamBuffer& in); - void skipLine(StreamBuffer& in); - std::string untilEnd(StreamBuffer& in); -- int32_t parseInt(StreamBuffer& in, uint32_t& len); -- float parseFloat(StreamBuffer& in); -+ int32_t parseInt(StreamBuffer& in, uint32_t& len) throw (DimacsParseError); -+ float parseFloat(StreamBuffer& in) throw (DimacsParseError); - void parseString(StreamBuffer& in, std::string& str); -- void readClause(StreamBuffer& in, vec& lits); -+ void readClause(StreamBuffer& in, vec& lits) throw (DimacsParseError); - void parseClauseParameters(StreamBuffer& in, bool& learnt, uint32_t& glue, float& miniSatAct); -- void readFullClause(StreamBuffer& in); -+ void readFullClause(StreamBuffer& in) throw (DimacsParseError); - void readBranchingOrder(StreamBuffer& in); - bool match(StreamBuffer& in, const char* str); -- void printHeader(StreamBuffer& in); -- void parseComments(StreamBuffer& in, const std::string str); -+ void printHeader(StreamBuffer& in) throw (DimacsParseError); -+ void parseComments(StreamBuffer& in, const std::string str) throw (DimacsParseError); - std::string stringify(uint32_t x); - - ---- ./Solver/Main.cpp.orig 2011-05-25 05:58:41.000000000 -0600 -+++ ./Solver/Main.cpp 2011-12-07 10:40:07.776736368 -0700 -@@ -698,8 +698,12 @@ const int Main::singleThreadSolve() - } - - if (conf.needToDumpLearnts) { -- solver.dumpSortedLearnts(conf.learntsFilename, conf.maxDumpLearntsSize); -- std::cout << "c Sorted learnt clauses dumped to file '" << conf.learntsFilename << "'" << std::endl; -+ 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") { -@@ -711,7 +715,10 @@ const int Main::singleThreadSolve() - std::cout << (solver.model[i] == l_True ? "" : "-") << i+1 << " 0" << std::endl; - } - } else { -- solver.dumpOrigClauses(conf.origFilename); -+ 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; -@@ -807,14 +814,20 @@ const int Main::oneThreadSolve() - if (finished.size() == (unsigned)numThreads) mustWait = false; - } - if (conf.needToDumpLearnts) { -- solver.dumpSortedLearnts(conf.learntsFilename, conf.maxDumpLearntsSize); -+ 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) { -- solver.dumpOrigClauses(conf.origFilename); -+ 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; -@@ -902,8 +915,20 @@ int main(int argc, char** argv) - signal(SIGINT, SIGINT_handler); - //signal(SIGHUP,SIGINT_handler); - -- if (main.numThreads == 1) -- return main.singleThreadSolve(); -- else -- return main.multiThreadSolve(); -+ 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; - } ---- ./Solver/SolverMisc.cpp.orig 2011-05-25 06:00:50.000000000 -0600 -+++ ./Solver/SolverMisc.cpp 2011-12-07 10:40:07.777736367 -0700 -@@ -40,13 +40,11 @@ using namespace CMSat; - - static const int space = 10; - --void Solver::dumpSortedLearnts(const std::string& fileName, const uint32_t maxSize) -+bool Solver::dumpSortedLearnts(const std::string& fileName, const uint32_t maxSize) - { - FILE* outfile = fopen(fileName.c_str(), "w"); -- if (!outfile) { -- std::cout << "Error: Cannot open file '" << fileName << "' to write learnt clauses!" << std::endl;; -- exit(-1); -- } -+ if (!outfile) -+ return false; - - fprintf(outfile, "c \nc ---------\n"); - fprintf(outfile, "c unitaries\n"); -@@ -93,6 +91,7 @@ void Solver::dumpSortedLearnts(const std - end: - - fclose(outfile); -+ return true; - } - - void Solver::printStrangeBinLit(const Lit lit) const -@@ -179,15 +178,13 @@ void Solver::printBinClause(const Lit li - } - } - --void Solver::dumpOrigClauses(const std::string& fileName) const -+bool Solver::dumpOrigClauses(const std::string& fileName) const - { - FILE* outfile; - if (fileName != std::string("stdout")) { - outfile = fopen(fileName.c_str(), "w"); -- if (!outfile) { -- std::cout << "Error: Cannot open file '" << fileName << "' to write learnt clauses!" << std::endl; -- exit(-1); -- } -+ if (!outfile) -+ return false; - } else { - outfile = stdout; - } -@@ -306,6 +303,7 @@ void Solver::dumpOrigClauses(const std:: - } - - if (fileName != "stdout") fclose(outfile); -+ return true; - } - - const vector Solver::get_unitary_learnts() const -@@ -595,14 +593,10 @@ newVar() and addClause(), addXorClause() - file and then can be re-read with special arguments to the main program. This - can help simulate a segfaulting library-call - */ --void Solver::needLibraryCNFFile(const std::string& fileName) -+bool Solver::needLibraryCNFFile(const std::string& fileName) - { - libraryCNFFile = fopen(fileName.c_str(), "w"); -- if (libraryCNFFile == NULL) { -- std::cout << "Couldn't open library-call dump file " -- << libraryCNFFile << std::endl; -- exit(-1); -- } -+ return libraryCNFFile != NULL; - } - - template ---- ./Solver/Solver.cpp.orig 2011-05-25 06:00:50.000000000 -0600 -+++ ./Solver/Solver.cpp 2011-12-07 10:40:07.778736366 -0700 -@@ -150,13 +150,11 @@ classes used inside Solver - @p dvar The new variable should be used as a decision variable? - NOTE: this has effects on the meaning of a SATISFIABLE result - */ --Var Solver::newVar(bool dvar) -+Var Solver::newVar(bool dvar) throw (std::out_of_range) - { - Var v = nVars(); -- if (v >= 1<<30) { -- std::cout << "ERROR! Variable requested is far too large" << std::endl; -- exit(-1); -- } -+ if (v >= 1<<30) -+ throw std::out_of_range("ERROR! Variable requested is far too large"); - - watches .push(); // (list for positive literal) - watches .push(); // (list for negative literal) -@@ -206,15 +204,13 @@ xor clause-adding function addXorClause( - inside are decision variables, have not been replaced, eliminated, etc. - */ - template --XorClause* Solver::addXorClauseInt(T& ps, bool xorEqualFalse, const uint32_t group, const bool learnt) -+XorClause* Solver::addXorClauseInt(T& ps, bool xorEqualFalse, const uint32_t group, const bool learnt) throw (std::out_of_range) - { - assert(qhead == trail.size()); - assert(decisionLevel() == 0); - -- if (ps.size() > (0x01UL << 18)) { -- std::cout << "Too long clause!" << std::endl; -- exit(-1); -- } -+ if (ps.size() > (0x01UL << 18)) -+ throw std::out_of_range("Too long clause!"); - std::sort(ps.getData(), ps.getDataEnd()); - Lit p; - uint32_t i, j; -@@ -280,13 +276,11 @@ and then calls addXorClauseInt() to actu - @p xorEqualFalse The xor must be equal to TRUE or false? - */ - template --bool Solver::addXorClause(T& ps, bool xorEqualFalse, const uint32_t group, const char* group_name) -+bool Solver::addXorClause(T& ps, bool xorEqualFalse, const uint32_t group, const char* group_name) throw (std::out_of_range) - { - assert(decisionLevel() == 0); -- if (ps.size() > (0x01UL << 18)) { -- std::cout << "Too long clause!" << std::endl; -- exit(-1); -- } -+ if (ps.size() > (0x01UL << 18)) -+ throw std::out_of_range("Too long clause!"); - - if (libraryCNFFile) { - fprintf(libraryCNFFile, "x"); -@@ -380,13 +374,11 @@ Clause* Solver::addClauseInt(T& ps, uint - template Clause* Solver::addClauseInt(Clause& ps, const uint32_t group, const bool learnt, const uint32_t glue, const float miniSatActivity, const bool inOriginalInput); - template Clause* Solver::addClauseInt(vec& ps, const uint32_t group, const bool learnt, const uint32_t glue, const float miniSatActivity, const bool inOriginalInput); - --template const bool Solver::addClauseHelper(T& ps, const uint32_t group, const char* group_name) -+template const bool Solver::addClauseHelper(T& ps, const uint32_t group, const char* group_name) throw (std::out_of_range) - { - assert(decisionLevel() == 0); -- if (ps.size() > (0x01UL << 18)) { -- std::cout << "Too long clause!" << std::endl; -- exit(-1); -- } -+ if (ps.size() > (0x01UL << 18)) -+ throw std::out_of_range("Too long clause!"); - - if (libraryCNFFile) { - for (uint32_t i = 0; i != ps.size(); i++) ps[i].print(libraryCNFFile); ---- ./Solver/DimacsParser.cpp.orig 2011-05-25 06:00:50.000000000 -0600 -+++ ./Solver/DimacsParser.cpp 2011-12-07 10:40:41.485714153 -0700 -@@ -21,6 +21,11 @@ Modifications for CryptoMiniSat are unde - - using namespace CMSat; - -+DimacsParseError::DimacsParseError(const std::string& arg) -+ : std::runtime_error(arg) { } -+ -+DimacsParseError::~DimacsParseError() throw() { } -+ - DimacsParser::DimacsParser(Solver* _solver, const bool _debugLib, const bool _debugNewVar, const bool _grouping, const bool _addAsLearnt): - solver(_solver) - , debugLib(_debugLib) -@@ -72,7 +77,7 @@ std::string DimacsParser::untilEnd(Strea - /** - @brief Parses in an integer - */ --int32_t DimacsParser::parseInt(StreamBuffer& in, uint32_t& lenParsed) -+int32_t DimacsParser::parseInt(StreamBuffer& in, uint32_t& lenParsed) throw (DimacsParseError) - { - lenParsed = 0; - int32_t val = 0; -@@ -80,7 +85,11 @@ int32_t DimacsParser::parseInt(StreamBuf - skipWhitespace(in); - if (*in == '-') neg = true, ++in; - else if (*in == '+') ++in; -- if (*in < '0' || *in > '9') printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3); -+ if (*in < '0' || *in > '9') { -+ std::ostringstream ostr; -+ ostr << "Unexpected char (parseInt): " << *in; -+ throw DimacsParseError(ostr.str()); -+ } - while (*in >= '0' && *in <= '9') { - lenParsed++; - val = val*10 + (*in - '0'), -@@ -89,13 +98,14 @@ int32_t DimacsParser::parseInt(StreamBuf - return neg ? -val : val; - } - --float DimacsParser::parseFloat(StreamBuffer& in) -+float DimacsParser::parseFloat(StreamBuffer& in) throw (DimacsParseError) - { - uint32_t len; - uint32_t main = parseInt(in, len); - if (*in != '.') { -- printf("PARSE ERROR! Float does not contain a dot! Instead it contains: %c\n", *in); -- exit(3); -+ std::ostringstream ostr; -+ ostr << "Float does not contain a dot! Instead it contains: " << *in; -+ throw DimacsParseError(ostr.str()); - } - ++in; - uint32_t sub = parseInt(in, len); -@@ -132,7 +142,7 @@ void DimacsParser::parseString(StreamBuf - @brief Reads in a clause and puts it in lit - @p[out] lits - */ --void DimacsParser::readClause(StreamBuffer& in, vec& lits) -+void DimacsParser::readClause(StreamBuffer& in, vec& lits) throw (DimacsParseError) - { - int32_t parsed_lit; - Var var; -@@ -144,8 +154,9 @@ void DimacsParser::readClause(StreamBuff - var = abs(parsed_lit)-1; - if (!debugNewVar) { - if (var >= ((uint32_t)1)<<25) { -- std::cout << "ERROR! Variable requested is far too large: " << var << std::endl; -- exit(-1); -+ std::ostringstream ostr; -+ ostr << "Variable requested is far too large: " << var; -+ throw DimacsParseError(ostr.str()); - } - while (var >= solver->nVars()) solver->newVar(); - } -@@ -174,7 +185,7 @@ completely wrong, thanks to MiniSat prin - Not checking it is \b not a problem. The problem is printing it such that - people believe it's validated - */ --void DimacsParser::printHeader(StreamBuffer& in) -+void DimacsParser::printHeader(StreamBuffer& in) throw (DimacsParseError) - { - uint32_t len; - -@@ -186,7 +197,9 @@ void DimacsParser::printHeader(StreamBuf - std::cout << "c -- header says num clauses:" << std::setw(12) << clauses << std::endl; - } - } else { -- printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3); -+ std::ostringstream ostr; -+ ostr << "Unexpected char: " << *in; -+ throw DimacsParseError(ostr.str()); - } - } - -@@ -202,7 +215,7 @@ solution to debugLibPartX.out, where X i - increases to N, where N is the number of solve() instructions - \li variable names in the form of "c var VARNUM NAME" - */ --void DimacsParser::parseComments(StreamBuffer& in, const std::string str) -+void DimacsParser::parseComments(StreamBuffer& in, const std::string str) throw (DimacsParseError) - { - uint32_t len; - #ifdef DEBUG_COMMENT_PARSING -@@ -212,7 +225,8 @@ void DimacsParser::parseComments(StreamB - if (str == "v" || str == "var") { - int var = parseInt(in, len); - skipWhitespace(in); -- if (var <= 0) std::cout << "PARSE ERROR! Var number must be a positive integer" << std::endl, exit(3); -+ if (var <= 0) -+ throw DimacsParseError("Var number must be a positive integer"); - std::string name = untilEnd(in); - solver->setVariableName(var-1, name.c_str()); - -@@ -321,7 +335,7 @@ make the clause learnt. - "c Solver::newVar() called", which needs to be parsed with parseComments() - -- this, we delegate - */ --void DimacsParser::readFullClause(StreamBuffer& in) -+void DimacsParser::readFullClause(StreamBuffer& in) throw (DimacsParseError) - { - bool xor_clause = false; - bool learnt = false; -@@ -340,21 +354,20 @@ void DimacsParser::readFullClause(Stream - //now read in grouping information, etc. - if (!grouping) groupId++; - else { -- if (*in != 'c') { -- std::cout << "PARSE ERROR! Group must be present after earch clause ('c' missing after clause line)" << std::endl; -- exit(3); -- } -+ if (*in != 'c') -+ throw DimacsParseError("Group must be present after each clause ('c' missing after clause line)"); - ++in; - - parseString(in, str); - if (str != "g" && str != "group") { -- std::cout << "PARSE ERROR! Group must be present after each clause('group' missing)!" << std::endl; -- std::cout << "Instead of 'group' there was:" << str << std::endl; -- exit(3); -+ std::ostringstream ostr; -+ ostr << "Group must be present after each clause('group' missing)!\nInstead of 'group' there was: " << str; -+ throw DimacsParseError(ostr.str()); - } - - groupId = parseInt(in, len); -- if (groupId <= 0) printf("PARSE ERROR! Group number must be a positive integer\n"), exit(3); -+ if (groupId <= 0) -+ throw DimacsParseError("Group number must be a positive integer"); - - skipWhitespace(in); - name = untilEnd(in); ---- ./Solver/ClauseAllocator.cpp.orig 2011-05-25 06:00:50.000000000 -0600 -+++ ./Solver/ClauseAllocator.cpp 2011-12-07 10:40:07.780736365 -0700 -@@ -118,7 +118,7 @@ Clause* ClauseAllocator::Clause_new(Clau - It tries to add the clause to the end of any already created stacks - if that is impossible, it creates a new stack, and adds the clause there - */ --void* ClauseAllocator::allocEnough(const uint32_t size) -+void* ClauseAllocator::allocEnough(const uint32_t size) throw (std::bad_alloc) - { - assert(sizes.size() == dataStarts.size()); - assert(maxSizes.size() == dataStarts.size()); -@@ -127,10 +127,8 @@ void* ClauseAllocator::allocEnough(const - assert(sizeof(Clause)%sizeof(BASE_DATA_TYPE) == 0); - assert(sizeof(Lit)%sizeof(BASE_DATA_TYPE) == 0); - -- if (dataStarts.size() == (1< 2); - - uint32_t needed = (sizeof(Clause)+sizeof(Lit)*size)/sizeof(BASE_DATA_TYPE); -@@ -166,7 +164,7 @@ void* ClauseAllocator::allocEnough(const - dataStart = (BASE_DATA_TYPE *)malloc(sizeof(BASE_DATA_TYPE) * nextSize); - #else - int ret = posix_memalign((void**)&dataStart, getpagesize(), sizeof(BASE_DATA_TYPE) * nextSize); -- if (ret != 0) exit(-1); -+ if (ret != 0) throw std::bad_alloc(); - assert(dataStart != NULL); - int err = madvise(dataStart, sizeof(BASE_DATA_TYPE) * nextSize, MADV_RANDOM); - assert(err == 0); -@@ -276,7 +274,7 @@ small compared to the problem size. If i - large, then it allocates new stacks, copies the non-freed clauses to these new - stacks, updates all pointers and offsets, and frees the original stacks. - */ --void ClauseAllocator::consolidate(Solver* solver, const bool force) -+void ClauseAllocator::consolidate(Solver* solver, const bool force) throw (std::bad_alloc) - { - double myTime = cpuTime(); - #ifdef DEBUG_PROPAGATEFROM -@@ -350,10 +348,8 @@ void ClauseAllocator::consolidate(Solver - std::cout << "c ------------------" << std::endl; - #endif //DEBUG_CLAUSEALLOCATOR - -- if (newMaxSizeNeed > 0) { -- std::cerr << "We cannot handle the memory need load. Exiting." << std::endl; -- exit(-1); -- } -+ if (newMaxSizeNeed > 0) -+ throw std::bad_alloc(); - - vec newSizes; - vec > newOrigClauseSizes; -@@ -367,7 +363,7 @@ void ClauseAllocator::consolidate(Solver - pointer = (BASE_DATA_TYPE*)malloc(sizeof(BASE_DATA_TYPE) * newMaxSizes[i]); - #else - int ret = posix_memalign((void**)&pointer, getpagesize(), sizeof(BASE_DATA_TYPE) * newMaxSizes[i]); -- if (ret != 0) exit(-1); -+ if (ret != 0) throw std::bad_alloc(); - assert(pointer != NULL); - int err = madvise(pointer, sizeof(BASE_DATA_TYPE) * newMaxSizes[i], MADV_RANDOM); - assert(err == 0); ---- ./Solver/Solver.h.orig 2011-05-25 06:23:52.000000000 -0600 -+++ ./Solver/Solver.h 2011-12-07 10:40:07.781736365 -0700 -@@ -26,6 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR - #include - #include - #include -+#include - - #ifdef _MSC_VER - #include -@@ -134,13 +135,13 @@ public: - - // Problem specification: - // -- Var newVar (bool dvar = true); // Add a new variable with parameters specifying variable mode. -+ Var newVar (bool dvar = true) throw (std::out_of_range); // Add a new variable with parameters specifying variable mode. - template - bool addClause (T& ps, const uint32_t group = 0, const char* group_name = NULL); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method! - template - bool addLearntClause(T& ps, const uint32_t group = 0, const char* group_name = NULL, const uint32_t glue = 10, const float miniSatActivity = 10.0); - template -- bool addXorClause (T& ps, bool xorEqualFalse, const uint32_t group = 0, const char* group_name = NULL); // Add a xor-clause to the solver. NOTE! 'ps' may be shrunk by this method! -+ bool addXorClause (T& ps, bool xorEqualFalse, const uint32_t group = 0, const char* group_name = NULL) throw (std::out_of_range); // Add a xor-clause to the solver. NOTE! 'ps' may be shrunk by this method! - - // Solving: - // -@@ -185,9 +186,9 @@ public: - const vec& get_learnts() const; //Get all learnt clauses that are >1 long - const vector get_unitary_learnts() const; //return the set of unitary learnt clauses - const uint32_t get_unitary_learnts_num() const; //return the number of unitary learnt clauses -- void dumpSortedLearnts(const std::string& fileName, const uint32_t maxSize); // Dumps all learnt clauses (including unitary ones) into the file -- void needLibraryCNFFile(const std::string& fileName); //creates file in current directory with the filename indicated, and puts all calls from the library into the file. -- void dumpOrigClauses(const std::string& fileName) const; -+ bool dumpSortedLearnts(const std::string& fileName, const uint32_t maxSize); // Dumps all learnt clauses (including unitary ones) into the file; returns true for success, false for failure -+ bool needLibraryCNFFile(const std::string& fileName); //creates file in current directory with the filename indicated, and puts all calls from the library into the file. -+ bool dumpOrigClauses(const std::string& fileName) const; - void printBinClause(const Lit litP1, const Lit litP2, FILE* outfile) const; - - const uint32_t get_sum_gauss_called() const; -@@ -452,11 +453,11 @@ protected: - ///////////////// - // Operations on clauses: - ///////////////// -- template const bool addClauseHelper(T& ps, const uint32_t group, const char* group_name); -+ template const bool addClauseHelper(T& ps, const uint32_t group, const char* group_name) throw (std::out_of_range); - template - Clause* addClauseInt(T& ps, uint32_t group, const bool learnt = false, const uint32_t glue = 10, const float miniSatActivity = 10.0, const bool inOriginalInput = false); - template -- XorClause* addXorClauseInt(T& ps, bool xorEqualFalse, const uint32_t group, const bool learnt = false); -+ XorClause* addXorClauseInt(T& ps, bool xorEqualFalse, const uint32_t group, const bool learnt = false) throw (std::out_of_range); - void attachBinClause(const Lit lit1, const Lit lit2, const bool learnt); - void attachClause (XorClause& c); - void attachClause (Clause& c); // Attach a clause to watcher lists. ---- ./Solver/ClauseAllocator.h.orig 2011-05-25 05:33:08.000000000 -0600 -+++ ./Solver/ClauseAllocator.h 2011-12-07 10:40:07.781736365 -0700 -@@ -81,7 +81,7 @@ class ClauseAllocator { - - void clauseFree(Clause* c); - -- void consolidate(Solver* solver, const bool force = false); -+ void consolidate(Solver* solver, const bool force = false) throw (std::bad_alloc); - - const uint32_t getNewClauseNum(); - -@@ -120,7 +120,7 @@ class ClauseAllocator { - */ - vec currentlyUsedSizes; - -- void* allocEnough(const uint32_t size); -+ void* allocEnough(const uint32_t size) throw (std::bad_alloc); - - /** - @brief The clause's data is replaced by this to aid updating diff --git a/cryptominisat-x86.patch b/cryptominisat-x86.patch deleted file mode 100644 index c11566e..0000000 --- a/cryptominisat-x86.patch +++ /dev/null @@ -1,12 +0,0 @@ -diff -up cryptominisat-2.9.1/Solver/Main.cpp.x86 cryptominisat-2.9.1/Solver/Main.cpp ---- cryptominisat-2.9.1/Solver/Main.cpp.x86 2011-12-19 11:38:13.000000000 +0100 -+++ cryptominisat-2.9.1/Solver/Main.cpp 2011-12-19 11:38:40.000000000 +0100 -@@ -645,7 +645,7 @@ FILE* Main::openOutputFile() - - void Main::setDoublePrecision(const uint32_t verbosity) - { -- #if defined(__linux__) -+ #if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) - fpu_control_t oldcw, newcw; - _FPU_GETCW(oldcw); - newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; diff --git a/cryptominisat.1 b/cryptominisat.1 deleted file mode 100644 index f1201c8..0000000 --- a/cryptominisat.1 +++ /dev/null @@ -1,198 +0,0 @@ -.TH "CRYPTOMINISAT" "1" "@VERSION@" "Mate Soos" "User Commands" -.SH "NAME" -cryptominisat \- SAT solver -.SH "SYNOPSIS" -.B cryptominisat -[\fIOPTIONS\fP] <\fIinput\-file\fP> <\fIoutput\-file\fP> -.SH "DESCRIPTION" -.PP -CryptoMiniSat is a SAT solver that aims to become a premiere SAT solver with -all the features and speed of successful SAT solvers, such as MiniSat and -PrecoSat. The long-term goals of CryptoMiniSat are to be an efficient -sequential, parallel and distributed solver. There are solvers that are good -at one or the other, e.g. ManySat (parallel) or PSolver (distributed), but we -wish to excel at all. -.SH "OPTIONS" -.TP -\fB\-\-polarity\-mode\fP = \fI{true,false,rnd,auto}\fP [default: auto] -Selects the polarity mode. Auto is the Jeroslow&Wang method. -.TP -\fB\-\-rnd\-freq\fP = <\fInum\fP> [0-1] -.TP -\fB\-\-verbosity\fP = <\fInum\fP> [0-2] -.TP -\fB\-\-randomize\fP = <\fIseed\fP> [0 - 2^32-1] -Sets the random seed, used for picking decision variables (default = 0). -.TP -\fB\-\-restrict\fP = <\fInum\fP> [1 - varnum] -When picking random variables to branch on, pick one that is in the \fInum\fP -most active vars useful for cryptographic problems, where the question is the -key, which is usually small (e.g., 80 bits). -.TP -\fB\-\-gaussuntil\fP = <\fInum\fP> -Depth until which Gaussian elimination is active. Giving 0 switches off -Gaussian elimination. -.TP -\fB\-\-restarts\fP = <\fInum\fP> [1 - 2^32-1] -No more than the given number of restarts will be performed during search. -.TP -\fB\-\-nonormxorfind\fP -Don't find and collect >2-long xor-clauses from regular clauses. -.TP -\fB\-\-nobinxorfind\fP -Don't find and collect 2-long xor-clauses from regular clauses. -.TP -\fB\-\-noregbxorfind\fP -Don't regularly find and collect 2-long xor-clauses from regular clauses. -.TP -\fB\-\-noextendedscc\fP -Don't do strongly connected component finding using non-existent bins. -.TP -\fB\-\-noconglomerate\fP -Don't conglomerate 2 xor clauses when one var is dependent. -.TP -\fB\-\-nosimplify\fP -Don't do regular simplification rounds. -.TP -\fB\-\-greedyunbound\fP -Greedily unbound variables that are not needed for SAT. -.TP -\fB\-\-debuglib\fP -Solve at specific \fBc Solver::solve()\fP points in the CNF file. Used to -debug file generated by Solver's \fBneedLibraryCNFFile()\fP function. -.TP -\fB\-\-debugnewvar\fP -Add new vars at specific \fBc Solver::newVar()\fP points in the CNF file. -Used to debug file generated by Solver's \fBneedLibraryCNFFile()\fP function. -.TP -\fB\-\-novarreplace\fP -Don't perform variable replacement. Needed for programmable solver feature. -.TP -\fB\-\-restart\fP = \fI{auto, static, dynamic}\fP -Which kind of restart strategy to follow. Default is \fIauto\fP. -.TP -\fB\-\-dumplearnts\fP = <\fIfilename\fP> -If interrupted or reached restart limit, dump the learnt clauses to the -specified file. Maximum size of dumped clauses can be specified with the -\fB\-\-maxdumplearnts\fP option. -.TP -\fB\-\-maxdumplearnts\fP = [0 - 2^32-1] -When dumping the learnts to file, what should be maximum length of the clause -dumped. Useful to make the resulting file smaller. Default is 2^32-1. Note: -2-long XORs are always dumped. -.TP -\fB\-\-dumporig\fP = <\fIfilename\fP> -If interrupted or reached restart limit, dump the original problem instance, -simplified to the current point. -.TP -\fB\-\-alsoread\fP = <\fIfilename\fP> -Also read this file in. Can be used to re-read dumped learnts, for example. -.TP -\fB\-\-maxsolutions\fP = <\fInum\fP> -Search for given amount of solutions. Can only be used in single-threaded -mode (\fB--threads=1\fP). -.TP -\fB\-\-pavgbranch\fP -Print average branch depth. -.TP -\fB\-\-nofailedlit\fP -Don't search for failed literals, and don't search for literals propagated -both by \fIvarX\fP and \fI-varX\fP. -.TP -\fB\-\-noheuleprocess\fP -Don't try to minimise XORs by XOR-ing them together. Algorithm as per -global/local substitution in Heule's thesis. -.TP -\fB\-\-nosatelite\fP -Don't do clause subsumption, clause strengthening and variable elimination -(implies \fB\-\-novarelim\fP and \fB\-\-nosubsume1\fP). -.TP -\fB\-\-noxorsubs\fP -Don't try to subsume xor-clauses. -.TP -\fB\-\-nosolprint\fP -Don't print the satisfying assignment if the solution is SAT. -.TP -\fB\-\-novarelim\fP -Don't perform variable elimination as per Een and Biere. -.TP -\fB\-\-nosubsume1\fP -Don't perform clause contraction through resolution. -.TP -\fB\-\-noparthandler\fP -Don't find and solve subroblems with subsolvers. -.TP -\fB\-\-nomatrixfind\fP -Don't find distinct matrixes. Put all xors into one big matrix. -.TP -\fB\-\-noordercol\fP -Don't order variables in the columns of Gaussian elimination. Effectively -disables iterative reduction of the matrix. -.TP -\fB\-\-noiterreduce\fP -Don't reduce iteratively the matrix that is updated. -.TP -\fB\-\-maxmatrixrows\fP = [0 - 2^32-1] -Set maximum number of rows for gaussian matrix. Too large matrixes should be -discarded for reasons of efficiency. Default: 1000. -.TP -\fB\-\-minmatrixrows\fP = [0 - 2^32-1] -Set minimum number of rows for gaussian matrix. Normally, too small matrixes -are discarded for reasons of efficiency. Default: 20. -.TP -\fB\-\-savematrix\fP = [0 - 2^32-1] -Save matrix every Nth decision level. Default: 2. -.TP -\fB\-\-maxnummatrixes\fP = [0 - 2^32-1] -Maximum number of matrixes to treat. Default: 3. -.TP -\fB\-\-nohyperbinres\fP -Don't add binary clauses when doing failed lit probing. -.TP -\fB\-\-noremovebins\fP -Don't remove useless binary clauses. -.TP -\fB\-\-noremlbins\fP -Don't remove useless learnt binary clauses. -.TP -\fB\-\-nosubswithbins\fP -Don't subsume with binary clauses. -.TP -\fB\-\-nosubswithnbins\fP -Don't subsume with non-existent binary clauses. -.TP -\fB\-\-noclausevivif\fP -Don't perform clause vivification. -.TP -\fB\-\-nosortwatched\fP -Don't sort watches according to size: bin, tri, etc. -.TP -\fB\-\-nolfminim\fP -Don't do on-the-fly self-subsuming resolution (called 'strong minimisation' in -PrecoSat). -.TP -\fB\-\-nocalcreach\fP -Don't calculate reachability and interfere with variable decisions accordingly. -.TP -\fB\-\-nobxor\fP -Don't find equivalent literals during failed literal search. -.TP -\fB\-\-norecotfssr\fP -Don't perform recursive/transitive OTF self-subsuming resolution. -.TP -\fB\-\-nocacheotfssr\fP -Don't cache 1-level equeue. Less memory used, but disables trans OTFSSR, -adv. clause vivifier, etc. Throw the clause away on backtrack. -.TP -\fB\-\-threads\fP = <\fInum\fP> -Number of threads (default is 1). -.SH "EXIT STATUS" -.PP -The output is a solution, together with some timing information. -The exit status indicates the following: -.IP 10 -The problem is satisfiable. -.IP 15 -The problem's satisfiability was not determined. -.IP 20 -The problem is unsatisfiable. diff --git a/cryptominisat.spec b/cryptominisat.spec index 5ffeb7f..beae727 100644 --- a/cryptominisat.spec +++ b/cryptominisat.spec @@ -1,6 +1,6 @@ Name: cryptominisat -Version: 2.9.1 -Release: 3%{?dist} +Version: 2.9.2 +Release: 1%{?dist} Summary: SAT solver # Some source files were borrowed from minisat2, which is MIT-licensed. @@ -8,15 +8,7 @@ Summary: SAT solver # Original sources for this project are licensed GPL v3 or later. License: GPLv3+ URL: http://www.msoos.org/cryptominisat2 -Source0: https://gforge.inria.fr/frs/download.php/28579/%{name}-%{version}.tar.gz -# Man page written by Jerry James, using text found in the sources. -# The man page therefore has the same copyright and license as the sources. -Source1: %{name}.1 -# This patch was sent upstream 7 Dec 2011. It converts calls to exit() inside -# the library into either boolean return codes or exceptions. -Patch0: %{name}-exit.patch -# FPU handling is x86 specific -Patch1: %{name}-x86.patch +Source0: https://gforge.inria.fr/frs/download.php/30138/%{name}-%{version}.tar.gz BuildRequires: zlib-devel Requires: %{name}-libs%{?_isa} = %{version}-%{release} @@ -47,8 +39,6 @@ The %{name} library. %prep %setup -q -%patch0 -%patch1 -p1 %build %configure --disable-static @@ -62,15 +52,11 @@ make %{?_smp_mflags} make install DESTDIR=$RPM_BUILD_ROOT rm -f $RPM_BUILD_ROOT%{_libdir}/*.la -# Install the man page -mkdir -p $RPM_BUILD_ROOT%{_mandir}/man1 -sed "s/@VERSION@/%{version}/" %{SOURCE1} > $RPM_BUILD_ROOT%{_mandir}/man1/%{name}.1 - -%check -cd tests -set +e -LD_LIBRARY_PATH=../Solver/.libs ../cryptominisat --nosolprint --verbosity=1 AProVE09-12.cnf.gz -[ $? = 10 ] +# %%check +# cd tests +# set +e +# LD_LIBRARY_PATH=../Solver/.libs ../cryptominisat --nosolprint --verbosity=1 AProVE09-12.cnf.gz +# [ $? = 10 ] %post -p /sbin/ldconfig @@ -89,6 +75,12 @@ LD_LIBRARY_PATH=../Solver/.libs ../cryptominisat --nosolprint --verbosity=1 APro %{_libdir}/lib%{name}-%{version}.so %changelog +* Mon Jan 23 2012 Jerry James - 2.9.2-1 +- New upstream version +- Man page is now upstream +- All patches have been applied upstream +- Tests have been removed from the source distribution + * Mon Jan 9 2012 Jerry James - 2.9.1-3 - Rebuild for GCC 4.7 diff --git a/sources b/sources index 05cf677..98c96cd 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -292a7136423e24dbdd9765e2b80ae883 cryptominisat-2.9.1.tar.gz +0b677776d0fbff4911ad539732034927 cryptominisat-2.9.2.tar.gz