From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 25 Feb 2021 11:43:56 +0000 (-0800)
Subject: google test: printer: Migrate smt2_printer_black. (#5970)
X-Git-Tag: cvc5-1.0.0~2215
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=55fa8adde06371e2fe8c6ca4e732703469232cd9;p=cvc5.git

google test: printer: Migrate smt2_printer_black. (#5970)
---

diff --git a/test/unit/printer/CMakeLists.txt b/test/unit/printer/CMakeLists.txt
index 973488a3e..607e92be4 100644
--- a/test/unit/printer/CMakeLists.txt
+++ b/test/unit/printer/CMakeLists.txt
@@ -11,4 +11,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_cxx_unit_test_black(smt2_printer_black printer)
+cvc4_add_unit_test_black(smt2_printer_black printer)
diff --git a/test/unit/printer/smt2_printer_black.cpp b/test/unit/printer/smt2_printer_black.cpp
new file mode 100644
index 000000000..e2e1062f4
--- /dev/null
+++ b/test/unit/printer/smt2_printer_black.cpp
@@ -0,0 +1,62 @@
+/*********************                                                        */
+/*! \file smt2_printer_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of the SMT2 printer
+ **
+ ** Black box testing of the SMT2 printer.
+ **/
+
+#include <iostream>
+
+#include "api/cvc4cpp.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "options/language.h"
+#include "smt/smt_engine.h"
+#include "test_smt.h"
+
+namespace CVC4 {
+
+using namespace kind;
+
+namespace test {
+
+class TestPrinterBlackSmt2 : public TestSmt
+{
+ protected:
+  void checkToString(TNode n, const std::string& expected)
+  {
+    std::stringstream ss;
+    ss << Node::setdepth(-1)
+       << Node::setlanguage(language::output::LANG_SMTLIB_V2_6) << n;
+    ASSERT_EQ(ss.str(), expected);
+  }
+};
+
+TEST_F(TestPrinterBlackSmt2, regexp_repeat)
+{
+  Node n = d_nodeManager->mkNode(
+      d_nodeManager->mkConst(RegExpRepeat(5)),
+      d_nodeManager->mkNode(STRING_TO_REGEXP,
+                            d_nodeManager->mkConst(String("x"))));
+  checkToString(n, "((_ re.^ 5) (str.to_re \"x\"))");
+}
+
+TEST_F(TestPrinterBlackSmt2, regexp_loop)
+{
+  Node n = d_nodeManager->mkNode(
+      d_nodeManager->mkConst(RegExpLoop(1, 3)),
+      d_nodeManager->mkNode(STRING_TO_REGEXP,
+                            d_nodeManager->mkConst(String("x"))));
+  checkToString(n, "((_ re.loop 1 3) (str.to_re \"x\"))");
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/printer/smt2_printer_black.h b/test/unit/printer/smt2_printer_black.h
deleted file mode 100644
index 8540c3cc8..000000000
--- a/test/unit/printer/smt2_printer_black.h
+++ /dev/null
@@ -1,68 +0,0 @@
-/*********************                                                        */
-/*! \file smt2_printer_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of the SMT2 printer
- **
- ** Black box testing of the SMT2 printer.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <iostream>
-
-#include "api/cvc4cpp.h"
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "options/language.h"
-#include "smt/smt_engine.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-
-class Smt2PrinterBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() override
-  {
-    d_slv.reset(new api::Solver());
-    d_nm = d_slv->getSmtEngine()->getNodeManager();
-  }
-
-  void tearDown() override { d_slv.reset(); }
-
-  void checkToString(TNode n, const std::string& expected)
-  {
-    std::stringstream ss;
-    ss << Node::setdepth(-1)
-       << Node::setlanguage(language::output::LANG_SMTLIB_V2_6) << n;
-    TS_ASSERT_EQUALS(ss.str(), expected);
-  }
-
-  void testRegexpRepeat()
-  {
-    Node n = d_nm->mkNode(
-        d_nm->mkConst(RegExpRepeat(5)),
-        d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("x"))));
-    checkToString(n, "((_ re.^ 5) (str.to_re \"x\"))");
-  }
-
-  void testRegexpLoop()
-  {
-    Node n = d_nm->mkNode(
-        d_nm->mkConst(RegExpLoop(1, 3)),
-        d_nm->mkNode(STRING_TO_REGEXP, d_nm->mkConst(String("x"))));
-    checkToString(n, "((_ re.loop 1 3) (str.to_re \"x\"))");
-  }
-
- private:
-  std::unique_ptr<api::Solver> d_slv;
-  NodeManager* d_nm;
-};