New C++ API: Clean up usage of internal types in Op. (#6045)

This disables the temporarily available internals of Op.

7 files changed, 181 insertions, 20 deletions

diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 3123607c7..ba4ee31e7 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -14,7 +14,10 @@
 cvc4_add_unit_test_black(datatype_api_black api)
 cvc4_add_unit_test_black(grammar_black api)
 cvc4_add_unit_test_black(op_black api)
+cvc4_add_unit_test_white(op_white api)
 cvc4_add_unit_test_black(result_black api)
 cvc4_add_unit_test_black(solver_black api)
+cvc4_add_unit_test_white(solver_white api)
 cvc4_add_unit_test_black(sort_black api)
 cvc4_add_unit_test_black(term_black api)
+cvc4_add_unit_test_white(term_white api)
diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp
index 19bd4bb03..379d16850 100644
--- a/test/unit/api/op_black.cpp
+++ b/test/unit/api/op_black.cpp
@@ -9,7 +9,7 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of the Term class
+ ** \brief Black box testing of the Op class.
  **/
 
 #include "test_api.h"
@@ -41,12 +41,7 @@ TEST_F(TestApiBlackOp, isNull)
 
 TEST_F(TestApiBlackOp, opFromKind)
 {
-  Op plus(&d_solver, PLUS);
-  ASSERT_FALSE(plus.isIndexed());
-  ASSERT_THROW(plus.getIndices<uint32_t>(), CVC4ApiException);
-
   ASSERT_NO_THROW(d_solver.mkOp(PLUS));
-  ASSERT_EQ(plus, d_solver.mkOp(PLUS));
   ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT), CVC4ApiException);
 }
 
