}
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);
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("-");
+/***********************************************************************************
+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 <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
#include "ClauseCleaner.h"
namespace MINISAT
vec<Lit> 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
+/***********************************************************************************
+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 <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
#include "Conglomerate.h"
#include "Solver.h"
#include "VarReplacer.h"
for (Lit* it = &(S->trail[0]), *end = it + S->trail.size(); it != end; it++)
blocked[it->var()] = true;
- const vec<Clause*>& clauses = S->toReplace->getClauses();
+ const vec<Clause*>& 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++) {
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;
+/***********************************************************************************
+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 <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
#ifndef CONGLOMERATE_H
#define CONGLOMERATE_H
+/***********************************************************************************
+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 <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
#include "FindUndef.h"
#include "Solver.h"
}
}
- vector<Var> replacingVars = S.toReplace->getReplacingVars();
+ vector<Var> replacingVars = S.varReplacer->getReplacingVars();
for (Var *it = &replacingVars[0], *end = it + replacingVars.size(); it != end; it++) {
if (isPotential[*it]) {
isPotential[*it] = false;
+/***********************************************************************************
+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 <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
#ifndef FINDUNDEF_H
#define FINDUNDEF_H
#include "Clause.h"
#include <algorithm>
#include "ClauseCleaner.h"
+
using std::ostream;
using std::cout;
using std::endl;
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;
{
using namespace MINISAT;
+#ifdef VERBOSE_DEBUG
using std::vector;
using std::cout;
using std::endl;
+#endif
class Clause;
}
}
-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<Lit>& v);
};
//#define VERBOSE_DEBUG
-#ifdef VERBOSE_DEBUG
using std::cout;
using std::endl;
-#endif
//#define PART_FINDING
const Var fingerprint2 = xorFingerprintInMatrix[ai2];
if (((fingerprint & fingerprint2) == fingerprint) && firstPartOfSecond(**a, **a2)) {
cout << "First part of second:" << endl;
- (*a)->plain_print();
- (*a2)->plain_print();
+ (*a)->plainPrint();
+ (*a2)->plainPrint();
cout << "END" << endl;
}
}
+/***********************************************************************************
+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 <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
#include "PackedRow.h"
namespace MINISAT
{
#include "XorFinder.h"
#include "ClauseCleaner.h"
-//#define DEBUG_LIB
-
-#ifdef DEBUG_LIB
-#include <sstream>
-FILE* myoutputfile;
-static uint numcalled = 0;
-#endif //DEBUG_LIB
-
namespace MINISAT
{
using namespace MINISAT;
, 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]);
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);
}
//=================================================================================================
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;
}
bool Solver::addXorClause(vec<Lit>& 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);
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();
}
}
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: {
xorclauses.push(c);
attachClause(*c);
if (!internal)
- toReplace->newClause();
+ varReplacer->newClause();
break;
}
}
{
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);
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();
}
}
clauses.push(c);
attachClause(*c);
- toReplace->newClause();
+ varReplacer->newClause();
}
return true;
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)
sort(learnts, reduceDB_lt());
for (int i = learnts.size()-1; i >= 0 ; i--) {
- learnts[i]->plain_print(outfile);
+ learnts[i]->plainPrint(outfile);
}
fclose(outfile);
}
lbool Solver::solve(const vec<Lit>& 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();
conglomerate->addRemovedClauses();
if (performReplace) {
- toReplace->performReplace();
+ varReplacer->performReplace();
if (!ok) return l_False;
}
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;
}
}
}
if (performReplace) {
- toReplace->performReplace();
+ varReplacer->performReplace();
if (!ok) return l_False;
}
}
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);
}
if (!final) {
printf("unsatisfied clause: ");
- printClause(*xorclauses[i]);
- printf("\n");
+ xorclauses[i]->plainPrint();
failed = true;
}
}
goto next;
printf("unsatisfied clause: ");
- printClause(*clauses[i]);
- printf("\n");
+ clauses[i]->plainPrint();
failed = true;
next:
;
#include <cstdio>
#include <string.h>
+#include <stdio.h>
#include "mtl/Vec.h"
#include "mtl/Heap.h"
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<Clause*>& 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<Clause*>& get_learnts() const; //Get all learnt clauses
+ 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 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<Gaussian*> gauss_matrixes;
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:
//
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:
//
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<XorClause*>& cs) const;
void checkLiteralCount();
CryptoMiniSat
-SVN revision: 579
-GIT revision: d7ef400c6dbb9bc0b6b3fd98a0c43b178916a849
+SVN revision: 586
+GIT revision: 8b5929ba71ceaf5bf6c905436cde96e640bee4b7
+/***********************************************************************************
+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 <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
#include "VarReplacer.h"
#include "Solver.h"
+/***********************************************************************************
+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 <http://www.gnu.org/licenses/>.
+**************************************************************************************************/
+
#ifndef VARREPLACER_H
#define VARREPLACER_H
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);
+/****************************************************************************************[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
+/****************************************************************************************[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
projects / francis / stp.git / commitdiff