#include <InstructionHandler.h>

Inheritance diagram for smtrat::parser::InstructionHandler:

Collaboration diagram for smtrat::parser::InstructionHandler:

[legend]

Public Types
typedef types::AttributeValue	Value

Public Member Functions
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

	InstructionHandler ()

virtual	~InstructionHandler ()

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	add (const FormulaT &f)=0

virtual void	addSoft (const FormulaT &f, Rational weight, const std::string &id)=0

virtual void	annotateName (const FormulaT &f, const std::string &name)=0

virtual void	check ()=0

virtual void	declareFun (const carl::Variable &)=0

virtual void	declareSort (const std::string &, const unsigned &)=0

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

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

virtual void	qe ()=0

virtual void	exit ()=0

virtual void	getAllModels ()=0

virtual void	getAssertions ()=0

virtual void	getAssignment ()=0

void	getInfo (const std::string &key)

virtual void	getModel ()=0

virtual void	getObjectives ()=0

void	getOption (const std::string &key)

virtual void	getProof ()=0

virtual void	getUnsatCore ()=0

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

virtual void	addObjective (const Poly &p, OptimizationType ot)=0

virtual void	pop (std::size_t)=0

virtual void	push (std::size_t)=0

virtual void	reset ()

virtual void	resetAssertions ()=0

void	setInfo (const Attribute &attr)

virtual void	setLogic (const carl::Logic &)=0

void	setOption (const Attribute &option)

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
std::queue< std::function< void()> >	instructionQueue

std::vector< smtrat::ModelVariable >	mArtificialVariables

Detailed Description

Definition at line 46 of file InstructionHandler.h.

Member Typedef Documentation

◆ Value

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

Definition at line 48 of file InstructionHandler.h.

Constructor & Destructor Documentation

◆ InstructionHandler()

smtrat::parser::InstructionHandler::InstructionHandler ( )

inline

Definition at line 109 of file InstructionHandler.h.

Here is the call graph for this function:

◆ ~InstructionHandler()

virtual smtrat::parser::InstructionHandler::~InstructionHandler ( )

inlinevirtual

Definition at line 114 of file InstructionHandler.h.

Member Function Documentation

◆ add()

virtual void smtrat::parser::InstructionHandler::add ( const FormulaT & f )

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

Here is the caller graph for this function:

◆ addInstruction()

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

inline

Definition at line 54 of file InstructionHandler.h.

Here is the caller graph for this function:

◆ addObjective()

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

pure virtual

Implemented in smtrat::Executor< Strategy >, and smtrat::parseformula::FormulaCollector.

Here is the caller graph for this function:

◆ addSoft()

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

pure virtual

Implemented in smtrat::Executor< Strategy >, and smtrat::parseformula::FormulaCollector.

Here is the caller graph for this function:

◆ annotateName()

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

pure virtual

Implemented in smtrat::Executor< Strategy >, and smtrat::parseformula::FormulaCollector.

Here is the caller graph for this function:

◆ check()

virtual void smtrat::parser::InstructionHandler::check ( )

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

Here is the caller graph for this function:

◆ cleanModel()

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

inline

Definition at line 69 of file InstructionHandler.h.

◆ declareFun()

virtual void smtrat::parser::InstructionHandler::declareFun ( const carl::Variable & )

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

◆ declareSort()

virtual void smtrat::parser::InstructionHandler::declareSort	(	const std::string &	,
		const unsigned &
	)

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

◆ defineSort()

virtual void smtrat::parser::InstructionHandler::defineSort	(	const std::string &	,
		const std::vector< std::string > &	,
		const carl::Sort &
	)

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

◆ diagnostic() [1/2]

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

inline

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 )

inline

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 )

inlinevirtual

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 ( )

inline

Definition at line 130 of file InstructionHandler.h.

Here is the caller graph for this function:

◆ exit()

virtual void smtrat::parser::InstructionHandler::exit ( )

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

Here is the caller graph for this function:

◆ get_info()

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

inline

