Change tests to reflect new reality around quoting symbols.

Author: NlightNFotis

unit/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -11,9 +11,29 @@
 #include <solvers/smt2_incremental/smt_to_smt2_string.h>
 #include <testing-utils/use_catch.h>
 
+#include <tuple>
+
 TEST_CASE("Test smt_indext to string conversion", "[core][smt2_incremental]")
 {
-  CHECK(smt_to_smt2_string(smt_symbol_indext{"green"}) == "|green|");
+  std::string input_term;
+  std::string expected_term;
+  using rowt = std::pair<std::string, std::string>;
+
+  std::tie(input_term, expected_term) = GENERATE(
+    rowt{"green", "green"},
+    rowt{"abc76473*^&", "abc76473*^&"},
+    rowt{"my name is", "|my name is|"},
+    // The following are example symbols from the SMTLIB spec.
+    rowt{"+", "+"},
+    rowt{"**", "**"},
+    rowt{".kkk", ".kkk"},
+    rowt{"-32", "-32"},
+    rowt{" \" can occur too", "| \" can occur too|"});
+
+  SECTION("check that index identifiers are constructed accordingly")
+  {
+    CHECK(smt_to_smt2_string(smt_symbol_indext{input_term}) == expected_term);
+  }
   CHECK(smt_to_smt2_string(smt_numeral_indext{42}) == "42");
 }
 
@@ -36,7 +56,7 @@ TEST_CASE(
 {
   CHECK(
     smt_to_smt2_string(smt_bit_vector_theoryt::extract(7, 3)(
-      smt_bit_vector_constant_termt{0, 8})) == "((_ |extract| 7 3) (_ bv0 8))");
+      smt_bit_vector_constant_termt{0, 8})) == "((_ extract 7 3) (_ bv0 8))");
 }
 
 TEST_CASE(
@@ -51,23 +71,38 @@ TEST_CASE(
   "Test smt_identifier_termt to string conversion",
   "[core][smt2_incremental]")
 {
+  std::string input_term;
+  std::string expected_term;
+  using rowt = std::pair<std::string, std::string>;
+
+  std::tie(input_term, expected_term) = GENERATE(
+    rowt{"abc", "abc"},
+    rowt{"\\", "|&92;|"},
+    rowt{"green", "green"},
+    rowt{"abc76473*^&", "abc76473*^&"},
+    rowt{"my name is", "|my name is|"},
+    // The following are example symbols from the SMTLIB spec.
+    rowt{"+", "+"},
+    rowt{"**", "**"},
+    rowt{".kkk", ".kkk"},
+    rowt{"-32", "-32"},
+    rowt{" \" can occur too", "| \" can occur too|"});
+
   SECTION("Simple identifiers")
   {
     CHECK(
-      smt_to_smt2_string(smt_identifier_termt{"abc", smt_bool_sortt{}}) ==
-      "|abc|");
-    CHECK(
-      smt_to_smt2_string(smt_identifier_termt{"\\", smt_bool_sortt{}}) ==
-      "|&92;|");
+      smt_to_smt2_string(smt_identifier_termt{input_term, smt_bool_sortt{}}) ==
+      expected_term);
   }
+
   SECTION("Indexed identifier")
   {
     CHECK(
       smt_to_smt2_string(smt_identifier_termt{
         "foo",
         smt_bool_sortt{},
         {smt_symbol_indext{"bar"}, smt_numeral_indext{42}}}) ==
-      "(_ |foo| |bar| 42)");
+      "(_ foo bar 42)");
   }
 }
 
@@ -78,8 +113,7 @@ TEST_CASE(
   CHECK(
     smt_to_smt2_string(smt_core_theoryt::equal(
       smt_identifier_termt{"foo", smt_bit_vector_sortt{32}},
-      smt_identifier_termt{"bar", smt_bit_vector_sortt{32}})) ==
-    "(|=| |foo| |bar|)");
+      smt_identifier_termt{"bar", smt_bit_vector_sortt{32}})) == "(= foo bar)");
 }
 
 TEST_CASE(
@@ -102,7 +136,7 @@ TEST_CASE(
 {
   CHECK(
     smt_to_smt2_string(smt_get_value_commandt{
-      smt_identifier_termt{"foo", smt_bool_sortt{}}}) == "(get-value (|foo|))");
+      smt_identifier_termt{"foo", smt_bool_sortt{}}}) == "(get-value (foo))");
 }
 
 TEST_CASE(
@@ -138,7 +172,7 @@ TEST_CASE(
     smt_to_smt2_string(smt_declare_function_commandt{
       smt_identifier_termt{"f", smt_bit_vector_sortt{31}},
       {smt_bit_vector_sortt{32}, smt_bit_vector_sortt{33}}}) ==
-    "(declare-fun |f| ((_ BitVec 32) (_ BitVec 33)) (_ BitVec 31))");
+    "(declare-fun f ((_ BitVec 32) (_ BitVec 33)) (_ BitVec 31))");
 }
 
 TEST_CASE(
@@ -151,8 +185,7 @@ TEST_CASE(
   CHECK(
     smt_to_smt2_string(smt_define_function_commandt{
       "f", {g, h}, smt_core_theoryt::equal(g, h)}) ==
-    "(define-fun |f| ((|g| (_ BitVec 32)) (|h| (_ BitVec 32))) Bool (|=| |g| "
-    "|h|))");
+    "(define-fun f ((g (_ BitVec 32)) (h (_ BitVec 32))) Bool (= g h))");
 }
 
 TEST_CASE(