ValuationDescriptionBuilder.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
#include "storm/storage/valuations/ValuationDescription.h"
#include "storm/utility/NumberTraits.h"
 
namespace storm {
namespace expressions {
class Variable;
class ExpressionManager;
}  // namespace expressions
 
namespace storage::sparse {
class ValuationDescriptionBuilder {
   public:
    using Integer = storm::NumberTraits<storm::RationalNumber>::IntegerType;
 
    ValuationDescriptionBuilder(std::shared_ptr<storm::expressions::ExpressionManager const> const& expressionManager);
 
    storm::expressions::ExpressionManager const& getManager() const;

    void addBooleanVariable(storm::expressions::Variable const& variable, bool optional = false);

    void addIntegerVariable(storm::expressions::Variable const& variable, int64_t const lowerBound, int64_t const upperBound, bool optional = false);

    void addIntegerVariable(storm::expressions::Variable const& variable, Integer const lowerBound, Integer const upperBound, bool optional = false);

    void addDoubleVariable(storm::expressions::Variable const& variable, bool optional = false);

    void addRationalVariable(storm::expressions::Variable const& variable, uint64_t bitSize, bool optional = false);

    void addStringVariable(storm::expressions::Variable const& variable, bool optional = false);

    void addVariable(ValuationClassDescription::Variable const& variable);

    void addVariables(ValuationClassDescription const& description, bool addPadding = false);

    ValuationClassDescription buildClassDescription();
 
   private:
    void assertAndCollectVariable(storm::expressions::Variable const& variable);
 
    void finalize();
    std::shared_ptr<storm::expressions::ExpressionManager const> const manager;
    ValuationClassDescription descr;
    std::set<storm::expressions::Variable> addedVariables;
};
 
}  // namespace storage::sparse
}  // namespace storm