OKlibrary  0.2.1.6
OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy > Class Template Reference

Given a file with competition results, computes sorted lists of scores for the SAT, UNSAT and SAT+UNSAT categories. More...

#include <Scoring.hpp>

List of all members.

Classes

class  scoring
 Contains scoring related data for one solver. More...
struct  series_info
struct  solved_series

Public Types

typedef
Result_database_from_file
< ParserResult, ResultClass,
ParserExtension > 
result_database_from_file
typedef
result_database_from_file::database_type 
database
typedef ElementaryAnalysis
< database
indexed_database
typedef PurseScoring
< indexed_database,
SeriesPursePolicy > 
purse_scoring_type
typedef
purse_scoring_type::number_type 
number_type
typedef std::vector< scoringscoring_vector

Public Member Functions

 Scoring_from_file (const std::string file_name, const number_type standard_problem_purse=1000, const number_type standard_speed_factor=1, const number_type standard_series_factor=3)

Public Attributes

result_database_from_file rdb
indexed_database idb
scoring_vector scores_all
scoring_vector scores_sat
scoring_vector scores_unsat
const number_type standard_problem_purse
const number_type standard_speed_factor
const number_type standard_series_factor

Detailed Description

template<template< typename CharT, typename ParseIterator > class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
class OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >

Given a file with competition results, computes sorted lists of scores for the SAT, UNSAT and SAT+UNSAT categories.

Todo:

PROBLEM: When restricting to the SAT or to the UNSAT case (see objects rdb_sat and rdb_unsat), then it might happen that in case less then 5 but at least one of the benchmarks in the series has been solved, that we apply the rule for diminishing the series purse by the factor of three to the series, while actually the series had enough SAT resp. UNSAT instances in them.

Additional to the current computation for the SAT+UNSAT category, compute the scores when considering only "complete" solvers.

This class is a "blob" --- many things are done here, which should be split over several classes.

Definition at line 353 of file Scoring.hpp.


Member Typedef Documentation

template<template< typename CharT, typename ParseIterator > class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
typedef result_database_from_file::database_type OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >::database

Definition at line 355 of file Scoring.hpp.

template<template< typename CharT, typename ParseIterator > class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
typedef ElementaryAnalysis<database> OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >::indexed_database

Definition at line 356 of file Scoring.hpp.

template<template< typename CharT, typename ParseIterator > class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
typedef purse_scoring_type::number_type OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >::number_type

Definition at line 362 of file Scoring.hpp.

template<template< typename CharT, typename ParseIterator > class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
typedef PurseScoring<indexed_database, SeriesPursePolicy> OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >::purse_scoring_type

Definition at line 357 of file Scoring.hpp.

template<template< typename CharT, typename ParseIterator > class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
typedef Result_database_from_file<ParserResult, ResultClass, ParserExtension> OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >::result_database_from_file

Definition at line 354 of file Scoring.hpp.

template<template< typename CharT, typename ParseIterator > class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
typedef std::vector<scoring> OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >::scoring_vector

Definition at line 431 of file Scoring.hpp.


Constructor & Destructor Documentation

template<template< typename CharT, typename ParseIterator > class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >::Scoring_from_file ( const std::string  file_name,
const number_type  standard_problem_purse = 1000,
const number_type  standard_speed_factor = 1,
const number_type  standard_series_factor = 3 
) [inline]

Member Data Documentation

template<template< typename CharT, typename ParseIterator > class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
indexed_database OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >::idb
template<template< typename CharT, typename ParseIterator > class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
result_database_from_file OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >::rdb
template<template< typename CharT, typename ParseIterator > class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
scoring_vector OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >::scores_all
template<template< typename CharT, typename ParseIterator > class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
scoring_vector OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >::scores_sat
template<template< typename CharT, typename ParseIterator > class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
scoring_vector OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >::scores_unsat
template<template< typename CharT, typename ParseIterator > class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
const number_type OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >::standard_problem_purse
template<template< typename CharT, typename ParseIterator > class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
const number_type OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >::standard_series_factor
template<template< typename CharT, typename ParseIterator > class ParserExtension = ParserEmpty, class ResultClass = Result, class SeriesPursePolicy = SAT2005SeriesPurse>
const number_type OKlib::SATCompetition::Scoring_from_file< ParserExtension, ResultClass, SeriesPursePolicy >::standard_speed_factor

The documentation for this class was generated from the following file: