benchmax::SMTRAT Class Reference

Tool wrapper for SMT-RAT for SMT-LIB. More...

#include <SMTRAT.h>

Inheritance diagram for benchmax::SMTRAT:

Collaboration diagram for benchmax::SMTRAT:

Public Member Functions
	SMTRAT (const fs::path &binary, const std::string &arguments)
	New SMT-RAT tool. More...
virtual bool	canHandle (const fs::path &path) const override
	Only handle .smt2 files. More...
std::string	getStatusFromOutput (const BenchmarkResult &result) const
	Try to parse memouts from stderr. More...
bool	parse_stats (BenchmarkResult &result) const
virtual void	additionalResults (const fs::path &, BenchmarkResult &result) const override
	Computes the answer string from the exit code and parses statistics output. More...
std::string	name () const
	Common name of this tool. More...
fs::path	binary () const
	Full path to the binary. More...
const std::map< std::string, std::string > &	attributes () const
	A set of attributes, for example compilation options. More...
std::vector< std::string >	resolveDependencies () const
	Get dependencies of binary required to run it (via ldd) More...
std::size_t	attributeHash () const
	Hash of the attributes. More...
virtual std::string	getCommandline (const std::string &file) const
	Compose commandline for this tool and the given input file. More...
virtual std::string	getCommandline (const std::string &file, const std::string &localBinary) const
	Compose commandline for this tool with another binary name and the given input file. More...
virtual std::optional< std::string >	parseCommandline (const std::string &cmdline) const
	Compose commandline for this tool and the given input file. More...

Protected Attributes
std::string	mName
	(Non-unique) identifier for the tool. More...
fs::path	mBinary
	Path to the binary. More...
std::string	mArguments
	Command line arguments that should be passed to the binary. More...
std::map< std::string, std::string >	mAttributes
	Attributes of the tool obtained by introspection of the binary. More...

Detailed Description

Tool wrapper for SMT-RAT for SMT-LIB.

Definition at line 63 of file SMTRAT.h.

Constructor & Destructor Documentation

SMTRAT()

benchmax::SMTRAT::SMTRAT ( const fs::path &  binary, const std::string &  arguments  )

inline

New SMT-RAT tool.

Definition at line 66 of file SMTRAT.h.

Here is the call graph for this function:

Member Function Documentation

additionalResults()

virtual void benchmax::SMTRAT::additionalResults ( const fs::path &  , BenchmarkResult &  result  ) const

inlineoverridevirtual

Computes the answer string from the exit code and parses statistics output.

Reimplemented from benchmax::Tool.

Definition at line 115 of file SMTRAT.h.

Here is the call graph for this function:

attributeHash()

std::size_t benchmax::Tool::attributeHash ( ) const

inlineinherited

Hash of the attributes.

Definition at line 112 of file Tool.h.

attributes()

const std::map<std::string,std::string>& benchmax::Tool::attributes ( ) const

inlineinherited

A set of attributes, for example compilation options.

Definition at line 72 of file Tool.h.

binary()

fs::path benchmax::Tool::binary ( ) const

inlineinherited

Full path to the binary.

Definition at line 67 of file Tool.h.

Here is the caller graph for this function:

canHandle()

virtual bool benchmax::SMTRAT::canHandle ( const fs::path &  path ) const

inlineoverridevirtual

Only handle .smt2 files.

Reimplemented from benchmax::Tool.

Reimplemented in benchmax::SMTRAT_OPB.

Definition at line 71 of file SMTRAT.h.

Here is the call graph for this function:

getCommandline() [1/2]

virtual std::string benchmax::Tool::getCommandline ( const std::string &  file ) const

inlinevirtualinherited

Compose commandline for this tool and the given input file.

Definition at line 122 of file Tool.h.

Here is the caller graph for this function:

getCommandline() [2/2]

virtual std::string benchmax::Tool::getCommandline ( const std::string &  file, const std::string &  localBinary  ) const

inlinevirtualinherited

Compose commandline for this tool with another binary name and the given input file.

Definition at line 126 of file Tool.h.

getStatusFromOutput()

std::string benchmax::SMTRAT::getStatusFromOutput ( const BenchmarkResult &  result ) const

inline

Try to parse memouts from stderr.

Definition at line 76 of file SMTRAT.h.

Here is the caller graph for this function:

name()

std::string benchmax::Tool::name ( ) const

inlineinherited

Common name of this tool.

Definition at line 62 of file Tool.h.

Here is the caller graph for this function:

parse_stats()

bool benchmax::SMTRAT::parse_stats ( BenchmarkResult &  result ) const

inline

Definition at line 82 of file SMTRAT.h.

Here is the call graph for this function:

Here is the caller graph for this function:

parseCommandline()

virtual std::optional<std::string> benchmax::Tool::parseCommandline ( const std::string &  cmdline ) const

inlinevirtualinherited

Compose commandline for this tool and the given input file.

Definition at line 130 of file Tool.h.

Here is the call graph for this function:

resolveDependencies()

std::vector<std::string> benchmax::Tool::resolveDependencies ( ) const

inlineinherited

Get dependencies of binary required to run it (via ldd)

Definition at line 77 of file Tool.h.

Here is the call graph for this function:

Field Documentation

mArguments

std::string benchmax::Tool::mArguments

protectedinherited

Command line arguments that should be passed to the binary.

Definition at line 45 of file Tool.h.

mAttributes

std::map<std::string,std::string> benchmax::Tool::mAttributes

protectedinherited

Attributes of the tool obtained by introspection of the binary.

Definition at line 47 of file Tool.h.

mBinary

fs::path benchmax::Tool::mBinary

protectedinherited

Path to the binary.

Definition at line 43 of file Tool.h.

mName

std::string benchmax::Tool::mName

protectedinherited

(Non-unique) identifier for the tool.

Definition at line 41 of file Tool.h.

---

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

• benchmax/tools/SMTRAT.h