Default clasp format printer. More...

#include <clasp_output.h>

Inheritance diagram for Clasp::Cli::TextOutput:

Public Types
enum	CategoryKey { cat_comment, cat_value, cat_objective, cat_result, cat_value_term, cat_atom, num_cat }
enum	Format { format_asp, format_aspcomp, format_sat09, format_pb09 }
enum	ResultStr { res_unknonw = 0, res_sat = 1, res_unsat = 2, res_opt = 3, num_str }
Public Member Functions
void	comment (uint32 v, const char *fmt,...) const
	Prints a comment message.
virtual void	onEvent (const Event &ev)
	Prints progress events (preprocessing/solving) if verbosity() > 1.
virtual void	printModel (const SymbolTable &sym, const Model &m, PrintLevel x)
	Prints the given model.
virtual void	printStatistics (const ClaspFacade::Summary &s, bool final)
	Shall print the given statistics.
virtual void	printSummary (const ClaspFacade::Summary &s, bool final)
	Called once a solving step has completed.
virtual void	run (const char solver, const char version, const std::string begInput, const std::string endInput)
	Prints a (comment) message containing the given solver and input.
virtual void	shutdown ()
virtual void	startStep (const ClaspFacade &)
	A solving step has started.
	TextOutput (uint32 verbosity, Format f, const char *catAtom=0, char ifs= ' ')
	~TextOutput ()
Public Attributes
const char *	format [num_cat]
const char *	result [num_str]
Private Member Functions
void	printCosts (const SharedMinimizeData &) const
virtual void	printNames (const SymbolTable &sym, const Model &m)
int	printSep (CategoryKey c) const
void	printSolveProgress (const Event &ev)
void	setState (uint32 state, uint32 verb, const char *st)
void	startObject (const char *n, uint32 i) const
void	startSection (const char *n) const
virtual void	visitCoreSolverStats (double cpuTime, uint64 models, const SolverStats &stats, bool accu)
virtual void	visitExtSolverStats (const ExtendedStats &stats, bool accu)
virtual void	visitHcc (uint32 i, const SharedContext &ctx)
virtual void	visitHccs (const SharedContext &ctx)
virtual void	visitJumpStats (const JumpStats &stats, bool accu)
virtual void	visitLogicProgramStats (const Asp::LpStats &stats)
virtual void	visitProblemStats (const ProblemStats &stats, const Asp::LpStats *lp)
virtual void	visitProblemStats (const ProblemStats &stats)
virtual void	visitSolverStats (const Clasp::SolverStats &s, bool accu)
virtual void	visitThread (uint32 i, const SolverStats &s)
virtual void	visitThreads (const SharedContext &ctx)
Private Attributes
Clasp::atomic< int >	ev_
char	ifs_ [2]
int	line_
uint32	state_
double	stTime_
int	width_

Detailed Description

Default clasp format printer.

Prints all output to stdout in given format:

format_asp prints in clasp's default asp format
format_aspcomp prints in in ASP competition format
format_sat09 prints in SAT-competition format
format_pb09 in PB-competition format

See also:: https://www.mat.unical.it/aspcomp2013/; http://www.satcompetition.org/2009/format-solvers2009.html; http://www.cril.univ-artois.fr/PB09/solver_req.html

Definition at line 179 of file clasp_output.h.

Member Enumeration Documentation

enum Clasp::Cli::TextOutput::CategoryKey

Enumerator:

cat_comment
cat_value
cat_objective
cat_result
cat_value_term
cat_atom
num_cat

Definition at line 183 of file clasp_output.h.

enum Clasp::Cli::TextOutput::Format

Enumerator:

format_asp
format_aspcomp
format_sat09
format_pb09

Definition at line 181 of file clasp_output.h.

enum Clasp::Cli::TextOutput::ResultStr

Enumerator:

res_unknonw
res_sat
res_unsat
res_opt
num_str

Definition at line 182 of file clasp_output.h.

Constructor & Destructor Documentation

Clasp::Cli::TextOutput::TextOutput	(	uint32	verbosity,
		Format	f,
		const char *	catAtom = `0`,
		char	ifs = `' '`
	)

Definition at line 565 of file clasp_output.cpp.

Clasp::Cli::TextOutput::~TextOutput ( )

Definition at line 621 of file clasp_output.cpp.

Member Function Documentation

void Clasp::Cli::TextOutput::comment	(	uint32	v,
		const char *	fmt,
			...
	)		const

Prints a comment message.

Definition at line 623 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::onEvent ( const Event & ev ) [virtual]

Prints progress events (preprocessing/solving) if verbosity() > 1.

Reimplemented from Clasp::Cli::Output.

Definition at line 691 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::printCosts ( const SharedMinimizeData & costs ) const [private]

Definition at line 808 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::printModel	(	const SymbolTable &	sym,
		const Model &	m,
		PrintLevel	x
	)		`[virtual]`

Prints the given model.

Prints format[cat_value] followed by the elements of the model. Individual elements e are printed as format[cat_atom] and separated by the internal field separator.

Implements Clasp::Cli::Output.

Definition at line 762 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::printNames	(	const SymbolTable &	sym,
		const Model &	m
	)		`[private, virtual]`

Definition at line 797 of file clasp_output.cpp.

