#include <Executor.h>

Inheritance diagram for smtrat::Executor< Strategy >:

Collaboration diagram for smtrat::Executor< Strategy >:

[legend]

Public Types
typedef types::AttributeValue	Value

Public Member Functions
	Executor (Strategy &solver)

	~Executor ()

void	add (const smtrat::FormulaT &f)

void	addSoft (const smtrat::FormulaT &f, smtrat::Rational weight, const std::string &id)

void	annotateName (const smtrat::FormulaT &f, const std::string &name)

void	check ()

void	declareFun (const carl::Variable &)

void	declareSort (const std::string &, const unsigned &)

void	defineSort (const std::string &, const std::vector< std::string > &, const carl::Sort &)

void	qe ()

void	exit ()

void	getAssertions ()

void	getAllModels ()

void	getAssignment ()

void	getModel ()

void	getProof ()

void	getObjectives ()

void	getUnsatCore ()

void	getValue (const std::vector< carl::Variable > &)

void	addObjective (const smtrat::Poly &p, smtrat::parser::OptimizationType ot)

void	pop (std::size_t n)

void	push (std::size_t n)

void	reset ()

void	resetAssertions ()

void	setLogic (const carl::Logic &logic)

int	getExitCode () const

void	addInstruction (std::function< void()> bind)

bool	hasInstructions () const

void	runInstructions ()

void	setArtificialVariables (std::vector< smtrat::ModelVariable > &&vars)

void	cleanModel (smtrat::Model &model) const

bool	has_info (const std::string &key) const

const auto &	get_info (const std::string &key) const

template<typename T >
T	option (const std::string &key) const

bool	printInstruction () const

std::ostream &	diagnostic ()

void	diagnostic (const std::string &s)

std::ostream &	regular ()

void	regular (const std::string &s)

OutputWrapper	error ()

OutputWrapper	warn ()

OutputWrapper	info ()

virtual void	echo (const std::string &s)

void	getInfo (const std::string &key)

void	getOption (const std::string &key)

void	setInfo (const Attribute &attr)

void	setOption (const Attribute &option)

Data Fields
smtrat::Answer	lastAnswer

Protected Member Functions
void	setStream (const std::string &s, std::ostream &os)

Protected Attributes
VariantMap< std::string, Value >	infos

VariantMap< std::string, Value >	options

std::ostream	mRegular

std::ostream	mDiagnostic

std::map< std::string, std::ofstream >	streams

Private Attributes
execution::ExecutionState	state

Strategy &	solver

MaxSMT< Strategy, MaxSMTStrategy::LINEAR_SEARCH >	maxsmt

Optimization< Strategy >	optimization

UnsatCore< Strategy, UnsatCoreStrategy::ModelExclusion >	unsatcore

int	exitCode

std::queue< std::function< void()> >	instructionQueue

std::vector< smtrat::ModelVariable >	mArtificialVariables

Detailed Description

template<typename Strategy>
class smtrat::Executor< Strategy >

Definition at line 20 of file Executor.h.

Member Typedef Documentation

◆ Value

typedef types::AttributeValue smtrat::parser::InstructionHandler::Value

inherited

Definition at line 48 of file InstructionHandler.h.

Constructor & Destructor Documentation

◆ Executor()

template<typename Strategy >

smtrat::Executor< Strategy >::Executor ( Strategy & solver )

inline

Definition at line 29 of file Executor.h.

Here is the call graph for this function:

◆ ~Executor()

template<typename Strategy >

smtrat::Executor< Strategy >::~Executor ( )

inline

Definition at line 63 of file Executor.h.

Member Function Documentation

◆ add()

template<typename Strategy >

void smtrat::Executor< Strategy >::add ( const smtrat::FormulaT & f )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 65 of file Executor.h.

Here is the call graph for this function:

◆ addInstruction()

void smtrat::parser::InstructionHandler::addInstruction ( std::function< void()> bind )

inlineinherited

Definition at line 54 of file InstructionHandler.h.

Here is the caller graph for this function:

◆ addObjective()

template<typename Strategy >

void smtrat::Executor< Strategy >::addObjective	(	const smtrat::Poly &	p,
		smtrat::parser::OptimizationType	ot
	)

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 283 of file Executor.h.

Here is the call graph for this function:

◆ addSoft()

template<typename Strategy >

void smtrat::Executor< Strategy >::addSoft	(	const smtrat::FormulaT &	f,
		smtrat::Rational	weight,
		const std::string &	id
	)

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 78 of file Executor.h.

Here is the call graph for this function:

◆ annotateName()

template<typename Strategy >

void smtrat::Executor< Strategy >::annotateName	(	const smtrat::FormulaT &	f,
		const std::string &	name
	)

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 90 of file Executor.h.

Here is the call graph for this function:

◆ check()

template<typename Strategy >

void smtrat::Executor< Strategy >::check ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 103 of file Executor.h.

Here is the call graph for this function:

◆ cleanModel()

void smtrat::parser::InstructionHandler::cleanModel ( smtrat::Model & model ) const

inlineinherited

Definition at line 69 of file InstructionHandler.h.

◆ declareFun()

template<typename Strategy >

void smtrat::Executor< Strategy >::declareFun ( const carl::Variable & )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 171 of file Executor.h.

◆ declareSort()

template<typename Strategy >

void smtrat::Executor< Strategy >::declareSort	(	const std::string &	,
		const unsigned &
	)

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 176 of file Executor.h.

◆ defineSort()

template<typename Strategy >

void smtrat::Executor< Strategy >::defineSort	(	const std::string &	,
		const std::vector< std::string > &	,
		const carl::Sort &
	)

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 179 of file Executor.h.

◆ diagnostic() [1/2]

std::ostream& smtrat::parser::InstructionHandler::diagnostic ( )

inlineinherited

Definition at line 118 of file InstructionHandler.h.

Here is the caller graph for this function:

◆ diagnostic() [2/2]

void smtrat::parser::InstructionHandler::diagnostic ( const std::string & s )

inlineinherited

Definition at line 121 of file InstructionHandler.h.

Here is the call graph for this function:

◆ echo()

virtual void smtrat::parser::InstructionHandler::echo ( const std::string & s )

inlinevirtualinherited

Definition at line 146 of file InstructionHandler.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ error()

OutputWrapper smtrat::parser::InstructionHandler::error ( )

inlineinherited

Definition at line 130 of file InstructionHandler.h.

Here is the caller graph for this function:

◆ exit()

template<typename Strategy >

void smtrat::Executor< Strategy >::exit ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 205 of file Executor.h.

◆ get_info()

const auto& smtrat::parser::InstructionHandler::get_info ( const std::string & key ) const

inlineinherited

Definition at line 81 of file InstructionHandler.h.

◆ getAllModels()

template<typename Strategy >

void smtrat::Executor< Strategy >::getAllModels ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 218 of file Executor.h.

Here is the call graph for this function:

◆ getAssertions()

template<typename Strategy >

void smtrat::Executor< Strategy >::getAssertions ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 207 of file Executor.h.

Here is the call graph for this function:

◆ getAssignment()

template<typename Strategy >

void smtrat::Executor< Strategy >::getAssignment ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 227 of file Executor.h.

Here is the call graph for this function:

◆ getExitCode()

template<typename Strategy >

int smtrat::Executor< Strategy >::getExitCode ( ) const

inline

Definition at line 328 of file Executor.h.

Here is the caller graph for this function:

◆ getInfo()

void smtrat::parser::InstructionHandler::getInfo ( const std::string & key )

inlineinherited

Definition at line 154 of file InstructionHandler.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getModel()

template<typename Strategy >

void smtrat::Executor< Strategy >::getModel ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 233 of file Executor.h.

Here is the call graph for this function:

◆ getObjectives()

template<typename Strategy >

void smtrat::Executor< Strategy >::getObjectives ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 243 of file Executor.h.

Here is the call graph for this function:

◆ getOption()

void smtrat::parser::InstructionHandler::getOption ( const std::string & key )

inlineinherited

Definition at line 160 of file InstructionHandler.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getProof()

template<typename Strategy >

void smtrat::Executor< Strategy >::getProof ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 240 of file Executor.h.

