PolytopeTree.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
#include <vector>
#include "storm/storage/geometry/Polytope.h"
 
namespace storm {
namespace storage {
namespace geometry {
 
template<typename ValueType>
class PolytopeTree {
   public:
    PolytopeTree(std::shared_ptr<Polytope<ValueType>> const& polytope = nullptr) : polytope(polytope) {
        // Intentionally left empty
    }
 
    void setMinus(std::shared_ptr<Polytope<ValueType>> const& rhs) {
        // This operation only has an effect if the intersection of this and rhs is non-empty.
        if (!isEmpty() && !polytope->intersection(rhs)->isEmpty()) {
            if (children.empty()) {
                // This is a leaf node.
                // Apply splitting.
                auto newChildren = polytope->setMinus(rhs);
                if (newChildren.empty()) {
                    // Delete this node.
                    polytope = nullptr;
                } else if (newChildren.size() == 1) {
                    // Replace this node with its only child
                    polytope = newChildren.front()->clean();
                } else {
                    // Add the new children to this node. There is no need to traverse them.
                    for (auto& c : newChildren) {
                        children.push_back(c->clean());
                    }
                }
            } else {
                // This is an inner node. Traverse the children and set this to the convex union of its children.
                std::vector<PolytopeTree<ValueType>> newChildren;
                std::vector<std::vector<ValueType>> newPolytopeVertices;
                for (auto& c : children) {
                    c.setMinus(rhs);
                    if (c.polytope != nullptr) {
                        newChildren.push_back(c);
                        auto cVertices = c.polytope->getVertices();
                        newPolytopeVertices.insert(newPolytopeVertices.end(), cVertices.begin(), cVertices.end());
                    }
                }
                if (newPolytopeVertices.empty()) {
                    polytope = nullptr;
                } else {
                    polytope = storm::storage::geometry::Polytope<ValueType>::create(newPolytopeVertices);
                }
                children = std::move(newChildren);
            }
        }
    }
 
    void substractDownwardClosure(std::vector<ValueType> const& point) {
        setMinus(Polytope<ValueType>::createDownwardClosure({point}));
    }
 
    void substractDownwardClosure(std::vector<ValueType> const& point, std::vector<ValueType> const& offset) {
        assert(point.size() == offset.size());
        std::vector<ValueType> pointPrime(point.size());
        storm::utility::vector::addVectors(point, offset, pointPrime);
        setMinus(Polytope<ValueType>::createDownwardClosure({pointPrime}));
    }
 
    bool isEmpty() const {
        return polytope == nullptr;
    }
 
    void clear() {
        children.clear();
        polytope = nullptr;
    }
 
    std::shared_ptr<Polytope<ValueType>>& getPolytope() {
        return polytope;
    }
 
    std::vector<PolytopeTree>& getChildren() {
        return children;
    }
 
    std::string toId() {
        if (isEmpty()) {
            return "empty";
        }
        std::stringstream s;
        s << "p";
        auto vertices = getPolytope()->getVertices();
        for (auto const& v : vertices) {
            s << "_";
            for (auto const& vi : v) {
                s << storm::utility::convertNumber<double>(vi) << "-";
            }
        }
        s << "_id" << children.data();
        return s.str();
    }
 
    std::string toString() {
        if (isEmpty()) {
            return "Empty PolytopeTree";
        }
        std::stringstream s;
        s << "PolytopeTree node with " << getChildren().size() << " children: " << getPolytope()->toString(true) << "\nVertices: ";
        auto vertices = getPolytope()->getVertices();
        for (auto const& v : vertices) {
            s << "[";
            for (auto const& vi : v) {
                s << storm::utility::convertNumber<double>(vi) << ",";
            }
            s << "]\t";
        }
        s << '\n';
        return s.str();
    }
 
   private:
    std::shared_ptr<Polytope<ValueType>> polytope;
    std::vector<PolytopeTree<ValueType>> children;
};
}  // namespace geometry
}  // namespace storage
}  // namespace storm