storm::adapters::Smt2ExpressionAdapter Class Reference

#include <Smt2ExpressionAdapter.h>

Public Member Functions
	Smt2ExpressionAdapter (storm::expressions::ExpressionManager &, bool useReadableVarNames)
	Creates an expression adapter that can translate expressions to the format of Smt2.
std::string	translateExpression (storm::expressions::Expression const &)
	Translates the given expression to an equivalent expression for Smt2.
std::string	translateExpression (storm::RationalFunction const &leftHandSide, storm::CompareRelation const &relation, storm::RationalFunction const &rightHandSide)
	Translates the given constraint "leftHandSide relation rightHandSide" to an equivalent expression for Smt2.
std::string	translateExpression (storm::RationalFunction const &leftHandSide, storm::CompareRelation const &relation)
	Translates the given constraint "leftHandSide relation 0" to an equivalent expression for Smt2.
std::string	translateExpression (storm::expressions::Variable const &)
	Translates the given variable to an equivalent expression for Smt2.
storm::expressions::Variable const &	getVariable (std::string const &)
	Finds the counterpart to the given smt2 variable declaration.
void	increaseScope (uint_fast64_t n=1)
void	decreaseScope (uint_fast64_t n=1)
std::vector< std::string > const	checkForUndeclaredVariables (std::set< storm::RationalFunctionVariable > const &variables)
	Checks whether the variables in the given set are already declared and creates them if necessary.

Detailed Description

Definition at line 19 of file Smt2ExpressionAdapter.h.

Constructor & Destructor Documentation

Smt2ExpressionAdapter()

storm::adapters::Smt2ExpressionAdapter::Smt2ExpressionAdapter ( storm::expressions::ExpressionManager &  , bool  useReadableVarNames  )

inline

Creates an expression adapter that can translate expressions to the format of Smt2.

Parameters

manager	The manager that can be used to build expressions.
useReadableVarNames	sets whether the expressions should use human readable names for the variables or the internal representation

Definition at line 27 of file Smt2ExpressionAdapter.h.

Member Function Documentation

checkForUndeclaredVariables()

std::vector< std::string > const storm::adapters::Smt2ExpressionAdapter::checkForUndeclaredVariables ( std::set< storm::RationalFunctionVariable > const &  variables )

inline

Checks whether the variables in the given set are already declared and creates them if necessary.

Parameters

variables

the set of variables to check

Definition at line 104 of file Smt2ExpressionAdapter.h.

decreaseScope()

void storm::adapters::Smt2ExpressionAdapter::decreaseScope ( uint_fast64_t  n = 1 )

inline

Definition at line 94 of file Smt2ExpressionAdapter.h.

getVariable()

storm::expressions::Variable const & storm::adapters::Smt2ExpressionAdapter::getVariable ( std::string const &  )

inline

Finds the counterpart to the given smt2 variable declaration.

Parameters

smt2Declaration

The declaration for which to find the equivalent.

Returns

The equivalent counterpart.

Definition at line 84 of file Smt2ExpressionAdapter.h.

increaseScope()

void storm::adapters::Smt2ExpressionAdapter::increaseScope ( uint_fast64_t  n = 1 )

inline

Definition at line 88 of file Smt2ExpressionAdapter.h.

translateExpression() [1/4]

std::string storm::adapters::Smt2ExpressionAdapter::translateExpression ( storm::expressions::Expression const &  )

inline

Translates the given expression to an equivalent expression for Smt2.

Parameters

expression

The expression to translate.

Returns

An equivalent expression for Smt2.

Definition at line 37 of file Smt2ExpressionAdapter.h.

translateExpression() [2/4]

std::string storm::adapters::Smt2ExpressionAdapter::translateExpression ( storm::expressions::Variable const &  )

inline

Translates the given variable to an equivalent expression for Smt2.

Parameters

variable

The variable to translate.

Returns

An equivalent expression for smt2.

Definition at line 74 of file Smt2ExpressionAdapter.h.

translateExpression() [3/4]

std::string storm::adapters::Smt2ExpressionAdapter::translateExpression ( storm::RationalFunction const &  leftHandSide, storm::CompareRelation const &  relation  )

inline

Translates the given constraint "leftHandSide relation 0" to an equivalent expression for Smt2.

Parameters

constraint

Returns

An equivalent expression for Smt2.

Definition at line 62 of file Smt2ExpressionAdapter.h.

translateExpression() [4/4]

std::string storm::adapters::Smt2ExpressionAdapter::translateExpression ( storm::RationalFunction const &  leftHandSide, storm::CompareRelation const &  relation, storm::RationalFunction const &  rightHandSide  )

inline

Translates the given constraint "leftHandSide relation rightHandSide" to an equivalent expression for Smt2.

Parameters

leftHandSide
relation
RightHandSide

Returns

An equivalent expression for Smt2.

Definition at line 49 of file Smt2ExpressionAdapter.h.

---

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

• src/storm/adapters/Smt2ExpressionAdapter.h