SmtConstraint.h

Go to the documentation of this file.

#pragma once
 
#include <storm/storage/expressions/Expression.h>
#include <string>
 
namespace storm::dft {
namespace modelchecker {
 
class SmtConstraint {
   public:
    virtual ~SmtConstraint() {}
 
    virtual std::string toSmtlib2(std::vector<std::string> const &varNames) const = 0;
 
    virtual storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const = 0;
 
    virtual std::string description() const {
        return descript;
    }
 
    void setDescription(std::string const &descr) {
        descript = descr;
    }
 
   private:
    std::string descript;
};
 
}  // namespace modelchecker
}  // namespace storm::dft