#include <parser_smtlib_utils.h>

Inheritance diagram for smtrat::parseformula::FormulaCollector:

Collaboration diagram for smtrat::parseformula::FormulaCollector:

[legend]

Public Types
typedef types::AttributeValue	Value

Public Member Functions
void	add (const smtrat::FormulaT &f)

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

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

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

void	getProof ()

void	getUnsatCore ()

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

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

void	pop (std::size_t)

void	push (std::size_t)

void	reset ()

void	resetAssertions ()

void	setLogic (const carl::Logic &l)

int	getExitCode () const

FormulaT	getFormula () const

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

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::vector< FormulaT >	mFormulas

carl::Logic	mLogic

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

std::vector< smtrat::ModelVariable >	mArtificialVariables

Detailed Description

Definition at line 7 of file parser_smtlib_utils.h.

Member Typedef Documentation

◆ Value

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

inherited

Definition at line 48 of file InstructionHandler.h.

Member Function Documentation

◆ add()

void smtrat::parseformula::FormulaCollector::add ( const smtrat::FormulaT & f )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 12 of file parser_smtlib_utils.h.

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

void smtrat::parseformula::FormulaCollector::addObjective	(	const smtrat::Poly &	,
		smtrat::parser::OptimizationType
	)

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 33 of file parser_smtlib_utils.h.

◆ addSoft()

void smtrat::parseformula::FormulaCollector::addSoft	(	const FormulaT &	f,
		Rational	,
		const std::string &
	)

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 15 of file parser_smtlib_utils.h.

◆ annotateName()

void smtrat::parseformula::FormulaCollector::annotateName	(	const smtrat::FormulaT &	,
		const std::string &
	)

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 18 of file parser_smtlib_utils.h.

◆ check()

void smtrat::parseformula::FormulaCollector::check ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 19 of file parser_smtlib_utils.h.

◆ cleanModel()

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

inlineinherited

Definition at line 69 of file InstructionHandler.h.

◆ declareFun()

void smtrat::parseformula::FormulaCollector::declareFun ( const carl::Variable & )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 20 of file parser_smtlib_utils.h.

◆ declareSort()

void smtrat::parseformula::FormulaCollector::declareSort	(	const std::string &	,
		const unsigned &
	)

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 21 of file parser_smtlib_utils.h.

◆ defineSort()

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

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 22 of file parser_smtlib_utils.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()

void smtrat::parseformula::FormulaCollector::exit ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 24 of file parser_smtlib_utils.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()

void smtrat::parseformula::FormulaCollector::getAllModels ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 26 of file parser_smtlib_utils.h.

◆ getAssertions()

void smtrat::parseformula::FormulaCollector::getAssertions ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 25 of file parser_smtlib_utils.h.

◆ getAssignment()

void smtrat::parseformula::FormulaCollector::getAssignment ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 27 of file parser_smtlib_utils.h.

◆ getExitCode()

int smtrat::parseformula::FormulaCollector::getExitCode ( ) const

inline

Definition at line 41 of file parser_smtlib_utils.h.

◆ getFormula()

FormulaT smtrat::parseformula::FormulaCollector::getFormula ( ) const

inline

Definition at line 45 of file parser_smtlib_utils.h.

◆ 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:

◆ getLogic()

auto smtrat::parseformula::FormulaCollector::getLogic ( ) const

inline

Definition at line 48 of file parser_smtlib_utils.h.

◆ getModel()

void smtrat::parseformula::FormulaCollector::getModel ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 28 of file parser_smtlib_utils.h.

◆ getObjectives()

void smtrat::parseformula::FormulaCollector::getObjectives ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 29 of file parser_smtlib_utils.h.

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

void smtrat::parseformula::FormulaCollector::getProof ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 30 of file parser_smtlib_utils.h.

◆ getUnsatCore()

void smtrat::parseformula::FormulaCollector::getUnsatCore ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 31 of file parser_smtlib_utils.h.

◆ getValue()

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

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 32 of file parser_smtlib_utils.h.

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

void smtrat::parseformula::FormulaCollector::pop ( std::size_t )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 34 of file parser_smtlib_utils.h.

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

void smtrat::parseformula::FormulaCollector::push ( std::size_t )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 35 of file parser_smtlib_utils.h.

◆ qe()

void smtrat::parseformula::FormulaCollector::qe ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 23 of file parser_smtlib_utils.h.

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

void smtrat::parseformula::FormulaCollector::reset ( )

inlinevirtual

Reimplemented from smtrat::parser::InstructionHandler.

Definition at line 36 of file parser_smtlib_utils.h.

◆ resetAssertions()

void smtrat::parseformula::FormulaCollector::resetAssertions ( )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 37 of file parser_smtlib_utils.h.

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

void smtrat::parseformula::FormulaCollector::setLogic ( const carl::Logic & l )

inlinevirtual

Implements smtrat::parser::InstructionHandler.

Definition at line 38 of file parser_smtlib_utils.h.

◆ 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

◆ 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.

◆ mArtificialVariables

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

privateinherited

Definition at line 52 of file InstructionHandler.h.

◆ mDiagnostic

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

protectedinherited

Definition at line 94 of file InstructionHandler.h.

◆ mFormulas

std::vector<FormulaT> smtrat::parseformula::FormulaCollector::mFormulas

private

Definition at line 9 of file parser_smtlib_utils.h.

◆ mLogic

carl::Logic smtrat::parseformula::FormulaCollector::mLogic

private

Definition at line 10 of file parser_smtlib_utils.h.

◆ mRegular

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

protectedinherited

Definition at line 93 of file InstructionHandler.h.

◆ options

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

protectedinherited

Definition at line 76 of file InstructionHandler.h.

◆ streams

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

protectedinherited

Definition at line 95 of file InstructionHandler.h.

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

cli/tools/parser_smtlib_utils.h

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Private Attributes

Detailed Description

Member Typedef Documentation

◆ Value

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

◆ getFormula()

◆ getInfo()

◆ getLogic()

◆ 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

◆ mFormulas

◆ mLogic

◆ mRegular

◆ options

◆ streams