int Clasp::Cli::TextOutput::printSep ( CategoryKey c ) const [private]

Definition at line 759 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::printSolveProgress ( const Event & ev ) [private]

Definition at line 732 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::printStatistics	(	const ClaspFacade::Summary &	summary,
		bool	final
	)		`[virtual]`

Shall print the given statistics.

Implements Clasp::Cli::Output.

Definition at line 683 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::printSummary	(	const ClaspFacade::Summary &	s,
		bool	final
	)		`[virtual]`

Called once a solving step has completed.

Always prints "format[cat_result] result[s.result()]". Furthermore, if verbosity() > 0, prints a summary consisting of

the number of computed models m and whether the search space was exhausted
the number of enumerated models e if e != m
the state of any optimization and whether the last model was optimal
the state of consequence computation and whether the last model corresponded to the consequences
timing information

Implements Clasp::Cli::Output.

Definition at line 642 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::run	(	const char *	solver,
		const char *	version,
		const std::string *	begInput,
		const std::string *	endInput
	)		`[virtual]`

Prints a (comment) message containing the given solver and input.

Implements Clasp::Cli::Output.

Definition at line 634 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::setState	(	uint32	state,
		uint32	verb,
		const char *	st
	)		`[private]`

Definition at line 718 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::shutdown ( ) [virtual]

Implements Clasp::Cli::Output.

Definition at line 641 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::startObject	(	const char *	n,
		uint32	i
	)		const `[private]`

Definition at line 819 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::startSection ( const char * n ) const [private]

Definition at line 815 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::startStep ( const ClaspFacade & f ) [virtual]

A solving step has started.

Reimplemented from Clasp::Cli::Output.

Definition at line 687 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::visitCoreSolverStats	(	double	cpuTime,
		uint64	models,
		const SolverStats &	stats,
		bool	accu
	)		`[private, virtual]`

Implements Clasp::Cli::StatsVisitor.

Definition at line 876 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::visitExtSolverStats	(	const ExtendedStats &	stats,
		bool	accu
	)		`[private, virtual]`

Implements Clasp::Cli::StatsVisitor.

Definition at line 892 of file clasp_output.cpp.

virtual void Clasp::Cli::TextOutput::visitHcc	(	uint32	i,
		const SharedContext &	ctx
	)		`[inline, private, virtual]`

Reimplemented from Clasp::Cli::StatsVisitor.

Definition at line 231 of file clasp_output.h.

virtual void Clasp::Cli::TextOutput::visitHccs ( const SharedContext & ctx ) [inline, private, virtual]

Reimplemented from Clasp::Cli::StatsVisitor.

Definition at line 230 of file clasp_output.h.

void Clasp::Cli::TextOutput::visitJumpStats	(	const JumpStats &	stats,
		bool	accu
	)		`[private, virtual]`

Implements Clasp::Cli::StatsVisitor.

Definition at line 927 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::visitLogicProgramStats ( const Asp::LpStats & stats ) [private, virtual]

Implements Clasp::Cli::StatsVisitor.

Definition at line 832 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::visitProblemStats	(	const ProblemStats &	stats,
		const Asp::LpStats *	lp
	)		`[private, virtual]`

Reimplemented from Clasp::Cli::StatsVisitor.

Definition at line 823 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::visitProblemStats ( const ProblemStats & stats ) [private, virtual]

Implements Clasp::Cli::StatsVisitor.

Definition at line 866 of file clasp_output.cpp.

void Clasp::Cli::TextOutput::visitSolverStats	(	const Clasp::SolverStats &	s,
		bool	accu
	)		`[private, virtual]`

Reimplemented from Clasp::Cli::StatsVisitor.

Definition at line 827 of file clasp_output.cpp.

virtual void Clasp::Cli::TextOutput::visitThread	(	uint32	i,
		const SolverStats &	s
	)		`[inline, private, virtual]`

Reimplemented from Clasp::Cli::StatsVisitor.

Definition at line 229 of file clasp_output.h.

virtual void Clasp::Cli::TextOutput::visitThreads ( const SharedContext & ctx ) [inline, private, virtual]

Reimplemented from Clasp::Cli::StatsVisitor.

Definition at line 228 of file clasp_output.h.

Member Data Documentation

Clasp::atomic<int> Clasp::Cli::TextOutput::ev_ [private]

Definition at line 239 of file clasp_output.h.

const char* Clasp::Cli::TextOutput::format[num_cat]

Format strings.

Definition at line 186 of file clasp_output.h.

char Clasp::Cli::TextOutput::ifs_[2] [private]

Definition at line 243 of file clasp_output.h.

int Clasp::Cli::TextOutput::line_ [private]

Definition at line 241 of file clasp_output.h.

const char* Clasp::Cli::TextOutput::result[num_str]

Default result strings.

Definition at line 185 of file clasp_output.h.

uint32 Clasp::Cli::TextOutput::state_ [private]

Definition at line 242 of file clasp_output.h.

double Clasp::Cli::TextOutput::stTime_ [private]

Definition at line 238 of file clasp_output.h.

int Clasp::Cli::TextOutput::width_ [private]

Definition at line 240 of file clasp_output.h.

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

Public Types

Public Member Functions

Public Attributes

Private Member Functions

Private Attributes

Detailed Description

Member Enumeration Documentation

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation