From: msoos Date: Tue, 8 Dec 2009 13:31:11 +0000 (+0000) Subject: Updating CryptoMiniSat to r586. Need to call 'void needLibraryCNFFile(const char... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=0bdada38814a91e4c40a417f78662cfb970326ce;p=francis%2Fstp.git Updating CryptoMiniSat to r586. Need to call 'void needLibraryCNFFile(const char* fileName);' once exactly after Solver object creation to have CNF file output from library calls git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@483 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/sat/cryptominisat2/Clause.h b/src/sat/cryptominisat2/Clause.h index 1c64836..a95ffad 100644 --- a/src/sat/cryptominisat2/Clause.h +++ b/src/sat/cryptominisat2/Clause.h @@ -140,9 +140,9 @@ public: } void print() { printf("Clause group: %d, size: %d, learnt:%d, lits: ", group, size(), learnt()); - plain_print(); + plainPrint(); } - void plain_print(FILE* to = stdout) const { + void plainPrint(FILE* to = stdout) const { for (uint i = 0; i < size(); i++) { if (data[i].sign()) fprintf(to, "-"); fprintf(to, "%d ", data[i].var() + 1); @@ -189,10 +189,10 @@ public: void print() { printf("XOR Clause group: %d, size: %d, learnt:%d, lits:\"", group, size(), learnt()); - plain_print(); + plainPrint(); } - void plain_print(FILE* to = stdout) const { + void plainPrint(FILE* to = stdout) const { fprintf(to, "x"); if (xor_clause_inverted()) printf("-"); diff --git a/src/sat/cryptominisat2/ClauseCleaner.cpp b/src/sat/cryptominisat2/ClauseCleaner.cpp index e7e23cf..114a3df 100644 --- a/src/sat/cryptominisat2/ClauseCleaner.cpp +++ b/src/sat/cryptominisat2/ClauseCleaner.cpp @@ -1,3 +1,20 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + #include "ClauseCleaner.h" namespace MINISAT @@ -139,7 +156,7 @@ void ClauseCleaner::cleanClauses(vec& cs, ClauseSetType type) vec ps(2); ps[0] = c[0].unsign(); ps[1] = c[1].unsign(); - solver.toReplace->replace(ps, c.xor_clause_inverted(), c.group); + solver.varReplacer->replace(ps, c.xor_clause_inverted(), c.group); solver.removeClause(c); s++; } else diff --git a/src/sat/cryptominisat2/Conglomerate.cpp b/src/sat/cryptominisat2/Conglomerate.cpp index e4454f6..f8ecf0c 100644 --- a/src/sat/cryptominisat2/Conglomerate.cpp +++ b/src/sat/cryptominisat2/Conglomerate.cpp @@ -1,3 +1,20 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + #include "Conglomerate.h" #include "Solver.h" #include "VarReplacer.h" @@ -61,7 +78,7 @@ void Conglomerate::fillVarToXor() for (Lit* it = &(S->trail[0]), *end = it + S->trail.size(); it != end; it++) blocked[it->var()] = true; - const vec& clauses = S->toReplace->getClauses(); + const vec& clauses = S->varReplacer->getClauses(); for (Clause *const*it = clauses.getData(), *const*end = it + clauses.size(); it != end; it++) { const Clause& c = **it; for (const Lit* a = &c[0], *end = a + c.size(); a != end; a++) { @@ -227,7 +244,7 @@ bool Conglomerate::dealWithNewClause(vec& ps, const bool inverted, const ui free(newX); #endif - S->toReplace->replace(ps, inverted, old_group); + S->varReplacer->replace(ps, inverted, old_group); blocked[ps[0].var()] = true; blocked[ps[1].var()] = true; break; diff --git a/src/sat/cryptominisat2/Conglomerate.h b/src/sat/cryptominisat2/Conglomerate.h index d0eeb7c..6fe7556 100644 --- a/src/sat/cryptominisat2/Conglomerate.h +++ b/src/sat/cryptominisat2/Conglomerate.h @@ -1,3 +1,20 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + #ifndef CONGLOMERATE_H #define CONGLOMERATE_H diff --git a/src/sat/cryptominisat2/FindUndef.cpp b/src/sat/cryptominisat2/FindUndef.cpp index 1fdff06..7d7b0a2 100644 --- a/src/sat/cryptominisat2/FindUndef.cpp +++ b/src/sat/cryptominisat2/FindUndef.cpp @@ -1,3 +1,20 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + #include "FindUndef.h" #include "Solver.h" @@ -43,7 +60,7 @@ void FindUndef::fillPotential() } } - vector replacingVars = S.toReplace->getReplacingVars(); + vector replacingVars = S.varReplacer->getReplacingVars(); for (Var *it = &replacingVars[0], *end = it + replacingVars.size(); it != end; it++) { if (isPotential[*it]) { isPotential[*it] = false; diff --git a/src/sat/cryptominisat2/FindUndef.h b/src/sat/cryptominisat2/FindUndef.h index e47a904..59835c2 100644 --- a/src/sat/cryptominisat2/FindUndef.h +++ b/src/sat/cryptominisat2/FindUndef.h @@ -1,3 +1,20 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + #ifndef FINDUNDEF_H #define FINDUNDEF_H diff --git a/src/sat/cryptominisat2/Gaussian.cpp b/src/sat/cryptominisat2/Gaussian.cpp index a4c6798..f589ee8 100644 --- a/src/sat/cryptominisat2/Gaussian.cpp +++ b/src/sat/cryptominisat2/Gaussian.cpp @@ -22,6 +22,7 @@ along with this program. If not, see . #include "Clause.h" #include #include "ClauseCleaner.h" + using std::ostream; using std::cout; using std::endl; @@ -908,6 +909,12 @@ void Gaussian::print_stats() const std::cout << " Gauss(" << matrix_no << ") not called."; } +void Gaussian::print_matrix_stats() const +{ + cout << "matrix size: " << cur_matrixset.num_rows << " x " << cur_matrixset.num_cols << endl; +} + + void Gaussian::reset_stats() { useful_prop = 0; diff --git a/src/sat/cryptominisat2/Gaussian.h b/src/sat/cryptominisat2/Gaussian.h index 1d692e7..00e9eb5 100644 --- a/src/sat/cryptominisat2/Gaussian.h +++ b/src/sat/cryptominisat2/Gaussian.h @@ -29,9 +29,11 @@ namespace MINISAT { using namespace MINISAT; +#ifdef VERBOSE_DEBUG using std::vector; using std::cout; using std::endl; +#endif class Clause; @@ -196,11 +198,6 @@ inline void Gaussian::canceling(const int sublevel) } } -inline void Gaussian::print_matrix_stats() const -{ - cout << "matrix size: " << cur_matrixset.num_rows << " x " << cur_matrixset.num_cols << endl; -} - std::ostream& operator << (std::ostream& os, const vec& v); }; diff --git a/src/sat/cryptominisat2/MatrixFinder.cpp b/src/sat/cryptominisat2/MatrixFinder.cpp index 19c8ad6..f4acd1d 100644 --- a/src/sat/cryptominisat2/MatrixFinder.cpp +++ b/src/sat/cryptominisat2/MatrixFinder.cpp @@ -34,10 +34,8 @@ using std::map; //#define VERBOSE_DEBUG -#ifdef VERBOSE_DEBUG using std::cout; using std::endl; -#endif //#define PART_FINDING @@ -215,8 +213,8 @@ void MatrixFinder::findParts(vector& xorFingerprintInMatrix, vectorplain_print(); - (*a2)->plain_print(); + (*a)->plainPrint(); + (*a2)->plainPrint(); cout << "END" << endl; } } diff --git a/src/sat/cryptominisat2/PackedRow.cpp b/src/sat/cryptominisat2/PackedRow.cpp index 0689c0d..25d2a32 100644 --- a/src/sat/cryptominisat2/PackedRow.cpp +++ b/src/sat/cryptominisat2/PackedRow.cpp @@ -1,3 +1,20 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + #include "PackedRow.h" namespace MINISAT { diff --git a/src/sat/cryptominisat2/Solver.cpp b/src/sat/cryptominisat2/Solver.cpp index a7acf2a..490d6c5 100644 --- a/src/sat/cryptominisat2/Solver.cpp +++ b/src/sat/cryptominisat2/Solver.cpp @@ -38,14 +38,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "XorFinder.h" #include "ClauseCleaner.h" -//#define DEBUG_LIB - -#ifdef DEBUG_LIB -#include -FILE* myoutputfile; -static uint numcalled = 0; -#endif //DEBUG_LIB - namespace MINISAT { using namespace MINISAT; @@ -96,20 +88,14 @@ Solver::Solver() : , maxRestarts(UINT_MAX) , MYFLAG (0) , learnt_clause_group(0) + , libraryCNFFile (NULL) { - toReplace = new VarReplacer(this); + varReplacer = new VarReplacer(this); conglomerate = new Conglomerate(this); clauseCleaner = new ClauseCleaner(*this); logger.setSolver(this); - - #ifdef DEBUG_LIB - std::stringstream ss; - ss << "inputfile" << numcalled << ".cnf"; - myoutputfile = fopen(ss.str().c_str(), "w"); - #endif } - Solver::~Solver() { for (int i = 0; i < learnts.size(); i++) free(learnts[i]); @@ -117,13 +103,12 @@ Solver::~Solver() for (int i = 0; i < xorclauses.size(); i++) free(xorclauses[i]); for (uint i = 0; i < gauss_matrixes.size(); i++) delete gauss_matrixes[i]; for (uint i = 0; i < freeLater.size(); i++) free(freeLater[i]); - delete toReplace; + delete varReplacer; delete conglomerate; delete clauseCleaner; - #ifdef DEBUG_LIB - fclose(myoutputfile); - #endif //DEBUG_LIB + if (libraryCNFFile) + fclose(libraryCNFFile); } //================================================================================================= @@ -149,16 +134,15 @@ Var Solver::newVar(bool sign, bool dvar) polarity .push_back((char)sign); decision_var.push_back(dvar); - toReplace->newVar(); + varReplacer->newVar(); conglomerate->newVar(); insertVarOrder(v); if (dynamic_behaviour_analysis) logger.new_var(v); - #ifdef DEBUG_LIB - fprintf(myoutputfile, "c Solver::newVar() called\n"); - #endif //DEBUG_LIB + if (libraryCNFFile) + fprintf(libraryCNFFile, "c Solver::newVar() called\n"); return v; } @@ -166,15 +150,13 @@ Var Solver::newVar(bool sign, bool dvar) bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint group, char* group_name, const bool internal) { assert(decisionLevel() == 0); - #ifdef DEBUG_LIB - if (!internal) { - fprintf(myoutputfile, "x"); + if (libraryCNFFile && !internal) { + fprintf(libraryCNFFile, "x"); for (uint i = 0; i < ps.size(); i++) { - fprintf(myoutputfile, "%s%d ", ps[i].sign() ? "-" : "", ps[i].var()+1); + fprintf(libraryCNFFile, "%s%d ", ps[i].sign() ? "-" : "", ps[i].var()+1); } - fprintf(myoutputfile, "0\n"); + fprintf(libraryCNFFile, "0\n"); } - #endif //DEBUG_LIB if (dynamic_behaviour_analysis) logger.set_group_name(group, group_name); @@ -182,9 +164,9 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro return false; // Check if clause is satisfied and remove false/duplicate literals: - if (toReplace->getNumLastReplacedVars()) { + if (varReplacer->getNumLastReplacedVars()) { for (int i = 0; i != ps.size(); i++) { - ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign(); + ps[i] = varReplacer->getReplaceTable()[ps[i].var()] ^ ps[i].sign(); } } @@ -227,7 +209,7 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro cout << "--> xor is 2-long, replacing var " << ps[0].var()+1 << " with " << (!xor_clause_inverted ? "-" : "") << ps[1].var()+1 << endl; #endif - toReplace->replace(ps, xor_clause_inverted, group); + varReplacer->replace(ps, xor_clause_inverted, group); break; } default: { @@ -237,7 +219,7 @@ bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint gro xorclauses.push(c); attachClause(*c); if (!internal) - toReplace->newClause(); + varReplacer->newClause(); break; } } @@ -249,12 +231,12 @@ bool Solver::addClause(vec& ps, const uint group, char* group_name) { assert(decisionLevel() == 0); - #ifdef DEBUG_LIB - for (int i = 0; i < ps.size(); i++) { - fprintf(myoutputfile, "%s%d ", ps[i].sign() ? "-" : "", ps[i].var()+1); + if (libraryCNFFile) { + for (int i = 0; i < ps.size(); i++) { + fprintf(libraryCNFFile, "%s%d ", ps[i].sign() ? "-" : "", ps[i].var()+1); + } + fprintf(libraryCNFFile, "0\n"); } - fprintf(myoutputfile, "0\n"); - #endif //DEBUG_LIB if (dynamic_behaviour_analysis) logger.set_group_name(group, group_name); @@ -263,9 +245,9 @@ bool Solver::addClause(vec& ps, const uint group, char* group_name) return false; // Check if clause is satisfied and remove false/duplicate literals: - if (toReplace->getNumLastReplacedVars()) { + if (varReplacer->getNumLastReplacedVars()) { for (int i = 0; i != ps.size(); i++) { - ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign(); + ps[i] = varReplacer->getReplaceTable()[ps[i].var()] ^ ps[i].sign(); } } @@ -296,7 +278,7 @@ bool Solver::addClause(vec& ps, const uint group, char* group_name) clauses.push(c); attachClause(*c); - toReplace->newClause(); + varReplacer->newClause(); } return true; @@ -441,26 +423,10 @@ void Solver::printLit(const Lit l) const printf("%s%d:%c", l.sign() ? "-" : "", l.var()+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X')); } - -void Solver::printClause(const Clause& c) const +void Solver::needLibraryCNFFile(const char* fileName) { - printf("(group: %d) ", c.group); - for (uint i = 0; i < c.size();) { - printLit(c[i]); - i++; - if (i < c.size()) printf(" "); - } -} - -void Solver::printClause(const XorClause& c) const -{ - printf("(group: %d) ", c.group); - if (c.xor_clause_inverted()) printf(" /inverted/ "); - for (uint i = 0; i < c.size();) { - printLit(c[i].unsign()); - i++; - if (i < c.size()) printf(" + "); - } + libraryCNFFile = fopen(fileName, "w"); + assert(libraryCNFFile != NULL); } void Solver::set_gaussian_decision_until(const uint to) @@ -1061,7 +1027,7 @@ void Solver::dump_sorted_learnts(const char* file) sort(learnts, reduceDB_lt()); for (int i = learnts.size()-1; i >= 0 ; i--) { - learnts[i]->plain_print(outfile); + learnts[i]->plainPrint(outfile); } fclose(outfile); } @@ -1348,9 +1314,8 @@ void Solver::print_gauss_sum_stats() const lbool Solver::solve(const vec& assumps) { - #ifdef DEBUG_LIB - fprintf(myoutputfile, "c Solver::solve() called\n"); - #endif + if (libraryCNFFile) + fprintf(libraryCNFFile, "c Solver::solve() called\n"); model.clear(); conflict.clear(); @@ -1372,7 +1337,7 @@ lbool Solver::solve(const vec& assumps) conglomerate->addRemovedClauses(); if (performReplace) { - toReplace->performReplace(); + varReplacer->performReplace(); if (!ok) return l_False; } @@ -1391,7 +1356,7 @@ lbool Solver::solve(const vec& assumps) printf("| Finding XORs: %5.2lf s (found: %7d, avg size: %3.1lf) |\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors); if (performReplace) { - toReplace->performReplace(); + varReplacer->performReplace(); if (!ok) return l_False; } } @@ -1420,7 +1385,7 @@ lbool Solver::solve(const vec& assumps) } if (performReplace) { - toReplace->performReplace(); + varReplacer->performReplace(); if (!ok) return l_False; } } @@ -1482,7 +1447,7 @@ lbool Solver::solve(const vec& assumps) if (status == l_True) { conglomerate->doCalcAtFinish(); - toReplace->extendModel(); + varReplacer->extendModel(); // Extend & copy model: model.growTo(nVars()); for (int i = 0; i < nVars(); i++) model[i] = value(i); @@ -1538,8 +1503,7 @@ bool Solver::verifyXorClauses(const vec& cs) const } if (!final) { printf("unsatisfied clause: "); - printClause(*xorclauses[i]); - printf("\n"); + xorclauses[i]->plainPrint(); failed = true; } } @@ -1557,8 +1521,7 @@ void Solver::verifyModel() goto next; printf("unsatisfied clause: "); - printClause(*clauses[i]); - printf("\n"); + clauses[i]->plainPrint(); failed = true; next: ; diff --git a/src/sat/cryptominisat2/Solver.h b/src/sat/cryptominisat2/Solver.h index d6ab797..9cba2cf 100644 --- a/src/sat/cryptominisat2/Solver.h +++ b/src/sat/cryptominisat2/Solver.h @@ -24,6 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include +#include #include "mtl/Vec.h" #include "mtl/Heap.h" @@ -157,10 +158,11 @@ public: void needProofGraph(); // Prepares the solver to output proof graphs during solving void setVariableName(int var, char* name); // Sets the name of the variable 'var' to 'name'. Useful for statistics and proof logs (i.e. used by 'logger') const vec& get_sorted_learnts(); //return the set of learned clauses, sorted according to the logic used in MiniSat to distinguish between 'good' and 'bad' clauses - const vec& get_learnts() const; //Get all learnt clauses + 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 uint get_unitary_learnts_num() const; //return the number of unitary learnt clauses - void dump_sorted_learnts(const char* file); + void dump_sorted_learnts(const char* file); // Dumps all learnt clauses (including unitary ones) into the file + void needLibraryCNFFile(const char* fileName); //creates file in current directory with the filename indicated, and puts all calls from the library into the file. protected: vector gauss_matrixes; @@ -237,7 +239,8 @@ protected: unsigned long int MYFLAG; //Logging - uint learnt_clause_group; //the group number of learnt clauses. Incremented at each added learnt clause + uint learnt_clause_group; //the group number of learnt clauses. Incremented at each added learnt clause + FILE *libraryCNFFile; //The file that all calls from the library are logged // Main internal methods: // @@ -264,7 +267,6 @@ protected: void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead. void varBumpActivity (Var v); // Increase a variable with the current 'bump' value. void claDecayActivity (); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead. - void claBumpActivity (Clause& c); // Increase a clause with the current 'bump' value. // Operations on clauses: // @@ -292,13 +294,11 @@ protected: friend class VarReplacer; friend class ClauseCleaner; Conglomerate* conglomerate; - VarReplacer* toReplace; + VarReplacer* varReplacer; ClauseCleaner* clauseCleaner; // Debug: void printLit (const Lit l) const; - void printClause (const Clause& c) const; - void printClause (const XorClause& c) const; void verifyModel (); bool verifyXorClauses (const vec& cs) const; void checkLiteralCount(); diff --git a/src/sat/cryptominisat2/VERSION b/src/sat/cryptominisat2/VERSION index 79378eb..7de8163 100644 --- a/src/sat/cryptominisat2/VERSION +++ b/src/sat/cryptominisat2/VERSION @@ -1,3 +1,3 @@ CryptoMiniSat -SVN revision: 579 -GIT revision: d7ef400c6dbb9bc0b6b3fd98a0c43b178916a849 +SVN revision: 586 +GIT revision: 8b5929ba71ceaf5bf6c905436cde96e640bee4b7 diff --git a/src/sat/cryptominisat2/VarReplacer.cpp b/src/sat/cryptominisat2/VarReplacer.cpp index b04f9e0..a8b9379 100644 --- a/src/sat/cryptominisat2/VarReplacer.cpp +++ b/src/sat/cryptominisat2/VarReplacer.cpp @@ -1,3 +1,20 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + #include "VarReplacer.h" #include "Solver.h" diff --git a/src/sat/cryptominisat2/VarReplacer.h b/src/sat/cryptominisat2/VarReplacer.h index 24d94d7..278baa4 100644 --- a/src/sat/cryptominisat2/VarReplacer.h +++ b/src/sat/cryptominisat2/VarReplacer.h @@ -1,3 +1,20 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +This program is free software: you can redistribute it and/or modify +it under the terms of the GNU General Public License as published by +the Free Software Foundation, either version 3 of the License, or +(at your option) any later version. + +This program is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +GNU General Public License for more details. + +You should have received a copy of the GNU General Public License +along with this program. If not, see . +**************************************************************************************************/ + #ifndef VARREPLACER_H #define VARREPLACER_H diff --git a/src/sat/cryptominisat2/XorFinder.cpp b/src/sat/cryptominisat2/XorFinder.cpp index c61a12d..1dabb10 100644 --- a/src/sat/cryptominisat2/XorFinder.cpp +++ b/src/sat/cryptominisat2/XorFinder.cpp @@ -105,7 +105,7 @@ uint XorFinder::findXors(uint& sumLengths) switch(lits.size()) { case 2: { - S->toReplace->replace(lits, impair, old_group); + S->varReplacer->replace(lits, impair, old_group); #ifdef VERBOSE_DEBUG XorClause* x = XorClause_new(lits, impair, old_group); diff --git a/src/sat/cryptominisat2/constants.h b/src/sat/cryptominisat2/constants.h index f429650..0633f0f 100644 --- a/src/sat/cryptominisat2/constants.h +++ b/src/sat/cryptominisat2/constants.h @@ -1,3 +1,23 @@ +/****************************************************************************************[Solver.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +glucose -- Gilles Audemard, Laurent Simon (2008) + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + #define RATIOREMOVECLAUSES 2 #define NBCLAUSESBEFOREREDUCE 20000 #define DYNAMICNBLEVEL diff --git a/src/sat/cryptominisat2/time_mem.h b/src/sat/cryptominisat2/time_mem.h index 1e09812..a4c6552 100644 --- a/src/sat/cryptominisat2/time_mem.h +++ b/src/sat/cryptominisat2/time_mem.h @@ -1,3 +1,23 @@ +/****************************************************************************************[Solver.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + #ifndef TIME_MEM_H #define TIME_MEM_H