Add method to get edges from graph

VeriFIT · Dec 14, 2022 · ea1fead · ea1fead
1 parent 4528f0d
commit ea1fead
Show file tree

Hide file tree

Showing 2 changed files with 31 additions and 1 deletion.
diff --git a/src/smt/theory_str_noodler/inclusion_graph.h b/src/smt/theory_str_noodler/inclusion_graph.h
@@ -2,11 +2,15 @@
 #ifndef Z3_INCLUSION_GRAPH_H
 #define Z3_INCLUSION_GRAPH_H
 
+#include <optional>
 #include "inclusion_graph_node.h"
 
 namespace smt::noodler {
     class Graph {
     public:
+        using TargetNodes = std::unordered_set<GraphNode*>;
+        using Edges = std::unordered_map<GraphNode*, TargetNodes>;
+
         Graph() = default;
 
         std::set<GraphNode> nodes;
@@ -24,6 +28,16 @@ namespace smt::noodler {
             return num_of_edges;
         }
 
+        const Edges& get_edges() const { return edges; }
+
+        std::optional<const std::reference_wrapper<TargetNodes>> get_edges(const GraphNode* const source) {
+            const auto source_edges{ edges.find(const_cast<GraphNode*>(source)) };
+            if (source_edges != edges.end()) {
+                return std::make_optional<const std::reference_wrapper<TargetNodes>>(source_edges->second);
+            }
+            return std::nullopt;
+        }
+
         // TODO: Method to get edges from node.
     }; // Class Graph.
 

diff --git a/src/test/noodler/inclusion-graph-node.cc b/src/test/noodler/inclusion-graph-node.cc
@@ -8,6 +8,22 @@
 
 using namespace smt::noodler;
 
+TEST_CASE("Graph::get_edges()", "[noodler]") {
+    Graph graph;
+    Formula formula;
+    BasicTerm x{ BasicTermType::Variable, "x" };
+    BasicTerm y{ BasicTermType::Variable, "y" };
+    Predicate predicate{ PredicateType::Equation, { { x }, { x, y } } };
+    Predicate predicate2{ PredicateType::Equation, { { x, y }, { y, x } } };
+    formula.add_predicate(predicate);
+    formula.add_predicate(predicate2);
+    graph = create_simplified_splitting_graph(formula);
+
+    auto edges{ graph.get_edges(&(*graph.nodes.begin())) };
+    REQUIRE(edges.has_value());
+    CHECK((*edges.value().get().begin())->get_predicate().to_string() == "Equation: y x = x y");
+}
+
 TEST_CASE( "Inclusion graph node", "[noodler]" ) {
     auto predicate{ Predicate(PredicateType::Equation) };
     auto predicate_ineq{ Predicate(PredicateType::Inequation) };
@@ -76,7 +92,7 @@ TEST_CASE("Conversion to strings", "[noodler]") {
     } );
 }
 
-TEST_CASE("Mata integration") {
+TEST_CASE("Mata integration", "[noodler]") {
     auto nfa = Mata::Nfa::Nfa(3);
     nfa.initial_states = { 0, 1};
     nfa.final_states = { 3, 1};