OKlibrary  0.2.1.6
OKlib::SATCompetition Namespace Reference

Tools for evaluating SAT competition (under various circumstances) More...

Namespaces

namespace  Testobjects
namespace  traits

Classes

class  ElementaryAnalysis
 Given a "database" of results, computes an "indexed database", providing elementary maps, for example assiging to a solver the set of solved benchmarks, and elementary sets, for example the set of "complete" solvers. More...
class  Test_ElementaryAnalysis
class  LexicographicalEvaluation
 Given an "indexed database" of results, map each solver to the map, which assigns to each solved super-series the map, which assigns to each solved series the pair of solved-count and average running time. More...
class  LexicographicalEvaluationRandom
 Given an "indexed database" of results, map each super-series to the set of solver-resultvector pairs, where the resultvectors contain the series evaluations computed by LexicographicalEvaluation, and the order of these pairs is some variation of lexicographical order. More...
struct  LexicographicalEvaluationRandom_from_file
class  Test_RepresentationSolverSeries
 Tests representations of the run of a solver on a series. More...
class  Test_LexicographicalEvaluation
 Testing the basic facility for lexicographical evaluation. More...
class  Test_LexicographicalEvaluationRandom
 Testing lexicographical evaluation. More...
struct  LexicographicalSeriesPolicy< Result >
struct  LexicographicalSeriesPolicy< ResultRandomSat >
class  LexicographicalSortingPolicy_induced_lexicographical
 Policy for LexicographicalEvaluationRandom yielding the order of evaluation vectors which is the lexicographical order based on the order given for numerics_solver_on_series_type. More...
class  LexicographicalSortingPolicy_unfolded_lexicographical
 Policy for LexicographicalEvaluationRandom yielding the order of evaluation vectors which is the lexicographical order when unfolding the pairs, that is, first all first components, then all second components. More...
class  ParserResultSequence
struct  Copy_results
struct  Copy_results_from_file
struct  Copy_results_from_file_to_container
class  Test_Copy_results_fill_from_file
class  Test_Copy_results_ParserResult_Result_positive_cases
class  Test_Copy_results_ParserResult_Result_negative_cases
class  Test_Copy_results_ParserResult_Result
class  Test_Copy_results_ParserResultRandomSat_ResultRandomSat_positive_cases
class  Test_Copy_results_ParserResultRandomSat_ResultRandomSat
struct  ParserError
class  ParserResultElement< SuperSeries, CharT, ParseIterator >
class  ParserResultElement< RandomKSat, CharT, ParseIterator >
class  ParserResultElement< Series, CharT, ParseIterator >
class  ParserResultElement< RandomKSat_n, CharT, ParseIterator >
class  ParserResultElement< Benchmark, CharT, ParseIterator >
class  ParserResultElement< Solver, CharT, ParseIterator >
class  ParserResultElement< SATStatus, CharT, ParseIterator >
class  ParserResultElement< AverageTime, CharT, ParseIterator >
class  ParserResultElement< TimeOut, CharT, ParseIterator >
struct  ParserEmpty
struct  ParserThreeElements
class  ParserResult< Result, CharT, ParseIterator, ParserExtension >
class  ParserResult< ResultRandomSat, CharT, ParseIterator, ParserExtension >
class  Test_ParserResultElement_SuperSeries_positive_cases
class  Test_ParserResultElement_SuperSeries_negative_cases
class  Test_ParserResultElement_SuperSeries
class  Test_ParserResultElement_RandomKSat_positive_cases
class  Test_ParserResultElement_RandomKSat_negative_cases
class  Test_ParserResultElement_RandomKSat
class  Test_ParserResultElement_Series_positive_cases
class  Test_ParserResultElement_Series_negative_cases
class  Test_ParserResultElement_Series
class  Test_ParserResultElement_RandomKSat_n_positive_cases
class  Test_ParserResultElement_RandomKSat_n_negative_cases
class  Test_ParserResultElement_RandomKSat_n
class  Test_ParserResultElement_Benchmark_positive_cases
class  Test_ParserResultElement_Benchmark_negative_cases
class  Test_ParserResultElement_Benchmark
class  Test_ParserResultElement_Solver_positive_cases
class  Test_ParserResultElement_Solver_negative_cases
class  Test_ParserResultElement_Solver
class  Test_ParserResultElement_SATStatus_positive_cases
class  Test_ParserResultElement_SATStatus_negative_cases
class  Test_ParserResultElement_SATStatus
class  Test_ParserResultElement_AverageTime_positive_cases
class  Test_ParserResultElement_AverageTime_negative_cases
class  Test_ParserResultElement_AverageTime
class  Test_ParserResultElement_TimeOut_positive_cases
class  Test_ParserResultElement_TimeOut_negative_cases
class  Test_ParserResultElement_TimeOut
struct  Add_positive_result_tuples< Container, TupleResult >
struct  Add_positive_result_tuples< Container, TupleResultRandomSat >
class  Test_ParserResult_Result_positive_cases
class  Test_ParserResult_Result_negative_cases
class  Test_ParserResult_Result
class  Test_ParserResult_ResultRandomSat_positive_cases
class  Test_ParserResult_ResultRandomSat
struct  ResultNode
class  ResultDatabase
 Creates the undirected ("bi-directed") bipartite attribute-result graphs from a sequence of results, and enables computation of the set of common results for a set of attribute-values (for different attributes). More...