diff --git a/test/unit/api/op_white.cpp b/test/unit/api/op_white.cpp
new file mode 100644
index 000000000..6f1ff549f
--- /dev/null
+++ b/test/unit/api/op_white.cpp
@@ -0,0 +1,35 @@
+/*********************                                                        */
+/*! \file op_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 White box testing of the Op class.
+ **/
+
+#include "test_api.h"
+
+namespace CVC4 {
+
+using namespace api;
+
+namespace test {
+
+class TestApiWhiteOp : public TestApi
+{
+};
+
+TEST_F(TestApiWhiteOp, opFromKind)
+{
+  Op plus(&d_solver, PLUS);
+  ASSERT_FALSE(plus.isIndexed());
+  ASSERT_THROW(plus.getIndices<uint32_t>(), CVC4ApiException);
+  ASSERT_EQ(plus, d_solver.mkOp(PLUS));
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 528d697ae..8e67d1287 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1328,13 +1328,8 @@ TEST_F(TestApiBlackSolver, getOp)
   Term listhead = d_solver.mkTerm(APPLY_SELECTOR, headTerm, listcons1);
 
   ASSERT_TRUE(listnil.hasOp());
-  ASSERT_EQ(listnil.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
-
   ASSERT_TRUE(listcons1.hasOp());
-  ASSERT_EQ(listcons1.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
-
   ASSERT_TRUE(listhead.hasOp());
-  ASSERT_EQ(listhead.getOp(), Op(&d_solver, APPLY_SELECTOR));
 }
 
 TEST_F(TestApiBlackSolver, getOption)
diff --git a/test/unit/api/solver_white.cpp b/test/unit/api/solver_white.cpp
new file mode 100644
index 000000000..e360bb2d0
--- /dev/null
+++ b/test/unit/api/solver_white.cpp
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file solver_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 Solver class of the  C++ API.
+ **
+ ** Black box testing of the Solver class of the  C++ API.
+ **/
+
+#include "base/configuration.h"
+#include "test_api.h"
+
+namespace CVC4 {
+
+using namespace api;
+
+namespace test {
+
+class TestApiWhiteSolver : public TestApi
+{
+};
+
+TEST_F(TestApiWhiteSolver, getOp)
+{
+  DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+  cons.addSelector("head", d_solver.getIntegerSort());
+  cons.addSelectorSelf("tail");
+  consListSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+  consListSpec.addConstructor(nil);
+  Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
+  Datatype consList = consListSort.getDatatype();
+
+  Term nilTerm = consList.getConstructorTerm("nil");
+  Term consTerm = consList.getConstructorTerm("cons");
+  Term headTerm = consList["cons"].getSelectorTerm("head");
+
+  Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm);
+  Term listcons1 = d_solver.mkTerm(
+      APPLY_CONSTRUCTOR, consTerm, d_solver.mkInteger(1), listnil);
+  Term listhead = d_solver.mkTerm(APPLY_SELECTOR, headTerm, listcons1);
+
+  ASSERT_EQ(listnil.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+  ASSERT_EQ(listcons1.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+  ASSERT_EQ(listhead.getOp(), Op(&d_solver, APPLY_SELECTOR));
+}
+
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index d43734295..21906f8ed 100644
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/term_black.cpp
@@ -9,7 +9,7 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of the Term class
+ ** \brief Black box testing of the Term class.
  **/
 
 #include "test_api.h"
@@ -158,10 +158,8 @@ TEST_F(TestApiBlackTerm, getOp)
   Term extb = d_solver.mkTerm(ext, b);
 
   ASSERT_TRUE(ab.hasOp());
-  ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT));
   ASSERT_FALSE(ab.getOp().isIndexed());
   // can compare directly to a Kind (will invoke Op constructor)
-  ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT));
   ASSERT_TRUE(extb.hasOp());
   ASSERT_TRUE(extb.getOp().isIndexed());
   ASSERT_EQ(extb.getOp(), ext);
@@ -172,7 +170,6 @@ TEST_F(TestApiBlackTerm, getOp)
   ASSERT_FALSE(f.hasOp());
   ASSERT_THROW(f.getOp(), CVC4ApiException);
   ASSERT_TRUE(fx.hasOp());
-  ASSERT_EQ(fx.getOp(), Op(&d_solver, APPLY_UF));
   std::vector<Term> children(fx.begin(), fx.end());
   // testing rebuild from op and children
   ASSERT_EQ(fx, d_solver.mkTerm(fx.getOp(), children));
@@ -208,11 +205,6 @@ TEST_F(TestApiBlackTerm, getOp)
   ASSERT_TRUE(headTerm.hasOp());
   ASSERT_TRUE(tailTerm.hasOp());
 
-  ASSERT_EQ(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
-  ASSERT_EQ(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
-  ASSERT_EQ(headTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
-  ASSERT_EQ(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
-
   // Test rebuilding
   children.clear();
   children.insert(children.begin(), headTerm.begin(), headTerm.end());
diff --git a/test/unit/api/term_white.cpp b/test/unit/api/term_white.cpp
new file mode 100644
index 000000000..da1557024
--- /dev/null
+++ b/test/unit/api/term_white.cpp
@@ -0,0 +1,84 @@
+/*********************                                                        */
+/*! \file term_white.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 White box testing of the Term class.
+ **/
+
+#include "test_api.h"
+
+namespace CVC4 {
+
+using namespace api;
+
+namespace test {
+
+class TestApiWhiteTerm : public TestApi
+{
+};
+
+TEST_F(TestApiWhiteTerm, getOp)
+{
+  Sort intsort = d_solver.getIntegerSort();
+  Sort bvsort = d_solver.mkBitVectorSort(8);
+  Sort arrsort = d_solver.mkArraySort(bvsort, intsort);
+  Sort funsort = d_solver.mkFunctionSort(intsort, bvsort);
+
+  Term x = d_solver.mkConst(intsort, "x");
+  Term a = d_solver.mkConst(arrsort, "a");
+  Term b = d_solver.mkConst(bvsort, "b");
+
+  Term ab = d_solver.mkTerm(SELECT, a, b);
+  Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
+  Term extb = d_solver.mkTerm(ext, b);
+
+  ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT));
+  // can compare directly to a Kind (will invoke Op constructor)
+  ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT));
+
+  Term f = d_solver.mkConst(funsort, "f");
+  Term fx = d_solver.mkTerm(APPLY_UF, f, x);
+
+  ASSERT_EQ(fx.getOp(), Op(&d_solver, APPLY_UF));
+  // testing rebuild from op and children
+
+  // Test Datatypes Ops
+  Sort sort = d_solver.mkParamSort("T");
+  DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+  cons.addSelector("head", sort);
+  cons.addSelectorSelf("tail");
+  listDecl.addConstructor(cons);
+  listDecl.addConstructor(nil);
+  Sort listSort = d_solver.mkDatatypeSort(listDecl);
+  Sort intListSort =
+      listSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()});
+  Term c = d_solver.mkConst(intListSort, "c");
+  Datatype list = listSort.getDatatype();
+  // list datatype constructor and selector operator terms
+  Term consOpTerm = list.getConstructorTerm("cons");
+  Term nilOpTerm = list.getConstructorTerm("nil");
+  Term headOpTerm = list["cons"].getSelectorTerm("head");
+  Term tailOpTerm = list["cons"].getSelectorTerm("tail");
+
+  Term nilTerm = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilOpTerm);
+  Term consTerm = d_solver.mkTerm(
+      APPLY_CONSTRUCTOR, consOpTerm, d_solver.mkInteger(0), nilTerm);
+  Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm);
+  Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm);
+
+  ASSERT_EQ(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+  ASSERT_EQ(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+  ASSERT_EQ(headTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
+  ASSERT_EQ(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
+}
+}  // namespace test
+}  // namespace CVC4