#include <ExecutionState.h>

Collaboration diagram for smtrat::execution::ExecutionState:

[legend]

Public Member Functions
	ExecutionState ()

void	set_add_assertion_handler (std::function< void(const FormulaT &)> f)

void	set_add_soft_assertion_handler (std::function< void(const FormulaT &, Rational, const std::string &)> f)

void	set_add_objective_handler (std::function< void(const Poly &, bool)> f)

void	set_add_annotated_name_handler (std::function< void(const FormulaT &, const std::string &)> f)

void	set_remove_assertion_handler (std::function< void(const FormulaT &)> f)

void	set_remove_soft_assertion_handler (std::function< void(const FormulaT &)> f)

void	set_remove_objective_handler (std::function< void(const Poly &)> f)

void	set_remove_annotated_name_handler (std::function< void(const FormulaT &)> f)

bool	is_mode (Mode mode) const

void	set_logic (carl::Logic logic)

auto	logic () const

void	add_assertion (const FormulaT &formula)

bool	has_assertion (const FormulaT &formula) const

const auto &	assertions () const

void	add_soft_assertion (const FormulaT &formula, Rational weight, const std::string &id)

bool	has_soft_assertion (const FormulaT &formula) const

void	add_objective (const Poly &function, bool minimize)

bool	has_objective (const Poly &function)

void	push ()

void	push (size_t n)

void	pop ()

void	pop (size_t n)

bool	has_annotated_name (const std::string &n)

bool	has_annotated_name_formula (const smtrat::FormulaT &f)

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

void	enter_sat (const smtrat::Model &model, const ObjectiveValues &objectiveValues)

void	enter_unsat ()

const smtrat::Model &	model () const

const smtrat::ObjectiveValues &	objectiveValues () const

void	reset ()

void	reset_assertions ()

void	reset_answer ()

Private Member Functions
void	set_mode (Mode mode)

Private Attributes
Mode	mMode

carl::Logic	mLogic

std::vector< Assertion >	mAssertions

std::vector< SoftAssertion >	mSoftAssertions

std::vector< Objective >	mObjectives

std::vector< std::pair< FormulaT, std::string > >	mAnnotatedNames

std::vector< std::tuple< size_t, size_t, size_t, size_t > >	mBacktrackPoints

smtrat::Model	mModel

smtrat::ObjectiveValues	mObjectiveValues

std::function< void(const FormulaT &)>	addAssertionHandler

std::function< void(const FormulaT &, Rational, const std::string &)>	addSoftAssertionHandler

std::function< void(const Poly &, bool)>	addObjectiveHandler

std::function< void(const FormulaT &, const std::string &)>	addAnnotatedNameHandler

std::function< void(const FormulaT &)>	removeAssertionHandler

std::function< void(const FormulaT &)>	removeSoftAssertionHandler

std::function< void(const Poly &)>	removeObjectiveHandler

std::function< void(const FormulaT &)>	removeAnnotatedNameHandler

Detailed Description

Definition at line 25 of file ExecutionState.h.

Constructor & Destructor Documentation

◆ ExecutionState()

smtrat::execution::ExecutionState::ExecutionState ( )

inline

Definition at line 54 of file ExecutionState.h.

Member Function Documentation

◆ add_assertion()

void smtrat::execution::ExecutionState::add_assertion ( const FormulaT & formula )

inline

Definition at line 79 of file ExecutionState.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ add_objective()

void smtrat::execution::ExecutionState::add_objective	(	const Poly &	function,
		bool	minimize
	)

inline

Definition at line 115 of file ExecutionState.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ add_soft_assertion()

void smtrat::execution::ExecutionState::add_soft_assertion	(	const FormulaT &	formula,
		Rational	weight,
		const std::string &	id
	)

inline

Definition at line 99 of file ExecutionState.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ annotate_name()

void smtrat::execution::ExecutionState::annotate_name	(	const std::string &	name,
		const smtrat::FormulaT &	f
	)

inline

Definition at line 182 of file ExecutionState.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ assertions()

const auto& smtrat::execution::ExecutionState::assertions ( ) const

inline

Definition at line 95 of file ExecutionState.h.

Here is the caller graph for this function:

◆ enter_sat()

void smtrat::execution::ExecutionState::enter_sat	(	const smtrat::Model &	model,
		const ObjectiveValues &	objectiveValues
	)

inline

Definition at line 192 of file ExecutionState.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ enter_unsat()

void smtrat::execution::ExecutionState::enter_unsat ( )

inline

Definition at line 200 of file ExecutionState.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ has_annotated_name()

bool smtrat::execution::ExecutionState::has_annotated_name ( const std::string & n )

inline

Definition at line 174 of file ExecutionState.h.

Here is the caller graph for this function:

◆ has_annotated_name_formula()