struct  Result_database_from_file
class  Check_sizes
class  Check_set
class  Test_Database_vs_Container
class  Test_ResultDatabase_ResultIterator
class  ConstantSeriesPurse
 Policy for PurseScoring, which does not change the series purse. More...
class  SAT2005SeriesPurse
 Policy for PurseScoring, which does divides the series purse by 3, if only 4 or less benchmarks are in the series. More...
class  PurseScoring
 Computing score(solver) = problem_purse(solver) + speed_award(solver) + series_purse(solver). More...
class  Scoring_from_file
 Given a file with competition results, computes sorted lists of scores for the SAT, UNSAT and SAT+UNSAT categories. More...
class  Test_PurseScoring
class  ResultElement
 Polymorphic base class for the representation of various forms of "results". More...
class  ResultElement_with_name
 Addition of a name to SATCompetition::ResultElement, by which result elements can be alphabetically sorted. More...
class  RandomKSat
class  Series
class  Series_with_n
class  RandomKSat_n
class  Benchmark
class  Solver
class  SATStatus
 Special result element representing the return value of the solver. More...
class  ResultBasis
class  Result
struct  tuple_type< Result >
class  ResultRandomSatBasis
class  ResultRandomSat
struct  tuple_type< ResultRandomSat >

Typedefs

typedef std::set< const
ResultNode * > 
SetResultNodesP
typedef std::map< SuperSeries,
SetResultNodesP * > 
MapSuperSeries
typedef std::map< Series,
SetResultNodesP * > 
MapSeries
typedef std::map< Benchmark,
SetResultNodesP * > 
MapBenchmark
typedef std::map< Solver,
SetResultNodesP * > 
MapSolver
typedef std::map< SATStatus,
SetResultNodesP * > 
MapSATStatus
typedef std::map< TimeOut,
SetResultNodesP * > 
MapTimeOut
typedef std::vector< const
ResultNode * > 
VectorResultNodesP
typedef std::pair< SuperSeries,
Series
SpecSeries
typedef std::pair< RandomKSat,
RandomKSat_n
SpecRandomKSat
typedef boost::tuple
< RandomKSat, RandomKSat_n,
Benchmark, Solver, SATStatus,
AverageTime, TimeOut > 
TupleResultRandomSat

Enumerations

enum  SolverResult { unknown = 0, sat = 10, unsat = 20, error = 1 }
 Codes for return values of SAT solvers. More...

Functions