Here is the call graph for this function:

◆ getUnsatCore()

template<typename Strategy >

void smtrat::Executor< Strategy >::getUnsatCore ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 262 of file Executor.h.

Here is the call graph for this function:

◆ getValue()

template<typename Strategy >

void smtrat::Executor< Strategy >::getValue ( const std::vector< carl::Variable > & )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 278 of file Executor.h.

Here is the call graph for this function:

◆ has_info()

bool smtrat::parser::InstructionHandler::has_info ( const std::string & key ) const

inlineinherited

Definition at line 78 of file InstructionHandler.h.

◆ hasInstructions()

bool smtrat::parser::InstructionHandler::hasInstructions ( ) const

inlineinherited

Definition at line 57 of file InstructionHandler.h.

Here is the caller graph for this function:

◆ info()

OutputWrapper smtrat::parser::InstructionHandler::info ( )

inlineinherited

Definition at line 136 of file InstructionHandler.h.

Here is the caller graph for this function:

◆ option()

template<typename T >

T smtrat::parser::InstructionHandler::option ( const std::string & key ) const

inlineinherited

Definition at line 85 of file InstructionHandler.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ pop()

template<typename Strategy >

void smtrat::Executor< Strategy >::pop ( std::size_t n )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 292 of file Executor.h.

Here is the call graph for this function:

◆ printInstruction()

bool smtrat::parser::InstructionHandler::printInstruction ( ) const

inlineinherited

Definition at line 88 of file InstructionHandler.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ push()

template<typename Strategy >

void smtrat::Executor< Strategy >::push ( std::size_t n )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 300 of file Executor.h.

Here is the call graph for this function:

◆ qe()

template<typename Strategy >

void smtrat::Executor< Strategy >::qe ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 183 of file Executor.h.

Here is the call graph for this function:

◆ regular() [1/2]

std::ostream& smtrat::parser::InstructionHandler::regular ( )

inlineinherited

Definition at line 124 of file InstructionHandler.h.

Here is the caller graph for this function:

◆ regular() [2/2]

void smtrat::parser::InstructionHandler::regular ( const std::string & s )

inlineinherited

Definition at line 127 of file InstructionHandler.h.

Here is the call graph for this function:

◆ reset()

template<typename Strategy >

void smtrat::Executor< Strategy >::reset ( )

inlinevirtual

Reimplemented from smtrat::parser::InstructionHandler.

Definition at line 308 of file Executor.h.

Here is the call graph for this function:

◆ resetAssertions()

template<typename Strategy >

void smtrat::Executor< Strategy >::resetAssertions ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 317 of file Executor.h.

Here is the call graph for this function:

◆ runInstructions()

void smtrat::parser::InstructionHandler::runInstructions ( )

inlineinherited

Definition at line 60 of file InstructionHandler.h.

Here is the caller graph for this function:

◆ setArtificialVariables()

void smtrat::parser::InstructionHandler::setArtificialVariables ( std::vector< smtrat::ModelVariable > && vars )

inlineinherited

Definition at line 66 of file InstructionHandler.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setInfo()

void smtrat::parser::InstructionHandler::setInfo ( const Attribute & attr )

inlineinherited

Definition at line 175 of file InstructionHandler.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setLogic()

template<typename Strategy >

void smtrat::Executor< Strategy >::setLogic ( const carl::Logic & logic )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 320 of file Executor.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setOption()

void smtrat::parser::InstructionHandler::setOption ( const Attribute & option )

inlineinherited

Definition at line 181 of file InstructionHandler.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setStream()

void smtrat::parser::InstructionHandler::setStream	(	const std::string &	s,
		std::ostream &	os
	)

inlineprotectedinherited

Definition at line 97 of file InstructionHandler.h.

Here is the caller graph for this function:

◆ warn()

OutputWrapper smtrat::parser::InstructionHandler::warn ( )

inlineinherited

Definition at line 133 of file InstructionHandler.h.

Here is the caller graph for this function:

Field Documentation

◆ exitCode

template<typename Strategy >

int smtrat::Executor< Strategy >::exitCode

private