Definition at line 81 of file InstructionHandler.h.

◆ getAllModels()

virtual void smtrat::parser::InstructionHandler::getAllModels ( )

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

Here is the caller graph for this function:

◆ getAssertions()

virtual void smtrat::parser::InstructionHandler::getAssertions ( )

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

Here is the caller graph for this function:

◆ getAssignment()

virtual void smtrat::parser::InstructionHandler::getAssignment ( )

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

Here is the caller graph for this function:

◆ getInfo()

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

inline

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()

virtual void smtrat::parser::InstructionHandler::getModel ( )

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

Here is the caller graph for this function:

◆ getObjectives()

virtual void smtrat::parser::InstructionHandler::getObjectives ( )

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

Here is the caller graph for this function:

◆ getOption()

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

inline

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()

virtual void smtrat::parser::InstructionHandler::getProof ( )

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

Here is the caller graph for this function:

◆ getUnsatCore()

virtual void smtrat::parser::InstructionHandler::getUnsatCore ( )

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

Here is the caller graph for this function:

◆ getValue()

virtual void smtrat::parser::InstructionHandler::getValue ( const std::vector< carl::Variable > & )

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

◆ has_info()

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

inline

Definition at line 78 of file InstructionHandler.h.

◆ hasInstructions()

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

inline

Definition at line 57 of file InstructionHandler.h.

Here is the caller graph for this function:

◆ info()

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

inline

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

inline

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()

virtual void smtrat::parser::InstructionHandler::pop ( std::size_t )

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

Here is the caller graph for this function:

◆ printInstruction()

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

inline

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()

virtual void smtrat::parser::InstructionHandler::push ( std::size_t )

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

Here is the caller graph for this function:

◆ qe()

virtual void smtrat::parser::InstructionHandler::qe ( )

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

Here is the caller graph for this function:

◆ regular() [1/2]

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

inline

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 )

inline

Definition at line 127 of file InstructionHandler.h.

Here is the call graph for this function:

◆ reset()

virtual void smtrat::parser::InstructionHandler::reset ( )

inlinevirtual

Reimplemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

Definition at line 170 of file InstructionHandler.h.

Here is the caller graph for this function:

◆ resetAssertions()

virtual void smtrat::parser::InstructionHandler::resetAssertions ( )

pure virtual

Implemented in smtrat::parseformula::FormulaCollector, and smtrat::Executor< Strategy >.

Here is the caller graph for this function:

◆ runInstructions()

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

inline

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 )

inline

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 )

inline

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()

virtual void smtrat::parser::InstructionHandler::setLogic ( const carl::Logic & )

pure virtual

Implemented in smtrat::Executor< Strategy >, and smtrat::parseformula::FormulaCollector.

Here is the caller graph for this function:

◆ setOption()

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

inline

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
	)

inlineprotected

Definition at line 97 of file InstructionHandler.h.

Here is the caller graph for this function:

◆ warn()

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

inline

Definition at line 133 of file InstructionHandler.h.

Here is the caller graph for this function:

Field Documentation

◆ infos

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

protected

Definition at line 75 of file InstructionHandler.h.

◆ instructionQueue

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

private

Definition at line 51 of file InstructionHandler.h.

◆ mArtificialVariables

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

private

Definition at line 52 of file InstructionHandler.h.

◆ mDiagnostic

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

protected

Definition at line 94 of file InstructionHandler.h.

◆ mRegular

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

protected

Definition at line 93 of file InstructionHandler.h.

◆ options

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

protected

Definition at line 76 of file InstructionHandler.h.

◆ streams

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

protected

Definition at line 95 of file InstructionHandler.h.

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

cli/parser/InstructionHandler.h

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Private Attributes

Detailed Description

Member Typedef Documentation

◆ Value

Constructor & Destructor Documentation

◆ InstructionHandler()

◆ ~InstructionHandler()

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()

◆ 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

◆ infos

◆ instructionQueue

◆ mArtificialVariables

◆ mDiagnostic

◆ mRegular

◆ options

◆ streams