Skip to content

Commit

Permalink
Build graph from predicates
Browse files Browse the repository at this point in the history
  • Loading branch information
Adda0 committed Nov 28, 2022
1 parent 20444a3 commit 8b253f3
Show file tree
Hide file tree
Showing 35 changed files with 6,478 additions and 1 deletion.
28 changes: 28 additions & 0 deletions src/smt/theory_str_noodler/3rdparty/include/CXXGraph/CXXGraph.hpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
#ifndef __CXXGRAPH_H__
#define __CXXGRAPH_H__

#include "CXXGraphConfig.h"
#include "Edge/Edge.hpp"
#include "Edge/DirectedEdge.hpp"
#include "Edge/DirectedWeightedEdge.hpp"
#include "Edge/UndirectedEdge.hpp"
#include "Edge/UndirectedWeightedEdge.hpp"
#include "Edge/Weighted.hpp"
#include "Graph/Graph.hpp"
#include "Node/Node.hpp"
#include "Partitioning/Partition.hpp"
#include "Partitioning/CoordinatedPartitionState.hpp"
#include "Partitioning/CoordinatedRecord.hpp"
#include "Partitioning/HDRF.hpp"
#include "Partitioning/EBV.hpp"
#include "Partitioning/EdgeBalancedVertexCut.hpp"
#include "Partitioning/GreedyVertexCut.hpp"
#include "Partitioning/PartitionAlgorithm.hpp"
#include "Partitioning/Partitioner.hpp"
#include "Partitioning/PartitionerThread.hpp"
#include "Partitioning/PartitioningStats.hpp"
#include "Partitioning/PartitionState.hpp"
#include "Partitioning/PartitionStrategy.hpp"
#include "Partitioning/Record.hpp"

#endif // __CXXGRAPH_H__
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
// the configured options and settings for CXXGraph
#define CXXGraph_VERSION_MAJOR 0
#define CXXGraph_VERSION_MINOR 4
#define CXXGraph_VERSION_PATCH 0
Original file line number Diff line number Diff line change
@@ -0,0 +1,104 @@
/***********************************************************/
/*** ______ ____ ______ _ ***/
/*** / ___\ \/ /\ \/ / ___|_ __ __ _ _ __ | |__ ***/
/*** | | \ / \ / | _| '__/ _` | '_ \| '_ \ ***/
/*** | |___ / \ / \ |_| | | | (_| | |_) | | | | ***/
/*** \____/_/\_\/_/\_\____|_| \__,_| .__/|_| |_| ***/
/*** |_| ***/
/***********************************************************/
/*** Header-Only C++ Library for Graph ***/
/*** Representation and Algorithms ***/
/***********************************************************/
/*** Author: ZigRazor ***/
/*** E-Mail: zigrazor@gmail.com ***/
/***********************************************************/
/*** Collaboration: ----------- ***/
/***********************************************************/
/*** License: AGPL v3.0 ***/
/***********************************************************/

#ifndef __CXXGRAPH_DIRECTEDEDGE_H__
#define __CXXGRAPH_DIRECTEDEDGE_H__

#pragma once

#include "Edge.hpp"

namespace CXXGRAPH
{
template <typename T>
class UndirectedEdge;

template <typename T>
class DirectedEdge;
// ostream operator
template <typename T>
std::ostream &operator<<(std::ostream &o, const DirectedEdge<T> &edge);
template <typename T>
class DirectedEdge : public Edge<T>
{
public:
DirectedEdge(const unsigned long id, const Node<T> &node1, const Node<T> &node2);
DirectedEdge(const unsigned long id, const std::pair<const Node<T> *, const Node<T> *> &nodepair);
DirectedEdge(const Edge<T> &edge);
virtual ~DirectedEdge() = default;
const Node<T> &getFrom() const;
const Node<T> &getTo() const;
const std::optional<bool> isDirected() const override;
const std::optional<bool> isWeighted() const override;
//operator
explicit operator UndirectedEdge<T>() const { return UndirectedEdge<T>(Edge<T>::getId(), Edge<T>::getNodePair()); }

friend std::ostream &operator<<<>(std::ostream &os, const DirectedEdge<T> &edge);
};

template <typename T>
DirectedEdge<T>::DirectedEdge(const unsigned long id, const Node<T> &node1, const Node<T> &node2) : Edge<T>(id, node1, node2)
{
}

template <typename T>
DirectedEdge<T>::DirectedEdge(const unsigned long id, const std::pair<const Node<T> *, const Node<T> *> &nodepair) : Edge<T>(id, nodepair)
{
}

template <typename T>
DirectedEdge<T>::DirectedEdge(const Edge<T> &edge) : DirectedEdge(edge.getId(), *(edge.getNodePair().first), *(edge.getNodePair().second))
{
}

template <typename T>
const Node<T> &DirectedEdge<T>::getFrom() const
{
return *(Edge<T>::getNodePair().first);
}

template <typename T>
const Node<T> &DirectedEdge<T>::getTo() const
{
return *(Edge<T>::getNodePair().second);
}

template <typename T>
const std::optional<bool> DirectedEdge<T>::isDirected() const
{
return true;
}

template <typename T>
const std::optional<bool> DirectedEdge<T>::isWeighted() const
{
return false;
}



template <typename T>
std::ostream &operator<<(std::ostream &os, const DirectedEdge<T> &edge)
{
os << "((Node: " << edge.getFrom().getId() << ")) +----- |Edge: #" << edge.getId() << "|-----> ((Node: " << edge.getTo().getId() << "))";
return os;
}
}

#endif // __CXXGRAPH_DIRECTEDEDGE_H__
Original file line number Diff line number Diff line change
@@ -0,0 +1,109 @@
/***********************************************************/
/*** ______ ____ ______ _ ***/
/*** / ___\ \/ /\ \/ / ___|_ __ __ _ _ __ | |__ ***/
/*** | | \ / \ / | _| '__/ _` | '_ \| '_ \ ***/
/*** | |___ / \ / \ |_| | | | (_| | |_) | | | | ***/
/*** \____/_/\_\/_/\_\____|_| \__,_| .__/|_| |_| ***/
/*** |_| ***/
/***********************************************************/
/*** Header-Only C++ Library for Graph ***/
/*** Representation and Algorithms ***/
/***********************************************************/
/*** Author: ZigRazor ***/
/*** E-Mail: zigrazor@gmail.com ***/
/***********************************************************/
/*** Collaboration: ----------- ***/
/***********************************************************/
/*** License: AGPL v3.0 ***/
/***********************************************************/
#ifndef __CXXGRAPH_DIRECTEDWEIGHTEDEDGE_H__
#define __CXXGRAPH_DIRECTEDWEIGHTEDEDGE_H__

#pragma once

#include "DirectedEdge.hpp"
#include "Weighted.hpp"

namespace CXXGRAPH
{
//Foward Declaration
template <typename T>
class UndirectedWeightedEdge;

template <typename T>
class DirectedWeightedEdge;

//ostream operator
template <typename T>
std::ostream &operator<<(std::ostream &o, const DirectedWeightedEdge<T> &edge);

template <typename T>
class DirectedWeightedEdge : public DirectedEdge<T>, public Weighted
{
public:
DirectedWeightedEdge(const unsigned long id, const Node<T> &node1, const Node<T> &node2, const double weight);
DirectedWeightedEdge(const unsigned long id, const std::pair<const Node<T> *, const Node<T> *> &nodepair, const double weight);
DirectedWeightedEdge(const DirectedEdge<T> &edge, const double weight);
DirectedWeightedEdge(const Edge<T> &edge, const double weight);
DirectedWeightedEdge(const DirectedEdge<T> &edge);
DirectedWeightedEdge(const Edge<T> &edge);
DirectedWeightedEdge(const UndirectedWeightedEdge<T> &edge);
virtual ~DirectedWeightedEdge() = default;
const std::optional<bool> isWeighted() const override;
//operator
explicit operator UndirectedWeightedEdge<T>() const { return UndirectedWeightedEdge<T>(Edge<T>::getId(), Edge<T>::getNodePair(), Weighted::getWeight()); }

friend std::ostream &operator<<<>(std::ostream &os, const DirectedWeightedEdge<T> &edge);
};

template <typename T>
DirectedWeightedEdge<T>::DirectedWeightedEdge(const unsigned long id, const Node<T> &node1, const Node<T> &node2, const double weight) : DirectedEdge<T>(id, node1, node2), Weighted(weight)
{
}

template <typename T>
DirectedWeightedEdge<T>::DirectedWeightedEdge(const unsigned long id, const std::pair<const Node<T> *, const Node<T> *> &nodepair, const double weight) : DirectedEdge<T>(id, nodepair), Weighted(weight)
{
}

template <typename T>
DirectedWeightedEdge<T>::DirectedWeightedEdge(const DirectedEdge<T> &edge, const double weight) : DirectedEdge<T>(edge), Weighted(weight)
{
}

template <typename T>
DirectedWeightedEdge<T>::DirectedWeightedEdge(const Edge<T> &edge, const double weight) : DirectedEdge<T>(edge), Weighted(weight)
{
}

template <typename T>
DirectedWeightedEdge<T>::DirectedWeightedEdge(const DirectedEdge<T> &edge) : DirectedEdge<T>(edge), Weighted()
{
}

template <typename T>
DirectedWeightedEdge<T>::DirectedWeightedEdge(const Edge<T> &edge) : DirectedEdge<T>(edge), Weighted()
{
}

template <typename T>
DirectedWeightedEdge<T>::DirectedWeightedEdge(const UndirectedWeightedEdge<T> &edge) : DirectedEdge<T>(edge), Weighted(edge.getWeight())
{
}

template <typename T>
const std::optional<bool> DirectedWeightedEdge<T>::isWeighted() const
{
return true;
}

template <typename T>
std::ostream &operator<<(std::ostream &os, const DirectedWeightedEdge<T> &edge)
{
os << "((Node: " << edge.getFrom().getId() << ")) +----- |Edge: #" << edge.getId() << " W:" << edge.getWeight() << "|-----> ((Node: " << edge.getTo().getId() << "))";
return os;
}

}

#endif // __CXXGRAPH_DIRECTEDWEIGHTEDEDGE_H__
117 changes: 117 additions & 0 deletions src/smt/theory_str_noodler/3rdparty/include/CXXGraph/Edge/Edge.hpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,117 @@
/***********************************************************/
/*** ______ ____ ______ _ ***/
/*** / ___\ \/ /\ \/ / ___|_ __ __ _ _ __ | |__ ***/
/*** | | \ / \ / | _| '__/ _` | '_ \| '_ \ ***/
/*** | |___ / \ / \ |_| | | | (_| | |_) | | | | ***/
/*** \____/_/\_\/_/\_\____|_| \__,_| .__/|_| |_| ***/
/*** |_| ***/
/***********************************************************/
/*** Header-Only C++ Library for Graph ***/
/*** Representation and Algorithms ***/
/***********************************************************/
/*** Author: ZigRazor ***/
/*** E-Mail: zigrazor@gmail.com ***/
/***********************************************************/
/*** Collaboration: ----------- ***/
/***********************************************************/
/*** License: AGPL v3.0 ***/
/***********************************************************/

#ifndef __CXXGRAPH_EDGE_H__
#define __CXXGRAPH_EDGE_H__

#pragma once

#include <utility>
#include <optional>

#include "CXXGraph/Node/Node.hpp"

namespace CXXGRAPH
{
template <typename T>
class Edge;
// ostream operator
template <typename T>
std::ostream &operator<<(std::ostream &o, const Edge<T> &edge);
template <typename T>
class Edge
{
private:
unsigned long long id = 0;
std::pair<const Node<T> *, const Node<T> *> nodePair;

public:
Edge(const unsigned long long id, const Node<T> &node1, const Node<T> &node2);
Edge(const unsigned long long id, const std::pair<const Node<T> *, const Node<T> *> &nodepair);
virtual ~Edge() = default;
const unsigned long long &getId() const;
const std::pair<const Node<T> *, const Node<T> *> &getNodePair() const;
virtual const std::optional<bool> isDirected() const;
virtual const std::optional<bool> isWeighted() const;
//operator
virtual bool operator==(const Edge<T> &b) const;
bool operator<(const Edge<T> &b) const;
//operator DirectedEdge<T>() const { return DirectedEdge<T>(id, nodePair); }
//operator UndirectedEdge<T>() const { return UndirectedEdge<T>(id, nodePair); }

friend std::ostream &operator<<<>(std::ostream &os, const Edge<T> &edge);
};

template <typename T>
Edge<T>::Edge(const unsigned long long id, const Node<T> &node1, const Node<T> &node2) : nodePair(&node1, &node2)
{
this->id = id;
}

template <typename T>
Edge<T>::Edge(const unsigned long long id, const std::pair<const Node<T> *, const Node<T> *> &nodepair) : nodePair(nodepair)
{
this->id = id;
}

template <typename T>
const unsigned long long &Edge<T>::getId() const
{
return id;
}

template <typename T>
const std::pair<const Node<T> *, const Node<T> *> &Edge<T>::getNodePair() const
{
return nodePair;
}

template <typename T>
const std::optional<bool> Edge<T>::isDirected() const
{
return std::nullopt;
}

template <typename T>
const std::optional<bool> Edge<T>::isWeighted() const
{
return std::nullopt;
}

template <typename T>
bool Edge<T>::operator==(const Edge<T> &b) const
{
return (this->id == b.id && this->nodePair == b.nodePair);
}

template <typename T>
bool Edge<T>::operator<(const Edge<T> &b) const
{
return (this->id < b.id);
}

template <typename T>
std::ostream &operator<<(std::ostream &os, const Edge<T> &edge)
{
os << "((Node: " << edge.nodePair.first->getId() << ")) ?----- |Edge: " << edge.id << "|-----? ((Node: " << edge.nodePair.second->getId() << "))";
return os;
}
}

#endif // __CXXGRAPH_EDGE_H__
Loading

0 comments on commit 8b253f3

Please sign in to comment.