Definition at line 26 of file Executor.h.

◆ infos

VariantMap<std::string, Value> smtrat::parser::InstructionHandler::infos

protectedinherited

Definition at line 75 of file InstructionHandler.h.

◆ instructionQueue

std::queue<std::function<void()> > smtrat::parser::InstructionHandler::instructionQueue

privateinherited

Definition at line 51 of file InstructionHandler.h.

◆ lastAnswer

template<typename Strategy >

smtrat::Answer smtrat::Executor< Strategy >::lastAnswer

Definition at line 28 of file Executor.h.

◆ mArtificialVariables

std::vector<smtrat::ModelVariable> smtrat::parser::InstructionHandler::mArtificialVariables

privateinherited

Definition at line 52 of file InstructionHandler.h.

◆ maxsmt

template<typename Strategy >

MaxSMT<Strategy, MaxSMTStrategy::LINEAR_SEARCH> smtrat::Executor< Strategy >::maxsmt

private

Definition at line 23 of file Executor.h.

◆ mDiagnostic

std::ostream smtrat::parser::InstructionHandler::mDiagnostic

protectedinherited

Definition at line 94 of file InstructionHandler.h.

◆ mRegular

std::ostream smtrat::parser::InstructionHandler::mRegular

protectedinherited

Definition at line 93 of file InstructionHandler.h.

◆ optimization

template<typename Strategy >

Optimization<Strategy> smtrat::Executor< Strategy >::optimization

private

Definition at line 24 of file Executor.h.

◆ options

VariantMap<std::string, Value> smtrat::parser::InstructionHandler::options

protectedinherited

Definition at line 76 of file InstructionHandler.h.

◆ solver

template<typename Strategy >

Strategy& smtrat::Executor< Strategy >::solver

private

Definition at line 22 of file Executor.h.

◆ state

template<typename Strategy >

execution::ExecutionState smtrat::Executor< Strategy >::state

private

Definition at line 21 of file Executor.h.

◆ streams

std::map<std::string, std::ofstream> smtrat::parser::InstructionHandler::streams

protectedinherited

Definition at line 95 of file InstructionHandler.h.

◆ unsatcore

template<typename Strategy >

UnsatCore<Strategy, UnsatCoreStrategy::ModelExclusion> smtrat::Executor< Strategy >::unsatcore

private

Definition at line 25 of file Executor.h.

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

cli/tools/Executor.h

Public Types

Public Member Functions

Data Fields

Protected Member Functions

Protected Attributes

Private Attributes

Detailed Description

template<typename Strategy> class smtrat::Executor< Strategy >

Member Typedef Documentation

◆ Value

Constructor & Destructor Documentation

◆ Executor()

◆ ~Executor()

Member Function Documentation

◆ add()

◆ addInstruction()

◆ addObjective()

◆ addSoft()

◆ annotateName()

◆ check()

◆ cleanModel()

◆ declareFun()

◆ declareSort()

◆ defineSort()

◆ diagnostic() [1/2]

◆ diagnostic() [2/2]

◆ echo()

◆ error()

◆ exit()

◆ get_info()

◆ getAllModels()

◆ getAssertions()

◆ getAssignment()

◆ getExitCode()

◆ getInfo()

◆ getModel()

◆ getObjectives()

◆ getOption()

◆ getProof()

◆ getUnsatCore()

◆ getValue()

◆ has_info()

◆ hasInstructions()

◆ info()

◆ option()

◆ pop()

◆ printInstruction()

◆ push()

◆ qe()

◆ regular() [1/2]

◆ regular() [2/2]

◆ reset()

◆ resetAssertions()

◆ runInstructions()

◆ setArtificialVariables()

◆ setInfo()

◆ setLogic()

◆ setOption()

◆ setStream()

◆ warn()

Field Documentation

◆ exitCode

◆ infos

◆ instructionQueue

◆ lastAnswer

◆ mArtificialVariables

◆ maxsmt

◆ mDiagnostic

◆ mRegular

◆ optimization

◆ options

◆ solver

◆ state

◆ streams

◆ unsatcore

template<typename Strategy>
class smtrat::Executor< Strategy >