Add tests

VeriFIT · Dec 14, 2022 · aabaa06 · aabaa06
1 parent e829756
commit aabaa06
Show file tree

Hide file tree

Showing 3 changed files with 94 additions and 23 deletions.
diff --git a/src/smt/theory_str_noodler/inclusion_graph.cc b/src/smt/theory_str_noodler/inclusion_graph.cc
@@ -27,18 +27,18 @@ Graph smt::noodler::create_inclusion_graph(const Formula& formula) {
             );
         }
 
-        for (auto iter{predicates.begin()}; iter != predicates.end(); ++iter) {
-            auto next_iter{iter};
-            next_iter++;
-            for (; next_iter != predicates.end(); ++next_iter) {
-                assert(*iter != *next_iter && "Two equal equations should never appear here in our algorithm");
+        for (auto predicate_iter{predicates.begin()}; predicate_iter != predicates.end(); ++predicate_iter) {
+            auto next_predicate_iter{predicate_iter};
+            next_predicate_iter++;
+            for (; next_predicate_iter != predicates.end(); ++next_predicate_iter) {
+                assert(*predicate_iter != *next_predicate_iter && "Two equal equations should never appear here in our algorithm");
             }
 
         }
     }
 
     Graph splitting_graph{ create_simplified_splitting_graph(formula) };
-    return create_inclusion_graph(std::move(splitting_graph));;
+    return create_inclusion_graph(splitting_graph);
 }
 
 Graph smt::noodler::create_simplified_splitting_graph(const Formula& formula) {
@@ -94,7 +94,7 @@ Graph smt::noodler::create_simplified_splitting_graph(const Formula& formula) {
     return graph;
 }
 
-Graph smt::noodler::create_inclusion_graph(Graph simplified_splitting_graph) {
+Graph smt::noodler::create_inclusion_graph(Graph& simplified_splitting_graph) {
     Graph inclusion_graph{};
 
     bool splitting_graph_changed{ true };
@@ -105,7 +105,6 @@ Graph smt::noodler::create_inclusion_graph(Graph simplified_splitting_graph) {
             auto node{ const_cast<GraphNode *>(&const_node) };
             if (simplified_splitting_graph.get_edges_to(node).empty()) {
                 inclusion_graph.nodes.insert(*node);
-                splitting_graph_changed = true;
 
                 auto switched_node{ simplified_splitting_graph.get_node(node->get_predicate().get_switched_sides_predicate()) };
 
@@ -115,6 +114,9 @@ Graph smt::noodler::create_inclusion_graph(Graph simplified_splitting_graph) {
 
                 simplified_splitting_graph.nodes.erase(*node);
                 simplified_splitting_graph.nodes.erase(*switched_node);
+
+                splitting_graph_changed = true;
+                break;
             }
         }
     }

diff --git a/src/smt/theory_str_noodler/inclusion_graph.h b/src/smt/theory_str_noodler/inclusion_graph.h
@@ -96,7 +96,7 @@ namespace smt::noodler {
 
     Graph create_simplified_splitting_graph(const Formula& formula);
 
-    Graph create_inclusion_graph(Graph simplified_splitting_graph);
+    Graph create_inclusion_graph(Graph& simplified_splitting_graph);
 
 }
 

diff --git a/src/test/noodler/inclusion-graph-node.cc b/src/test/noodler/inclusion-graph-node.cc
@@ -123,31 +123,85 @@ TEST_CASE("Graph::get_edges_to", "[noodler]") {
     CHECK(edges_to_target.find(graph.get_node(predicate2.get_switched_sides_predicate())) != edges_to_target.end());
 }
 
-TEST_CASE("Create inclusion graph", "[noodler]") {
+TEST_CASE("Inclusion graph", "[noodler]") {
     Graph graph;
     Formula formula;
 
     BasicTerm u{ BasicTermType::Variable, "u" };
-    BasicTerm z{ BasicTermType::Variable, "z" };
     BasicTerm v{ BasicTermType::Variable, "v" };
     BasicTerm x{ BasicTermType::Variable, "x" };
-    Predicate predicate{ PredicateType::Equation, { { u }, { z } } };
-    Predicate predicate2{ PredicateType::Equation, { { v }, { u } } };
-    Predicate predicate3{ PredicateType::Equation, { { x }, { u, v, x } } };
+    BasicTerm y{ BasicTermType::Variable, "y" };
+    BasicTerm z{ BasicTermType::Variable, "z" };
 
-    formula.add_predicate(predicate);
-    formula.add_predicate(predicate2);
-    formula.add_predicate(predicate3);
-    graph = create_inclusion_graph(formula);
-    CHECK(graph.nodes.size() == 5);
-    CHECK(graph.edges.size() == 5);
-    CHECK(graph.get_num_of_edges() == 12);
+    SECTION("u = z && v = u && x = uvx") {
+        Predicate predicate{ PredicateType::Equation, { { u }, { z } } };
+        Predicate predicate2{ PredicateType::Equation, { { v }, { u } } };
+        Predicate predicate3{ PredicateType::Equation, { { x }, { u, v, x } } };
+
+        formula.add_predicate(predicate);
+        formula.add_predicate(predicate2);
+        formula.add_predicate(predicate3);
+        graph = create_inclusion_graph(formula);
+        CHECK(graph.nodes.size() == 5);
+        CHECK(graph.edges.size() == 5);
+        CHECK(graph.get_num_of_edges() == 12);
+    }
+
+    SECTION("x = xy && xy = yx") {
+        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_inclusion_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() == 4);
+        CHECK(graph.get_num_of_edges() == 16);
+    }
+
+    SECTION("yx = yx") {
+        Predicate predicate{ PredicateType::Equation, { { x }, { y, x } } };
+
+        formula.add_predicate(predicate);
+        graph = create_inclusion_graph(formula);
+        CHECK(graph.nodes == std::set<GraphNode>{
+                GraphNode{ predicate }, GraphNode{ predicate.get_switched_sides_predicate() },
+        });
+        CHECK(graph.edges.size() == 2);
+        CHECK(graph.get_num_of_edges() == 4);
+    }
+
+    SECTION("x = xy") {
+        Predicate predicate{ PredicateType::Equation, { { x }, { x, y } } };
+
+        formula.add_predicate(predicate);
+        //CHECK_THROWS(create_inclusion_graph(formula)); // FIXME: Catch2 cannot catch failing assert.
+    }
+
+    SECTION("x=y && u = x") {
+        Predicate predicate{ PredicateType::Equation, { { x }, { y } } };
+        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{ predicate2.get_switched_sides_predicate() },
+        });
+        CHECK(graph.edges.empty());
+    }
 }
 
 TEST_CASE("Splitting graph", "[noodler]") {
     Graph graph;
     Formula formula;
 
+    BasicTerm u{ BasicTermType::Variable, "u" };
+    BasicTerm v{ BasicTermType::Variable, "v" };
     BasicTerm x{ BasicTermType::Variable, "x" };
     BasicTerm y{ BasicTermType::Variable, "y" };
 
@@ -213,7 +267,22 @@ TEST_CASE("Splitting graph", "[noodler]") {
             GraphNode{ predicate }, GraphNode{ predicate.get_switched_sides_predicate() },
             GraphNode{ predicate2 }, GraphNode{ predicate2.get_switched_sides_predicate() },
         });
-        REQUIRE(graph.edges.size() == 4);
-        REQUIRE(graph.get_num_of_edges() == 12);
+        CHECK(graph.edges.size() == 4);
+        CHECK(graph.get_num_of_edges() == 12);
+    }
+
+    SECTION("x=y && x = u") {
+        Predicate predicate{ PredicateType::Equation, { { x }, { y } } };
+        Predicate predicate2{ PredicateType::Equation, { { x }, { u } } };
+
+        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() == 2);
+        CHECK(graph.get_num_of_edges() == 2);
     }
 }
-Original file line number
+Diff line change
@@ Expand Up / @@ -96,7 +96,7 @@ namespace smt::noodler { @@
         Graph create_simplified_splitting_graph(const Formula& formula);
-        Graph create_inclusion_graph(Graph simplified_splitting_graph);
+        Graph create_inclusion_graph(Graph& simplified_splitting_graph);
     }
@@ Expand Down @@