Inheritance diagram for storm::dft::modelchecker::Iff:

Collaboration diagram for storm::dft::modelchecker::Iff:

Public Member Functions
	Iff (std::shared_ptr< SmtConstraint > l, std::shared_ptr< SmtConstraint > r)

std::string	toSmtlib2 (std::vector< std::string > const &varNames) const override
	Generate a string describing the constraint in Smtlib2 format.

storm::expressions::Expression	toExpression (std::vector< std::string > const &varNames, std::shared_ptr< storm::expressions::ExpressionManager > manager) const override
	Generate an expression describing the constraint in Storm format.

Public Member Functions inherited from storm::dft::modelchecker::SmtConstraint
virtual	~SmtConstraint ()

virtual std::string	description () const

void	setDescription (std::string const &descr)

Detailed Description

Definition at line 214 of file SmtConstraint.cpp.

Constructor & Destructor Documentation

storm::dft::modelchecker::Iff::Iff	(	std::shared_ptr< SmtConstraint >	l,
		std::shared_ptr< SmtConstraint >	r
	)

inline

Definition at line 216 of file SmtConstraint.cpp.

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

inlineoverridevirtual

Generate an expression describing the constraint in Storm format.

Parameters

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

Definition at line 224 of file SmtConstraint.cpp.

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

inlineoverridevirtual

Generate a string describing the constraint in Smtlib2 format.

Parameters

varNames vector of variable names

Definition at line 218 of file SmtConstraint.cpp.

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