[cryptominisat] Initial import.
Jerry James
jjames at fedoraproject.org
Wed Dec 7 18:11:56 UTC 2011
commit 746a0045cd2b320acf34918902d4da325c72e3ec
Author: Jerry James <loganjerry at gmail.com>
Date: Wed Dec 7 11:11:42 2011 -0700
Initial import.
.gitignore | 1 +
cryptominisat-exit.patch | 556 ++++++++++++++++++++++++++++++++++++++++++++++
cryptominisat.1 | 198 ++++++++++++++++
cryptominisat.spec | 90 ++++++++
sources | 1 +
5 files changed, 846 insertions(+), 0 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index e69de29..1006ba7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -0,0 +1 @@
+/cryptominisat-2.9.1.tar.gz
diff --git a/cryptominisat-exit.patch b/cryptominisat-exit.patch
new file mode 100644
index 0000000..3446992
--- /dev/null
+++ b/cryptominisat-exit.patch
@@ -0,0 +1,556 @@
+--- ./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 <stdexcept>
+ #include <string>
+ #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<Lit>& lits);
++ void readClause(StreamBuffer& in, vec<Lit>& 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<Lit> 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<class T, class T2>
+--- ./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<class T>
+-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<class T>
+-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<Lit>& ps, const uint32_t group, const bool learnt, const uint32_t glue, const float miniSatActivity, const bool inOriginalInput);
+
+-template<class T> const bool Solver::addClauseHelper(T& ps, const uint32_t group, const char* group_name)
++template<class T> 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<Lit>& lits)
++void DimacsParser::readClause(StreamBuffer& in, vec<Lit>& 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<<NUM_BITS_OUTER_OFFSET)) {
+- std::cerr << "Memory manager cannot handle the load. Sorry. Exiting." << std::endl;
+- exit(-1);
+- }
++ if (dataStarts.size() == (1<<NUM_BITS_OUTER_OFFSET))
++ throw std::bad_alloc();
+ assert(size > 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<uint32_t> newSizes;
+ vec<vec<uint32_t> > 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 <string.h>
+ #include <stdio.h>
+ #include <stack>
++#include <stdexcept>
+
+ #ifdef _MSC_VER
+ #include <msvc/stdint.h>
+@@ -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<class T>
+ 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<class T>
+ 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<class T>
+- 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<Clause*>& get_learnts() const; //Get all learnt clauses that are >1 long
+ const vector<Lit> 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<class T> const bool addClauseHelper(T& ps, const uint32_t group, const char* group_name);
++ template<class T> const bool addClauseHelper(T& ps, const uint32_t group, const char* group_name) throw (std::out_of_range);
+ template <class T>
+ 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<class T>
+- 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<size_t> 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.1 b/cryptominisat.1
new file mode 100644
index 0000000..f1201c8
--- /dev/null
+++ b/cryptominisat.1
@@ -0,0 +1,198 @@
+.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
new file mode 100644
index 0000000..f364a82
--- /dev/null
+++ b/cryptominisat.spec
@@ -0,0 +1,90 @@
+Name: cryptominisat
+Version: 2.9.1
+Release: 1%{?dist}
+Summary: SAT solver
+
+# Some source files were borrowed from minisat2, which is MIT-licensed.
+# The Mersenne Twister implementation is BSD-licensed.
+# 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
+
+BuildRequires: zlib-devel
+Requires: %{name}-libs%{?_isa} = %{version}-%{release}
+
+%description
+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.
+
+CryptoMiniSat 2.5 won the SAT Race 2010 among 20 solvers submitted by
+researchers and industry.
+
+%package devel
+Summary: Header files for developing with %{name}
+Requires: %{name}-libs%{?_isa} = %{version}-%{release}
+
+%description devel
+Header files for developing applications that use %{name}.
+
+%package libs
+Summary: Cryptominisat library
+
+%description libs
+The %{name} library.
+
+%prep
+%setup -q
+%patch0
+
+%build
+%configure --disable-static
+sed -e 's|^hardcode_libdir_flag_spec=.*|hardcode_libdir_flag_spec=""|g' \
+ -e 's|^runpath_var=LD_RUN_PATH|runpath_var=DIE_RPATH_DIE|g' \
+ -i libtool
+sed -i 's|^LIBS =.*|LIBS = -lz -lgomp|' Solver/Makefile
+make %{?_smp_mflags}
+
+%install
+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
+../cryptominisat --nosolprint --verbosity=1 AProVE09-12.cnf.gz
+[ $? = 10 ]
+
+%post -p /sbin/ldconfig
+
+%postun -p /sbin/ldconfig
+
+%files
+%{_bindir}/%{name}
+%{_mandir}/man1/%{name}*
+
+%files devel
+%{_includedir}/%{name}/
+%{_libdir}/lib%{name}.so
+
+%files libs
+%doc AUTHORS LICENSE-GPL LICENSE-MIT NEWS README TODO
+%{_libdir}/lib%{name}-%{version}.so
+
+%changelog
+* Wed Dec 7 2011 Jerry James <loganjerry at gmail.com> - 2.9.1-1
+- Initial RPM
diff --git a/sources b/sources
index e69de29..05cf677 100644
--- a/sources
+++ b/sources
@@ -0,0 +1 @@
+292a7136423e24dbdd9765e2b80ae883 cryptominisat-2.9.1.tar.gz
More information about the scm-commits
mailing list