OKlibrary  0.2.1.6
AnalysisTools_Tests.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 
00008 #ifndef ANALYSISTOOLSTESTS_37yh6fR4
00009 #define ANALYSISTOOLSTESTS_37yh6fR4
00010 
00011 #include <cassert>
00012 #include <iterator>
00013 #include <algorithm>
00014 #include <functional>
00015 #include <string>
00016 
00017 #include <boost/range/iterator_range.hpp>
00018 #include <boost/lexical_cast.hpp>
00019 
00020 #include <OKlib/General/IteratorHandling.hpp>
00021 
00022 #include <OKlib/TestSystem/TestBaseClass.hpp>
00023 #include <OKlib/TestSystem/TestExceptions.hpp>
00024 
00025 #include <OKlib/Structures/Sets/SetAlgorithms/BasicSetOperations.hpp>
00026 #include <OKlib/Structures/Sets/SetAlgorithms/SequenceOperations.hpp>
00027 
00028 #include <OKlib/Experimentation/Competition/SingleResult.hpp>
00029 #include <OKlib/Experimentation/Competition/ParsingSingleResult.hpp>
00030 #include <OKlib/Experimentation/Competition/ParsingResultSequences_Tests.hpp>
00031 #include <OKlib/Experimentation/Competition/ResultProcessing.hpp>
00032 
00033 namespace OKlib {
00034   namespace SATCompetition {
00035 
00036     template <template <class Database> class ElementaryAnalysis>
00037     class Test_ElementaryAnalysis : public ::OKlib::TestSystem::TestBase {
00038     public :
00039       typedef Test_ElementaryAnalysis test_type;
00040       Test_ElementaryAnalysis() {
00041         insert(this);
00042       }
00043     private :
00044 
00045       void perform_test_trivial() {
00046 
00047         test_result<Result>(filename_large_industrial, line_count_large_industrial, true);
00048         test_result<ResultRandomSat>(filename_large_random + "_inconsistency", line_count_large_random + 2, false);
00049       }
00050 
00051       template <class result_type>
00052       void test_result(const std::string& filename, const unsigned int line_count, const bool consistent) {
00053 
00054         typedef Result_database_from_file<ParserResult, result_type> result_database;
00055         result_database rdb(filename);
00056         assert(rdb.result_sequence.size() == line_count);
00057         typedef typename result_database::database_type database;
00058         typedef ElementaryAnalysis<database> elementary_analysis;
00059         elementary_analysis ea(rdb.db);
00060 
00061         typedef typename elementary_analysis::SolvedBenchmark SolvedBenchmark;
00062 
00063         typedef typename elementary_analysis::map_superseries_series map_superseries_series;
00064         typedef typename elementary_analysis::map_series_benchmarks map_series_benchmarks;
00065         typedef typename elementary_analysis::map_benchmark_series map_benchmark_series;
00066         typedef typename elementary_analysis::map_solver_benchmarks map_solver_benchmarks;
00067         typedef typename elementary_analysis::map_solver_series map_solver_series;
00068         typedef typename elementary_analysis::map_benchmark_solvers map_benchmark_solvers;
00069         typedef typename elementary_analysis::map_benchmark_satstatus map_benchmark_satstatus;
00070 
00071         typedef typename elementary_analysis::seq_series seq_series;
00072         typedef typename elementary_analysis::seq_spec_series seq_spec_series;
00073         typedef typename elementary_analysis::seq_benchmarks seq_benchmarks;
00074         typedef typename elementary_analysis::seq_solved_benchmarks seq_solved_benchmarks;
00075         typedef typename elementary_analysis::seq_solvers seq_solvers;
00076 
00077         { // testing ea.series_in_superseries()
00078           const map_superseries_series& map(ea.series_in_superseries());
00079           test_order(map);
00080           OKLIB_TEST_EQUAL_RANGES(
00081                                   IteratorHandling::range_first(map),
00082                                   IteratorHandling::range_first(rdb.db.super_series()));
00083           {
00084             seq_series s;
00085             OKlib::SetAlgorithms::union_sets(
00086                                              IteratorHandling::iterator_second(map.begin()),
00087                                              IteratorHandling::iterator_second(map.end()),
00088                                              std::back_inserter(s));
00089             OKLIB_TEST_EQUAL_RANGES(
00090                                     s,
00091                                     IteratorHandling::range_first(rdb.db.series()));
00092           }
00093           // ToDo: stronger testing
00094         }
00095 
00096        { // testing ea.benchmarks_in_series()
00097          const map_series_benchmarks& map(ea.benchmarks_in_series());
00098          test_order(map);
00099          typedef typename IteratorHandling::IteratorSecond<typename map_series_benchmarks::const_iterator>::type transform_iterator;
00100          const transform_iterator& begin(transform_iterator(map.begin()));
00101          const transform_iterator& end(transform_iterator(map.end()));
00102          OKLIB_TEST_EQUAL(OKlib::SetAlgorithms::sum_sizes(begin, end), rdb.db.benchmark().size());
00103          seq_benchmarks seq;
00104          OKlib::SetAlgorithms::union_sets(begin, end, std::back_inserter(seq));
00105          OKLIB_TEST_EQUAL_RANGES(
00106                                  seq,
00107                                  IteratorHandling::range_first(rdb.db.benchmark()));
00108        }
00109 
00110        { // testing ea.series_of_benchmark()
00111          const map_benchmark_series& map1(ea.series_of_benchmark());
00112          {
00113            const MapBenchmark& map2(rdb.db.benchmark());
00114            OKLIB_TEST_EQUAL_RANGES(
00115                                    IteratorHandling::range_first(map1),
00116                                    IteratorHandling::range_first(map2));
00117          }
00118          {
00119            typedef typename map_series_benchmarks::const_iterator iterator_series;
00120            typedef typename map_benchmark_series::const_iterator iterator_benchmark;
00121            const map_series_benchmarks& map2(ea.benchmarks_in_series());
00122            const iterator_series& end_series(map2.end());
00123            const iterator_benchmark& end_benchmarks(map1.end());
00124            for (iterator_series i = map2.begin(); i != end_series; ++i) {
00125              const SpecSeries& series(i -> first);
00126              const seq_benchmarks& benchs(i -> second);
00127              typedef typename seq_benchmarks::const_iterator iterator;
00128              const iterator& end(benchs.end());
00129              for (iterator j =benchs.begin(); j != end; ++j) {
00130                const Benchmark& bench(*j);
00131                const iterator_benchmark& position(map1.find(bench));
00132                OKLIB_TEST_NOTEQUAL(position, end_benchmarks);
00133                OKLIB_TEST_EQUAL(position -> second, series);
00134              }
00135            }
00136          }
00137          // ToDo: Testing whether elementary_analysis::AmbigueBenchmark is thrown.
00138        }
00139 
00140        {// testing ea.solved_benchmarks()
00141          const map_solver_benchmarks& map(ea.solved_benchmarks());;
00142          test_order(map);
00143          typedef MapSolver::const_iterator iterator;
00144          const MapSolver& map_solver(rdb.db.solver());
00145          const iterator end_map(map_solver.end());
00146          for (iterator i = map_solver.begin(); i != end_map; ++i) {
00147            const Solver& solver(i -> first);
00148            const SetResultNodesP* result_nodes_p = i -> second;
00149            rdb.db.vector_of_sets.clear();
00150            rdb.db.vector_of_sets.push_back(result_nodes_p);
00151            rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.sat_status(), SATStatus(sat)));
00152            const VectorResultNodesP sat_result_nodes(rdb.db.intersection());
00153            rdb.db.vector_of_sets.pop_back();
00154            rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.sat_status(), SATStatus(unsat)));
00155            const VectorResultNodesP& unsat_result_nodes(rdb.db.intersection());
00156            VectorResultNodesP sat_and_unsat; sat_and_unsat.reserve(sat_result_nodes.size() + unsat_result_nodes.size());
00157            std::set_union(sat_result_nodes.begin(), sat_result_nodes.end(), unsat_result_nodes.begin(), unsat_result_nodes.end(), std::back_inserter(sat_and_unsat));
00158            OKLIB_TEST_EQUAL(sat_and_unsat.size(), OKlib::SetAlgorithms::map_value(map, solver).size());
00159            // ToDo: Testing the sequences for equality (after appropriately sorting the second sequence).
00160          }
00161          // ToDo: testing for exception AmbigueSolution
00162        }
00163 
00164        { // testing ea.solved_series()
00165          const map_solver_series& map(ea.solved_series());
00166          test_order(map);
00167          typedef typename map_solver_series::const_iterator iterator_solver_series;
00168          const iterator_solver_series& end_map(map.end());
00169          {
00170            const map_solver_benchmarks& map2(ea.solved_benchmarks());
00171            OKLIB_TEST_EQUAL_RANGES(
00172                                    boost::make_iterator_range(IteratorHandling::iterator_first(map.begin()), IteratorHandling::iterator_first(end_map)),
00173                                    IteratorHandling::range_first(map2));
00174          }
00175          {
00176            for (iterator_solver_series i = map.begin(); i != end_map; ++i) {
00177              const Solver& solver(i -> first);
00178              const seq_spec_series& series_seq(i -> second);
00179              typedef typename seq_spec_series::const_iterator iterator;
00180              const iterator& end_series_seq(series_seq.end());
00181              for (iterator j = series_seq.begin(); j != end_series_seq; ++j) {
00182                const SpecSeries series(*j);
00183                rdb.db.vector_of_sets.clear();
00184                rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.solver(), solver));
00185                rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.super_series(), series.first));
00186                rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.series(), series.second));
00187                rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.sat_status(), SATStatus(sat)));
00188                if (rdb.db.intersection().empty()) {
00189                  rdb.db.vector_of_sets.pop_back();
00190                  rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.sat_status(), SATStatus(unsat)));
00191                  if (rdb.db.intersection().empty())
00192                    OKLIB_THROW("Solver " + boost::lexical_cast<std::string>(solver) + " has not solved series " +  boost::lexical_cast<std::string>(series.second) + " in super-series " + boost::lexical_cast<std::string>(series.first));
00193                }
00194              }
00195              seq_spec_series unsolved_series;
00196              std::set_difference(
00197                                  IteratorHandling::iterator_first(ea.benchmarks_in_series().begin()), IteratorHandling::iterator_first(ea.benchmarks_in_series().end()),
00198                                  series_seq.begin(), series_seq.end(),
00199                                  std::back_inserter(unsolved_series));
00200              const iterator& end_unsolved_series(unsolved_series.end());
00201              for (iterator j = unsolved_series.begin(); j != end_unsolved_series; ++j) {
00202                const SpecSeries series(*j);
00203                rdb.db.vector_of_sets.clear();
00204                rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.solver(), solver));
00205                rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.super_series(), series.first));
00206                rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.series(), series.second));
00207                rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.sat_status(), SATStatus(sat)));
00208                if (not rdb.db.intersection().empty())
00209                  OKLIB_THROW("Solver " + boost::lexical_cast<std::string>(solver) + " has solved series " +  boost::lexical_cast<std::string>(series.second) + " in super-series " + boost::lexical_cast<std::string>(series.first) + "as satisfiable");
00210                rdb.db.vector_of_sets.pop_back();
00211                rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.sat_status(), SATStatus(unsat)));
00212                if (not rdb.db.intersection().empty())
00213                  OKLIB_THROW("Solver " + boost::lexical_cast<std::string>(solver) + " has solved series " +  boost::lexical_cast<std::string>(series.second) + " in super-series " + boost::lexical_cast<std::string>(series.first) + "as unsatisfiable");
00214              }
00215            }
00216          }
00217        }
00218 
00219        { // testing ea.succesful_solvers()
00220          const map_benchmark_solvers& map(ea.succesful_solvers());
00221          test_order(map);
00222          OKLIB_TEST_EQUAL_RANGES(
00223                                  IteratorHandling::range_first(map),
00224                                  IteratorHandling::range_first(ea.series_of_benchmark()));
00225          typedef typename map_benchmark_solvers::const_iterator iterator;
00226          const iterator& end_map(map.end());
00227          for (iterator i = map.begin(); i != end_map; ++i) {
00228            const SolvedBenchmark& bench(i -> first);
00229            const seq_solvers& solvers(i -> second);
00230            typedef typename seq_solvers::const_iterator iterator_solvers;
00231            const iterator_solvers& end_solvers(solvers.end());
00232            for (iterator_solvers j = solvers.begin(); j != end_solvers; ++j) {
00233              const Solver& solver(*j);
00234              const seq_solved_benchmarks& benchs(OKlib::SetAlgorithms::map_value(ea.solved_benchmarks(), solver));
00235              if (not std::binary_search(benchs.begin(), benchs.end(), bench))
00236                OKLIB_THROW("Benchmark " + boost::lexical_cast<std::string>(bench) + " not solved by solver " + boost::lexical_cast<std::string>(solver));
00237            }
00238          }
00239          typedef typename map_solver_benchmarks::const_iterator iterator_solvers;
00240          const map_solver_benchmarks& map2(ea.solved_benchmarks());
00241          const iterator_solvers& end_solvers(map2.end());
00242          for (iterator_solvers i = map2.begin(); i != end_solvers; ++i) {
00243            const Solver& solver(i -> first);
00244            const seq_solved_benchmarks& benchs(i -> second);
00245            typedef typename seq_solved_benchmarks::const_iterator iterator_benchmarks;
00246            const iterator_benchmarks end_benchs(benchs.end());
00247            for (iterator_benchmarks j = benchs.begin(); j != end_benchs; ++j) {
00248              const SolvedBenchmark& bench(*j);
00249              const seq_solvers& succesful(OKlib::SetAlgorithms::map_value(map, bench));
00250              if (not std::binary_search(succesful.begin(), succesful.end(), solver))
00251                OKLIB_THROW("Benchmark " + boost::lexical_cast<std::string>(bench) + " solved by solver " + boost::lexical_cast<std::string>(solver));
00252            }
00253          }
00254        }
00255 
00256        { // testing ea.sat_status()
00257          const map_benchmark_satstatus& map(ea.sat_status());
00258          {
00259            const map_benchmark_solvers& map2(ea.succesful_solvers());
00260            const seq_benchmarks& inconsistent_results(ea.inconsistent_results());
00261            if (consistent) {
00262              if (not inconsistent_results.empty())
00263                OKLIB_THROW("Test case should not contain inconsistent results");
00264              OKLIB_TEST_EQUAL_RANGES(
00265                                      IteratorHandling::range_first(map),
00266                                      IteratorHandling::range_first(map2));
00267            }
00268            else {
00269              if (inconsistent_results.empty())
00270                OKLIB_THROW("Test case should contain inconsistent results");
00271              seq_benchmarks all_benchs;
00272              std::set_union(
00273                             IteratorHandling::iterator_first(map.begin()), IteratorHandling::iterator_first(map.end()),
00274                             inconsistent_results.begin(), inconsistent_results.end(),
00275                             std::back_inserter(all_benchs));
00276              OKLIB_TEST_EQUAL_RANGES(
00277                                      all_benchs,
00278                                      IteratorHandling::range_first(map2));
00279                }
00280          }
00281          typedef typename map_benchmark_satstatus::const_iterator iterator;
00282          const iterator& end_map(map.end());
00283          for (iterator i = map.begin(); i != end_map; ++i) {
00284            const Benchmark& bench(i -> first);
00285            const SATStatus& sat_status(i -> second);
00286            switch (sat_status.result()) {
00287            case unknown :
00288              if (not OKlib::SetAlgorithms::map_value(ea.succesful_solvers(), bench).empty())
00289                OKLIB_THROW("Benchmark " + boost::lexical_cast<std::string>(bench) + " was solved");
00290              break;
00291            case sat :
00292              rdb.db.vector_of_sets.clear();
00293              rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.benchmark(), bench));
00294              rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.sat_status(), sat_status));
00295              if (rdb.db.intersection().empty())
00296                OKLIB_THROW("Benchmark " + boost::lexical_cast<std::string>(bench) + " was not found satisfiable");
00297              rdb.db.vector_of_sets.pop_back();
00298              rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.sat_status(), SATStatus(unsat)));
00299              if (not rdb.db.intersection().empty())
00300                OKLIB_THROW("Benchmark " + boost::lexical_cast<std::string>(bench) + " was found unsatisfiable");
00301              break;
00302            case unsat :
00303              rdb.db.vector_of_sets.clear();
00304              rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.benchmark(), bench));
00305              rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.sat_status(), sat_status));
00306              if (rdb.db.intersection().empty())
00307                OKLIB_THROW("Benchmark " + boost::lexical_cast<std::string>(bench) + " was not found unsatisfiable");
00308              rdb.db.vector_of_sets.pop_back();
00309              rdb.db.vector_of_sets.push_back(OKlib::SetAlgorithms::map_value(rdb.db.sat_status(), SATStatus(sat)));
00310              if (not rdb.db.intersection().empty())
00311                OKLIB_THROW("Benchmark " + boost::lexical_cast<std::string>(bench) + " was found satisfiable");
00312              break;
00313            case error :
00314              OKLIB_THROW("Benchmark " + boost::lexical_cast<std::string>(bench) + " sat status was \"error\"");
00315            }
00316          }
00317        }
00318 
00319       }
00320 
00321       template <class Map>
00322       void test_order(const Map& map) {
00323         typedef typename Map::const_iterator iterator_map;
00324         const iterator_map& end_map(map.end());
00325         for (iterator_map i = map.begin(); i != end_map; ++i) {
00326           typedef typename Map::value_type value_type_pairs;
00327           typedef typename value_type_pairs::second_type seq_type;
00328           const seq_type& seq(i -> second);
00329           typedef typename seq_type::const_iterator iterator_seq;
00330           const iterator_seq& end_seq(seq.end());
00331           typedef typename seq_type::value_type value_type;
00332           if (std::adjacent_find(seq.begin(), end_seq, std::greater_equal<value_type>()) != end_seq)
00333             OKLIB_THROW(std::string("Vector with elements of type ") + typeid(value_type).name() + " not sorted");
00334         }
00335       }
00336 
00337     };
00338 
00339   }
00340 
00341 }
00342 
00343 #endif