storm::dft::modelchecker::IsUnequal Class Reference

#include <SmtConstraint.h>

Inheritance diagram for storm::dft::modelchecker::IsUnequal:

Collaboration diagram for storm::dft::modelchecker::IsUnequal:

Public Member Functions
	IsUnequal (uint64_t varIndex1, uint64_t varIndex2)
virtual	~IsUnequal ()
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 266 of file SmtConstraint.h.

Constructor & Destructor Documentation

IsUnequal()

storm::dft::modelchecker::IsUnequal::IsUnequal ( uint64_t varIndex1, uint64_t varIndex2 )

inline

Definition at line 268 of file SmtConstraint.h.

~IsUnequal()

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

inlinevirtual

Definition at line 270 of file SmtConstraint.h.

Member Function Documentation

toExpression()

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

overridevirtual

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

Implements storm::dft::modelchecker::SmtConstraint.

Definition at line 248 of file SmtConstraint.cpp.

toSmtlib2()

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

overridevirtual

Generate a string describing the constraint in Smtlib2 format.

Parameters

varNames

vector of variable names

Returns

Smtlib2 format string

Implements storm::dft::modelchecker::SmtConstraint.

Definition at line 244 of file SmtConstraint.cpp.

---

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

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