Storm
A Modern Probabilistic Model Checker
|
#include <SmtConstraint.h>
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) |
Definition at line 9 of file SmtConstraint.h.
|
inlinevirtual |
Definition at line 11 of file SmtConstraint.h.
|
inlinevirtual |
Definition at line 29 of file SmtConstraint.h.
|
inline |
Definition at line 33 of file SmtConstraint.h.
|
pure virtual |
Generate an expression describing the constraint in Storm format.
varNames | vector of variable names |
manager | the expression manager used to handle the expressions |
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.
|
pure virtual |
Generate a string describing the constraint in Smtlib2 format.
varNames | vector of variable names |
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.