|
|
@ -39,7 +39,7 @@ namespace abstract { |
|
|
|
* @see AbstractFormula |
|
|
|
* @see AbstractFormula |
|
|
|
*/ |
|
|
|
template <class T> |
|
|
|
template <class T, class FormulaType> |
|
|
|
class BoundedNaryUntil : public AbstractFormula<T> { |
|
|
|
|
|
|
|
public: |
|
|
@ -48,7 +48,7 @@ public: |
|
|
|
*/ |
|
|
|
BoundedNaryUntil() { |
|
|
|
this->left = nullptr; |
|
|
|
this->right = new std::vector<std::tuple<AbstractFormula<T>*,T,T>>(); |
|
|
|
this->right = new std::vector<std::tuple<FormulaType*,T,T>>(); |
|
|
|
} |
|
|
|
|
|
|
|
/*! |
|
|
@ -57,7 +57,7 @@ public: |
|
|
|
* @param left The left formula subtree |
|
|
|
* @param right The left formula subtree |
|
|
|
*/ |
|
|
|
BoundedNaryUntil(AbstractFormula<T>* left, std::vector<std::tuple<AbstractFormula<T>*,T,T>>* right) { |
|
|
|
BoundedNaryUntil(FormulaType* left, std::vector<std::tuple<FormulaType*,T,T>>* right) { |
|
|
|
this->left = left; |
|
|
|
this->right = right; |
|
|
|
} |
|
|
@ -77,44 +77,16 @@ public: |
|
|
|
} |
|
|
|
} |
|
|
|
|
|
|
|
/*! |
|
|
|
* @returns a string representation of the formula |
|
|
|
*/ |
|
|
|
virtual std::string toString() const { |
|
|
|
std::stringstream result; |
|
|
|
result << "( " << left->toString(); |
|
|
|
for (auto it = this->right->begin(); it != this->right->end(); ++it) { |
|
|
|
result << " U[" << std::get<1>(*it) << "," << std::get<2>(*it) << "] " << std::get<0>(*it)->toString(); |
|
|
|
} |
|
|
|
result << ")"; |
|
|
|
return result.str(); |
|
|
|
} |
|
|
|
|
|
|
|
/*! |
|
|
|
* @brief Checks if all subtrees conform to some logic. |
|
|
|
* |
|
|
|
* @param checker Formula checker object. |
|
|
|
* @return true iff all subtrees conform to some logic. |
|
|
|
*/ |
|
|
|
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const { |
|
|
|
bool res = checker.conforms(this->left); |
|
|
|
for (auto it = this->right->begin(); it != this->right->end(); ++it) { |
|
|
|
res &= checker.conforms(std::get<0>(*it)); |
|
|
|
} |
|
|
|
return res; |
|
|
|
} |
|
|
|
|
|
|
|
protected: |
|
|
|
/*! |
|
|
|
* Sets the left child node. |
|
|
|
* |
|
|
|
* @param newLeft the new left child. |
|
|
|
*/ |
|
|
|
void setLeft(AbstractFormula<T>* newLeft) { |
|
|
|
void setLeft(FormulaType* newLeft) { |
|
|
|
left = newLeft; |
|
|
|
} |
|
|
|
|
|
|
|
void setRight(std::vector<std::tuple<AbstractFormula<T>*,T,T>>* newRight) { |
|
|
|
void setRight(std::vector<std::tuple<FormulaType*,T,T>>* newRight) { |
|
|
|
right = newRight; |
|
|
|
} |
|
|
|
|
|
|
@ -124,28 +96,55 @@ protected: |
|
|
|
* |
|
|
|
* @param newRight the new right child. |
|
|
|
*/ |
|
|
|
void addRight(AbstractFormula<T>* newRight, T upperBound, T lowerBound) { |
|
|
|
this->right->push_back(std::tuple<AbstractFormula<T>*,T,T>(newRight, upperBound, lowerBound)); |
|
|
|
void addRight(FormulaType* newRight, T upperBound, T lowerBound) { |
|
|
|
this->right->push_back(std::tuple<FormulaType*,T,T>(newRight, upperBound, lowerBound)); |
|
|
|
} |
|
|
|
|
|
|
|
/*! |
|
|
|
* @returns a pointer to the left child node |
|
|
|
*/ |
|
|
|
const AbstractFormula<T>& getLeft() const { |
|
|
|
const FormulaType& getLeft() const { |
|
|
|
return *left; |
|
|
|
} |
|
|
|
|
|
|
|
/*! |
|
|
|
* @returns a pointer to the right child nodes. |
|
|
|
*/ |
|
|
|
const std::vector<std::tuple<AbstractFormula<T>*,T,T>>& getRight() const { |
|
|
|
const std::vector<std::tuple<FormulaType*,T,T>>& getRight() const { |
|
|
|
return *right; |
|
|
|
} |
|
|
|
|
|
|
|
/*! |
|
|
|
* @returns a string representation of the formula |
|
|
|
*/ |
|
|
|
virtual std::string toString() const { |
|
|
|
std::stringstream result; |
|
|
|
result << "( " << left->toString(); |
|
|
|
for (auto it = this->right->begin(); it != this->right->end(); ++it) { |
|
|
|
result << " U[" << std::get<1>(*it) << "," << std::get<2>(*it) << "] " << std::get<0>(*it)->toString(); |
|
|
|
} |
|
|
|
result << ")"; |
|
|
|
return result.str(); |
|
|
|
} |
|
|
|
|
|
|
|
/*! |
|
|
|
* @brief Checks if all subtrees conform to some logic. |
|
|
|
* |
|
|
|
* @param checker Formula checker object. |
|
|
|
* @return true iff all subtrees conform to some logic. |
|
|
|
*/ |
|
|
|
virtual bool conforms(const AbstractFormulaChecker<T>& checker) const { |
|
|
|
bool res = checker.conforms(this->left); |
|
|
|
for (auto it = this->right->begin(); it != this->right->end(); ++it) { |
|
|
|
res &= checker.conforms(std::get<0>(*it)); |
|
|
|
} |
|
|
|
return res; |
|
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
private: |
|
|
|
AbstractFormula<T>* left; |
|
|
|
std::vector<std::tuple<AbstractFormula<T>*,T,T>>* right; |
|
|
|
FormulaType* left; |
|
|
|
std::vector<std::tuple<FormulaType*,T,T>>* right; |
|
|
|
}; |
|
|
|
|
|
|
|
} //namespace abstract |
|
|
|