OKlibrary  0.2.1.6
ComputeAnalysis.cpp
Go to the documentation of this file.
00001 // Oliver Kullmann, 5.11.2005 (Swansea)
00002 /* Copyright 2005 - 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. */
00007 
00018 #include <cassert>
00019 #include <iostream>
00020 #include <utility>
00021 #include <ios>
00022 #include <ostream>
00023 
00024 #include <OKlib/Structures/Sets/SetAlgorithms/BasicMapOperations.hpp>
00025 
00026 #include <OKlib/Experimentation/Competition/SingleResult.hpp>
00027 #include <OKlib/Experimentation/Competition/ParsingSingleResult.hpp>
00028 #include <OKlib/Experimentation/Competition/Scoring.hpp>
00029 #include <OKlib/Experimentation/Competition/AnalysisTools.hpp>
00030 
00031 namespace {
00032 
00033   template <bool with_extension>
00034   struct result_database {
00035     typedef OKlib::SATCompetition:: Result_database_from_file<OKlib::SATCompetition::ParserResult, OKlib::SATCompetition::Result, OKlib::SATCompetition::ParserThreeElements> type;
00036   };
00037   template <>
00038   struct result_database<false> {
00039     typedef OKlib::SATCompetition:: Result_database_from_file<OKlib::SATCompetition::ParserResult> type;
00040   };
00041 
00042   // ###################
00043 
00044   struct PrintStandard {
00045     std::ostream& out;
00046     const std::streamsize precision;
00047     const bool fixed;
00048     
00049     PrintStandard(std::ostream& out) : out(out), precision(out.precision()), fixed(out.flags() & std::ios_base::fixed) {
00050       const std::streamsize new_precision = 1;
00051       out.precision(new_precision);
00052       if (not fixed)
00053         out.setf(std::ios_base::fixed);
00054     }
00055     ~PrintStandard() {
00056       out.precision(precision);
00057       if (not fixed)
00058         out.unsetf(std::ios_base::fixed);
00059     }
00060 
00061     template <class Benchmark, typename Counter, typename Number, class SatStatus>
00062     void operator() (const Benchmark& bench, Counter solved, const Number standard_problem_purse, const Number total_time, const SatStatus sat_status) const {
00063       const std::streamsize field_width_bench(5 + 5 + 1);
00064       out.width(field_width_bench);
00065       out << bench << ": ";
00066       const std::streamsize field_width_count(3);
00067       out.width(field_width_count);
00068       out << solved << " ";
00069       const std::streamsize field_width_score(4+2);
00070       out.width(field_width_score);
00071       if (not solved)
00072         out << "NaN" << "\n";
00073       else {
00074         out << standard_problem_purse / solved << "; ";
00075         const std::streamsize field_width_average_time(6+2);
00076         out.width(field_width_average_time);
00077         out << total_time / solved << "; ";
00078         assert(sat_status != OKlib::SATCompetition::error);
00079         assert(sat_status != OKlib::SATCompetition::unknown);
00080         switch (sat_status) {
00081         case OKlib::SATCompetition::sat :
00082           out << "SAT"; break;
00083         default :
00084           out << "UNSAT"; break;
00085         }
00086         out << "\n";
00087       }
00088     }
00089   };
00090   
00091   struct PrintLatex {
00092     std::ostream& out;
00093     const std::streamsize precision;
00094     const bool fixed;
00095     
00096     PrintLatex(std::ostream& out) : out(out), precision(out.precision()), fixed(out.flags() & std::ios_base::fixed) {
00097       const std::streamsize new_precision = 1;
00098       out.precision(new_precision);
00099       if (not fixed)
00100         out.setf(std::ios_base::fixed);
00101     }
00102     ~PrintLatex() {
00103       out.precision(precision);
00104       if (not fixed)
00105         out.unsetf(std::ios_base::fixed);
00106     }
00107     
00108     template <class Benchmark, typename Counter, typename Number, class SatStatus>
00109     void operator() (const Benchmark& bench, Counter solved, const Number standard_problem_purse, const Number total_time, const SatStatus sat_status) const {
00110       const int length_word_bench(5);
00111       assert(bench.name().size() >= length_word_bench + 1);
00112       out << " & " << bench.name().substr(length_word_bench) << " & $";
00113       if (not solved)
00114         out << "?$ & NaN";
00115       else {
00116         assert(sat_status != OKlib::SATCompetition::error);
00117         assert(sat_status != OKlib::SATCompetition::unknown);
00118         switch (sat_status) {
00119         case OKlib::SATCompetition::sat :
00120           out << "1"; break;
00121         case OKlib::SATCompetition::unsat :
00122           out << "0"; break;
00123         }
00124         out << "$ & $" << solved << "$ & $" << standard_problem_purse / solved << "$ & $" << total_time / solved << "$";
00125       }
00126       out << "\\\\\n";
00127     }
00128   };
00129 
00130   // ###################
00131 
00132 #ifdef LATEXOUTPUT
00133   typedef PrintLatex DefaultPolicy;
00134 #else
00135   typedef PrintStandard DefaultPolicy;
00136 #endif
00137 
00138   template <bool with_extension, class DataLinePolicy = DefaultPolicy>
00139   struct Evaluation {
00140     const std::string& filename;
00141     const char* const specifier;
00142     typedef typename result_database<with_extension>::type result_database_from_file_type;
00143     typedef typename result_database_from_file_type::database_type result_database_type;
00144     typedef OKlib::SATCompetition::ElementaryAnalysis<result_database_type> indexed_database_type;
00145     typedef OKlib::SATCompetition::PurseScoring<indexed_database_type> scoring_type;
00146     typedef typename scoring_type::number_type number_type;
00147     Evaluation(const std::string& filename, const char* const specifier) : filename(filename), specifier(specifier) {
00148       if (with_extension)
00149         assert(specifier);
00150     }
00151     void operator() (const number_type standard_problem_purse = 1000, const number_type standard_speed_factor = 1, const number_type standard_series_factor = 3) const {
00152       
00153       const result_database_from_file_type rdb(filename);
00154       const indexed_database_type idb(rdb.db);
00155       scoring_type scores(idb, standard_problem_purse, standard_speed_factor, standard_series_factor);
00156       
00157       std::cout << "\nFile name = " << filename;
00158       if (specifier)
00159         std::cout << "\nsyntax specifier = " << specifier << "\n";
00160       std::cout << "\n";
00161       std::cout << "Standard problem purse = " << standard_problem_purse << "\n";
00162       std::cout << "Standard speed factor = " << standard_speed_factor << "\n";
00163       std::cout << "Standard series factor = " << standard_series_factor << "\n\n";
00164       
00165       DataLinePolicy out(std::cout);
00166       
00167       typedef typename indexed_database_type::map_superseries_series map_superseries_series;
00168       const map_superseries_series& map_superseries(idb.series_in_superseries());
00169       typedef typename map_superseries_series::const_iterator iterator_superseries;
00170       const iterator_superseries& end_superseries(map_superseries.end());
00171       for (iterator_superseries i = map_superseries.begin(); i != end_superseries; ++i) {
00172         const OKlib::SATCompetition::SuperSeries& superseries(i -> first);
00173         std::cout << "###########################################\n\n" << superseries << "\n\n";
00174         typedef typename indexed_database_type:: seq_series seq_series_type;
00175         const seq_series_type& seq_series(i -> second);
00176         typedef typename seq_series_type::const_iterator iterator_series;
00177         const iterator_series& end_series(seq_series.end());
00178         for (iterator_series j = seq_series.begin(); j != end_series; ++j) {
00179           const OKlib::SATCompetition::Series& series(*j);
00180           std::cout << "#######\n" << series << "\n\n";
00181           typedef typename indexed_database_type::seq_benchmarks seq_benchmarks_type;
00182           const seq_benchmarks_type& seq_benchmarks(OKlib::SetAlgorithms::map_value(idb.benchmarks_in_series(), std::make_pair(superseries, series)));
00183           typedef typename seq_benchmarks_type::const_iterator iterator_benchmarks;
00184           const iterator_benchmarks end_benchmarks(seq_benchmarks.end());
00185           for (iterator_benchmarks k = seq_benchmarks.begin(); k != end_benchmarks; ++k) {
00186             const OKlib::SATCompetition::Benchmark& bench(*k);
00187             typedef typename scoring_type::size_type_solvers size_type_solvers;
00188             const size_type_solvers& solved(scores.solved(bench));
00189             const number_type& total_time(scores.total_time(bench));
00190             const OKlib::SATCompetition::SolverResult sat_status(OKlib::SetAlgorithms::map_value(idb.sat_status(), bench).result());
00191             out(bench, solved, standard_problem_purse, total_time, sat_status);
00192           }
00193           std::cout << "\n";
00194         }
00195       }
00196     }
00197   };
00198 }
00199 
00200 // ##########################################
00201 
00202 int main(const int argc, const char* const argv[]) {
00203 
00204   if (argc <= 1 or argc >= 4) {
00205     std::cerr << "One or two arguments required (the name of the file, optionally a syntax specifier \"syntax=...\").\n";
00206     return EXIT_FAILURE;
00207   }
00208   bool specifier = false;
00209   const char* specifier_text = (const char*)(0);
00210   const std::string& file_name(argv[1]);
00211   for (int i = 2; i < argc; ++i) {
00212     const int prefix_length = 6 + 1;
00213     assert(prefix_length >= 0);
00214     if (std::strlen(argv[i]) <= (unsigned int)prefix_length) {
00215       std::cerr << "Parameter \"" << argv[i] << "\" is not \"syntax=+\".\n";
00216       return EXIT_FAILURE;
00217     }
00218     if (std::strncmp(argv[i], "syntax=", prefix_length) == 0) {
00219       specifier = true;
00220       specifier_text = argv[i] + prefix_length;
00221     }
00222     else {
00223       std::cerr << "Parameter \"" << argv[i] << "\" does not start with \"syntax=\".\n";
00224       return EXIT_FAILURE;
00225     }
00226   }
00227 
00228   if (specifier)
00229       Evaluation<true>(file_name, specifier_text)();
00230   else
00231       Evaluation<false>(file_name, specifier_text)();
00232 }