OKlibrary  0.2.1.6
CreateStatistic.cpp
Go to the documentation of this file.
00001 // Oliver Kullmann, 3.7.2002 (Swansea)
00002 /* Copyright 2002 - 2007 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00013 #include <string>
00014 #include <algorithm>
00015 #include <memory>
00016 #include <iostream>
00017 #include <vector>
00018 #include <map>
00019 #include <cmath>
00020 #include <fstream>
00021 #include <sstream>
00022 #include <ostream>
00023 #include <limits>
00024 #include <cmath>
00025 #include <cassert>
00026 #include <numeric>
00027 #include <iomanip>
00028 
00029 #include <boost/test/floating_point_comparison.hpp>
00030 
00031 #include <OKlib/General/DatabaseHandler01.hpp>
00032 #include <OKlib/General/TimeHandling.hpp>
00033 #include <OKlib/General/Kommandozeile.hpp>
00034 #include <OKlib/General/Algorithms.hpp>
00035 #include <OKlib/General/ErrorHandling.hpp>
00036 
00037 using namespace DatabaseHandler01;
00038 using namespace StringHandling;
00039 using namespace TimeHandling;
00040 
00041 namespace {
00042 
00043 // Messages -----------------------------------
00044 
00045 char *Selbst = "CreateStatistic";
00046 
00047 const int number_languages = 2;
00048 KMZ::Sprachen language = KMZ::Englisch;
00049 
00050 const char * const Version = "0.75";
00051 const char * const Datum = "30.7.2002";
00052 const char * const Autor = "Oliver Kullmann (Swansea); O.Kullmann@Swansea.ac.uk";
00053 const char * const Uebersetzungsdatum = __DATE__ " " __TIME__;
00054 
00055 const char * const Meldungen[][number_languages] = {
00056   {"Einlesen der Tabelle bcls", // 0
00057    "Reading of table bcls"},
00058   {"Zeilen gelesen: ", // 1
00059    "Rows read: "},
00060   {"Geschaetzte Restzeit fuer diese Tabelle: ", // 2
00061    "Estimated remaining time for this table: "},
00062   {"Bestimmung des maximalen Indexes von cls_id in Tabelle bcls.", // 3
00063    "Computation of the maximal index of cls_id in table bcls."},
00064   {"Bestimmung des maximalen Indexes von b_info_id in Tabelle bcls_info.", // 4
00065    "Computation of the maximal index of b_info_id in table bcls_info."},
00066   {"Einlesen der Tabelle bcls_info", // 5
00067    "Reading of table bcls_info"},
00068   {"Einlesen der Tabelle b_unit_reductions", // 6
00069    "Reading of table b_unit_reductions"},
00070   {"Der maximale index ist ", // 7
00071    "The maximal index is "},
00072   {"Berechnung der statistischen Werte.", // 8
00073    "Computation of statistical values."},
00074   {"Die gesamte Berechnung dauerte", // 9
00075    "The whole computation needed"},
00076   {"FEHLER in", // 10
00077    "ERROR in"},
00078   {"Erzeugte Dateien:", // 11
00079    "Files created:"},
00080   {"Erzeugte Tabellen:", // 12
00081    "Tables created:"},
00082   {"Erfolgreiche Beendung um", // 13
00083    "Successful completion at"},
00084   {"Begin um", // 14
00085    "Start at"},
00086   {"Berechnung der Mittelwerte fuer die erfuellbaren bzw. unerfuellbaren Klauselmengen.", // 15
00087    "Computation of mean values for satisfiable resp. unsatisfiable formulas."},
00088   {"Berechnung der Wahrscheinlichkeit von Erfuellbarkeit.", // 16
00089    "Computation of probability of satisfiability."},
00090   {"Hinzuziehung der Tabelle SatUnsatAggregates fuer Wahrscheinlichkeit von Erfuellbarkeit.", // 17
00091     "Additional reading of table SatUnsatAggregates for probability of satisfiability."},
00092   {"Neusortierung der Matrizen.", // 18
00093    "New sorting of the matrices."},
00094   {"Dateien-Ausgabe", // 19
00095    "File output"},
00096   {"Tabellen in der Datenbank aktualisieren.", // 20
00097    "Updating of tables in database."},
00098   {"(Nochmaliges) Einlesen der Tabelle bcls_info zur Berechnung des Medians der Knotenanzahl.", // 21
00099    "(Second) reading of table bcls_info to compute the median of the node numbers."},
00100   {"Platz reservieren fuer die Berechnung des Medians der Knoten-Anzahlen.", // 22
00101    "Reserving space for the computation of the median values for the node counts."},
00102   {"Bereitstellung des Speicherplatzes fuer den Index der Tabelle bcls_info.", // 23
00103    "Preparation of space for the index of table bcsl_info."},
00104 };
00105 
00106 
00107 // global constants -------------------------------------
00108 
00109 const std::string database = "OKRandGen";
00110 const std::string SQL_true = "t";
00111 
00112 const std::string dim = "1";
00113 const unsigned int p = 3; // can be other values
00114 const std::string length = "{" + toString(p) + "}";
00115 // given dim and length, the frame_id is uniquely determined
00116 
00117 const std::string table_densities = "bd_" + dim;
00118 
00119 // output files
00120 
00121 const std::string directory = "/h/21/GemeinsameBasis/SAT-Algorithmen/RandomExperiments/Data";
00122 
00123 const std::string extension = ".csv";
00124 
00125 const std::string output_sat = directory + "/" + "OKgp" + toString(p) + "alleS" + extension;
00126 const std::string output_unsat = directory + "/" + "OKgp" + toString(p) + "alleU" + extension;
00127 const std::string output_stat_sat = directory + "/" + "OKgp" + toString(p) + "prob" + extension;
00128 
00129 // output tables
00130 
00131 const std::string output_table_sat = "statsatp" + toString(p);
00132 const std::string output_table_unsat = "statunsatp" + toString(p);
00133 const std::string output_table_prob = "probsatp" + toString(p);
00134 
00135 // formatting data
00136 
00137 const std::string separator = ",";
00138 
00139 const std::string null_sql = "NULL";
00140 const std::string null_r = "NA";
00141 
00142 const unsigned int precision = std::numeric_limits<double>::digits10;
00143 
00144 // minimal resolution complexity for unsatisfiable clause-sets
00145 
00146 inline unsigned int small_2_pow(unsigned int e) {
00147   return 1U << e;
00148 }
00149 const unsigned int min_complexity = small_2_pow(p-1) - 1;
00150 
00151 // buffer sizes
00152 
00153 const int cursor_step_bcls = 20000000;
00154 const int cursor_step_bcls_info = 10000000;
00155 const int cursor_step_b_unit_reductions = 20000000;
00156 const int cursor_step_intervalls = 20000000;
00157 const int cursor_step_bcls_info_median = 20000000;
00158 
00159 // watching the progress
00160 
00161 const int progress_step = 1000000;
00162 
00163 
00164 // querying the database -----------
00165 
00166 DatabaseHandler DH(database);
00167 Select Sel(DH);
00168 Command Comm(DH);
00169 
00170 
00171 // computation of maximal indices
00172 class Max_index {
00173 public :
00174   Max_index(const std::string& field, const std::string& table) {
00175     Sel.issue("select max(" + field + ") from " + table + ";");
00176     ++Sel;
00177     max = fromString<int>(Sel.value("max"));
00178   }
00179   operator int() const { return max; }
00180 private :
00181   int max;
00182 };
00183 
00184 
00185 // computation of the (unique) frame_id -----------------------
00186 
00187 class Frame_id {
00188 public :
00189   struct no_frame_id {};
00190   Frame_id() {
00191     TableHandler TFrames(DH, "frames");
00192     AllAttObj AFrames(TFrames);
00193     AFrames("l") << length;
00194     AFrames("dim") << dim; // for checking
00195     if (! TFrames.completion())
00196       throw no_frame_id();
00197     fi = Value(AFrames("frame_id"));
00198     nfi = fromString<int>(fi);
00199   }
00200   operator std::string() const { return fi; }
00201   operator int() const { return nfi; }
00202 private :
00203   std::string fi;
00204   int nfi;
00205 };
00206 
00207 // density handling -------------------------------------------
00208 
00209 struct density {
00210   bool fi; // whether equal to the unique frame identity or not
00211   std::string d1; // not as double to avoid rounding problems
00212   density(bool f, const std::string& d)
00213     : fi(f), d1(d) {}
00214   density() {}
00215 };
00216 
00217 class Densities {
00218   // the map from m_dens_id to densities
00219 public :
00220   Densities(const std::string& fi) {
00221     v.resize(Max_index("m_dens_id", table_densities) + 1);
00222     Sel.issue("select m_dens_id, frame_id, d1 from " + table_densities + ";");
00223     while (++Sel) {
00224       v[fromString<int>(Sel.value("m_dens_id"))] = density((std::string(Sel.value("frame_id")) == fi), Sel.value("d1"));
00225     }
00226   }
00227   const density& operator [] (int index) const {
00228     return v[index];
00229   }
00230 private :
00231   std::vector<density> v;
00232 };
00233 
00234 // handling of statistical values ----------------------------------------
00235 
00236 const std::string header_common = "n,d1,nds,count,depth,pl,aut,sn,qsn,l2r,an,countwa,ndswa,countws,ndsws,countwq,ndswq,maxnds,minnds,stdnds,mednds";
00237 const std::string header_unsat =  header_common + ",prm";
00238 const std::string header_sat = header_common + ",trv,nb,nl2r,ndswb";
00239 
00240 const std::string header_prob_sat = "n,d1,sat,c";
00241 
00242 class activate_median;
00243 
00244 class stat_values {
00245 public :
00246 
00247   stat_values()
00248     : nds(0), count(1), depth(0), pl(0), aut(0), sn(0), qsn(0), l2r(0), an(0),  countwa(0), ndswa(0), countws(0), ndsws(0), countwq(0), ndswq(0), maxnds(0), minnds(std::numeric_limits<double>::max()), stdnds(0), sum_sq_nds(0), vecndsp(0) {}
00249   virtual ~stat_values() {}
00250 
00251   virtual void enter_bcls_data(const Select& S) { ++count; }
00252 
00253   virtual void enter_bcls_info_data(const Select& S) {
00254     current_nds = fromString<double>(S.value("nodes"));
00255     nds += current_nds;
00256     current_depth = fromString<double>(S.value("tree_depth"));
00257     depth += current_depth;
00258     pl += fromString<double>(S.value("pure_literals"));
00259     const double current_aut = fromString<double>(S.value("real_autarkies"));
00260     aut += current_aut;
00261     const double current_sn = fromString<double>(S.value("single_nodes"));
00262     sn += current_sn;
00263     const double current_qsn = fromString<double>(S.value("quasi_s_nodes"));
00264     qsn += current_qsn;
00265     an += fromString<double>(S.value("an"));
00266     if (current_aut != 0) {
00267       ++countwa;
00268       ndswa += current_nds;
00269     }
00270     if (current_sn != 0) {
00271       ++countws;
00272       ndsws += current_nds;
00273     }
00274     if (current_qsn != 0) {
00275       ++countwq;
00276       ndswq += current_nds;
00277     }
00278     maxnds = std::max(maxnds, current_nds);
00279     minnds = std::min(minnds, current_nds);
00280     sum_sq_nds += current_nds * current_nds;
00281   }
00282 
00283   virtual void enter_b_unit_reductions_data(const Select& S) {
00284     current_l2r = fromString<double>(S.value("u_count"));
00285     l2r += current_l2r;
00286   }
00287 
00288   virtual void enter_bcls_info_mean_data(const Select& S) {
00289     vecndsp -> push_back(fromString<double>(S.value("nodes")));
00290   }
00291 
00292   virtual void compute_mean() {
00293     // must be called only once
00294     if (count != 1)
00295       stdnds = sqrt((count * sum_sq_nds - nds * nds) / count / (count - 1));
00296     nds /= count; depth /= count; pl /= count; aut /= count; sn /= count; qsn /= count; l2r /= count; an /= count;
00297     if (countwa != 0)
00298       ndswa /= countwa;
00299     if (countwq != 0)
00300       ndswq /= countwq;
00301     const std::vector<double> medianassert(*vecndsp);
00302     std::vector<double> medianasserttemp(*vecndsp);
00303     mednds = Algorithms::median_with_sorting(vecndsp -> begin(), vecndsp -> end());
00304     assert(mednds == Algorithms::median_with_sorting(medianasserttemp.begin(), medianasserttemp.end()));
00305     std::vector<double> medianassert2(*vecndsp);
00306     {
00307       assert(count == vecndsp -> size());
00308       assert(boost::test_tools::close_at_tolerance<double>(boost::test_tools::fraction_tolerance(10 * std::numeric_limits<double>::epsilon()))(nds, std::accumulate(vecndsp -> begin(), vecndsp -> end(), double(0)) / count));
00309       std::sort(vecndsp -> begin(), vecndsp -> end());
00310       const std::vector<double>::size_type size = vecndsp -> size();
00311       const std::vector<double>::size_type middle = size / 2;
00312       const double median2 = (size % 2 == 0) ? ((*vecndsp)[middle-1] + (*vecndsp)[middle]) / 2.0 : (*vecndsp)[middle];
00313       if (not boost::test_tools::close_at_tolerance<double>(boost::test_tools::fraction_tolerance(5 * std::numeric_limits<double>::epsilon()))(mednds, median2)) {
00314   std::cerr << "FEHLER!\ncount = " << count << ", mednds = " << mednds << ", median2 = " << median2 << "\n sortierter Vektor =\n";
00315   std::copy(vecndsp -> begin(), vecndsp -> end(), std::ostream_iterator<double>(std::cerr, " "));
00316   std::cerr << "\noriginaler Vektor =\n";
00317   std::copy(medianassert.begin(), medianassert.end(), std::ostream_iterator<double>(std::cerr, " "));
00318   std::cerr << "\nund nach Median-Berechnung:\n";
00319   std::copy(medianassert2.begin(), medianassert2.end(), std::ostream_iterator<double>(std::cerr, " "));
00320   std::cerr << "\n";
00321   assert(boost::test_tools::close_at_tolerance<double>(boost::test_tools::fraction_tolerance(5 * std::numeric_limits<double>::epsilon()))(mednds, median2));
00322       }
00323     }
00324     delete vecndsp;
00325     vecndsp = 0;
00326   }
00327 
00328   virtual void output(std::ostream& f, const std::string& null, const std::string& sep) const {
00329     f << nds << sep << count << sep << depth << sep << pl << sep << aut << sep << sn << sep << qsn << sep << l2r << sep << an;
00330     f << sep << countwa << sep;
00331     if (countwa == 0)
00332       f << null;
00333     else
00334       f << ndswa;
00335     f << sep << countws << sep;
00336     if (countws == 0)
00337       f << null;
00338     else
00339       f << ndsws;
00340     f << sep << countwq << sep;
00341     if (countwq == 0)
00342       f << null;
00343     else
00344       f << ndswq;
00345     f << sep << maxnds << sep << minnds << sep;
00346     if (count != 1)
00347       f << stdnds;
00348     else
00349       f << null;
00350     f << sep << mednds;
00351   }
00352 
00353 private :
00354   friend class SAT_values;
00355   friend class UNSAT_values;
00356   friend class update_sat;
00357 
00358   double nds, count, depth, pl, aut, sn, qsn, l2r, an;
00359   double countwa, ndswa, countws, ndsws, countwq, ndswq;
00360   double maxnds, minnds, stdnds, sum_sq_nds;
00361 
00362   std::vector<double>* vecndsp;
00363   double mednds;
00364   friend class activate_median;
00365 
00366   static double current_nds;
00367   static double current_depth;
00368   static double current_l2r;
00369 };
00370 
00371 double stat_values::current_nds;
00372 double stat_values::current_depth;
00373 double stat_values::current_l2r;
00374 
00375 class SAT_values : public stat_values {
00376 public :
00377 
00378   SAT_values()
00379   : stat_values(), trv(0), nb(0), nl2r(0), ndswb(0) {}
00380 
00381   virtual void enter_bcls_info_data(const Select& S) {
00382     stat_values::enter_bcls_info_data(S);
00383     trv += (current_nds == 1);
00384     if (current_nds == current_depth + 1)
00385       ++nb;
00386     else
00387       ndswb += current_nds;
00388     
00389   }
00390 
00391   virtual void enter_b_unit_reductions_data(const Select& S) {
00392     stat_values::enter_b_unit_reductions_data(S);
00393     nl2r += (current_l2r == 0);
00394   }
00395 
00396   virtual void compute_mean() {
00397     stat_values::compute_mean();
00398     if (double count_wb = (count - nb))
00399       ndswb /= count_wb;
00400     trv /= count; nb /= count; nl2r /= count;
00401     
00402   }
00403 
00404   virtual void output(std::ostream& f, const std::string& null = null_r, const std::string& sep = separator) const {
00405     stat_values::output(f, null, sep);
00406     f << sep << trv << sep << nb << sep << nl2r << sep << ndswb;
00407   }
00408 
00409 private :
00410   double trv, nb, nl2r, ndswb;
00411 };
00412 
00413 class UNSAT_values : public stat_values {
00414 public :
00415 
00416   UNSAT_values()
00417     : stat_values(), prm(0) {}
00418 
00419   virtual void enter_bcls_info_data(const Select& S) {
00420     stat_values::enter_bcls_info_data(S);
00421     prm += (current_nds == min_complexity);
00422   }
00423   
00424   virtual void compute_mean() {
00425     stat_values::compute_mean();
00426     prm /= count;
00427   }
00428 
00429   virtual void output(std::ostream& f, const std::string& null = null_r, const std::string& sep = separator) const {
00430     stat_values::output(f, null, sep);
00431     f << sep << prm;
00432   }
00433 
00434 private :
00435   double prm;
00436 };
00437 
00438 class prob_sat {
00439 public:
00440 
00441   prob_sat()
00442     : total(0), sat(0) {}
00443 
00444   void update_sat(const double m) {
00445     total += m;
00446     sat += m;
00447   }
00448 
00449   void update_unsat(const double m) {
00450     total += m;
00451   }
00452 
00453   void output(std::ostream& f, const std::string& null = null_r, const std::string& sep = separator) const {
00454     f << sat / total << sep << total;
00455   }
00456 
00457 private :
00458   double total, sat;
00459 };
00460 
00461 
00462 // the "matrices" containing all statistics -------------------------
00463 
00464 struct Matrix_key {
00465   int m_dens_id;
00466   int n;
00467 };
00468 inline bool operator < (const Matrix_key& k1, const Matrix_key& k2) {
00469   return (k1.m_dens_id < k2.m_dens_id) or (k1.m_dens_id == k2.m_dens_id and k1.n < k2.n);
00470 }
00471 inline bool operator == (const Matrix_key& k1, const Matrix_key& k2) {
00472   return (k1.m_dens_id == k2.m_dens_id) and (k1.n == k2.n);
00473 }
00474 inline bool operator != (const Matrix_key& k1, const Matrix_key& k2) {
00475   return !(k1 == k2);
00476 }
00477 class readable_sorting {
00478 public :
00479   readable_sorting(const Densities& D) : Den(D) {}
00480   bool operator () (const Matrix_key& k1, const Matrix_key& k2) {
00481     return (k1.n < k2.n) or (k1.n == k2.n and fromString<double>(Den[k1.m_dens_id].d1) < fromString<double>(Den[k2.m_dens_id].d1));
00482   }
00483 private :
00484   const Densities& Den;
00485 };
00486 
00487 typedef std::map<Matrix_key, UNSAT_values> UNSAT_matrices;
00488 typedef std::map<Matrix_key, SAT_values> SAT_matrices;
00489 typedef std::map<Matrix_key, prob_sat, readable_sorting> prob_matrices;
00490 
00491 UNSAT_matrices UNSAT_matrix;
00492 SAT_matrices SAT_matrix;
00493 
00494 // preparing for the median computation
00495 
00496 struct activate_median {
00497   template <class T> void operator() (std::pair<const Matrix_key, T>& x) const {
00498     x.second.vecndsp = new std::vector<double>;
00499     x.second.vecndsp -> reserve(int(x.second.count));
00500   }
00501 };
00502 
00503 // processing (after completed collection from the database)
00504 
00505 struct mean {
00506   template <class T> void operator() (std::pair<const Matrix_key, T>& x) const {
00507     x.second.compute_mean();
00508   }
00509 };
00510 
00511 class update_sat {
00512 public :
00513   update_sat(prob_matrices& pm) : prob_matrix(pm) {}
00514   template <class T> void operator() (const std::pair<const Matrix_key, T>& x) const;
00515 private :
00516   prob_matrices& prob_matrix;
00517 };
00518 template <> inline void update_sat::operator() (const std::pair<const Matrix_key, UNSAT_values>& x) const {
00519     prob_matrix[x.first].update_unsat(x.second.count);
00520   }
00521 template <> inline void update_sat::operator() (const std::pair<const Matrix_key, SAT_values>& x) const {
00522     prob_matrix[x.first].update_sat(x.second.count);
00523   }
00524 
00525 
00526 // the output functions --------------------------------
00527 
00528 
00529 template <class Transformer, class Matrix>
00530 inline void file_output(const std::string& filename, const std::string& header, const Matrix& M, const Densities& D) {
00531   std::ofstream out(filename.c_str());
00532   out << std::setprecision(precision);
00533   out << header << "\n";
00534   std::for_each(M.begin(), M.end(), Transformer(out, D));
00535 }
00536 
00537 template <class Transformer, class Matrix>
00538 inline void table_output(const std::string& tablename, const std::string& header, const Matrix& M, const Densities& D) {
00539   const std::string query_0 = "insert into " + tablename + "(" + header + ") values ";
00540   std::ostringstream s;
00541   const Transformer T(s, D, false);
00542   for (typename Matrix::const_iterator i = M.begin(); i != M.end(); ++i) {
00543 #ifdef DEBUG
00544     std::cout << "(1) s = " << s.str() << ";";
00545 #endif
00546     s.str("");
00547     T(*i);
00548 #ifdef DEBUG
00549     std::cout << " (2) s = " << s.str() << ";";
00550 #endif
00551     Comm.issue(query_0 + s.str() + ";");
00552 #ifdef DEBUG
00553     std::cout << "Comm.issue(query_0 + s.str() + \";\"); erfolgreich" << std::endl;
00554 #endif
00555   }
00556 }
00557 
00558 
00559 // internal output facilities (the "Transformers")
00560 
00561 class output_line {
00562   // line of values
00563 
00564 public :
00565   output_line(std::ostream& f, const Densities& D, const bool fR = true) : out(f), Den(D), for_R(fR) {}
00566   template <class T> void operator() (const std::pair<const Matrix_key, T>& x) const {
00567     if (for_R) {
00568       out << x.first.n << separator << Den[x.first.m_dens_id].d1 << separator;
00569       x.second.output(out);
00570       out << "\n";
00571     }
00572     else { // the value list for the insert command
00573       out << "(" << x.first.n << "," << Den[x.first.m_dens_id].d1 << ",";
00574       x.second.output(out, null_sql);
00575       out << ")";
00576     }
00577   }
00578 
00579 #ifdef DEBUG
00580   ~output_line() {
00581     std::cout << "Destruktor output_line" << std::endl;
00582   }
00583 #endif
00584 
00585 private :
00586   std::ostream& out;
00587   const Densities& Den;
00588   const bool for_R;
00589 };
00590 
00591 class output_prob_sat_line {
00592   // line of values
00593 
00594 public :
00595   output_prob_sat_line(std::ostream& f, const Densities& D, const bool fR = true) : out(f), Den(D), for_R(fR) {}
00596   void operator() (const std::pair<const Matrix_key, prob_sat>& x) const {
00597     if (for_R) {
00598       out << x.first.n << separator << Den[x.first.m_dens_id].d1 << separator;
00599       x.second.output(out);
00600       out << "\n";
00601     }
00602     else {
00603       out << "(" << x.first.n << "," << Den[x.first.m_dens_id].d1 << ",";
00604       x.second.output(out, null_sql);
00605       out << ")";
00606     }
00607   }
00608 
00609 private :
00610   std::ostream& out;
00611   const Densities& Den;
00612   const bool for_R;
00613 };
00614 
00615 
00616 
00617 // Indices --------------
00618 
00619 typedef std::vector<stat_values*> Matrix_indices;
00620 
00621 }
00622 
00623 
00624 // main program --------------------------------------------
00625 
00626 int main() {
00627 
00628   try {
00629 
00630     std::cout << "[" << Selbst << "] " << Meldungen[14][language] << " " << currentDateTime() << std::endl;
00631 
00632     WallTime Total_time;
00633 
00634     const Frame_id frame_id;
00635     const Densities densities(frame_id);
00636 
00637     std::cout << Meldungen[3][language] << std::endl;
00638     const Max_index max_cls_id("cls_id", "bcls");
00639     std::cout << Meldungen[7][language] << max_cls_id << std::endl;
00640     Matrix_indices* cls_id_index_p = new Matrix_indices(max_cls_id+1);
00641 
00642     { // Reading from bcls
00643       std::cout << Meldungen[0][language] << std::endl;
00644       Progress P(std::cout, max_cls_id, progress_step, Meldungen[1][language], Meldungen[2][language]);
00645       Sel.set_cursor_step(cursor_step_bcls);
00646       Sel.issue("select cls_id, n, m_dens_id, dim, sat from bcls", true);
00647       while (++Sel) {
00648   P();
00649   if (std::string(Sel.value("dim")) != dim)
00650     continue;
00651   const int m_dens_id = fromString<int>(Sel.value("m_dens_id"));
00652   if (! densities[m_dens_id].fi)
00653     continue;
00654   const int n = fromString<int>(Sel.value("n"));
00655   const bool sat = std::string(Sel.value("sat")) == SQL_true;
00656   const int cls_id = fromString<int>(Sel.value("cls_id"));
00657   const Matrix_key key = {m_dens_id, n};
00658   if (sat) {
00659     SAT_matrices::iterator i = SAT_matrix.lower_bound(key);
00660     if (i == SAT_matrix.end() or i -> first != key)
00661       i = SAT_matrix.insert(i, std::make_pair(key, SAT_values()));
00662     else
00663       i -> second.enter_bcls_data(Sel);
00664     (*cls_id_index_p)[cls_id] = &(i -> second);
00665   }
00666   else {
00667     UNSAT_matrices::iterator i = UNSAT_matrix.lower_bound(key);
00668     if (i == UNSAT_matrix.end() or i -> first != key)
00669       i = UNSAT_matrix.insert(i, std::make_pair(key, UNSAT_values()));
00670     else
00671       i -> second.enter_bcls_data(Sel);
00672     (*cls_id_index_p)[cls_id] = &(i -> second);
00673   }
00674       }
00675       Sel.truncate_result();
00676       std::cout << std::endl;
00677     }
00678     
00679     std::cout << Meldungen[4][language] << std::endl;
00680     const Max_index max_b_info_id("b_info_id", "bcls_info");
00681     std::cout << Meldungen[7][language] << max_b_info_id << std::endl;
00682     std::cout << Meldungen[23][language] << std::endl;
00683     Matrix_indices* b_info_id_index_p = new Matrix_indices(max_b_info_id+1);
00684     
00685     { // Reading from bcls_info
00686       std::cout << Meldungen[5][language] << std::endl;
00687       Progress P(std::cout, max_b_info_id, progress_step, Meldungen[1][language], Meldungen[2][language]);
00688       Sel.set_cursor_step(cursor_step_bcls_info);
00689       Sel.issue("select b_info_id, cls_id, tree_depth, pure_literals, real_autarkies, nodes, single_nodes, quasi_s_nodes, an from bcls_info", true);
00690       while (++Sel) {
00691   P();
00692   const int cls_id = fromString<int>(Sel.value("cls_id"));
00693 #ifdef DEBUG
00694   if (cls_id > max_cls_id)
00695     std::cout << "Fehler: cls_id = " << cls_id << ", max_cls_id = " << max_cls_id << std::endl;
00696 #endif
00697   stat_values* const p = (*cls_id_index_p)[cls_id];
00698   if (! p)
00699     continue;
00700   const int b_info_id = fromString<int>(Sel.value("b_info_id"));
00701 #ifdef DEBUG
00702   if (b_info_id > max_b_info_id)
00703     std::cout << "Fehler: b_info_id = " << b_info_id << ", max_b_info_id = " << max_b_info_id << std::endl;
00704 #endif
00705   (*b_info_id_index_p)[b_info_id] = p;
00706   p -> enter_bcls_info_data(Sel);
00707       }
00708       Sel.truncate_result();
00709       std::cout << std::endl;
00710     }
00711 
00712     delete cls_id_index_p;
00713 
00714     { // Reading from b_unit_reductions
00715       std::cout << Meldungen[6][language] << std::endl;
00716       std::cout << Meldungen[7][language] << max_b_info_id << std::endl;
00717       Progress P(std::cout, max_b_info_id, progress_step, Meldungen[1][language], Meldungen[2][language]);
00718       Sel.set_cursor_step(cursor_step_b_unit_reductions);
00719       Sel.issue("select * from b_unit_reductions", true);
00720       while (++Sel) {
00721   P();
00722   const int b_info_id = fromString<int>(Sel.value("b_info_id"));
00723   stat_values* const p = (*b_info_id_index_p)[b_info_id];
00724   if (! p or std::string(Sel.value("u_level")) != "2")
00725     continue;
00726   p -> enter_b_unit_reductions_data(Sel);
00727       }
00728       Sel.truncate_result();
00729       std::cout << std::endl;
00730     }
00731 
00732     { // reading from bcls_info to compute median(nds)
00733       std::cout << Meldungen[22][language] << std::endl;
00734       std::for_each(UNSAT_matrix.begin(), UNSAT_matrix.end(), activate_median());
00735       std::for_each(SAT_matrix.begin(), SAT_matrix.end(), activate_median());
00736       std::cout << Meldungen[21][language] << std::endl;
00737       std::cout << Meldungen[7][language] << max_b_info_id << std::endl;
00738       Progress P(std::cout, max_b_info_id, progress_step, Meldungen[1][language], Meldungen[2][language]);
00739       Sel.set_cursor_step(cursor_step_bcls_info_median);
00740       Sel.issue("select b_info_id, nodes from bcls_info", true);
00741       while (++Sel) {
00742   P();
00743   const int b_info_id = fromString<int>(Sel.value("b_info_id"));
00744   stat_values* const p = (*b_info_id_index_p)[b_info_id];
00745   if (! p)
00746     continue;
00747   p -> enter_bcls_info_mean_data(Sel);
00748       }
00749       Sel.truncate_result();
00750       std::cout << std::endl;
00751     }
00752 
00753     delete b_info_id_index_p;
00754     
00755     // computation of the mean values
00756 
00757     std::cout << Meldungen[8][language] << std::endl;
00758     std::cout << Meldungen[15][language] << std::endl;
00759     std::for_each(UNSAT_matrix.begin(), UNSAT_matrix.end(), mean());
00760     std::for_each(SAT_matrix.begin(), SAT_matrix.end(), mean());
00761     
00762     // computation of sat-statistics
00763     std::cout << Meldungen[16][language] << std::endl;
00764 
00765     prob_matrices prob_matrix((readable_sorting(densities)));
00766 
00767     std::for_each(UNSAT_matrix.begin(), UNSAT_matrix.end(), update_sat(prob_matrix));
00768     std::for_each(SAT_matrix.begin(), SAT_matrix.end(), update_sat(prob_matrix));
00769 
00770     {
00771       std::cout << Meldungen[17][language] << std::endl;
00772       Sel.set_cursor_step(cursor_step_intervalls);
00773       Sel.issue("select n, m_dens_id, dim, count_all, count_sat, stored_sat, stored_unsat from SatUnsatAggregates;");
00774       while (++Sel) {
00775   if (std::string(Sel.value("dim")) != dim)
00776     continue;
00777   const int m_dens_id = fromString<int>(Sel.value("m_dens_id"));
00778   if (! densities[m_dens_id].fi)
00779     continue;
00780   const int n = fromString<int>(Sel.value("n"));
00781   const Matrix_key key = {m_dens_id, n};
00782   const double count_all = fromString<double>(Sel.value("count_all"));
00783   const double count_sat = fromString<double>(Sel.value("count_sat"));
00784   const double count_unsat = count_all - count_sat;
00785   if (std::string(Sel.value("stored_sat")) != SQL_true)
00786     prob_matrix[key].update_sat(count_sat);
00787   if (std::string(Sel.value("stored_unsat")) != SQL_true)
00788     prob_matrix[key].update_unsat(count_unsat);
00789       }
00790     }
00791 
00792     // now the computations are finished, and we can write to the files
00793 
00794     // new sorting of the matrices for SAT and UNSAT
00795     std::cout << Meldungen[18][language] << std::endl;
00796     std::map<Matrix_key, UNSAT_values, readable_sorting> UNSAT_matrix_n(UNSAT_matrix.begin(), UNSAT_matrix.end(), readable_sorting(densities));
00797     UNSAT_matrix.clear();
00798     std::map<Matrix_key, SAT_values, readable_sorting> SAT_matrix_n(SAT_matrix.begin(), SAT_matrix.end(), readable_sorting(densities));
00799     SAT_matrix.clear();
00800       
00801     // file output
00802     std::cout << Meldungen[19][language] << std::endl;
00803     file_output<output_line>(output_unsat, header_unsat, UNSAT_matrix_n, densities);
00804     file_output<output_line>(output_sat, header_sat, SAT_matrix_n, densities);
00805     file_output<output_prob_sat_line>(output_stat_sat, header_prob_sat, prob_matrix, densities);      
00806 
00807     // table output
00808     std::cout << Meldungen[20][language] << std::endl;
00809     Comm.issue("truncate table " + output_table_unsat + ";");
00810     table_output<output_line>(output_table_unsat, header_unsat, UNSAT_matrix_n, densities);
00811 #ifdef DEBUG
00812     std::cout << "UNSAT" << std::endl;
00813 #endif
00814     Comm.issue("truncate table " + output_table_sat + ";");
00815     table_output<output_line>(output_table_sat, header_sat, SAT_matrix_n, densities);
00816 #ifdef DEBUG
00817     std::cout << "SAT" << std::endl;
00818 #endif
00819     Comm.issue("truncate table " + output_table_prob + ";");
00820     table_output<output_prob_sat_line>(output_table_prob, header_prob_sat, prob_matrix, densities);     
00821 
00822     // final messages
00823 
00824     std::cout << Meldungen[11][language] << " " << output_unsat << " " << output_sat << " " << output_stat_sat << std::endl;
00825     std::cout << Meldungen[12][language] << " " << output_table_unsat << " " << output_table_sat << " " << output_table_prob << std::endl;
00826     std::cout << Meldungen[9][language] << " " << Total_time / 60 << " m" << std::endl;
00827     std::cout << "[" << Selbst << "] " << Meldungen[13][language] << " " << currentDateTime() << std::endl;
00828   }
00829 
00830   catch (const ErrorHandling::Error& e) {
00831     std::cerr << ErrorHandling::Error2string(e) << std::endl;
00832     return 1;
00833   }
00834   catch (const std::exception& e) {
00835     std::cerr << ErrorHandling::Error2string(e) << std::endl;
00836     return 1;
00837   }
00838   catch (...) {
00839     std::cerr << "Unknown exception!\n";
00840     return 1;
00841   }
00842  
00843   return 0;
00844 }
00845 
00846