storm::dft::modelchecker::SmtConstraint Class Reference

#include <SmtConstraint.h>

Inheritance diagram for storm::dft::modelchecker::SmtConstraint:

Public Member Functions
virtual	~SmtConstraint ()
virtual std::string	toSmtlib2 (std::vector< std::string > const &varNames) const =0
	Generate a string describing the constraint in Smtlib2 format.
virtual storm::expressions::Expression	toExpression (std::vector< std::string > const &varNames, std::shared_ptr< storm::expressions::ExpressionManager > manager) const =0
	Generate an expression describing the constraint in Storm format.
virtual std::string	description () const
void	setDescription (std::string const &descr)

Detailed Description

Definition at line 9 of file SmtConstraint.h.

Constructor & Destructor Documentation

~SmtConstraint()

virtual storm::dft::modelchecker::SmtConstraint::~SmtConstraint ( )

inlinevirtual

Definition at line 11 of file SmtConstraint.h.

Member Function Documentation

description()

virtual std::string storm::dft::modelchecker::SmtConstraint::description ( ) const

inlinevirtual

Definition at line 29 of file SmtConstraint.h.

setDescription()

void storm::dft::modelchecker::SmtConstraint::setDescription ( std::string const &  descr )

inline

Definition at line 33 of file SmtConstraint.h.

toExpression()

virtual storm::expressions::Expression storm::dft::modelchecker::SmtConstraint::toExpression ( std::vector< std::string > const &  varNames, std::shared_ptr< storm::expressions::ExpressionManager >  manager  ) const

pure virtual

Generate an expression describing the constraint in Storm format.

Parameters

varNames	vector of variable names
manager	the expression manager used to handle the expressions

Returns

the expression

Implemented in storm::dft::modelchecker::IsMaximum, storm::dft::modelchecker::IsMinimum, storm::dft::modelchecker::BetweenValues, storm::dft::modelchecker::And, storm::dft::modelchecker::Or, storm::dft::modelchecker::Implies, storm::dft::modelchecker::Iff, storm::dft::modelchecker::IsTrue, storm::dft::modelchecker::IsBoolValue, storm::dft::modelchecker::IsConstantValue, storm::dft::modelchecker::IsNotConstantValue, storm::dft::modelchecker::IsLessConstant, storm::dft::modelchecker::IsGreaterConstant, storm::dft::modelchecker::IsLessEqualConstant, storm::dft::modelchecker::IsGreaterEqualConstant, storm::dft::modelchecker::IsEqual, storm::dft::modelchecker::IsUnequal, storm::dft::modelchecker::IsLess, storm::dft::modelchecker::IsLessEqual, storm::dft::modelchecker::IsGreaterEqual, storm::dft::modelchecker::PairwiseDifferent, storm::dft::modelchecker::Sorted, storm::dft::modelchecker::IfThenElse, storm::dft::modelchecker::TrueCountIsLessConstant, storm::dft::modelchecker::FalseCountIsEqualConstant, and storm::dft::modelchecker::TrueCountIsConstantValue.

toSmtlib2()

virtual std::string storm::dft::modelchecker::SmtConstraint::toSmtlib2 ( std::vector< std::string > const &  varNames ) const

pure virtual

Generate a string describing the constraint in Smtlib2 format.

Parameters

varNames

vector of variable names

Returns

Smtlib2 format string

Implemented in storm::dft::modelchecker::IsMaximum, storm::dft::modelchecker::IsMinimum, storm::dft::modelchecker::BetweenValues, storm::dft::modelchecker::And, storm::dft::modelchecker::Or, storm::dft::modelchecker::Implies, storm::dft::modelchecker::Iff, storm::dft::modelchecker::IsTrue, storm::dft::modelchecker::IsBoolValue, storm::dft::modelchecker::IsConstantValue, storm::dft::modelchecker::IsNotConstantValue, storm::dft::modelchecker::IsLessConstant, storm::dft::modelchecker::IsGreaterConstant, storm::dft::modelchecker::IsLessEqualConstant, storm::dft::modelchecker::IsGreaterEqualConstant, storm::dft::modelchecker::IsEqual, storm::dft::modelchecker::IsUnequal, storm::dft::modelchecker::IsLess, storm::dft::modelchecker::IsLessEqual, storm::dft::modelchecker::IsGreaterEqual, storm::dft::modelchecker::PairwiseDifferent, storm::dft::modelchecker::Sorted, storm::dft::modelchecker::IfThenElse, storm::dft::modelchecker::TrueCountIsLessConstant, storm::dft::modelchecker::FalseCountIsEqualConstant, and storm::dft::modelchecker::TrueCountIsConstantValue.

---

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

• src/storm-dft/modelchecker/SmtConstraint.h