Add tests for splitting and inclusion graphs

VeriFIT · Dec 14, 2022 · b95c3f0 · b95c3f0
1 parent aabaa06
commit b95c3f0
Showing 1 changed file with 59 additions and 0 deletions.
diff --git a/src/test/noodler/inclusion-graph-node.cc b/src/test/noodler/inclusion-graph-node.cc
@@ -194,6 +194,36 @@ TEST_CASE("Inclusion graph", "[noodler]") {
         });
         CHECK(graph.edges.empty());
     }
+
+    SECTION("x=yx && u = x") {
+        Predicate predicate{ PredicateType::Equation, { { x }, { y, x } } };
+        Predicate predicate2{ PredicateType::Equation, { { u }, { x } } };
+
+        formula.add_predicate(predicate);
+        formula.add_predicate(predicate2);
+        graph = create_inclusion_graph(formula);
+        CHECK(graph.nodes == std::set<GraphNode>{
+                GraphNode{ predicate }, GraphNode{ predicate.get_switched_sides_predicate() },
+                GraphNode{ predicate2.get_switched_sides_predicate() },
+        });
+        CHECK(graph.edges.size() == 3);
+        CHECK(graph.get_num_of_edges() == 6);
+    }
+
+    SECTION("x=y && u = v") {
+        Predicate predicate{ PredicateType::Equation, { { x }, { y } } };
+        Predicate predicate2{ PredicateType::Equation, { { u }, { v } } };
+
+        formula.add_predicate(predicate);
+        formula.add_predicate(predicate2);
+        graph = create_inclusion_graph(formula);
+        CHECK(graph.nodes == std::set<GraphNode>{
+                GraphNode{ predicate },
+                GraphNode{ predicate2 },
+        });
+        CHECK(graph.nodes.size() == 2);
+        CHECK(graph.edges.empty());
+    }
 }
 
 TEST_CASE("Splitting graph", "[noodler]") {
@@ -285,4 +315,33 @@ TEST_CASE("Splitting graph", "[noodler]") {
         CHECK(graph.edges.size() == 2);
         CHECK(graph.get_num_of_edges() == 2);
     }
+
+    SECTION("x=yx && u = x") {
+        Predicate predicate{ PredicateType::Equation, { { x }, { y, x } } };
+        Predicate predicate2{ PredicateType::Equation, { { u }, { x } } };
+
+        formula.add_predicate(predicate);
+        formula.add_predicate(predicate2);
+        graph = create_simplified_splitting_graph(formula);
+        CHECK(graph.nodes == std::set<GraphNode>{
+                GraphNode{ predicate }, GraphNode{ predicate.get_switched_sides_predicate() },
+                GraphNode{ predicate2 }, GraphNode{ predicate2.get_switched_sides_predicate() },
+        });
+        CHECK(graph.edges.size() == 3);
+        CHECK(graph.get_num_of_edges() == 6);
+    }
+
+    SECTION("x=y && u = v") {
+        Predicate predicate{ PredicateType::Equation, { { x }, { y } } };
+        Predicate predicate2{ PredicateType::Equation, { { u }, { v } } };
+
+        formula.add_predicate(predicate);
+        formula.add_predicate(predicate2);
+        graph = create_simplified_splitting_graph(formula);
+        CHECK(graph.nodes == std::set<GraphNode>{
+                GraphNode{ predicate }, GraphNode{ predicate.get_switched_sides_predicate() },
+                GraphNode{ predicate2 }, GraphNode{ predicate2.get_switched_sides_predicate() },
+        });
+        CHECK(graph.edges.empty());
+    }
 }