Valuation.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <memory>
#include <vector>
 
namespace storm {
namespace expressions {
class ExpressionManager;
class Variable;

class Valuation {
   public:
    Valuation(std::shared_ptr<ExpressionManager const> const& manager);

    virtual ~Valuation();

    virtual bool getBooleanValue(Variable const& booleanVariable) const = 0;

    virtual void setBooleanValue(Variable const& booleanVariable, bool value) = 0;

    virtual int_fast64_t getIntegerValue(Variable const& integerVariable) const = 0;

    virtual int_fast64_t getBitVectorValue(Variable const& bitVectorVariable) const = 0;

    virtual void setIntegerValue(Variable const& integerVariable, int_fast64_t value) = 0;

    virtual void setBitVectorValue(Variable const& bitVectorVariable, int_fast64_t value) = 0;

    virtual double getRationalValue(Variable const& rationalVariable) const = 0;

    virtual void setRationalValue(Variable const& rationalVariable, double value) = 0;

    ExpressionManager const& getManager() const;
 
   protected:
    std::shared_ptr<ExpressionManager const> const& getManagerAsSharedPtr() const;

    void setManager(std::shared_ptr<ExpressionManager const> const& manager);
 
   private:
    // The manager responsible for the variables of this valuation.
    std::shared_ptr<ExpressionManager const> manager;
};
}  // namespace expressions
}  // namespace storm