bool smtrat::execution::ExecutionState::has_annotated_name_formula ( const smtrat::FormulaT & f )

inline

Definition at line 178 of file ExecutionState.h.

Here is the caller graph for this function:

◆ has_assertion()

bool smtrat::execution::ExecutionState::has_assertion ( const FormulaT & formula ) const

inline

Definition at line 91 of file ExecutionState.h.

Here is the caller graph for this function:

◆ has_objective()

bool smtrat::execution::ExecutionState::has_objective ( const Poly & function )

inline

Definition at line 126 of file ExecutionState.h.

Here is the caller graph for this function:

◆ has_soft_assertion()

bool smtrat::execution::ExecutionState::has_soft_assertion ( const FormulaT & formula ) const

inline

Definition at line 111 of file ExecutionState.h.

Here is the caller graph for this function:

◆ is_mode()

bool smtrat::execution::ExecutionState::is_mode ( Mode mode ) const

inline

Definition at line 66 of file ExecutionState.h.

Here is the caller graph for this function:

◆ logic()

auto smtrat::execution::ExecutionState::logic ( ) const

inline

Definition at line 75 of file ExecutionState.h.

Here is the caller graph for this function:

◆ model()

const smtrat::Model& smtrat::execution::ExecutionState::model ( ) const

inline

Definition at line 206 of file ExecutionState.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ objectiveValues()

const smtrat::ObjectiveValues& smtrat::execution::ExecutionState::objectiveValues ( ) const

inline

Definition at line 211 of file ExecutionState.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ pop() [1/2]

void smtrat::execution::ExecutionState::pop ( )

inline

Definition at line 139 of file ExecutionState.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ pop() [2/2]

void smtrat::execution::ExecutionState::pop ( size_t n )

inline

Definition at line 170 of file ExecutionState.h.

Here is the call graph for this function:

◆ push() [1/2]

void smtrat::execution::ExecutionState::push ( )

inline

Definition at line 130 of file ExecutionState.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ push() [2/2]

void smtrat::execution::ExecutionState::push ( size_t n )

inline

Definition at line 136 of file ExecutionState.h.

Here is the call graph for this function:

◆ reset()

void smtrat::execution::ExecutionState::reset ( )

inline

Definition at line 216 of file ExecutionState.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ reset_answer()

void smtrat::execution::ExecutionState::reset_answer ( )

inline

Definition at line 240 of file ExecutionState.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ reset_assertions()

void smtrat::execution::ExecutionState::reset_assertions ( )

inline

Definition at line 231 of file ExecutionState.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ set_add_annotated_name_handler()

void smtrat::execution::ExecutionState::set_add_annotated_name_handler ( std::function< void(const FormulaT &, const std::string &)> f )

inline

Definition at line 59 of file ExecutionState.h.

Here is the caller graph for this function:

◆ set_add_assertion_handler()

void smtrat::execution::ExecutionState::set_add_assertion_handler ( std::function< void(const FormulaT &)> f )

inline

Definition at line 56 of file ExecutionState.h.

Here is the caller graph for this function:

◆ set_add_objective_handler()

void smtrat::execution::ExecutionState::set_add_objective_handler ( std::function< void(const Poly &, bool)> f )

inline

Definition at line 58 of file ExecutionState.h.

Here is the caller graph for this function:

◆ set_add_soft_assertion_handler()

void smtrat::execution::ExecutionState::set_add_soft_assertion_handler ( std::function< void(const FormulaT &, Rational, const std::string &)> f )

inline

Definition at line 57 of file ExecutionState.h.

Here is the caller graph for this function:

◆ set_logic()

void smtrat::execution::ExecutionState::set_logic ( carl::Logic logic )

inline

Definition at line 70 of file ExecutionState.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ set_mode()

void smtrat::execution::ExecutionState::set_mode ( Mode mode )

inlineprivate

Definition at line 49 of file ExecutionState.h.

Here is the caller graph for this function:

◆ set_remove_annotated_name_handler()

void smtrat::execution::ExecutionState::set_remove_annotated_name_handler ( std::function< void(const FormulaT &)> f )

inline

Definition at line 63 of file ExecutionState.h.

Here is the caller graph for this function:

◆ set_remove_assertion_handler()

void smtrat::execution::ExecutionState::set_remove_assertion_handler ( std::function< void(const FormulaT &)> f )

inline

Definition at line 60 of file ExecutionState.h.

Here is the caller graph for this function:

◆ set_remove_objective_handler()

void smtrat::execution::ExecutionState::set_remove_objective_handler ( std::function< void(const Poly &)> f )

inline

Definition at line 62 of file ExecutionState.h.

Here is the caller graph for this function:

◆ set_remove_soft_assertion_handler()

void smtrat::execution::ExecutionState::set_remove_soft_assertion_handler ( std::function< void(const FormulaT &)> f )

