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< PurseScoring >	test_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

typedef std::map<Benchmark, SetResultNodesP*> OKlib::SATCompetition::MapBenchmark

Definition at line 49 of file ResultProcessing.hpp.

typedef std::map<SATStatus, SetResultNodesP*> OKlib::SATCompetition::MapSATStatus

Definition at line 51 of file ResultProcessing.hpp.

typedef std::map<Series, SetResultNodesP*> OKlib::SATCompetition::MapSeries

Definition at line 48 of file ResultProcessing.hpp.

typedef std::map<Solver, SetResultNodesP*> OKlib::SATCompetition::MapSolver

Definition at line 50 of file ResultProcessing.hpp.

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

Definition at line 47 of file ResultProcessing.hpp.

typedef std::map<TimeOut, SetResultNodesP*> OKlib::SATCompetition::MapTimeOut

Definition at line 52 of file ResultProcessing.hpp.

typedef std::set<const ResultNode*> OKlib::SATCompetition::SetResultNodesP

Definition at line 43 of file ResultProcessing.hpp.

typedef std::pair<RandomKSat, RandomKSat_n> OKlib::SATCompetition::SpecRandomKSat

Definition at line 144 of file SingleResult.hpp.

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

Definition at line 138 of file SingleResult.hpp.

typedef boost::tuple<RandomKSat, RandomKSat_n, Benchmark, Solver, SATStatus, AverageTime, TimeOut> OKlib::SATCompetition::TupleResultRandomSat

Definition at line 258 of file SingleResult.hpp.

typedef std::vector<const ResultNode*> OKlib::SATCompetition::VectorResultNodesP

Definition at line 71 of file ResultProcessing.hpp.

Enumeration Type Documentation

enum OKlib::SATCompetition::SolverResult

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

OKlib::SATCompetition::OKLIB_DERIVED_UNEQUAL ( SATStatus ) const

OKlib::SATCompetition::OKLIB_DERIVED_UNEQUAL ( AverageTime )

Definition at line 220 of file SingleResult.hpp.

OKlib::SATCompetition::OKLIB_DERIVED_UNEQUAL ( TimeOut ) const

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
	)

Definition at line 82 of file SingleResult.hpp.

References OKlib::SATCompetition::ResultElement_with_name::name().

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 &	r
	)

Definition at line 293 of file SingleResult.hpp.

References OKlib::SATCompetition::ResultBasis::average(), OKlib::SATCompetition::ResultBasis::benchmark(), OKlib::SATCompetition::ResultBasis::sat_status(), OKlib::SATCompetition::ResultBasis::series(), OKlib::SATCompetition::ResultBasis::solver(), OKlib::SATCompetition::ResultBasis::super_series(), and OKlib::SATCompetition::ResultBasis::time_out().

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
	)

Definition at line 86 of file SingleResult.hpp.

References OKlib::SATCompetition::ResultElement_with_name::name().

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 TupleResult &	lhs,
		const Result &	rhs
	)

Definition at line 377 of file SingleResult.hpp.

References OKlib::SATCompetition::ResultBasis::average(), OKlib::SATCompetition::ResultBasis::benchmark(), OKlib::SATCompetition::ResultBasis::sat_status(), OKlib::SATCompetition::ResultBasis::series(), OKlib::SATCompetition::ResultBasis::solver(), OKlib::SATCompetition::ResultBasis::super_series(), and OKlib::SATCompetition::ResultBasis::time_out().

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

Definition at line 380 of file SingleResult.hpp.

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

Definition at line 477 of file SingleResult.hpp.

References OKlib::SATCompetition::ResultBasis::average(), OKlib::SATCompetition::ResultBasis::benchmark(), OKlib::SATCompetition::ResultBasis::sat_status(), OKlib::SATCompetition::ResultBasis::series(), OKlib::SATCompetition::ResultBasis::solver(), OKlib::SATCompetition::ResultBasis::super_series(), and OKlib::SATCompetition::ResultBasis::time_out().

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]`