Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
JaniSyntacticalEqualityCheckVisitor.cpp
Go to the documentation of this file.
2
4
5namespace storm {
6
7namespace expressions {
8
12
13boost::any JaniSyntacticalEqualityCheckVisitor::visit(ValueArrayExpression const& expression, boost::any const& data) {
14 BaseExpression const& otherBaseExpression = boost::any_cast<std::reference_wrapper<BaseExpression const>>(data).get();
15 auto const rhs = std::dynamic_pointer_cast<storm::expressions::ValueArrayExpression const>(otherBaseExpression.getSharedPointer());
16 if (rhs) {
17 STORM_LOG_ASSERT(!expression.size()->containsVariables(), "non-const size of value array expr");
18 STORM_LOG_ASSERT(!rhs->size()->containsVariables(), "non-const size of value array expr");
19 auto lhsSize = expression.size()->evaluateAsInt();
20 auto rhsSize = rhs->size()->evaluateAsInt();
21 if (lhsSize != rhsSize) {
22 return false;
23 }
24 for (int64_t i = 0; i < lhsSize; ++i) {
25 if (!boost::any_cast<bool>(expression.at(i)->accept(*this, std::ref(*rhs->at(i))))) {
26 return false;
27 }
28 }
29 return true;
30 } else {
31 return false;
32 }
33}
34
35boost::any JaniSyntacticalEqualityCheckVisitor::visit(ConstructorArrayExpression const& expression, boost::any const& data) {
36 BaseExpression const& otherBaseExpression = boost::any_cast<std::reference_wrapper<BaseExpression const>>(data).get();
37 auto const rhs = std::dynamic_pointer_cast<storm::expressions::ConstructorArrayExpression const>(otherBaseExpression.getSharedPointer());
38 if (rhs) {
39 return boost::any_cast<bool>(expression.size()->accept(*this, std::ref(*rhs->size()))) &&
40 boost::any_cast<bool>(expression.getElementExpression()->accept(*this, std::ref(*rhs->getElementExpression()))) &&
41 (expression.getIndexVar() == rhs->getIndexVar());
42 } else {
43 return false;
44 }
45}
46
47boost::any JaniSyntacticalEqualityCheckVisitor::visit(ArrayAccessExpression const& expression, boost::any const& data) {
48 BaseExpression const& otherBaseExpression = boost::any_cast<std::reference_wrapper<BaseExpression const>>(data).get();
49 auto const rhs = std::dynamic_pointer_cast<storm::expressions::ArrayAccessExpression const>(otherBaseExpression.getSharedPointer());
50 if (rhs) {
51 return boost::any_cast<bool>(expression.getFirstOperand()->accept(*this, std::ref(*rhs->getFirstOperand()))) &&
52 boost::any_cast<bool>(expression.getSecondOperand()->accept(*this, std::ref(*rhs->getSecondOperand())));
53 } else {
54 return false;
55 }
56}
57
58boost::any JaniSyntacticalEqualityCheckVisitor::visit(FunctionCallExpression const& expression, boost::any const& data) {
59 BaseExpression const& otherBaseExpression = boost::any_cast<std::reference_wrapper<BaseExpression const>>(data).get();
60 auto const rhs = std::dynamic_pointer_cast<storm::expressions::FunctionCallExpression const>(otherBaseExpression.getSharedPointer());
61 if (rhs) {
62 if (expression.getFunctionIdentifier() != rhs->getFunctionIdentifier() || expression.getNumberOfArguments() != rhs->getNumberOfArguments()) {
63 return false;
64 }
65 for (uint64_t i = 0; i < expression.getNumberOfArguments(); ++i) {
66 if (!boost::any_cast<bool>(expression.getArgument(i)->accept(*this, std::ref(*rhs->getArgument(i))))) {
67 return false;
68 }
69 }
70 return true;
71 } else {
72 return false;
73 }
74}
75
76boost::any JaniSyntacticalEqualityCheckVisitor::visit(TranscendentalNumberLiteralExpression const& expression, boost::any const& data) {
77 BaseExpression const& otherBaseExpression = boost::any_cast<std::reference_wrapper<BaseExpression const>>(data).get();
78 auto const rhs = std::dynamic_pointer_cast<storm::expressions::TranscendentalNumberLiteralExpression const>(otherBaseExpression.getSharedPointer());
79 if (rhs) {
80 return expression.getTranscendentalNumber() == rhs->getTranscendentalNumber();
81 } else {
82 return false;
83 }
84}
85
86} // namespace expressions
87} // namespace storm
The base class of all expression classes.
std::shared_ptr< BaseExpression const > getSharedPointer() const
Retrieves a shared pointer to this expression.
std::shared_ptr< BaseExpression const > const & getSecondOperand() const
Retrieves the second operand of the expression.
std::shared_ptr< BaseExpression const > const & getFirstOperand() const
Retrieves the first operand of the expression.
Represents an array of the given size, where the i'th entry is determined by the elementExpression,...
virtual std::shared_ptr< BaseExpression const > size() const override
std::shared_ptr< BaseExpression const > const & getElementExpression() const
storm::expressions::Variable const & getIndexVar() const
Represents an array with a given list of elements.
std::shared_ptr< BaseExpression const > getArgument(uint64_t i) const
virtual boost::any visit(ValueArrayExpression const &expression, boost::any const &data) override
JaniSyntacticalEqualityCheckVisitor()
Creates a visitor that checks if the given expressions are syntactically equal.
TranscendentalNumber const & getTranscendentalNumber() const
Getter for the constant value stored by the object.
Represents an array with a given list of elements.
virtual std::shared_ptr< BaseExpression const > size() const override
virtual std::shared_ptr< BaseExpression const > at(uint64_t i) const override
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
LabParser.cpp.
Definition cli.cpp:18