inline

Definition at line 61 of file ExecutionState.h.

Here is the caller graph for this function:

Field Documentation

◆ addAnnotatedNameHandler

std::function<void (const FormulaT&, const std::string&)> smtrat::execution::ExecutionState::addAnnotatedNameHandler

private

Definition at line 43 of file ExecutionState.h.

◆ addAssertionHandler

std::function<void (const FormulaT&)> smtrat::execution::ExecutionState::addAssertionHandler

private

Definition at line 40 of file ExecutionState.h.

◆ addObjectiveHandler

std::function<void (const Poly&, bool)> smtrat::execution::ExecutionState::addObjectiveHandler

private

Definition at line 42 of file ExecutionState.h.

◆ addSoftAssertionHandler

std::function<void (const FormulaT&, Rational, const std::string&)> smtrat::execution::ExecutionState::addSoftAssertionHandler

private

Definition at line 41 of file ExecutionState.h.

◆ mAnnotatedNames

std::vector<std::pair<FormulaT, std::string> > smtrat::execution::ExecutionState::mAnnotatedNames

private

Definition at line 33 of file ExecutionState.h.

◆ mAssertions

std::vector<Assertion> smtrat::execution::ExecutionState::mAssertions

private

Definition at line 30 of file ExecutionState.h.

◆ mBacktrackPoints

std::vector<std::tuple<size_t,size_t,size_t,size_t> > smtrat::execution::ExecutionState::mBacktrackPoints

private

Definition at line 34 of file ExecutionState.h.

◆ mLogic

carl::Logic smtrat::execution::ExecutionState::mLogic

private

Definition at line 28 of file ExecutionState.h.

◆ mMode

Mode smtrat::execution::ExecutionState::mMode

private

Definition at line 26 of file ExecutionState.h.

◆ mModel

smtrat::Model smtrat::execution::ExecutionState::mModel

private

Definition at line 36 of file ExecutionState.h.

◆ mObjectives

std::vector<Objective> smtrat::execution::ExecutionState::mObjectives

private

Definition at line 32 of file ExecutionState.h.

◆ mObjectiveValues

smtrat::ObjectiveValues smtrat::execution::ExecutionState::mObjectiveValues

private

Definition at line 37 of file ExecutionState.h.

◆ mSoftAssertions

std::vector<SoftAssertion> smtrat::execution::ExecutionState::mSoftAssertions

private

Definition at line 31 of file ExecutionState.h.

◆ removeAnnotatedNameHandler

std::function<void (const FormulaT&)> smtrat::execution::ExecutionState::removeAnnotatedNameHandler

private

Definition at line 47 of file ExecutionState.h.

◆ removeAssertionHandler

std::function<void (const FormulaT&)> smtrat::execution::ExecutionState::removeAssertionHandler

private

Definition at line 44 of file ExecutionState.h.

◆ removeObjectiveHandler

std::function<void (const Poly&)> smtrat::execution::ExecutionState::removeObjectiveHandler

private

Definition at line 46 of file ExecutionState.h.

◆ removeSoftAssertionHandler

std::function<void (const FormulaT&)> smtrat::execution::ExecutionState::removeSoftAssertionHandler

private

Definition at line 45 of file ExecutionState.h.

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

cli/tools/ExecutionState.h

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ ExecutionState()

Member Function Documentation

◆ add_assertion()

◆ add_objective()

◆ add_soft_assertion()

◆ annotate_name()

◆ assertions()

◆ enter_sat()

◆ enter_unsat()

◆ has_annotated_name()

◆ has_annotated_name_formula()

◆ has_assertion()

◆ has_objective()

◆ has_soft_assertion()

◆ is_mode()

◆ logic()

◆ model()

◆ objectiveValues()

◆ pop() [1/2]

◆ pop() [2/2]

◆ push() [1/2]

◆ push() [2/2]

◆ reset()

◆ reset_answer()

◆ reset_assertions()

◆ set_add_annotated_name_handler()

◆ set_add_assertion_handler()

◆ set_add_objective_handler()

◆ set_add_soft_assertion_handler()

◆ set_logic()

◆ set_mode()

◆ set_remove_annotated_name_handler()

◆ set_remove_assertion_handler()

◆ set_remove_objective_handler()

◆ set_remove_soft_assertion_handler()

Field Documentation

◆ addAnnotatedNameHandler

◆ addAssertionHandler

◆ addObjectiveHandler

◆ addSoftAssertionHandler

◆ mAnnotatedNames

◆ mAssertions

◆ mBacktrackPoints

◆ mLogic

◆ mMode

◆ mModel

◆ mObjectives

◆ mObjectiveValues

◆ mSoftAssertions

◆ removeAnnotatedNameHandler

◆ removeAssertionHandler

◆ removeObjectiveHandler

◆ removeSoftAssertionHandler