OKlibrary  0.2.1.6
SingleResult.hpp
Go to the documentation of this file.
00001 // Oliver Kullmann, 8.5.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 
00025 #ifndef SINGLERESULT_jdj277yYt
00026 #define SINGLERESULT_jdj277yYt
00027 
00028 #include <string>
00029 #include <ostream>
00030 #include <cassert>
00031 #include <algorithm>
00032 
00033 #include <boost/tuple/tuple.hpp>
00034 
00035 #include <OKlib/Concepts/ResultElements.hpp>
00036 
00037 #include <OKlib/Programming/Utilities/OrderRelations/DerivedRelations.hpp>
00038 
00039 namespace OKlib {
00040   namespace SATCompetition {
00041 
00051     class ResultElement {
00052     public :
00053       typedef OKlib::Concepts::ResultElement_tag concept_tag;
00054       typedef std::string string_type;
00055       typedef double floating_point_type;
00056       typedef unsigned int natural_number_type;
00057       virtual const ResultElement* self() const { return this; }
00058       virtual ~ResultElement() {}
00059     };
00060 
00061     // #################
00062 
00072     class ResultElement_with_name : public ResultElement {
00073       string_type name_;
00074     public :
00075       typedef OKlib::Concepts::ResultElementWithName_tag concept_tag;
00076       ResultElement_with_name() {}
00077       ResultElement_with_name(const string_type& name) : name_(name) {}
00078       string_type name() const { return name_; }
00079       const ResultElement_with_name* self() const { return this; }
00080     };
00081 
00082     std::ostream& operator <<(std::ostream& out, const ResultElement_with_name& e) {
00083       return out << e.name();
00084     }
00085 
00086     bool operator ==(const ResultElement_with_name& lhs, const ResultElement_with_name& rhs) {
00087       return lhs.name() == rhs.name();
00088     }
00089     OKLIB_DERIVED_UNEQUAL(ResultElement_with_name)
00090 
00091     bool operator <(const ResultElement_with_name& lhs, const ResultElement_with_name& rhs) {
00092       return lhs.name() < rhs.name();
00093     }
00094     OKLIB_DERIVED_ORDERRELATIONS(ResultElement_with_name)
00095 
00096     // #################
00097     
00098     class SuperSeries : public ResultElement_with_name {
00099     public :
00100       SuperSeries() {}
00101       SuperSeries(const string_type& name) : ResultElement_with_name(name) {}
00102       const SuperSeries* self() const { return this; }
00103     };
00104     class RandomKSat : public SuperSeries {
00105       natural_number_type k;
00106     public :
00107       RandomKSat() {}
00108       RandomKSat(const string_type& name, const natural_number_type k) : SuperSeries(name), k(k) {}
00109       natural_number_type clause_length() const { return k; }
00110       const RandomKSat* self() const { return this; }
00111     };
00112 
00113     // #################
00114 
00115     class Series  : public ResultElement_with_name {
00116     public :
00117       Series() {}
00118       Series(const string_type& name) : ResultElement_with_name(name) {}
00119       const Series* self() const { return this; }
00120     };
00121     class Series_with_n : public Series {
00122       natural_number_type n;
00123     public :
00124       Series_with_n() {}
00125       Series_with_n(const string_type& name, const natural_number_type n) : Series(name), n(n) {}
00126       natural_number_type count_variables() const { return n; }
00127       const Series_with_n* self() const { return this; }
00128     };
00129     class RandomKSat_n : public Series_with_n {
00130     public :
00131       RandomKSat_n() {}
00132       RandomKSat_n(const string_type& name, const natural_number_type n) : Series_with_n(name, n) {}
00133       const RandomKSat_n* self() const { return this; }
00134     };
00135 
00136     // #################
00137 
00138     typedef std::pair<SuperSeries, Series> SpecSeries;
00139 
00140     std::ostream& operator <<(std::ostream& out, const SpecSeries& series) {
00141       return out << series.first << "::" << series.second;
00142     }
00143 
00144     typedef std::pair<RandomKSat, RandomKSat_n> SpecRandomKSat;
00145 
00146     // #################
00147 
00148     class Benchmark  : public ResultElement_with_name {
00149     public :
00150       Benchmark() {}
00151       Benchmark(const string_type& name) : ResultElement_with_name(name) {}
00152       const Benchmark* self() const { return this; }
00153     };
00154 
00155     // #################
00156 
00157     class Solver  : public ResultElement_with_name {
00158     public :
00159       Solver() {}
00160       Solver(const string_type& name) : ResultElement_with_name(name) {}
00161       const Solver* self() const { return this; }
00162     };
00163 
00164     // #################
00165 
00172     enum SolverResult { unknown = 0, sat = 10, unsat = 20, error = 1 };
00173 
00179     class SATStatus : public ResultElement {
00180       SolverResult result_;
00181     public :
00182       SATStatus() {}
00183       SATStatus(const SolverResult result) : result_(result) {}
00184       SolverResult result() const { return result_; }
00185       const SATStatus* self() const { return this; }
00186     };
00187 
00188     std::ostream& operator <<(std::ostream& out, const SATStatus& e) {
00189       return out << e.result();
00190     }
00191 
00192     bool operator ==(const SATStatus& lhs, const SATStatus& rhs) {
00193       return lhs.result() == rhs.result();
00194     }
00195     OKLIB_DERIVED_UNEQUAL(SATStatus)
00196 
00197     bool operator <(const SATStatus& lhs, const SATStatus& rhs) {
00198       return lhs.result() < rhs.result();
00199     }
00200     OKLIB_DERIVED_ORDERRELATIONS(SATStatus)
00201 
00202     // #################
00203 
00204     class AverageTime : public ResultElement {
00205       floating_point_type average_;
00206     public :
00207       AverageTime() {}
00208       AverageTime(const floating_point_type average) : average_(average) {}
00209       floating_point_type average() const { return average_; }
00210       const AverageTime* self() const { return this; }
00211     };
00212 
00213     std::ostream& operator <<(std::ostream& out, const AverageTime& e) {
00214       return out << e.average();
00215     }
00216 
00217     bool operator ==(const AverageTime& lhs, const AverageTime& rhs) {
00218       return lhs.average() == rhs.average();
00219     }
00220     OKLIB_DERIVED_UNEQUAL(AverageTime)
00221 
00222     // #################
00223 
00224     class TimeOut : public ResultElement {
00225       natural_number_type time_out_;
00226     public :
00227       TimeOut() {}
00228       TimeOut(const natural_number_type time_out) : time_out_(time_out) {}
00229       natural_number_type time_out() const { return time_out_; }
00230       const TimeOut* self() const { return this; }
00231     };
00232 
00233     std::ostream& operator <<(std::ostream& out, const TimeOut& e) {
00234       return out << e.time_out();
00235     }
00236  
00237     bool operator ==(const TimeOut& lhs, const TimeOut& rhs) {
00238       return lhs.time_out() == rhs.time_out();
00239     }
00240     OKLIB_DERIVED_UNEQUAL(TimeOut)
00241 
00242     bool operator <(const TimeOut& lhs, const TimeOut& rhs) {
00243       return lhs.time_out() < rhs.time_out();
00244     }
00245     OKLIB_DERIVED_ORDERRELATIONS(TimeOut)
00246 
00247     // ######################################################
00248     // ######################################################
00249 
00250     // ToDo: This should go into a separate file
00251     
00252     typedef boost::tuple<SuperSeries, Series, Benchmark, Solver, SATStatus, AverageTime, TimeOut> TupleResult;
00253 
00254     inline std::ostream& operator <<(std::ostream& out, const TupleResult& t) {
00255       return out << t.get<0>() << " " << t.get<1>() << " " << t.get<2>() << " " << t.get<3>() << " " << t.get<4>() << " " << t.get<5>() << " " << t.get<6>();
00256     }
00257 
00258     typedef boost::tuple<RandomKSat, RandomKSat_n, Benchmark, Solver, SATStatus, AverageTime, TimeOut> TupleResultRandomSat;
00259 
00260     inline std::ostream& operator <<(std::ostream& out, const TupleResultRandomSat& t) {
00261       return out << t.get<0>() << " " << t.get<1>() << " " << t.get<2>() << " " << t.get<3>() << " " << t.get<4>() << " " << t.get<5>() << " " << t.get<6>();
00262     }
00263 
00264     template <class result_type>
00265     struct tuple_type;
00266 
00267     // #################
00268 
00269     class ResultBasis {
00270       // ToDo: This should be an instance of a general pattern.
00271       // Instead of all the name duplications, the elements should be
00272       // accessible via the type name, e.g., element<SuperSeries>().
00273       // Template metaprogramming should yield a generic result container, for a given typelist.
00274     public :
00275       const SuperSeries& super_series() const { return super_series_(); };
00276       const Series& series() const { return series_(); }
00277       const Benchmark& benchmark() const { return benchmark_(); }
00278       const Solver& solver() const { return solver_(); }
00279       const SATStatus& sat_status() const { return sat_status_(); }
00280       const AverageTime& average() const { return average_(); }
00281       const TimeOut& time_out() const { return time_out_(); }
00282       virtual ~ResultBasis() {}
00283     private :
00284       virtual const SuperSeries& super_series_() const = 0;
00285       virtual const Series& series_() const = 0;
00286       virtual const Benchmark& benchmark_() const = 0;
00287       virtual const Solver& solver_() const = 0;
00288       virtual const SATStatus& sat_status_() const = 0;
00289       virtual const AverageTime& average_() const = 0;
00290       virtual const TimeOut& time_out_() const = 0;
00291     };
00292 
00293     std::ostream& operator <<(std::ostream& out, const ResultBasis& r) {
00294       return out << r.super_series() << " " <<r.series() << " " <<r.benchmark() << " " << r.solver() << " " << r.sat_status() << " " << r.average() << " " <<r.time_out();
00295     }
00296     std::ostream& operator <<(std::ostream& out, const ResultBasis* const r) {
00297       return out << r -> super_series() << " " <<r -> series() << " " <<r -> benchmark() << " " << r -> solver() << " " << r -> sat_status() << " " << r -> average() << " " <<r -> time_out();
00298     }
00299 
00300     // #################
00301 
00302     template <typename CharT, typename ParseIterator>
00303     struct ParserEmpty;
00304     template <class Result, typename CharT = char, typename ParseIterator = const CharT*, class ParserExtension = ParserEmpty<CharT, ParseIterator> > class ParserResult;
00305 
00306     class Result : public ResultBasis {
00307       template <class, typename, typename, class>
00308       friend class ParserResult; // ToDo: Only when the first template parameter is this class Result, we should have a friend --- but this seems not to be possible?
00309 
00310       SuperSeries* sup_ser;
00311       Series* ser;
00312       Benchmark* bench;
00313       Solver* solv;
00314       SATStatus* sat_stat;
00315       AverageTime* avg;
00316       TimeOut* tmo;
00317 
00318       const SuperSeries& super_series_() const {
00319         assert(sup_ser);
00320         return *sup_ser;
00321       };
00322       const Series& series_() const {
00323         assert(ser);
00324         return *ser;
00325       }
00326       const Benchmark& benchmark_() const {
00327         assert(bench);
00328         return *bench;
00329       }
00330       const Solver& solver_() const {
00331         assert(solv);
00332         return *solv;
00333       }
00334       const SATStatus& sat_status_() const {
00335         assert(sat_stat);
00336         return *sat_stat;
00337       }
00338       const AverageTime& average_() const {
00339         assert(avg);
00340         return *avg;
00341       }
00342       const TimeOut& time_out_() const {
00343         assert(tmo);
00344         return *tmo;
00345       }
00346     public :
00347 
00348       Result() : sup_ser(new SuperSeries), ser(new Series), bench(new Benchmark), solv(new Solver), sat_stat(new SATStatus), avg(new AverageTime), tmo(new TimeOut) {}
00349 
00350       Result(const TupleResult& r) : sup_ser(new SuperSeries(r.get<0>())), ser(new Series(r.get<1>())), bench(new Benchmark(r.get<2>())), solv(new Solver(r.get<3>())), sat_stat(new SATStatus(r.get<4>())), avg(new AverageTime(r.get<5>())), tmo(new TimeOut(r.get<6>())) {}
00351 
00352       Result(const Result& r) : sup_ser(new SuperSeries(*r.sup_ser)), ser(new Series(*r.ser)), bench(new Benchmark(*r.bench)), solv(new Solver(*r.solv)), sat_stat(new SATStatus(*r.sat_stat)), avg(new AverageTime(*r.avg)), tmo(new TimeOut(*r.tmo)) {}
00353 
00354       Result& operator =(const Result& rhs) {
00355         Result new_r(rhs);
00356         std::swap(new_r.sup_ser, sup_ser);
00357         std::swap(new_r.ser, ser);
00358         std::swap(new_r.bench, bench);
00359         std::swap(new_r.solv, solv);
00360         std::swap(new_r.sat_stat, sat_stat);
00361         std::swap(new_r.avg, avg);
00362         std::swap(new_r.tmo, tmo);
00363         return *this;
00364       }
00365 
00366       ~Result() {
00367         assert(sup_ser); delete sup_ser; 
00368         assert(ser); delete ser;
00369         assert(bench); delete bench;
00370         assert(solv); delete solv;
00371         assert(sat_stat); delete sat_stat;
00372         assert(avg); delete avg;
00373         assert(tmo); delete tmo;
00374       }
00375     };
00376 
00377     bool operator ==(const TupleResult& lhs, const Result& rhs) {
00378       return lhs.get<0>() == rhs.super_series() and lhs.get<1>() == rhs.series() and lhs.get<2>() == rhs.benchmark() and lhs.get<3>() == rhs.solver() and lhs.get<4>() == rhs.sat_status() and lhs.get<5>() == rhs.average() and lhs.get<6>() == rhs.time_out();
00379     }
00380     bool operator ==(const Result& lhs, const TupleResult& rhs) {
00381       return rhs == lhs;
00382     }
00383     bool operator !=(const TupleResult& lhs, const Result& rhs) {
00384       return not (lhs == rhs);
00385     }
00386     bool operator !=(const Result& lhs, const TupleResult& rhs) {
00387       return not (lhs == rhs);
00388     }
00389 
00390     template <>
00391     struct tuple_type<Result> {
00392       typedef TupleResult type;
00393     };
00394 
00395     // #################
00396 
00397     class ResultRandomSatBasis : public ResultBasis {
00398     public :
00399       const RandomKSat& super_series_random() const { return super_series_random_(); }
00400       const RandomKSat_n& series_random() const { return series_random_(); }
00401     private :
00402       virtual const RandomKSat& super_series_random_() const = 0;
00403       const SuperSeries& super_series_() const { return super_series_random_(); }
00404       virtual const RandomKSat_n& series_random_() const = 0;
00405       virtual const Series& series_() const { return series_random_(); }
00406     };
00407 
00408     class ResultRandomSat : public ResultRandomSatBasis {
00409       template <class, typename, typename, class>
00410       friend class ParserResult; // ToDo: Only when the first template parameter is this class Result, we should have a friend --- but this seems not to be possible?
00411 
00412       RandomKSat* sup_ser;
00413       RandomKSat_n* ser;
00414       Benchmark* bench;
00415       Solver* solv;
00416       SATStatus* sat_stat;
00417       AverageTime* avg;
00418       TimeOut* tmo;
00419 
00420       const RandomKSat& super_series_random_() const {
00421         assert(sup_ser);
00422         return *sup_ser;
00423       };
00424       const RandomKSat_n& series_random_() const {
00425         assert(ser);
00426         return *ser;
00427       }
00428       const Benchmark& benchmark_() const {
00429         assert(bench);
00430         return *bench;
00431       }
00432       const Solver& solver_() const {
00433         assert(solv);
00434         return *solv;
00435       }
00436       const SATStatus& sat_status_() const { assert(sat_stat);
00437         return *sat_stat;
00438       }
00439       const AverageTime& average_() const {
00440         assert(avg);
00441         return *avg;
00442       }
00443       const TimeOut& time_out_() const {
00444         assert(tmo);
00445         return *tmo;
00446       }
00447     public :
00448 
00449       ResultRandomSat() : sup_ser(new RandomKSat), ser(new RandomKSat_n), bench(new Benchmark), solv(new Solver), sat_stat(new SATStatus), avg(new AverageTime), tmo(new TimeOut) {}
00450 
00451       ResultRandomSat(const ResultRandomSat& r) : sup_ser(new RandomKSat(*r.sup_ser)), ser(new RandomKSat_n(*r.ser)), bench(new Benchmark(*r.bench)), solv(new Solver(*r.solv)), sat_stat(new SATStatus(*r.sat_stat)), avg(new AverageTime(*r.avg)), tmo(new TimeOut(*r.tmo)) {}
00452 
00453       ResultRandomSat& operator =(const ResultRandomSat& rhs) {
00454         ResultRandomSat new_r(rhs);
00455         std::swap(new_r.sup_ser, sup_ser);
00456         std::swap(new_r.ser, ser);
00457         std::swap(new_r.bench, bench);
00458         std::swap(new_r.solv, solv);
00459         std::swap(new_r.sat_stat, sat_stat);
00460         std::swap(new_r.avg, avg);
00461         std::swap(new_r.tmo, tmo);
00462         return *this;
00463       }
00464 
00465       ~ResultRandomSat() {
00466         assert(sup_ser); delete sup_ser; 
00467         assert(ser); delete ser;
00468         assert(bench); delete bench;
00469         assert(solv); delete solv;
00470         assert(sat_stat); delete sat_stat;
00471         assert(avg); delete avg;
00472         assert(tmo); delete tmo;
00473       }
00474       
00475     };
00476 
00477     bool operator ==(const TupleResultRandomSat& lhs, const ResultRandomSat& rhs) {
00478       return lhs.get<0>() == rhs.super_series() and lhs.get<1>() == rhs.series() and lhs.get<2>() == rhs.benchmark() and lhs.get<3>() == rhs.solver() and lhs.get<4>() == rhs.sat_status() and lhs.get<5>() == rhs.average() and lhs.get<6>() == rhs.time_out();
00479     }
00480     bool operator ==(const ResultRandomSat& lhs, const TupleResultRandomSat& rhs) {
00481       return rhs == lhs;
00482     }
00483     bool operator !=(const TupleResultRandomSat& lhs, const ResultRandomSat& rhs) {
00484       return not (lhs == rhs);
00485     }
00486     bool operator !=(const ResultRandomSat& lhs, const TupleResultRandomSat& rhs) {
00487       return not (lhs == rhs);
00488     }
00489 
00490     template <>
00491     struct tuple_type<ResultRandomSat> {
00492       typedef TupleResultRandomSat type;
00493     };
00494 
00495   }
00496 
00497 }
00498 
00499 #endif