google test: theory: Migrate theory_black. (#5985)

diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 1af33ff19599a7c3ae434d8469ad324874a697ba..f972efd47350e74be6507427b5f574136d7a4f28 100644 (file)
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -9,7 +9,7 @@
 ## directory for licensing information.
 ##
 cvc4_add_unit_test_black(regexp_operation_black theory)
-cvc4_add_cxx_unit_test_black(theory_black theory)
+cvc4_add_unit_test_black(theory_black theory)
 cvc4_add_unit_test_white(evaluator_white theory)
 cvc4_add_unit_test_white(logic_info_white theory)
 cvc4_add_unit_test_white(sequences_rewriter_white theory)

diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp
new file mode 100644 (file)
index 0000000..0aba243
--- /dev/null
+++ b/test/unit/theory/theory_black.cpp
@@ -0,0 +1,133 @@
+/*********************                                                        */
+/*! \file theory_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** 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 CVC4::theory
+ **
+ ** Black box testing of CVC4::theory
+ **/
+
+#include <sstream>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/node_builder.h"
+#include "expr/node_value.h"
+#include "test_smt.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace context;
+using namespace theory;
+using namespace smt;
+
+namespace test {
+
+class TestTheoryBlack : public TestSmt
+{
+};
+
+TEST_F(TestTheoryBlack, array_const)
+{
+  TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+                                                d_nodeManager->integerType());
+  Node zero = d_nodeManager->mkConst(Rational(0));
+  Node one = d_nodeManager->mkConst(Rational(1));
+  Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
+  ASSERT_TRUE(storeAll.isConst());
+
+  Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
+  ASSERT_FALSE(arr.isConst());
+  arr = Rewriter::rewrite(arr);
+  ASSERT_TRUE(arr.isConst());
+  arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
+  ASSERT_TRUE(arr.isConst());
+  Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
+  ASSERT_FALSE(arr2.isConst());
+  arr2 = Rewriter::rewrite(arr2);
+  ASSERT_TRUE(arr2.isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr, one, one);
+  ASSERT_TRUE(arr2.isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
+  ASSERT_FALSE(arr2.isConst());
+  arr2 = Rewriter::rewrite(arr2);
+  ASSERT_TRUE(arr2.isConst());
+
+  arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1),
+                                       d_nodeManager->mkBitVectorType(1));
+  zero = d_nodeManager->mkConst(BitVector(1, 0u));
+  one = d_nodeManager->mkConst(BitVector(1, 1u));
+  storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
+  ASSERT_TRUE(storeAll.isConst());
+
+  arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
+  ASSERT_FALSE(arr.isConst());
+  arr = Rewriter::rewrite(arr);
+  ASSERT_TRUE(arr.isConst());
+  arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
+  arr = Rewriter::rewrite(arr);
+  ASSERT_TRUE(arr.isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
+  ASSERT_FALSE(arr2.isConst());
+  arr2 = Rewriter::rewrite(arr2);
+  ASSERT_TRUE(arr2.isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr, one, one);
+  ASSERT_FALSE(arr2.isConst());
+  arr2 = Rewriter::rewrite(arr2);
+  ASSERT_TRUE(arr2.isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
+  ASSERT_FALSE(arr2.isConst());
+  arr2 = Rewriter::rewrite(arr2);
+  ASSERT_TRUE(arr2.isConst());
+
+  arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(2),
+                                       d_nodeManager->mkBitVectorType(2));
+  zero = d_nodeManager->mkConst(BitVector(2, 0u));
+  one = d_nodeManager->mkConst(BitVector(2, 1u));
+  Node two = d_nodeManager->mkConst(BitVector(2, 2u));
+  Node three = d_nodeManager->mkConst(BitVector(2, 3u));
+  storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, one));
+  ASSERT_TRUE(storeAll.isConst());
+
+  arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
+  ASSERT_TRUE(arr.isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
+  ASSERT_FALSE(arr2.isConst());
+  arr2 = Rewriter::rewrite(arr2);
+  ASSERT_TRUE(arr2.isConst());
+
+  arr = d_nodeManager->mkNode(STORE, storeAll, one, three);
+  ASSERT_TRUE(arr.isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr, one, one);
+  ASSERT_FALSE(arr2.isConst());
+  arr2 = Rewriter::rewrite(arr2);
+  ASSERT_TRUE(arr2 == storeAll);
+
+  arr2 = d_nodeManager->mkNode(STORE, arr, zero, zero);
+  ASSERT_FALSE(arr2.isConst());
+  ASSERT_TRUE(Rewriter::rewrite(arr2).isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr2, two, two);
+  ASSERT_FALSE(arr2.isConst());
+  ASSERT_TRUE(Rewriter::rewrite(arr2).isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr2, three, one);
+  ASSERT_FALSE(arr2.isConst());
+  ASSERT_TRUE(Rewriter::rewrite(arr2).isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr2, three, three);
+  ASSERT_FALSE(arr2.isConst());
+  ASSERT_TRUE(Rewriter::rewrite(arr2).isConst());
+  arr2 = d_nodeManager->mkNode(STORE, arr2, two, zero);
+  ASSERT_FALSE(arr2.isConst());
+  arr2 = Rewriter::rewrite(arr2);
+  ASSERT_TRUE(arr2.isConst());
+}
+}  // namespace test
+}  // namespace CVC4

diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
deleted file mode 100644 (file)
index bd843eb..0000000
--- a/test/unit/theory/theory_black.h
+++ /dev/null
@@ -1,158 +0,0 @@
-/*********************                                                        */
-/*! \file theory_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Clark Barrett, Andres Noetzli, Tim King
- ** 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 CVC4::theory
- **
- ** Black box testing of CVC4::theory
- **/
-
-#include <cxxtest/TestSuite.h>
-
-//Used in some of the tests
-#include <sstream>
-#include <vector>
-
-#include "api/cvc4cpp.h"
-#include "expr/expr_manager.h"
-#include "expr/node.h"
-#include "expr/node_builder.h"
-#include "expr/node_manager.h"
-#include "expr/node_value.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "theory/rewriter.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::smt;
-
-class TheoryBlack : public CxxTest::TestSuite {
- public:
-  void setUp() override
-  {
-    d_slv = new api::Solver();
-    d_em = d_slv->getExprManager();
-    d_smt = d_slv->getSmtEngine();
-    d_scope = new SmtScope(d_smt);
-    // Ensure that the SMT engine is fully initialized (required for the
-    // rewriter)
-    d_smt->push();
-
-    d_nm = NodeManager::fromExprManager(d_em);
-  }
-
-  void tearDown() override
-  {
-    delete d_scope;
-    delete d_slv;
-  }
-
-  void testArrayConst() {
-    TypeNode arrType = d_nm->mkArrayType(d_nm->integerType(), d_nm->integerType());
-    Node zero = d_nm->mkConst(Rational(0));
-    Node one = d_nm->mkConst(Rational(1));
-    Node storeAll = d_nm->mkConst(ArrayStoreAll(arrType, zero));
-    TS_ASSERT(storeAll.isConst());
-
-    Node arr = d_nm->mkNode(STORE, storeAll, zero, zero);
-    TS_ASSERT(!arr.isConst());
-    arr = Rewriter::rewrite(arr);
-    TS_ASSERT(arr.isConst());
-    arr = d_nm->mkNode(STORE, storeAll, zero, one);
-    TS_ASSERT(arr.isConst());
-    Node arr2 = d_nm->mkNode(STORE, arr, one, zero);
-    TS_ASSERT(!arr2.isConst());
-    arr2 = Rewriter::rewrite(arr2);
-    TS_ASSERT(arr2.isConst());
-    arr2 = d_nm->mkNode(STORE, arr, one, one);
-    TS_ASSERT(arr2.isConst());
-    arr2 = d_nm->mkNode(STORE, arr, zero, one);
-    TS_ASSERT(!arr2.isConst());
-    arr2 = Rewriter::rewrite(arr2);
-    TS_ASSERT(arr2.isConst());
-
-    arrType = d_nm->mkArrayType(d_nm->mkBitVectorType(1), d_nm->mkBitVectorType(1));
-    zero = d_nm->mkConst(BitVector(1,unsigned(0)));
-    one = d_nm->mkConst(BitVector(1,unsigned(1)));
-    storeAll = d_nm->mkConst(ArrayStoreAll(arrType, zero));
-    TS_ASSERT(storeAll.isConst());
-
-    arr = d_nm->mkNode(STORE, storeAll, zero, zero);
-    TS_ASSERT(!arr.isConst());
-    arr = Rewriter::rewrite(arr);
-    TS_ASSERT(arr.isConst());
-    arr = d_nm->mkNode(STORE, storeAll, zero, one);
-    arr = Rewriter::rewrite(arr); 
-    TS_ASSERT(arr.isConst());
-    arr2 = d_nm->mkNode(STORE, arr, one, zero);
-    TS_ASSERT(!arr2.isConst());
-    arr2 = Rewriter::rewrite(arr2);
-    TS_ASSERT(arr2.isConst());
-    arr2 = d_nm->mkNode(STORE, arr, one, one);
-    TS_ASSERT(!arr2.isConst());
-    arr2 = Rewriter::rewrite(arr2);
-    TS_ASSERT(arr2.isConst());
-    arr2 = d_nm->mkNode(STORE, arr, zero, one);
-    TS_ASSERT(!arr2.isConst());
-    arr2 = Rewriter::rewrite(arr2);
-    TS_ASSERT(arr2.isConst());
-
-    arrType = d_nm->mkArrayType(d_nm->mkBitVectorType(2), d_nm->mkBitVectorType(2));
-    zero = d_nm->mkConst(BitVector(2,unsigned(0)));
-    one = d_nm->mkConst(BitVector(2,unsigned(1)));
-    Node two = d_nm->mkConst(BitVector(2,unsigned(2)));
-    Node three = d_nm->mkConst(BitVector(2,unsigned(3)));
-    storeAll = d_nm->mkConst(ArrayStoreAll(arrType, one));
-    TS_ASSERT(storeAll.isConst());
-
-    arr = d_nm->mkNode(STORE, storeAll, zero, zero);
-    TS_ASSERT(arr.isConst());
-    arr2 = d_nm->mkNode(STORE, arr, one, zero);
-    TS_ASSERT(!arr2.isConst());
-    arr2 = Rewriter::rewrite(arr2);
-    TS_ASSERT(arr2.isConst());
-
-    arr = d_nm->mkNode(STORE, storeAll, one, three);
-    TS_ASSERT(arr.isConst());
-    arr2 = d_nm->mkNode(STORE, arr, one, one);
-    TS_ASSERT(!arr2.isConst());
-    arr2 = Rewriter::rewrite(arr2);
-    TS_ASSERT(arr2 == storeAll);
-
-    arr2 = d_nm->mkNode(STORE, arr, zero, zero);
-    TS_ASSERT(!arr2.isConst());
-    TS_ASSERT(Rewriter::rewrite(arr2).isConst());
-    arr2 = d_nm->mkNode(STORE, arr2, two, two);
-    TS_ASSERT(!arr2.isConst());
-    TS_ASSERT(Rewriter::rewrite(arr2).isConst());
-    arr2 = d_nm->mkNode(STORE, arr2, three, one);
-    TS_ASSERT(!arr2.isConst());
-    TS_ASSERT(Rewriter::rewrite(arr2).isConst());
-    arr2 = d_nm->mkNode(STORE, arr2, three, three);
-    TS_ASSERT(!arr2.isConst());
-    TS_ASSERT(Rewriter::rewrite(arr2).isConst());
-    arr2 = d_nm->mkNode(STORE, arr2, two, zero);
-    TS_ASSERT(!arr2.isConst());
-    arr2 = Rewriter::rewrite(arr2);
-    TS_ASSERT(arr2.isConst());
-
-  }
-
- private:
-  api::Solver* d_slv;
-  ExprManager* d_em;
-  SmtEngine* d_smt;
-  NodeManager* d_nm;
-  SmtScope* d_scope;
-};