summaryrefslogtreecommitdiff
path: root/src/prop/cryptominisat/Solver/SolverMisc.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/cryptominisat/Solver/SolverMisc.cpp')
-rw-r--r--src/prop/cryptominisat/Solver/SolverMisc.cpp713
1 files changed, 713 insertions, 0 deletions
diff --git a/src/prop/cryptominisat/Solver/SolverMisc.cpp b/src/prop/cryptominisat/Solver/SolverMisc.cpp
new file mode 100644
index 000000000..c2007af2e
--- /dev/null
+++ b/src/prop/cryptominisat/Solver/SolverMisc.cpp
@@ -0,0 +1,713 @@
+/***************************************************************************
+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 "Solver.h"
+#include "VarReplacer.h"
+#include "Subsumer.h"
+#include "XorSubsumer.h"
+#include "time_mem.h"
+#include "DimacsParser.h"
+#include "FailedLitSearcher.h"
+#include "DataSync.h"
+#include "SCCFinder.h"
+#include <iomanip>
+#include <omp.h>
+
+#ifdef USE_GAUSS
+#include "Gaussian.h"
+#endif
+
+#ifndef _MSC_VER
+#include <sys/time.h>
+#include <sys/resource.h>
+#endif
+
+using namespace CMSat;
+
+static const int space = 10;
+
+bool Solver::dumpSortedLearnts(const std::string& fileName, const uint32_t maxSize)
+{
+ FILE* outfile = fopen(fileName.c_str(), "w");
+ if (!outfile)
+ return false;
+
+ fprintf(outfile, "c \nc ---------\n");
+ fprintf(outfile, "c unitaries\n");
+ fprintf(outfile, "c ---------\n");
+ for (uint32_t i = 0, end = (trail_lim.size() > 0) ? trail_lim[0] : trail.size() ; i < end; i++) {
+ trail[i].printFull(outfile);
+ }
+
+ fprintf(outfile, "c conflicts %lu\n", (unsigned long)conflicts);
+ if (maxSize == 1) goto end;
+
+ fprintf(outfile, "c \nc ---------------------------------\n");
+ fprintf(outfile, "c learnt binary clauses (extracted from watchlists)\n");
+ fprintf(outfile, "c ---------------------------------\n");
+ dumpBinClauses(true, false, outfile);
+
+ fprintf(outfile, "c \nc ---------------------------------------\n");
+ fprintf(outfile, "c clauses representing 2-long XOR clauses\n");
+ fprintf(outfile, "c ---------------------------------------\n");
+ {
+ const vector<Lit>& table = varReplacer->getReplaceTable();
+ for (Var var = 0; var != table.size(); var++) {
+ Lit lit = table[var];
+ if (lit.var() == var)
+ continue;
+
+ fprintf(outfile, "%s%d %d 0\n", (!lit.sign() ? "-" : ""), lit.var()+1, var+1);
+ fprintf(outfile, "%s%d -%d 0\n", (lit.sign() ? "-" : ""), lit.var()+1, var+1);
+ }
+ }
+ fprintf(outfile, "c \nc --------------------\n");
+ fprintf(outfile, "c clauses from learnts\n");
+ fprintf(outfile, "c --------------------\n");
+ if (lastSelectedRestartType == dynamic_restart)
+ std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltGlucose());
+ else
+ std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltMiniSat());
+ for (int i = learnts.size()-1; i >= 0 ; i--) {
+ if (learnts[i]->size() <= maxSize) {
+ learnts[i]->print(outfile);
+ }
+ }
+
+ end:
+
+ fclose(outfile);
+ return true;
+}
+
+void Solver::printStrangeBinLit(const Lit lit) const
+{
+ const vec<Watched>& ws = watches[(~lit).toInt()];
+ for (vec<Watched>::const_iterator it2 = ws.getData(), end2 = ws.getDataEnd(); it2 != end2; it2++) {
+ if (it2->isBinary()) {
+ std::cout << "bin: " << lit << " , " << it2->getOtherLit() << " learnt : " << (it2->getLearnt()) << std::endl;
+ } else if (it2->isTriClause()) {
+ std::cout << "tri: " << lit << " , " << it2->getOtherLit() << " , " << (it2->getOtherLit2()) << std::endl;
+ } else if (it2->isClause()) {
+ std::cout << "cla:" << it2->getNormOffset() << std::endl;
+ } else {
+ assert(it2->isXorClause());
+ std::cout << "xor:" << it2->getXorOffset() << std::endl;
+ }
+ }
+}
+
+uint32_t Solver::countNumBinClauses(const bool alsoLearnt, const bool alsoNonLearnt) const
+{
+ uint32_t num = 0;
+
+ uint32_t wsLit = 0;
+ for (const vec<Watched> *it = watches.getData(), *end = watches.getDataEnd(); it != end; it++, wsLit++) {
+ const vec<Watched>& ws = *it;
+ for (vec<Watched>::const_iterator it2 = ws.getData(), end2 = ws.getDataEnd(); it2 != end2; it2++) {
+ if (it2->isBinary()) {
+ if (it2->getLearnt()) num += alsoLearnt;
+ else num+= alsoNonLearnt;
+ }
+ }
+ }
+
+ assert(num % 2 == 0);
+ return num/2;
+}
+
+void Solver::dumpBinClauses(const bool alsoLearnt, const bool alsoNonLearnt, FILE* outfile) const
+{
+ uint32_t wsLit = 0;
+ for (const vec<Watched> *it = watches.getData(), *end = watches.getDataEnd(); it != end; it++, wsLit++) {
+ Lit lit = ~Lit::toLit(wsLit);
+ const vec<Watched>& ws = *it;
+ for (vec<Watched>::const_iterator it2 = ws.getData(), end2 = ws.getDataEnd(); it2 != end2; it2++) {
+ if (it2->isBinary() && lit.toInt() < it2->getOtherLit().toInt()) {
+ bool toDump = false;
+ if (it2->getLearnt() && alsoLearnt) toDump = true;
+ if (!it2->getLearnt() && alsoNonLearnt) toDump = true;
+
+ if (toDump) it2->dump(outfile, lit);
+ }
+ }
+ }
+}
+
+uint32_t Solver::getBinWatchSize(const bool alsoLearnt, const Lit lit)
+{
+ uint32_t num = 0;
+ const vec<Watched>& ws = watches[lit.toInt()];
+ for (vec<Watched>::const_iterator it2 = ws.getData(), end2 = ws.getDataEnd(); it2 != end2; it2++) {
+ if (it2->isBinary() && (alsoLearnt || !it2->getLearnt())) {
+ num++;
+ }
+ }
+
+ return num;
+}
+
+void Solver::printBinClause(const Lit litP1, const Lit litP2, FILE* outfile) const
+{
+ if (value(litP1) == l_True) {
+ litP1.printFull(outfile);
+ } else if (value(litP1) == l_False) {
+ litP2.printFull(outfile);
+ } else if (value(litP2) == l_True) {
+ litP2.printFull(outfile);
+ } else if (value(litP2) == l_False) {
+ litP1.printFull(outfile);
+ } else {
+ litP1.print(outfile);
+ litP2.printFull(outfile);
+ }
+}
+
+bool Solver::dumpOrigClauses(const std::string& fileName) const
+{
+ FILE* outfile;
+ if (fileName != std::string("stdout")) {
+ outfile = fopen(fileName.c_str(), "w");
+ if (!outfile)
+ return false;
+ } else {
+ outfile = stdout;
+ }
+
+ uint32_t numClauses = 0;
+ //unitary clauses
+ for (uint32_t i = 0, end = (trail_lim.size() > 0) ? trail_lim[0] : trail.size() ; i < end; i++)
+ numClauses++;
+
+ //binary XOR clauses
+ const vector<Lit>& table = varReplacer->getReplaceTable();
+ for (Var var = 0; var != table.size(); var++) {
+ Lit lit = table[var];
+ if (lit.var() == var)
+ continue;
+ numClauses += 2;
+ }
+
+ //binary normal clauses
+ numClauses += countNumBinClauses(false, true);
+
+ //normal clauses
+ numClauses += clauses.size();
+
+ //xor clauses
+ numClauses += xorclauses.size();
+
+ //previously eliminated clauses
+ const map<Var, vector<vector<Lit> > >& elimedOutVar = subsumer->getElimedOutVar();
+ for (map<Var, vector<vector<Lit> > >::const_iterator it = elimedOutVar.begin(); it != elimedOutVar.end(); it++) {
+ const vector<vector<Lit> >& cs = it->second;
+ numClauses += cs.size();
+ }
+ const map<Var, vector<std::pair<Lit, Lit> > >& elimedOutVarBin = subsumer->getElimedOutVarBin();
+ for (map<Var, vector<std::pair<Lit, Lit> > >::const_iterator it = elimedOutVarBin.begin(); it != elimedOutVarBin.end(); it++) {
+ numClauses += it->second.size();
+ }
+
+ const map<Var, vector<XorSubsumer::XorElimedClause> >& xorElimedOutVar = xorSubsumer->getElimedOutVar();
+ for (map<Var, vector<XorSubsumer::XorElimedClause> >::const_iterator it = xorElimedOutVar.begin(); it != xorElimedOutVar.end(); it++) {
+ const vector<XorSubsumer::XorElimedClause>& cs = it->second;
+ numClauses += cs.size();
+ }
+
+ fprintf(outfile, "p cnf %d %d\n", nVars(), numClauses);
+
+ ////////////////////////////////////////////////////////////////////
+
+ fprintf(outfile, "c \nc ---------\n");
+ fprintf(outfile, "c unitaries\n");
+ fprintf(outfile, "c ---------\n");
+ for (uint32_t i = 0, end = (trail_lim.size() > 0) ? trail_lim[0] : trail.size() ; i < end; i++) {
+ trail[i].printFull(outfile);
+ }
+
+ fprintf(outfile, "c \nc ---------------------------------------\n");
+ fprintf(outfile, "c clauses representing 2-long XOR clauses\n");
+ fprintf(outfile, "c ---------------------------------------\n");
+ for (Var var = 0; var != table.size(); var++) {
+ Lit lit = table[var];
+ if (lit.var() == var)
+ continue;
+
+ Lit litP1 = ~lit;
+ Lit litP2 = Lit(var, false);
+ printBinClause(litP1, litP2, outfile);
+ printBinClause(~litP1, ~litP2, outfile);
+ }
+
+ fprintf(outfile, "c \nc ------------\n");
+ fprintf(outfile, "c binary clauses\n");
+ fprintf(outfile, "c ---------------\n");
+ dumpBinClauses(false, true, outfile);
+
+ fprintf(outfile, "c \nc ------------\n");
+ fprintf(outfile, "c normal clauses\n");
+ fprintf(outfile, "c ---------------\n");
+ for (Clause *const *i = clauses.getData(); i != clauses.getDataEnd(); i++) {
+ assert(!(*i)->learnt());
+ (*i)->print(outfile);
+ }
+
+ fprintf(outfile, "c \nc ------------\n");
+ fprintf(outfile, "c xor clauses\n");
+ fprintf(outfile, "c ---------------\n");
+ for (XorClause *const *i = xorclauses.getData(); i != xorclauses.getDataEnd(); i++) {
+ assert(!(*i)->learnt());
+ (*i)->print(outfile);
+ }
+
+ fprintf(outfile, "c -------------------------------\n");
+ fprintf(outfile, "c previously eliminated variables\n");
+ fprintf(outfile, "c -------------------------------\n");
+ for (map<Var, vector<vector<Lit> > >::const_iterator it = elimedOutVar.begin(); it != elimedOutVar.end(); it++) {
+ fprintf(outfile, "c ########### cls for eliminated var %d ### start\n", it->first + 1);
+ const vector<vector<Lit> >& cs = it->second;
+ for (vector<vector<Lit> >::const_iterator it2 = cs.begin(); it2 != cs.end(); it2++) {
+ printClause(outfile, *it2);
+ }
+ fprintf(outfile, "c ########### cls for eliminated var %d ### finish\n", it->first + 1);
+ }
+ for (map<Var, vector<std::pair<Lit, Lit> > >::const_iterator it = elimedOutVarBin.begin(); it != elimedOutVarBin.end(); it++) {
+ for (uint32_t i = 0; i < it->second.size(); i++) {
+ it->second[i].first.print(outfile);
+ it->second[i].second.printFull(outfile);
+ }
+ }
+
+ fprintf(outfile, "c -------------------------------\n");
+ fprintf(outfile, "c previously xor-eliminated variables\n");
+ fprintf(outfile, "c -------------------------------\n");
+ for (map<Var, vector<XorSubsumer::XorElimedClause> >::const_iterator it = xorElimedOutVar.begin(); it != xorElimedOutVar.end(); it++) {
+ for (vector<XorSubsumer::XorElimedClause>::const_iterator it2 = it->second.begin(), end2 = it->second.end(); it2 != end2; it2++) {
+ it2->plainPrint(outfile);
+ }
+ }
+
+ if (fileName != "stdout") fclose(outfile);
+ return true;
+}
+
+vector<Lit> Solver::get_unitary_learnts() const
+{
+ vector<Lit> unitaries;
+ if (decisionLevel() > 0) {
+ for (uint32_t i = 0; i != trail_lim[0]; i++) {
+ unitaries.push_back(trail[i]);
+ }
+ }
+
+ return unitaries;
+}
+
+const vec<Clause*>& Solver::get_learnts() const
+{
+ return learnts;
+}
+
+const vec<Clause*>& Solver::get_sorted_learnts()
+{
+ if (lastSelectedRestartType == dynamic_restart)
+ std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltGlucose());
+ else
+ std::sort(learnts.getData(), learnts.getData()+learnts.size(), reduceDB_ltMiniSat());
+ return learnts;
+}
+
+uint32_t Solver::getNumElimSubsume() const
+{
+ return subsumer->getNumElimed();
+}
+
+uint32_t Solver::getNumElimXorSubsume() const
+{
+ return xorSubsumer->getNumElimed();
+}
+
+uint32_t Solver::getNumXorTrees() const
+{
+ return varReplacer->getNumTrees();
+}
+
+uint32_t Solver::getNumXorTreesCrownSize() const
+{
+ return varReplacer->getNumReplacedVars();
+}
+
+double Solver::getTotalTimeSubsumer() const
+{
+ return subsumer->getTotalTime();
+}
+
+double Solver::getTotalTimeFailedLitSearcher() const
+{
+ return failedLitSearcher->getTotalTime();
+}
+
+double Solver::getTotalTimeXorSubsumer() const
+{
+ return xorSubsumer->getTotalTime();
+}
+
+double Solver::getTotalTimeSCC() const
+{
+ return sCCFinder->getTotalTime();
+}
+
+void Solver::printStatHeader() const
+{
+ if (conf.verbosity >= 2) {
+ std::cout << "c "
+ << "========================================================================================="
+ << std::endl;
+ std::cout << "c"
+ << " types(t): F = full restart, N = normal restart" << std::endl;
+ std::cout << "c"
+ << " types(t): S = simplification begin/end, E = solution found" << std::endl;
+ std::cout << "c"
+ << " restart types(rt): st = static, dy = dynamic" << std::endl;
+
+ std::cout << "c "
+ << std::setw(2) << "t"
+ << std::setw(3) << "rt"
+ << std::setw(6) << "Rest"
+ << std::setw(space) << "Confl"
+ << std::setw(space) << "Vars"
+ << std::setw(space) << "NormCls"
+ << std::setw(space) << "XorCls"
+ << std::setw(space) << "BinCls"
+ << std::setw(space) << "Learnts"
+ << std::setw(space) << "ClLits"
+ << std::setw(space) << "LtLits"
+ << std::setw(space) << "LGlueHist"
+ << std::setw(space) << "SGlueHist"
+ << std::endl;
+ }
+}
+
+void Solver::printRestartStat(const char* type)
+{
+ if (conf.verbosity >= 2) {
+ //printf("c | %9d | %7d %8d %8d | %8d %8d %6.0f |", (int)conflicts, (int)order_heap.size(), (int)(nClauses()-nbBin), (int)clauses_literals, (int)(nbclausesbeforereduce*curRestart+nbCompensateSubsumer), (int)(nLearnts()+nbBin), (double)learnts_literals/(double)(nLearnts()+nbBin));
+
+ std::cout << "c "
+ << std::setw(2) << type
+ << std::setw(3) << ((restartType == static_restart) ? "st" : "dy")
+ << std::setw(6) << starts
+ << std::setw(space) << conflicts
+ << std::setw(space) << order_heap.size()
+ << std::setw(space) << clauses.size()
+ << std::setw(space) << xorclauses.size()
+ << std::setw(space) << numBins
+ << std::setw(space) << learnts.size()
+ << std::setw(space) << clauses_literals
+ << std::setw(space) << learnts_literals;
+
+ if (glueHistory.getTotalNumeElems() > 0) {
+ std::cout << std::setw(space) << std::fixed << std::setprecision(2) << glueHistory.getAvgAllDouble();
+ } else {
+ std::cout << std::setw(space) << "no data";
+ }
+ if (glueHistory.isvalid()) {
+ std::cout << std::setw(space) << std::fixed << std::setprecision(2) << glueHistory.getAvgDouble();
+ } else {
+ std::cout << std::setw(space) << "no data";
+ }
+
+ #ifdef RANDOM_LOOKAROUND_SEARCHSPACE
+ if (conf.doPrintAvgBranch) {
+ if (avgBranchDepth.isvalid())
+ std::cout << std::setw(space) << avgBranchDepth.getAvgUInt();
+ else
+ std::cout << std::setw(space) << "no data";
+ }
+ #endif //RANDOM_LOOKAROUND_SEARCHSPACE
+
+ #ifdef USE_GAUSS
+ print_gauss_sum_stats();
+ #endif //USE_GAUSS
+
+ std::cout << std::endl;
+ }
+}
+
+void Solver::printEndSearchStat()
+{
+ if (conf.verbosity >= 1) {
+ printRestartStat("E");
+ }
+}
+
+#ifdef USE_GAUSS
+void Solver::print_gauss_sum_stats()
+{
+ if (gauss_matrixes.size() == 0 && conf.verbosity >= 2) {
+ std::cout << " --";
+ return;
+ }
+
+ uint32_t called = 0;
+ uint32_t useful_prop = 0;
+ uint32_t useful_confl = 0;
+ uint32_t disabled = 0;
+ for (vector<Gaussian*>::const_iterator gauss = gauss_matrixes.begin(), end= gauss_matrixes.end(); gauss != end; gauss++) {
+ disabled += (*gauss)->get_disabled();
+ called += (*gauss)->get_called();
+ useful_prop += (*gauss)->get_useful_prop();
+ useful_confl += (*gauss)->get_useful_confl();
+ sum_gauss_unit_truths += (*gauss)->get_unit_truths();
+ //gauss->print_stats();
+ //gauss->print_matrix_stats();
+ }
+ sum_gauss_called += called;
+ sum_gauss_confl += useful_confl;
+ sum_gauss_prop += useful_prop;
+
+ if (conf.verbosity >= 2) {
+ if (called == 0) {
+ std::cout << " --";
+ } else {
+ std::cout << " "
+ << std::fixed << std::setprecision(1) << std::setw(5)
+ << ((double)useful_prop/(double)called*100.0) << "% "
+ << std::fixed << std::setprecision(1) << std::setw(5)
+ << ((double)useful_confl/(double)called*100.0) << "% "
+ << std::fixed << std::setprecision(1) << std::setw(5)
+ << (100.0-(double)disabled/(double)gauss_matrixes.size()*100.0) << "%";
+ }
+ }
+}
+#endif //USE_GAUSS
+
+/**
+@brief Sorts the watchlists' clauses as: binary, tertiary, normal, xor
+*/
+void Solver::sortWatched()
+{
+ #ifdef VERBOSE_DEBUG
+ std::cout << "Sorting watchlists:" << std::endl;
+ #endif
+ double myTime = cpuTime();
+ for (vec<Watched> *i = watches.getData(), *end = watches.getDataEnd(); i != end; i++) {
+ if (i->size() == 0) continue;
+ #ifdef VERBOSE_DEBUG
+ vec<Watched>& ws = *i;
+ std::cout << "Before sorting:" << std::endl;
+ for (uint32_t i2 = 0; i2 < ws.size(); i2++) {
+ if (ws[i2].isBinary()) std::cout << "Binary,";
+ if (ws[i2].isTriClause()) std::cout << "Tri,";
+ if (ws[i2].isClause()) std::cout << "Normal,";
+ if (ws[i2].isXorClause()) std::cout << "Xor,";
+ }
+ std::cout << std::endl;
+ #endif //VERBOSE_DEBUG
+
+ std::sort(i->getData(), i->getDataEnd(), WatchedSorter());
+
+ #ifdef VERBOSE_DEBUG
+ std::cout << "After sorting:" << std::endl;
+ for (uint32_t i2 = 0; i2 < ws.size(); i2++) {
+ if (ws[i2].isBinary()) std::cout << "Binary,";
+ if (ws[i2].isTriClause()) std::cout << "Tri,";
+ if (ws[i2].isClause()) std::cout << "Normal,";
+ if (ws[i2].isXorClause()) std::cout << "Xor,";
+ }
+ std::cout << std::endl;
+ #endif //VERBOSE_DEBUG
+ }
+
+ if (conf.verbosity >= 3) {
+ std::cout << "c watched "
+ << "sorting time: " << cpuTime() - myTime
+ << std::endl;
+ }
+}
+
+void Solver::addSymmBreakClauses()
+{
+ if (xorclauses.size() > 0) {
+ std::cout << "c xor clauses present -> no saucy" << std::endl;
+ return;
+ }
+ double myTime = cpuTime();
+ std::cout << "c Doing saucy" << std::endl;
+ dumpOrigClauses("origProblem.cnf");
+
+ int rvalue;
+ rvalue= system("grep -v \"^c\" origProblem.cnf > origProblem2.cnf");
+ if (rvalue >= 2) { // unsuccessful grep in POSIX standard
+ std::cout << "c impossible to complete saucy" << std::endl;
+ return;
+ }
+ rvalue= system("python saucyReader.py origProblem2.cnf > output");
+ if (rvalue != 0) { // unsuccessful saucyReader.py
+ std::cout << "c impossible to complete saucy" << std::endl;
+ return;
+ }
+
+
+ DimacsParser parser(this, false, false, false, true);
+
+ #ifdef DISABLE_ZLIB
+ FILE * in = fopen("output", "rb");
+ #else
+ gzFile in = gzopen("output", "rb");
+ #endif // DISABLE_ZLIB
+ parser.parse_DIMACS(in);
+ #ifdef DISABLE_ZLIB
+ fclose(in);
+ #else
+ gzclose(in);
+ #endif // DISABLE_ZLIB
+ std::cout << "c Finished saucy, time: " << (cpuTime() - myTime) << std::endl;
+}
+
+/**
+@brief Pretty-prints a literal
+*/
+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'));
+}
+
+/**
+@brief Sets that we need a CNF file that documents all commands
+
+newVar() and addClause(), addXorClause() commands are logged to this CNF
+file and then can be re-read with special arguments to the main program. This
+can help simulate a segfaulting library-call
+*/
+bool Solver::needLibraryCNFFile(const std::string& fileName)
+{
+ libraryCNFFile = fopen(fileName.c_str(), "w");
+ return libraryCNFFile != NULL;
+}
+
+template<class T, class T2>
+void Solver::printStatsLine(std::string left, T value, T2 value2, std::string extra)
+{
+ std::cout << std::fixed << std::left << std::setw(27) << left << ": " << std::setw(11) << std::setprecision(2) << value << " (" << std::left << std::setw(9) << std::setprecision(2) << value2 << " " << extra << ")" << std::endl;
+}
+
+template<class T>
+void Solver::printStatsLine(std::string left, T value, std::string extra)
+{
+ std::cout << std::fixed << std::left << std::setw(27) << left << ": " << std::setw(11) << std::setprecision(2) << value << extra << std::endl;
+}
+
+/**
+@brief prints the statistics line at the end of solving
+
+Prints all sorts of statistics, like number of restarts, time spent in
+SatELite-type simplification, number of unit claues found, etc.
+*/
+void Solver::printStats()
+{
+ double cpu_time = cpuTime();
+ uint64_t mem_used = memUsed();
+
+ int numThreads = omp_get_num_threads();
+ if (numThreads > 1) {
+ std::cout << "c Following stats are for *FIRST FINISHED THREAD ONLY*" << std::endl;
+ #if !defined(_MSC_VER) && !defined(RUSAGE_THREAD)
+ std::cout << "c There is no platform-independent way to measure time per thread" << std::endl;
+ std::cout << "c All times indicated are sum of ALL threads" << std::endl;
+ std::cout << "c Use a utilty provided by your platform to get total thread time, etc." << std::endl;
+ #endif
+ }
+ printStatsLine("c num threads" , numThreads);
+
+ //Restarts stats
+ printStatsLine("c restarts", starts);
+ printStatsLine("c dynamic restarts", dynStarts);
+ printStatsLine("c static restarts", staticStarts);
+ printStatsLine("c full restarts", fullStarts);
+ printStatsLine("c total simplify time", totalSimplifyTime);
+
+ //Learnts stats
+ printStatsLine("c learnts DL2", nbGlue2);
+ printStatsLine("c learnts size 2", numNewBin);
+ printStatsLine("c learnts size 1", get_unitary_learnts_num(), (double)get_unitary_learnts_num()/(double)nVars()*100.0, "% of vars");
+ printStatsLine("c filedLit time", getTotalTimeFailedLitSearcher(), getTotalTimeFailedLitSearcher()/cpu_time*100.0, "% time");
+
+ //Subsumer stats
+ printStatsLine("c v-elim SatELite", getNumElimSubsume(), (double)getNumElimSubsume()/(double)nVars()*100.0, "% vars");
+ printStatsLine("c SatELite time", getTotalTimeSubsumer(), getTotalTimeSubsumer()/cpu_time*100.0, "% time");
+
+ //XorSubsumer stats
+ printStatsLine("c v-elim xor", getNumElimXorSubsume(), (double)getNumElimXorSubsume()/(double)nVars()*100.0, "% vars");
+ printStatsLine("c xor elim time", getTotalTimeXorSubsumer(), getTotalTimeXorSubsumer()/cpu_time*100.0, "% time");
+
+ //VarReplacer stats
+ printStatsLine("c num binary xor trees", getNumXorTrees());
+ printStatsLine("c binxor trees' crown", getNumXorTreesCrownSize(), (double)getNumXorTreesCrownSize()/(double)getNumXorTrees(), "leafs/tree");
+ printStatsLine("c bin xor find time", getTotalTimeSCC());
+
+ //OTF clause improvement stats
+ printStatsLine("c OTF clause improved", improvedClauseNo, (double)improvedClauseNo/(double)conflicts, "clauses/conflict");
+ printStatsLine("c OTF impr. size diff", improvedClauseSize, (double)improvedClauseSize/(double)improvedClauseNo, " lits/clause");
+
+ //Clause-shrinking through watchlists
+ printStatsLine("c OTF cl watch-shrink", numShrinkedClause, (double)numShrinkedClause/(double)conflicts, "clauses/conflict");
+ printStatsLine("c OTF cl watch-sh-lit", numShrinkedClauseLits, (double)numShrinkedClauseLits/(double)numShrinkedClause, " lits/clause");
+ printStatsLine("c tried to recurMin cls", moreRecurMinLDo, (double)moreRecurMinLDo/(double)conflicts*100.0, " % of conflicts");
+ printStatsLine("c updated cache", updateTransCache, updateTransCache/(double)moreRecurMinLDo, " lits/tried recurMin");
+
+ //Multi-threading
+ if (numThreads > 1) {
+ printStatsLine("c unit cls received", dataSync->getRecvUnitData(), (double)dataSync->getRecvUnitData()/(double)get_unitary_learnts_num()*100.0, "% of units");
+ printStatsLine("c unit cls sent", dataSync->getSentUnitData(), (double)dataSync->getSentUnitData()/(double)get_unitary_learnts_num()*100.0, "% of units");
+ printStatsLine("c bin cls received", dataSync->getRecvBinData());
+ printStatsLine("c bin cls sent", dataSync->getSentBinData());
+ }
+
+ #ifdef USE_GAUSS
+ if (gaussconfig.decision_until > 0) {
+ std::cout << "c " << std::endl;
+ printStatsLine("c gauss unit truths ", get_sum_gauss_unit_truths());
+ printStatsLine("c gauss called", get_sum_gauss_called());
+ printStatsLine("c gauss conflicts ", get_sum_gauss_confl(), (double)get_sum_gauss_confl() / (double)get_sum_gauss_called() * 100.0, " %");
+ printStatsLine("c gauss propagations ", get_sum_gauss_prop(), (double)get_sum_gauss_prop() / (double)get_sum_gauss_called() * 100.0, " %");
+ printStatsLine("c gauss useful", ((double)get_sum_gauss_prop() + (double)get_sum_gauss_confl())/ (double)get_sum_gauss_called() * 100.0, " %");
+ std::cout << "c " << std::endl;
+ }
+ #endif
+
+ printStatsLine("c clauses over max glue", nbClOverMaxGlue, (double)nbClOverMaxGlue/(double)conflicts*100.0, "% of all clauses");
+
+ //Search stats
+ printStatsLine("c conflicts", conflicts, (double)conflicts/cpu_time, "/ sec");
+ printStatsLine("c decisions", decisions, (double)rnd_decisions*100.0/(double)decisions, "% random");
+ printStatsLine("c bogo-props", propagations, (double)propagations/cpu_time, "/ sec");
+ printStatsLine("c conflict literals", tot_literals, (double)(max_literals - tot_literals)*100.0/ (double)max_literals, "% deleted");
+
+ //General stats
+ printStatsLine("c Memory used", (double)mem_used / 1048576.0, " MB");
+ if (numThreads > 1) {
+ #if !defined(_MSC_VER) && defined(RUSAGE_THREAD)
+ printStatsLine("c single-thread CPU time", cpu_time, " s");
+ printStatsLine("c all-threads sum CPU time", cpuTimeTotal(), " s");
+ #else
+ printStatsLine("c all-threads sum CPU time", cpu_time, " s");
+ #endif
+ } else {
+ printStatsLine("c CPU time", cpu_time, " s");
+ }
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback