Add methods to get edges leading to target state

VeriFIT · Dec 14, 2022 · 3d3a88c · 3d3a88c
1 parent ea1fead
commit 3d3a88c
Show file tree

Hide file tree

Showing 3 changed files with 45 additions and 8 deletions.
diff --git a/src/smt/theory_str_noodler/inclusion_graph.h b/src/smt/theory_str_noodler/inclusion_graph.h
@@ -8,8 +8,8 @@
 namespace smt::noodler {
     class Graph {
     public:
-        using TargetNodes = std::unordered_set<GraphNode*>;
-        using Edges = std::unordered_map<GraphNode*, TargetNodes>;
+        using Nodes = std::unordered_set<GraphNode*>;
+        using Edges = std::unordered_map<GraphNode*, Nodes>;
 
         Graph() = default;
 
@@ -30,15 +30,29 @@ namespace smt::noodler {
 
         const Edges& get_edges() const { return edges; }
 
-        std::optional<const std::reference_wrapper<TargetNodes>> get_edges(const GraphNode* const source) {
+        std::optional<const std::reference_wrapper<Nodes>> 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::make_optional<const std::reference_wrapper<Nodes>>(source_edges->second);
             }
             return std::nullopt;
         }
 
-        // TODO: Method to get edges from node.
+        Nodes get_edges_to(GraphNode* const target) const {
+            Nodes source_nodes{};
+            for (const auto& source_edges: edges) {
+                if (source_edges.second.find(target) != source_edges.second.end()) {
+                    source_nodes.insert(source_edges.first);
+                }
+            }
+            return source_nodes;
+        }
+
+        GraphNode* get_node(Predicate predicate) {
+            auto node{ nodes.find(GraphNode{ predicate }) };
+            if (node == nodes.end()) { return nullptr; }
+            return const_cast<GraphNode*>(&*node);
+        }
     }; // Class Graph.
 
     class Formula {
@@ -60,6 +74,7 @@ namespace smt::noodler {
     Graph create_simplified_splitting_graph(const Formula& formula);
 
     Graph create_inclusion_graph(const Graph& simplified_splitting_graph);
+
 }
 
 

diff --git a/src/smt/theory_str_noodler/inclusion_graph_node.h b/src/smt/theory_str_noodler/inclusion_graph_node.h
@@ -241,6 +241,8 @@ namespace smt::noodler {
     private:
         PredicateType type;
         std::vector<std::vector<BasicTerm>> params;
+
+        // TODO: Add additional attributes such as cost, etc.
     }; // Class Predicate.
 
     [[nodiscard]] static std::string to_string(const Predicate& predicate) {
@@ -274,8 +276,8 @@ namespace smt::noodler {
         explicit GraphNode(const Predicate& predicate) : node_predicate(predicate) {}
 
         void set_predicate(const Predicate& predicate) { this->node_predicate = predicate; }
-        Predicate& get_predicate() { return node_predicate; }
-        const Predicate& get_predicate() const { return node_predicate; }
+        [[nodiscard]] Predicate& get_predicate() { return node_predicate; }
+        [[nodiscard]] const Predicate& get_predicate() const { return node_predicate; }
 
         struct HashFunction {
             size_t operator()(const GraphNode& graph_node) const {
@@ -288,7 +290,9 @@ namespace smt::noodler {
         }
 
     private:
-         Predicate node_predicate;
+        Predicate node_predicate;
+
+        // TODO: Add additional attributes such as cost, etc.
     }; // Class GraphNode.
 
     static bool operator==(const GraphNode& lhs, const GraphNode& rhs) { return lhs.equals(rhs); }

diff --git a/src/test/noodler/inclusion-graph-node.cc b/src/test/noodler/inclusion-graph-node.cc
@@ -105,6 +105,24 @@ TEST_CASE("Mata integration", "[noodler]") {
     CHECK(!nfa.has_no_transitions());
 }
 
+TEST_CASE("Graph::get_edges_to", "[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 target{ graph.get_node(predicate) };
+    auto edges_to_target{ graph.get_edges_to(target) };
+    CHECK(edges_to_target.find(graph.get_node(predicate)) != edges_to_target.end());
+    CHECK(edges_to_target.find(graph.get_node(predicate2)) != edges_to_target.end());
+    CHECK(edges_to_target.find(graph.get_node(predicate2.get_switched_sides_predicate())) != edges_to_target.end());
+}
+
 TEST_CASE("Splitting graph", "[noodler]") {
     Graph graph;
     Formula formula;