google test: theory: Migrate theory_strings_skolem_cache_black. (#6002)

diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 0d24da50be52ede05a22b037853d72d2dded6291..c52b4196692f1b374e97c4c0dfa172e12d9b41e4 100644 (file)
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -25,7 +25,7 @@ cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
 cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_inverter_white theory)
 cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory)
 cvc4_add_unit_test_white(theory_sets_type_rules_white theory)
-cvc4_add_cxx_unit_test_white(theory_strings_skolem_cache_black theory)
+cvc4_add_unit_test_white(theory_strings_skolem_cache_black theory)
 cvc4_add_unit_test_white(theory_strings_word_white theory)
 cvc4_add_unit_test_white(theory_white theory)
 cvc4_add_unit_test_white(type_enumerator_white theory)

diff --git a/test/unit/theory/theory_strings_skolem_cache_black.cpp b/test/unit/theory/theory_strings_skolem_cache_black.cpp
new file mode 100644 (file)
index 0000000..fbe9761
--- /dev/null
+++ b/test/unit/theory/theory_strings_skolem_cache_black.cpp
@@ -0,0 +1,62 @@
+/*********************                                                        */
+/*! \file theory_strings_skolem_cache_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 skolem cache of the theory of strings.
+ **/
+
+#include <memory>
+
+#include "expr/node.h"
+#include "test_smt.h"
+#include "theory/strings/skolem_cache.h"
+#include "util/rational.h"
+#include "util/string.h"
+
+namespace CVC4 {
+
+using namespace theory::strings;
+
+namespace test {
+
+class TestTheoryBlackStringsSkolemCache : public TestSmt
+{
+};
+
+TEST_F(TestTheoryBlackStringsSkolemCache, mkSkolemCached)
+{
+  Node zero = d_nodeManager->mkConst(Rational(0));
+  Node n = d_nodeManager->mkSkolem("n", d_nodeManager->integerType());
+  Node a = d_nodeManager->mkSkolem("a", d_nodeManager->stringType());
+  Node b = d_nodeManager->mkSkolem("b", d_nodeManager->stringType());
+  Node c = d_nodeManager->mkSkolem("c", d_nodeManager->stringType());
+  Node d = d_nodeManager->mkSkolem("d", d_nodeManager->stringType());
+  Node sa = d_nodeManager->mkNode(
+      kind::STRING_SUBSTR,
+      a,
+      zero,
+      d_nodeManager->mkNode(kind::STRING_STRIDOF, a, b, zero));
+  Node sc = d_nodeManager->mkNode(kind::STRING_SUBSTR, c, zero, n);
+
+  SkolemCache sk;
+
+  // Check that skolems are shared between:
+  //
+  // SK_FIRST_CTN(a, b)
+  //
+  // SK_FIRST_CTN(a, b)
+  {
+    Node s1 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo");
+    Node s2 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo");
+    ASSERT_EQ(s1, s2);
+  }
+}
+}  // namespace test
+}  // namespace CVC4

diff --git a/test/unit/theory/theory_strings_skolem_cache_black.h b/test/unit/theory/theory_strings_skolem_cache_black.h
deleted file mode 100644 (file)
index 72a9b7e..0000000
--- a/test/unit/theory/theory_strings_skolem_cache_black.h
+++ /dev/null
@@ -1,82 +0,0 @@
-/*********************                                                        */
-/*! \file theory_strings_skolem_cache_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andres Noetzli, Andrew Reynolds
- ** 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 skolem cache of the theory of strings.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <memory>
-
-#include "expr/expr_manager.h"
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "theory/strings/skolem_cache.h"
-#include "util/rational.h"
-#include "util/string.h"
-
-using namespace CVC4;
-using namespace CVC4::smt;
-using namespace CVC4::theory::strings;
-
-class TheoryStringsSkolemCacheBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() override
-  {
-    d_em.reset(new ExprManager());
-    d_nm = NodeManager::fromExprManager(d_em.get());
-    d_smt.reset(new SmtEngine(d_nm));
-    d_scope.reset(new SmtScope(d_smt.get()));
-    // Ensure that the SMT engine is fully initialized (required for the
-    // rewriter)
-    d_smt->push();
-
-  }
-
-  void tearDown() override {}
-
-  void testMkSkolemCached()
-  {
-    Node zero = d_nm->mkConst(Rational(0));
-    Node n = d_nm->mkSkolem("n", d_nm->integerType());
-    Node a = d_nm->mkSkolem("a", d_nm->stringType());
-    Node b = d_nm->mkSkolem("b", d_nm->stringType());
-    Node c = d_nm->mkSkolem("c", d_nm->stringType());
-    Node d = d_nm->mkSkolem("d", d_nm->stringType());
-    Node sa = d_nm->mkNode(kind::STRING_SUBSTR,
-                           a,
-                           zero,
-                           d_nm->mkNode(kind::STRING_STRIDOF, a, b, zero));
-    Node sc = d_nm->mkNode(kind::STRING_SUBSTR, c, zero, n);
-
-    SkolemCache sk;
-
-    // Check that skolems are shared between:
-    //
-    // SK_FIRST_CTN(a, b)
-    //
-    // SK_FIRST_CTN(a, b)
-    {
-      Node s1 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo");
-      Node s2 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo");
-      TS_ASSERT_EQUALS(s1, s2);
-    }
-  }
-
- private:
-  std::unique_ptr<ExprManager> d_em;
-  std::unique_ptr<SmtEngine> d_smt;
-  NodeManager* d_nm;
-  std::unique_ptr<SmtScope> d_scope;
-};