template<class ParserResult , class OutputIterator >
Copy_results< ParserResult,
OutputIterator >
::parse_info_it 
copy_results (const typename ParserResult::ParseIterator begin_in, const typename ParserResult::ParseIterator end_in, const OutputIterator begin_out)
template<class ParserResult , typename PIterator , class OutputIterator >
Copy_results< ParserResult,
OutputIterator >::parse_info_c 
copy_results (const PIterator begin_in, const OutputIterator begin_out)
template<class Container >
Test_Copy_results_fill_from_file
< Container > 
test_Copy_results_fill_from_file (const boost::filesystem::path &filename, Container &C)
template<class Container >
void add_positive_result_tuples (Container &C)
std::ostream & operator<< (std::ostream &out, const ResultNode &r)
std::ostream & operator<< (std::ostream &out, const VectorResultNodesP &vec)
template<class Map , typename Size >
Check_sizes< Map, Size > check_sizes (const Map &m, const Size s)
template<class Map , class Set >
Check_set< Map, Set > check_set (const Map &m, const Set &s)
template<class ResultDatabase , class ResultContainer >
Test_Database_vs_Container
< ResultDatabase,
ResultContainer > 
test_Database_vs_Container (ResultDatabase &rdb, ResultContainer &rc)
std::ostream & operator<< (std::ostream &out, const ResultElement_with_name &e)
bool operator== (const ResultElement_with_name &lhs, const ResultElement_with_name &rhs)
 OKLIB_DERIVED_UNEQUAL (ResultElement_with_name) bool operator<(const ResultElement_with_name &lhs
std::ostream & operator<< (std::ostream &out, const SpecSeries &series)
std::ostream & operator<< (std::ostream &out, const SATStatus &e)
bool operator== (const SATStatus &lhs, const SATStatus &rhs)
 OKLIB_DERIVED_UNEQUAL (SATStatus) bool operator<(const SATStatus &lhs
std::ostream & operator<< (std::ostream &out, const AverageTime &e)
bool operator== (const AverageTime &lhs, const AverageTime &rhs)
 OKLIB_DERIVED_UNEQUAL (AverageTime) class TimeOut
std::ostream & operator<< (std::ostream &out, const TimeOut &e)
bool operator== (const TimeOut &lhs, const TimeOut &rhs)
 OKLIB_DERIVED_UNEQUAL (TimeOut) bool operator<(const TimeOut &lhs
std::ostream & operator<< (std::ostream &out, const TupleResult &t)
std::ostream & operator<< (std::ostream &out, const TupleResultRandomSat &t)
std::ostream & operator<< (std::ostream &out, const ResultBasis &r)
std::ostream & operator<< (std::ostream &out, const ResultBasis *const r)
bool operator== (const TupleResult &lhs, const Result &rhs)
bool operator== (const Result &lhs, const TupleResult &rhs)
bool operator!= (const TupleResult &lhs, const Result &rhs)
bool operator!= (const Result &lhs, const TupleResult &rhs)
bool operator== (const TupleResultRandomSat &lhs, const ResultRandomSat &rhs)
bool operator== (const ResultRandomSat &lhs, const TupleResultRandomSat &rhs)
bool operator!= (const TupleResultRandomSat &lhs, const ResultRandomSat &rhs)
bool operator!= (const ResultRandomSat &lhs, const TupleResultRandomSat &rhs)

Variables

Test_ElementaryAnalysis
< ElementaryAnalysis
test_elementary_analysis
Test_RepresentationSolverSeries
< LexicographicalEvaluation
test_representation_solver_series
Test_LexicographicalEvaluation
< LexicographicalEvaluation
test_lexicographical_evaluation
Test_LexicographicalEvaluationRandom
< LexicographicalEvaluationRandom
test_lexicographical_evaluation_random
Test_Copy_results_ParserResult_Result test_CopyResults
Test_Copy_results_ParserResultRandomSat_ResultRandomSat test_CopyResultsRandomSat
const std::string filename_large_industrial = "Data/export-industrial_2005_Round1.txt"
const unsigned int line_count_large_industrial = 17168
const std::string filename_large_random = "Data/export-random_2005_Round1_corrected.txt"
const unsigned int line_count_large_random = 11700
Test_PurseScoring< PurseScoringtest_PurseScoring
 Series
 Benchmark
 Solver
 SATStatus
 AverageTime
TimeOut TupleResult
::OKlib::Concepts::ResultElement_basic_test
< SATCompetition::ResultElement
test_ResultElement
::OKlib::Concepts::ResultElementWithName_basic_test
< SATCompetition::ResultElement_with_name
test_ResultElement_with_name

Detailed Description

Tools for evaluating SAT competition (under various circumstances)


Typedef Documentation

Definition at line 49 of file ResultProcessing.hpp.

Definition at line 51 of file ResultProcessing.hpp.

Definition at line 48 of file ResultProcessing.hpp.

Definition at line 50 of file ResultProcessing.hpp.

typedef std::map<SuperSeries, SetResultNodesP*> OKlib::SATCompetition::MapSuperSeries

Definition at line 47 of file ResultProcessing.hpp.

Definition at line 52 of file ResultProcessing.hpp.

Definition at line 43 of file ResultProcessing.hpp.

Definition at line 144 of file SingleResult.hpp.

typedef std::pair<SuperSeries, Series> OKlib::SATCompetition::SpecSeries

Definition at line 138 of file SingleResult.hpp.

Definition at line 71 of file ResultProcessing.hpp.


Enumeration Type Documentation

Codes for return values of SAT solvers.

Todo:
This should come from the general library ?!
Enumerator:
unknown 
sat 
unsat 
error 

Definition at line 172 of file SingleResult.hpp.


Function Documentation

template<class Container >
void OKlib::SATCompetition::add_positive_result_tuples ( Container &  C) [inline]

Definition at line 590 of file ParsingSingleResult_Tests.hpp.

template<class Map , class Set >
Check_set<Map, Set> OKlib::SATCompetition::check_set ( const Map &  m,
const Set &  s 
) [inline]

Definition at line 94 of file ResultProcessing_Tests.hpp.

References s.

template<class Map , typename Size >
Check_sizes<Map, Size> OKlib::SATCompetition::check_sizes ( const Map &  m,
const Size  s 
) [inline]

Definition at line 56 of file ResultProcessing_Tests.hpp.

References s.

template<class ParserResult , class OutputIterator >
Copy_results<ParserResult, OutputIterator>::parse_info_it OKlib::SATCompetition::copy_results ( const typename ParserResult::ParseIterator  begin_in,
const typename ParserResult::ParseIterator  end_in,
const OutputIterator  begin_out 
) [inline]

Definition at line 75 of file ParsingResultSequences.hpp.

template<class ParserResult , typename PIterator , class OutputIterator >
Copy_results<ParserResult, OutputIterator>::parse_info_c OKlib::SATCompetition::copy_results ( const PIterator  begin_in,
const OutputIterator  begin_out 
) [inline]

Definition at line 79 of file ParsingResultSequences.hpp.

OKlib::SATCompetition::OKLIB_DERIVED_UNEQUAL ( ResultElement_with_name  ) const

Definition at line 220 of file SingleResult.hpp.

bool OKlib::SATCompetition::operator!= ( const TupleResult &  lhs,
const Result &  rhs 
)

Definition at line 383 of file SingleResult.hpp.

bool OKlib::SATCompetition::operator!= ( const Result &  lhs,
const TupleResult &  rhs 
)

Definition at line 386 of file SingleResult.hpp.

bool OKlib::SATCompetition::operator!= ( const TupleResultRandomSat &  lhs,
const ResultRandomSat &  rhs 
)

Definition at line 483 of file SingleResult.hpp.

bool OKlib::SATCompetition::operator!= ( const ResultRandomSat &  lhs,
const TupleResultRandomSat &  rhs 
)

Definition at line 486 of file SingleResult.hpp.

std::ostream& OKlib::SATCompetition::operator<< ( std::ostream &  out,
const ResultNode &  r 
) [inline]

Definition at line 67 of file ResultProcessing.hpp.

References OKlib::SATCompetition::ResultNode::rb.

std::ostream& OKlib::SATCompetition::operator<< ( std::ostream &  out,
const VectorResultNodesP &  vec 
) [inline]

Definition at line 73 of file ResultProcessing.hpp.

References end.

std::ostream& OKlib::SATCompetition::operator<< ( std::ostream &  out,
const ResultElement_with_name &  e 
)
std::ostream& OKlib::SATCompetition::operator<< ( std::ostream &  out,
const SpecSeries &  series 
)

Definition at line 140 of file SingleResult.hpp.

std::ostream& OKlib::SATCompetition::operator<< ( std::ostream &  out,
const SATStatus &  e 
)

Definition at line 188 of file SingleResult.hpp.

References OKlib::SATCompetition::SATStatus::result().

std::ostream& OKlib::SATCompetition::operator<< ( std::ostream &  out,
const AverageTime &  e 
)

Definition at line 213 of file SingleResult.hpp.

std::ostream& OKlib::SATCompetition::operator<< ( std::ostream &  out,
const TimeOut &  e 
)

Definition at line 233 of file SingleResult.hpp.

std::ostream& OKlib::SATCompetition::operator<< ( std::ostream &  out,
const TupleResult &  t 
) [inline]

Definition at line 254 of file SingleResult.hpp.

std::ostream& OKlib::SATCompetition::operator<< ( std::ostream &  out,
const TupleResultRandomSat &  t 
) [inline]

Definition at line 260 of file SingleResult.hpp.

std::ostream& OKlib::SATCompetition::operator<< ( std::ostream &  out,
const ResultBasis *const  r 
)

Definition at line 296 of file SingleResult.hpp.

bool OKlib::SATCompetition::operator== ( const ResultElement_with_name &  lhs,
const ResultElement_with_name &  rhs 
)
bool OKlib::SATCompetition::operator== ( const SATStatus &  lhs,
const SATStatus &  rhs 
)

Definition at line 192 of file SingleResult.hpp.

References OKlib::SATCompetition::SATStatus::result().

bool OKlib::SATCompetition::operator== ( const AverageTime &  lhs,
const AverageTime &  rhs 
)

Definition at line 217 of file SingleResult.hpp.

bool OKlib::SATCompetition::operator== ( const TimeOut &  lhs,
const TimeOut &  rhs 
)

Definition at line 237 of file SingleResult.hpp.

bool OKlib::SATCompetition::operator== ( const Result &  lhs,
const TupleResult &  rhs 
)

Definition at line 380 of file SingleResult.hpp.

bool OKlib::SATCompetition::operator== ( const ResultRandomSat &  lhs,
const TupleResultRandomSat &  rhs 
)

Definition at line 480 of file SingleResult.hpp.

template<class Container >
Test_Copy_results_fill_from_file<Container> OKlib::SATCompetition::test_Copy_results_fill_from_file ( const boost::filesystem::path &  filename,
Container &  C 
) [inline]

Definition at line 43 of file ParsingResultSequences_Tests.hpp.

template<class ResultDatabase , class ResultContainer >
Test_Database_vs_Container<ResultDatabase, ResultContainer> OKlib::SATCompetition::test_Database_vs_Container ( ResultDatabase &  rdb,
ResultContainer &  rc 
) [inline]

Definition at line 247 of file ResultProcessing_Tests.hpp.


Variable Documentation

const std::string OKlib::SATCompetition::filename_large_industrial = "Data/export-industrial_2005_Round1.txt"

Definition at line 99 of file ParsingResultSequences_Tests.hpp.

const std::string OKlib::SATCompetition::filename_large_random = "Data/export-random_2005_Round1_corrected.txt"

Definition at line 156 of file ParsingResultSequences_Tests.hpp.

Definition at line 100 of file ParsingResultSequences_Tests.hpp.

Definition at line 157 of file ParsingResultSequences_Tests.hpp.

Definition at line 252 of file SingleResult.hpp.

Definition at line 252 of file SingleResult.hpp.