Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::dft::modelchecker::SmtConstraint Class Referenceabstract

#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()

◆ toSmtlib2()


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