1 files changed, 85 insertions, 0 deletions
diff --git a/test/unit/api/cpp/term_white.cpp b/test/unit/api/cpp/term_white.cpp
new file mode 100644
index 000000000..ace5645dc
--- /dev/null
+++ b/test/unit/api/cpp/term_white.cpp
@@ -0,0 +1,85 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Makai Mann, Aina Niemetz, Andrew Reynolds
+ *
+ * This file is part of the cvc5 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.
+ * ****************************************************************************
+ *
+ * White box testing of the Term class.
+ */
+
+#include "test_api.h"
+
+namespace cvc5 {
+
+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 cvc5