OKlibrary  0.2.1.6
AnalysisTools.hpp
Go to the documentation of this file.
00001 // Oliver Kullmann, 7.6.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 
00013 #ifndef ANALYSISTOOLS_946TglQ
00014 #define ANALYSISTOOLS_946TglQ
00015 
00016 #include <vector>
00017 #include <utility>
00018 #include <algorithm>
00019 #include <iterator>
00020 #include <stdexcept>
00021 #include <string>
00022 #include <ostream>
00023 
00024 #include <boost/lexical_cast.hpp>
00025 
00026 #include <OKlib/General/IteratorHandling.hpp>
00027 
00028 #include <OKlib/Structures/Sets/SetAlgorithms/BasicMapOperations.hpp>
00029 
00030 #include <OKlib/Experimentation/Competition/SingleResult.hpp>
00031 #include <OKlib/Experimentation/Competition/ResultProcessing.hpp>
00032 
00033 namespace OKlib {
00034 
00035   namespace SATCompetition {
00036 
00056     template <class Database>
00057     class ElementaryAnalysis {
00058       ElementaryAnalysis(const ElementaryAnalysis&);
00059       ElementaryAnalysis& operator =(const ElementaryAnalysis&);
00060 
00061     public :
00062 
00063       ElementaryAnalysis(const Database& db) : db(db) {
00064         fill_series_in_superseries();
00065         fill_benchmarks_in_series();
00066         fill_series_of_benchmark();
00067         fill_solved_benchmarks();
00068         fill_solved_series();
00069         fill_succesful_solvers();
00070         fill_sat_status();
00071       }
00072 
00073       typedef Database database_type;
00074       const Database& db;
00075 
00076       struct SolvedBenchmark {
00077         const Benchmark bench;
00078         const ResultNode* const node;
00079         SolvedBenchmark(const Benchmark& bench) : bench(bench), node(0) {}
00080         SolvedBenchmark(const Benchmark& bench, const ResultNode* node) : bench(bench), node(node) {}
00081         operator Benchmark() const { return bench; }
00082         operator ResultNode*() const { return node; }
00083       };
00084       friend std::ostream& operator <<(std::ostream& out, const SolvedBenchmark sb) {
00085         return out << sb.bench;
00086       }
00087       friend inline bool operator ==(const SolvedBenchmark& b1, const SolvedBenchmark& b2) {
00088         return b1.bench == b2.bench;
00089       }
00090       friend inline bool operator <(const SolvedBenchmark& b1, const SolvedBenchmark& b2) {
00091         return b1.bench < b2.bench;
00092       }
00093       OKLIB_DERIVED_RELATIONS_FRIENDS(SolvedBenchmark);
00094 
00095       typedef std::vector<Series> seq_series;
00096       typedef std::vector<Benchmark> seq_benchmarks;
00097       typedef std::vector<Solver> seq_solvers;
00098       // such vectors are always sorted
00099 
00100       typedef std::vector<SpecSeries> seq_spec_series;
00101       typedef std::vector<SolvedBenchmark> seq_solved_benchmarks;
00102 
00103       typedef std::map<SuperSeries, seq_series> map_superseries_series;
00104       typedef std::map<SpecSeries, seq_benchmarks> map_series_benchmarks;
00105       typedef std::map<Benchmark, SpecSeries> map_benchmark_series;
00106       typedef std::map<Solver, seq_solved_benchmarks> map_solver_benchmarks;
00107       typedef std::map<Solver, seq_spec_series> map_solver_series;
00108       typedef std::map<Benchmark, seq_solvers> map_benchmark_solvers;
00109       typedef std::map<Benchmark, SATStatus> map_benchmark_satstatus;
00110 
00111       const map_superseries_series& series_in_superseries() const { return series_in_superseries_; }
00112       const map_series_benchmarks & benchmarks_in_series() const { return benchmarks_in_series_; }
00113       const map_benchmark_series& series_of_benchmark() const { return series_of_benchmark_; }
00114       const map_solver_benchmarks& solved_benchmarks() const { return solved_benchmarks_; }
00115       const map_solver_series& solved_series() const { return solved_series_; }
00116       const map_benchmark_solvers& succesful_solvers() const { return succesful_solvers_; }
00117       const map_benchmark_satstatus& sat_status() const { return sat_status_; }
00118 
00119       const seq_benchmarks& inconsistent_results() const { return inconsistent_results_; }
00120 
00121       struct ErrorElementaryAnalysis : std::runtime_error {
00122         ErrorElementaryAnalysis(const std::string& message) : std::runtime_error(message) {}
00123       };
00124       struct AmbigueBenchmark : ErrorElementaryAnalysis {
00125         AmbigueBenchmark(const Benchmark& benchmark, const SpecSeries& series1, const SpecSeries& series2) : ErrorElementaryAnalysis(boost::lexical_cast<std::string>(benchmark) + " in " + boost::lexical_cast<std::string>(series1) + " and " + boost::lexical_cast<std::string>(series2)) {}
00126       };
00127       struct AmbigueSolution : ErrorElementaryAnalysis {
00128         AmbigueSolution(const ResultNode* const solution1, const ResultNode* const solution2) : ErrorElementaryAnalysis("Ambigue solutions:\n" + boost::lexical_cast<std::string>(solution1 -> rb) + "\n" + boost::lexical_cast<std::string>(solution2 -> rb)) {}
00129       };
00130 
00131     private :
00132 
00133       map_superseries_series series_in_superseries_;
00134       map_series_benchmarks benchmarks_in_series_;
00135       map_benchmark_series series_of_benchmark_;
00136       map_solver_benchmarks solved_benchmarks_;
00137       map_solver_series solved_series_;
00138       map_benchmark_solvers succesful_solvers_;
00139       map_benchmark_satstatus sat_status_;
00140 
00141       seq_benchmarks inconsistent_results_;
00142 
00143       typedef SetResultNodesP::iterator set_iterator;
00144 
00145       void fill_series_in_superseries() {
00146         typedef map_superseries_series::iterator iterator;
00147         iterator current = series_in_superseries_.begin();
00148         typedef MapSuperSeries::const_iterator other_iterator;
00149         const other_iterator end_other(db.super_series().end());
00150         for (other_iterator i(db.super_series().begin()); i != end_other; ++i) {
00151           const SuperSeries super_series = i -> first;
00152           assert(i -> second);
00153           const SetResultNodesP& result_nodes_p = *(i -> second);
00154           std::set<Series> set_series;
00155           const set_iterator end_set(result_nodes_p.end());
00156           for (set_iterator j(result_nodes_p.begin()); j != end_set; ++j) {
00157             assert((*j) -> rb);
00158             set_series.insert((*j) -> rb -> series()); // ToDO: Using STL
00159             assert((*j) -> rb -> super_series() == super_series);
00160           }
00161           current = series_in_superseries_.insert(current, std::make_pair(super_series, seq_series(set_series.begin(), set_series.end())));
00162           assert(current -> first == super_series);
00163           assert((current -> second).size() == set_series.size());
00164         }
00165       }
00166       void fill_benchmarks_in_series() {
00167         typedef map_series_benchmarks::iterator iterator;
00168         typedef map_superseries_series::const_iterator iterator_superseries;
00169         typedef seq_series::const_iterator iterator_series;
00170         iterator current = benchmarks_in_series_.begin();
00171         const iterator_superseries& end_superseries(series_in_superseries().end());
00172         for (iterator_superseries i = series_in_superseries().begin(); i != end_superseries; ++i) {
00173           const SuperSeries& super_series(i -> first);
00174           const seq_series& vec_series(i -> second);
00175           const iterator_series& end_series(vec_series.end());
00176           for (iterator_series j = vec_series.begin(); j != end_series; ++j) {
00177             const Series& series(*j);
00178             std::set<Benchmark> set_benchmarks;
00179             const SetResultNodesP& result_nodes_p = *OKlib::SetAlgorithms::map_value(db.series(), series);
00180             const set_iterator& end_results(result_nodes_p.end());
00181             for (set_iterator k = result_nodes_p.begin(); k != end_results; ++k) {
00182               const ResultNode& node(**k);
00183               const ResultBasis& result(*node.rb);
00184               if (result.super_series() == super_series)
00185                 set_benchmarks.insert(result.benchmark());
00186             }
00187             current = benchmarks_in_series_.insert(current, std::make_pair(std::make_pair(super_series, series), seq_benchmarks(set_benchmarks.begin(), set_benchmarks.end())));
00188           }
00189         }
00190       }
00191       void fill_series_of_benchmark() {
00192         typedef map_series_benchmarks::const_iterator iterator_series;
00193         typedef seq_benchmarks::const_iterator iterator_benchmarks;
00194         typedef map_benchmark_series::iterator iterator;
00195         const iterator_series& end_series(benchmarks_in_series().end());
00196         const iterator& end_map(series_of_benchmark_.end());
00197         for (iterator_series i = benchmarks_in_series().begin(); i != end_series; ++i) {
00198           const SpecSeries& series(i -> first);
00199           const seq_benchmarks& benchs(i -> second);
00200           const iterator_benchmarks& end_benchmarks(benchs.end());
00201           for (iterator_benchmarks j = benchs.begin(); j != end_benchmarks; ++j) {
00202             const Benchmark& bench(*j);
00203             const iterator position(series_of_benchmark_.find(bench));
00204             if (position == end_map)
00205               series_of_benchmark_.insert(std::make_pair(bench, series));
00206             else {
00207               const SpecSeries& series2(position -> second);
00208               assert(series2 != series);
00209               throw AmbigueBenchmark(bench, series, series2);
00210             }
00211               
00212             series_of_benchmark_[*j] = series;
00213           }
00214         }
00215       }
00216       void fill_solved_benchmarks() {
00217         typedef typename map_solver_benchmarks::iterator iterator;
00218         iterator current = solved_benchmarks_.begin();
00219         std::set<Solver> set_solvers;
00220         const MapSolver& map(db.solver());
00221         typedef MapSolver::const_iterator other_iterator;
00222         const other_iterator end(map.end());
00223         for (other_iterator i = map.begin(); i != end; ++i) {
00224           const Solver& solver(i -> first);
00225           const SetResultNodesP& result_nodes_p = *(i -> second);
00226           typedef std::set<SolvedBenchmark> set_benchmarks_type;
00227           set_benchmarks_type set_benchmarks;
00228           const set_iterator& end_results(result_nodes_p.end());
00229           for (set_iterator j = result_nodes_p.begin(); j != end_results; ++j) {
00230             const ResultNode* node_p(*j);
00231             const ResultNode& node(*node_p);
00232             const ResultBasis& result(*node.rb);
00233             const SolverResult& solv_res(result.sat_status().result());
00234             if (solv_res == sat or solv_res == unsat) {
00235               typedef typename set_benchmarks_type::iterator set_benchmarks_iterator;
00236               typedef std::pair<set_benchmarks_iterator, bool> insert_return_type;
00237               const Benchmark& bench(result.benchmark());
00238               const SolvedBenchmark new_solved_benchmark(bench, node_p);
00239               const insert_return_type& insert_result(set_benchmarks.insert(new_solved_benchmark));
00240               if (not insert_result.second) {
00241                 throw AmbigueSolution(node_p, insert_result.first -> node);
00242               }
00243             }
00244           }
00245           current = solved_benchmarks_.insert(current, std::make_pair(solver, seq_solved_benchmarks(set_benchmarks.begin(), set_benchmarks.end())));
00246         }
00247       }
00248       void fill_solved_series() {
00249         typedef map_solver_series::iterator iterator;
00250         iterator current = solved_series_.begin();
00251         typedef typename map_solver_benchmarks::const_iterator iterator_solvers;
00252         const iterator_solvers& end_solvers(solved_benchmarks().end());
00253         for (iterator_solvers i = solved_benchmarks().begin(); i != end_solvers; ++i) {
00254           std::set<SpecSeries> set_series;
00255           const Solver& solver(i -> first);
00256           const seq_solved_benchmarks& benchs(i -> second);
00257           typedef typename seq_solved_benchmarks::const_iterator iterator_benchmarks;
00258           const iterator_benchmarks end_benchs(benchs.end());
00259           for (iterator_benchmarks j = benchs.begin(); j != end_benchs; ++j) {
00260             const Benchmark& bench(*j);
00261             const SpecSeries& series(OKlib::SetAlgorithms::map_value(series_of_benchmark(), bench));
00262             set_series.insert(series);
00263           }
00264           current = solved_series_.insert(current, std::make_pair(solver, seq_spec_series(set_series.begin(), set_series.end())));
00265         }
00266       }
00267       void fill_succesful_solvers() {
00268         typedef typename map_solver_benchmarks::const_iterator iterator_solvers;
00269         typedef typename seq_solved_benchmarks::const_iterator iterator_solved_benchmarks;
00270         const iterator_solvers& end_solvers(solved_benchmarks().end());
00271         for (iterator_solvers i = solved_benchmarks().begin(); i != end_solvers; ++i) {
00272           const Solver& solver(i -> first);
00273           const seq_solved_benchmarks& benchs(i -> second);
00274           const iterator_solved_benchmarks& end_benchmarks(benchs.end());
00275           for (iterator_solved_benchmarks j = benchs.begin(); j != end_benchmarks; ++j) {
00276             const Benchmark& bench(*j);
00277             succesful_solvers_[bench].push_back(solver);
00278           }
00279         }
00280         seq_benchmarks unsolved;
00281         std::set_difference(
00282                             IteratorHandling::iterator_first(series_of_benchmark().begin()), IteratorHandling::iterator_first(series_of_benchmark().end()),
00283                             IteratorHandling::iterator_first(succesful_solvers_.begin()), IteratorHandling::iterator_first(succesful_solvers_.end()),
00284                             std::back_inserter(unsolved));
00285         typedef map_benchmark_solvers::iterator iterator;
00286         iterator current(succesful_solvers_.begin());
00287         typedef typename seq_benchmarks::const_iterator iterator_benchmarks;
00288         const iterator_benchmarks& end_benchmarks(unsolved.end());
00289         for (iterator_benchmarks i = unsolved.begin(); i != end_benchmarks; ++i) {
00290           const Benchmark& bench(*i);
00291           current = succesful_solvers_.insert(current, std::make_pair(bench, seq_solvers()));
00292           // ToDo: Ideally, the temporary store unsolved would not be needed.
00293         }
00294       }
00295       
00296       void fill_sat_status() {
00297         typedef map_benchmark_solvers::const_iterator iterator_benchmarks;
00298         const iterator_benchmarks end_benchmarks(succesful_solvers().end());
00299         for (iterator_benchmarks i = succesful_solvers().begin(); i != end_benchmarks; ++i) {
00300           const Benchmark& bench(i -> first);
00301           {
00302             const seq_solvers& solvers(i -> second);
00303             if (solvers.empty()) {
00304               sat_status_.insert(std::make_pair(bench, SATStatus(unknown))); 
00305               continue;
00306             }
00307           }
00308           typedef std::set<SATStatus> set_result_type;
00309           set_result_type set_results;
00310           const MapBenchmark& map(db.benchmark());
00311           const SetResultNodesP& set(*OKlib::SetAlgorithms::map_value(map, bench));
00312           typedef SetResultNodesP::iterator iterator;
00313           const iterator& end_set(set.end());
00314           for (iterator j = set.begin(); j != end_set; ++j) {
00315             const ResultNode& result_node(**j);
00316             const ResultBasis& result(*result_node.rb);
00317             const SATStatus& sat_status(result.sat_status());
00318             switch (sat_status.result()) {
00319             case sat :
00320               set_results.insert(SATStatus(sat)); break;
00321             case unsat :
00322               set_results.insert(SATStatus(unsat)); break;
00323             case error : break;
00324             case unknown : break;
00325             default :
00326               assert(false);
00327             }
00328           }
00329           assert(not set_results.empty());
00330           assert(set_results.size() <= 2);
00331           if (set_results.size() == 1)
00332             sat_status_.insert(std::make_pair(bench, *set_results.begin()));
00333           else
00334             inconsistent_results_.push_back(bench);
00335         }
00336       }
00337 
00338     };
00339     
00340   }
00341 
00342 }
00343 
00344 #endif