Test printing terms and predicates

VeriFIT · Nov 21, 2022 · 6b7348b · 6b7348b
1 parent 19927f0
commit 6b7348b
Show file tree

Hide file tree

Showing 2 changed files with 12 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
@@ -369,6 +369,11 @@ namespace smt::noodler {
         return predicate.to_string();
     }
 
+    std::ostream& operator<<(std::ostream& os, const Predicate& predicate) {
+        os << predicate.to_string();
+        return os;
+    }
+
     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/test/noodler/inclusion-graph-node.cc b/src/test/noodler/inclusion-graph-node.cc
@@ -59,5 +59,12 @@ TEST_CASE("Conversion to strings") {
     } } };
 
     CHECK(pred.to_string() == "Equation: . \"4\" (Literal) . x_42 (Variable) = . xyz (Variable) . y_58 (Variable)");
+
+    auto pred_ineq{ Predicate{ PredicateType::Inequation, {
+            { { BasicTermType::Literal, "4" }, { BasicTermType::Variable, "x_42" } } ,
+            { { BasicTermType::Variable, "xyz" }, { BasicTermType::Variable, "y_58" } },
+    } } };
+
+    CHECK(pred_ineq.to_string() == "Inequation: . \"4\" (Literal) . x_42 (Variable) != . xyz (Variable) . y_58 (Variable)");
 }