Print terms and predicates in a formatted string

VeriFIT · Nov 21, 2022 · 19927f0 · 19927f0
1 parent 046d177
commit 19927f0
Show file tree

Hide file tree

Showing 3 changed files with 120 additions and 0 deletions.
diff --git a/src/smt/theory_str_noodler/inclusion_graph_node.h b/src/smt/theory_str_noodler/inclusion_graph_node.h
@@ -26,12 +26,28 @@
 
 namespace smt::noodler {
     enum struct PredicateType {
+        Default,
         Equation,
         Inequation,
         Contains,
         // TODO: Add additional predicate types.
     };
 
+    [[nodiscard]] std::string to_string(PredicateType predicate_type) {
+        switch (predicate_type) {
+            case PredicateType::Default:
+                return "Default";
+            case PredicateType::Equation:
+                return "Equation";
+            case PredicateType::Inequation:
+                return "Inequation";
+            case PredicateType::Contains:
+                return "Contains";
+        }
+
+        throw std::runtime_error("Unhandled predicate type passed to to_string().");
+    }
+
     enum struct BasicTermType {
         Variable,
         Literal,
@@ -41,6 +57,23 @@ namespace smt::noodler {
         // TODO: Add additional basic term types.
     };
 
+    [[nodiscard]] std::string to_string(BasicTermType term_type) {
+        switch (term_type) {
+            case BasicTermType::Variable:
+                return "Variable";
+            case BasicTermType::Literal:
+                return "Literal";
+            case BasicTermType::Length:
+                return "Length";
+            case BasicTermType::Substring:
+                return "Substring";
+            case BasicTermType::IndexOf:
+                return "IndexOf";
+        }
+
+        throw std::runtime_error("Unhandled basic term type passed to to_string().");
+    }
+
     class BasicTerm {
     public:
         explicit BasicTerm(BasicTermType type): type(type) {}
@@ -58,11 +91,37 @@ namespace smt::noodler {
             return type == other.get_type() && name == other.get_name();
         }
 
+        [[nodiscard]] std::string to_string() const {
+            switch (type) {
+                case BasicTermType::Literal: {
+                    std::string result{};
+                    if (!name.empty()) {
+                        result += "\"" + name + "\" ";
+                    }
+                    result += "(" + noodler::to_string(type) + ")";
+                    return result;
+                }
+                case BasicTermType::Variable:
+                    return name + " (" + noodler::to_string(type) + ")";
+                case BasicTermType::Length:
+                case BasicTermType::Substring:
+                case BasicTermType::IndexOf:
+                    return name + " (" + noodler::to_string(type) + ")";
+                    // TODO: Decide what will have names and when to use them.
+            }
+
+            throw std::runtime_error("Unhandled basic term type passed as 'this' to to_string().");
+        }
+
     private:
         BasicTermType type;
         std::string name;
     }; // Class BasicTerm.
 
+    [[nodiscard]] std::string to_string(const BasicTerm& basic_term) {
+        return basic_term.to_string();
+    }
+
     static bool operator==(const BasicTerm& lhs, const BasicTerm& rhs) { return lhs.equals(rhs); }
     static bool operator!=(const BasicTerm& lhs, const BasicTerm& rhs) { return !(lhs == rhs); }
     static bool operator<(const BasicTerm& lhs, const BasicTerm& rhs) {
@@ -86,6 +145,7 @@ namespace smt::noodler {
             Right,
         };
 
+        Predicate() : type(PredicateType::Default) {}
         explicit Predicate(const PredicateType type): type(type) {
             if (is_equation() || is_inequation()) {
                 params.resize(2);
@@ -259,13 +319,56 @@ namespace smt::noodler {
             return false;
         }
 
+        [[nodiscard]] std::string to_string() const {
+            switch (type) {
+                case PredicateType::Default: {
+                    return "Default (missing type and data)";
+                }
+                case PredicateType::Equation: {
+                    std::string result{ "Equation:" };
+                    for (const auto& item: get_left_side()) {
+                        result += " . " + item.to_string();
+                    }
+                    result += " =";
+                    for (const auto& item: get_right_side()) {
+                        result += " . " + item.to_string();
+                    }
+                    return result;
+                }
+
+                case PredicateType::Inequation: {
+                    std::string result{ "Inequation:" };
+                    for (const auto& item: get_left_side()) {
+                        result += " . " + item.to_string();
+                    }
+                    result += " !=";
+                    for (const auto& item: get_right_side()) {
+                        result += " . " + item.to_string();
+                    }
+                    return result;
+                }
+
+                // TODO: Implement prints for other predicates.
+
+                case PredicateType::Contains: {
+                    break;
+                }
+            }
+
+            throw std::runtime_error("Unhandled predicate type passed as 'this' to to_string().");
+        }
+
         // TODO: Additional operations.
 
     private:
         PredicateType type;
         std::vector<std::vector<BasicTerm>> params;
     }; // Class Predicate.
 
+    [[nodiscard]] std::string to_string(const Predicate& predicate) {
+        return predicate.to_string();
+    }
+
     static bool operator==(const Predicate& lhs, const Predicate& rhs) { return lhs.equals(rhs); }
     static bool operator!=(const Predicate& lhs, const Predicate& rhs) { return !(lhs == rhs); }
 

diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp
@@ -6,6 +6,7 @@ Eternal glory to Yu-Fang.
 #include <algorithm>
 #include <sstream>
 #include <iostream>
+#include <cmath>
 #include "ast/ast_pp.h"
 #include "smt/theory_str_noodler/theory_str_noodler.h"
 #include "smt/smt_context.h"

diff --git a/src/test/noodler/inclusion-graph-node.cc b/src/test/noodler/inclusion-graph-node.cc
@@ -45,3 +45,19 @@ TEST_CASE( "Inclusion graph node", "[noodler]" ) {
     CHECK(term_var2 < term_lit2);
     CHECK(term != term_var);
 }
+
+TEST_CASE("Conversion to strings") {
+    CHECK(smt::noodler::to_string(BasicTermType::Literal) == "Literal");
+    CHECK(smt::noodler::to_string(BasicTermType::Variable) == "Variable");
+    CHECK(BasicTerm{ BasicTermType::Literal }.to_string() == "(Literal)");
+    CHECK(BasicTerm{ BasicTermType::Literal, "4" }.to_string() == "\"4\" (Literal)");
+    CHECK(BasicTerm{ BasicTermType::Variable, "x_42" }.to_string() == "x_42 (Variable)");
+
+    auto pred{ Predicate{ PredicateType::Equation, {
+        { { BasicTermType::Literal, "4" }, { BasicTermType::Variable, "x_42" } } ,
+        { { BasicTermType::Variable, "xyz" }, { BasicTermType::Variable, "y_58" } },
+    } } };
+
+    CHECK(pred.to_string() == "Equation: . \"4\" (Literal) . x_42 (Variable) = . xyz (Variable) . y_58 (Variable)");
+}
+