diff options
Diffstat (limited to 'src/prop/cryptominisat/Solver/SolverMisc.cpp')
-rw-r--r-- | src/prop/cryptominisat/Solver/SolverMisc.cpp | 713 |
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"); + } +} |