New C++ API: Split unit tests. (#2688)

4 files changed, 511 insertions, 474 deletions

diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 025575e41..eeab46f99 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -1,5 +1,6 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(api_guards_black api)
+cvc4_add_unit_test_black(solver_black api)
+cvc4_add_unit_test_black(sort_black api)
 cvc4_add_unit_test_black(term_black api)
diff --git a/test/unit/api/api_guards_black.h b/test/unit/api/api_guards_black.h
deleted file mode 100644
index 777ce81f1..000000000
--- a/test/unit/api/api_guards_black.h
+++ /dev/null
@@ -1,473 +0,0 @@
-/*********************                                                        */
-/*! \file api_guards_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 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 guards of the C++ API functions.
- **
- ** Black box testing of the guards of the C++ API functions.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "api/cvc4cpp.h"
-
-using namespace CVC4::api;
-
-class ApiGuardsBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() override;
-  void tearDown() override;
-
-  void testSolverMkBitVectorSort();
-  void testSolverMkFloatingPointSort();
-  void testSolverMkDatatypeSort();
-  void testSolverMkFunctionSort();
-  void testSolverMkPredicateSort();
-  void testSolverMkTupleSort();
-  void testSortGetDatatype();
-  void testSortInstantiate();
-  void testSortGetFunctionArity();
-  void testSortGetFunctionDomainSorts();
-  void testSortGetFunctionCodomainSort();
-  void testSortGetArrayIndexSort();
-  void testSortGetArrayElementSort();
-  void testSortGetSetElementSort();
-  void testSortGetUninterpretedSortName();
-  void testSortIsUninterpretedSortParameterized();
-  void testSortGetUninterpretedSortParamSorts();
-  void testSortGetUninterpretedSortConstructorName();
-  void testSortGetUninterpretedSortConstructorArity();
-  void testSortGetBVSize();
-  void testSortGetFPExponentSize();
-  void testSortGetFPSignificandSize();
-  void testSortGetDatatypeParamSorts();
-  void testSortGetDatatypeArity();
-  void testSortGetTupleLength();
-  void testSortGetTupleSorts();
-  void testSolverDeclareFun();
-  void testSolverDefineFun();
-  void testSolverDefineFunRec();
-  void testSolverDefineFunsRec();
-
- private:
-  Solver d_solver;
-};
-
-void ApiGuardsBlack::setUp() {}
-
-void ApiGuardsBlack::tearDown() {}
-
-void ApiGuardsBlack::testSolverMkBitVectorSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVectorSort(32));
-  TS_ASSERT_THROWS(d_solver.mkBitVectorSort(0), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverMkFloatingPointSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkFloatingPointSort(4, 8));
-  TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(0, 8), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(4, 0), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverMkDatatypeSort()
-{
-  DatatypeDecl dtypeSpec("list");
-  DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
-  cons.addSelector(head);
-  dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
-  dtypeSpec.addConstructor(nil);
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkDatatypeSort(dtypeSpec));
-  DatatypeDecl throwsDtypeSpec("list");
-  TS_ASSERT_THROWS(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverMkFunctionSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort(
-      d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()));
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                         d_solver.getIntegerSort());
-  TS_ASSERT_THROWS(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort(
-      {d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()},
-      d_solver.getIntegerSort()));
-  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                          d_solver.getIntegerSort());
-  TS_ASSERT_THROWS(
-      d_solver.mkFunctionSort({funSort2, d_solver.mkUninterpretedSort("u")},
-                              d_solver.getIntegerSort()),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.mkFunctionSort({d_solver.getIntegerSort(),
-                                            d_solver.mkUninterpretedSort("u")},
-                                           funSort2),
-                   CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverMkPredicateSort()
-{
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver.mkPredicateSort({d_solver.getIntegerSort()}));
-  TS_ASSERT_THROWS(d_solver.mkPredicateSort({}), CVC4ApiException&);
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                         d_solver.getIntegerSort());
-  TS_ASSERT_THROWS(
-      d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort}),
-      CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverMkTupleSort()
-{
-  TS_ASSERT_THROWS_NOTHING(d_solver.mkTupleSort({d_solver.getIntegerSort()}));
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                         d_solver.getIntegerSort());
-  TS_ASSERT_THROWS(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}),
-                   CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetDatatype()
-{
-  // create datatype sort, check should not fail
-  DatatypeDecl dtypeSpec("list");
-  DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
-  cons.addSelector(head);
-  dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
-  dtypeSpec.addConstructor(nil);
-  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
-  TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatype());
-  // create bv sort, check should fail
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getDatatype(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortInstantiate()
-{
-  // instantiate parametric datatype, check should not fail
-  Sort sort = d_solver.mkParamSort("T");
-  DatatypeDecl paramDtypeSpec("paramlist", sort);
-  DatatypeConstructorDecl paramCons("cons");
-  DatatypeConstructorDecl paramNil("nil");
-  DatatypeSelectorDecl paramHead("head", sort);
-  paramCons.addSelector(paramHead);
-  paramDtypeSpec.addConstructor(paramCons);
-  paramDtypeSpec.addConstructor(paramNil);
-  Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec);
-  TS_ASSERT_THROWS_NOTHING(
-      paramDtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}));
-  // instantiate non-parametric datatype sort, check should fail
-  DatatypeDecl dtypeSpec("list");
-  DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
-  cons.addSelector(head);
-  dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
-  dtypeSpec.addConstructor(nil);
-  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
-  TS_ASSERT_THROWS(
-      dtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}),
-      CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetFunctionArity()
-{
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                         d_solver.getIntegerSort());
-  TS_ASSERT_THROWS_NOTHING(funSort.getFunctionArity());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getFunctionArity(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetFunctionDomainSorts()
-{
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                         d_solver.getIntegerSort());
-  TS_ASSERT_THROWS_NOTHING(funSort.getFunctionDomainSorts());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getFunctionDomainSorts(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetFunctionCodomainSort()
-{
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                         d_solver.getIntegerSort());
-  TS_ASSERT_THROWS_NOTHING(funSort.getFunctionCodomainSort());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getFunctionCodomainSort(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetArrayIndexSort()
-{
-  Sort elementSort = d_solver.mkBitVectorSort(32);
-  Sort indexSort = d_solver.mkBitVectorSort(32);
-  Sort arraySort = d_solver.mkArraySort(indexSort, elementSort);
-  TS_ASSERT_THROWS_NOTHING(arraySort.getArrayIndexSort());
-  TS_ASSERT_THROWS(indexSort.getArrayIndexSort(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetArrayElementSort()
-{
-  Sort elementSort = d_solver.mkBitVectorSort(32);
-  Sort indexSort = d_solver.mkBitVectorSort(32);
-  Sort arraySort = d_solver.mkArraySort(indexSort, elementSort);
-  TS_ASSERT_THROWS_NOTHING(arraySort.getArrayElementSort());
-  TS_ASSERT_THROWS(indexSort.getArrayElementSort(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetSetElementSort()
-{
-  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-  TS_ASSERT_THROWS_NOTHING(setSort.getSetElementSort());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getSetElementSort(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetUninterpretedSortName()
-{
-  Sort uSort = d_solver.mkUninterpretedSort("u");
-  TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortName());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getUninterpretedSortName(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortIsUninterpretedSortParameterized()
-{
-  Sort uSort = d_solver.mkUninterpretedSort("u");
-  TS_ASSERT_THROWS_NOTHING(uSort.isUninterpretedSortParameterized());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.isUninterpretedSortParameterized(),
-                   CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetUninterpretedSortParamSorts()
-{
-  Sort uSort = d_solver.mkUninterpretedSort("u");
-  TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortParamSorts());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetUninterpretedSortConstructorName()
-{
-  Sort sSort = d_solver.mkSortConstructorSort("s", 2);
-  TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorName());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getSortConstructorName(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetUninterpretedSortConstructorArity()
-{
-  Sort sSort = d_solver.mkSortConstructorSort("s", 2);
-  TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorArity());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getSortConstructorArity(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetBVSize()
-{
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS_NOTHING(bvSort.getBVSize());
-  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-  TS_ASSERT_THROWS(setSort.getBVSize(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetFPExponentSize()
-{
-  Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
-  TS_ASSERT_THROWS_NOTHING(fpSort.getFPExponentSize());
-  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-  TS_ASSERT_THROWS(setSort.getFPExponentSize(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetFPSignificandSize()
-{
-  Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
-  TS_ASSERT_THROWS_NOTHING(fpSort.getFPSignificandSize());
-  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-  TS_ASSERT_THROWS(setSort.getFPSignificandSize(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetDatatypeParamSorts()
-{
-  // create parametric datatype, check should not fail
-  Sort sort = d_solver.mkParamSort("T");
-  DatatypeDecl paramDtypeSpec("paramlist", sort);
-  DatatypeConstructorDecl paramCons("cons");
-  DatatypeConstructorDecl paramNil("nil");
-  DatatypeSelectorDecl paramHead("head", sort);
-  paramCons.addSelector(paramHead);
-  paramDtypeSpec.addConstructor(paramCons);
-  paramDtypeSpec.addConstructor(paramNil);
-  Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec);
-  TS_ASSERT_THROWS_NOTHING(paramDtypeSort.getDatatypeParamSorts());
-  // create non-parametric datatype sort, check should fail
-  DatatypeDecl dtypeSpec("list");
-  DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
-  cons.addSelector(head);
-  dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
-  dtypeSpec.addConstructor(nil);
-  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
-  TS_ASSERT_THROWS(dtypeSort.getDatatypeParamSorts(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetDatatypeArity()
-{
-  // create datatype sort, check should not fail
-  DatatypeDecl dtypeSpec("list");
-  DatatypeConstructorDecl cons("cons");
-  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
-  cons.addSelector(head);
-  dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
-  dtypeSpec.addConstructor(nil);
-  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
-  TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatypeArity());
-  // create bv sort, check should fail
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getDatatypeArity(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetTupleLength()
-{
-  Sort tupleSort = d_solver.mkTupleSort(
-      {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
-  TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleLength());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getTupleLength(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSortGetTupleSorts()
-{
-  Sort tupleSort = d_solver.mkTupleSort(
-      {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
-  TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleSorts());
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  TS_ASSERT_THROWS(bvSort.getTupleSorts(), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverDeclareFun()
-{
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                         d_solver.getIntegerSort());
-  TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f1", bvSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f2", funSort));
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort));
-  TS_ASSERT_THROWS(d_solver.declareFun("f4", {bvSort, funSort}, bvSort),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.declareFun("f5", {bvSort, bvSort}, funSort),
-                   CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverDefineFun()
-{
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
-  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                          d_solver.getIntegerSort());
-  Term b1 = d_solver.mkBoundVar("b1", bvSort);
-  Term b11 = d_solver.mkBoundVar("b1", bvSort);
-  Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort());
-  Term b3 = d_solver.mkBoundVar("b3", funSort2);
-  Term v1 = d_solver.mkBoundVar("v1", bvSort);
-  Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort());
-  Term v3 = d_solver.mkVar("v3", funSort2);
-  Term f1 = d_solver.declareFun("f1", funSort1);
-  Term f2 = d_solver.declareFun("f2", funSort2);
-  Term f3 = d_solver.declareFun("f3", bvSort);
-  TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("f", {}, bvSort, v1));
-  TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("ff", {b1, b2}, bvSort, v1));
-  TS_ASSERT_THROWS_NOTHING(d_solver.defineFun(f1, {b1, b11}, v1));
-  TS_ASSERT_THROWS(d_solver.defineFun("fff", {b1}, bvSort, v3),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFun("ffff", {b1}, funSort2, v3),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1}, v1), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v3), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFun(f2, {b1}, v2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFun(f3, {b1}, v1), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverDefineFunRec()
-{
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
-  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
-                                          d_solver.getIntegerSort());
-  Term b1 = d_solver.mkBoundVar("b1", bvSort);
-  Term b11 = d_solver.mkBoundVar("b1", bvSort);
-  Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort());
-  Term b3 = d_solver.mkBoundVar("b3", funSort2);
-  Term v1 = d_solver.mkBoundVar("v1", bvSort);
-  Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort());
-  Term v3 = d_solver.mkVar("v3", funSort2);
-  Term f1 = d_solver.declareFun("f1", funSort1);
-  Term f2 = d_solver.declareFun("f2", funSort2);
-  Term f3 = d_solver.declareFun("f3", bvSort);
-  TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("f", {}, bvSort, v1));
-  TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("ff", {b1, b2}, bvSort, v1));
-  TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec(f1, {b1, b11}, v1));
-  TS_ASSERT_THROWS(d_solver.defineFunRec("fff", {b1}, bvSort, v3),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunRec("ffff", {b1}, funSort2, v3),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1}, v1), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunRec(f2, {b1}, v2), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunRec(f3, {b1}, v1), CVC4ApiException&);
-}
-
-void ApiGuardsBlack::testSolverDefineFunsRec()
-{
-  Sort uSort = d_solver.mkUninterpretedSort("u");
-  Sort bvSort = d_solver.mkBitVectorSort(32);
-  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
-  Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
-  Term b1 = d_solver.mkBoundVar("b1", bvSort);
-  Term b11 = d_solver.mkBoundVar("b1", bvSort);
-  Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort());
-  Term b3 = d_solver.mkBoundVar("b3", funSort2);
-  Term b4 = d_solver.mkBoundVar("b4", uSort);
-  Term v1 = d_solver.mkBoundVar("v1", bvSort);
-  Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort());
-  Term v3 = d_solver.mkVar("v3", funSort2);
-  Term v4 = d_solver.mkVar("v4", uSort);
-  Term f1 = d_solver.declareFun("f1", funSort1);
-  Term f2 = d_solver.declareFun("f2", funSort2);
-  Term f3 = d_solver.declareFun("f3", bvSort);
-  TS_ASSERT_THROWS_NOTHING(
-      d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2}));
-  TS_ASSERT_THROWS(
-      d_solver.defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}),
-      CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}),
-                   CVC4ApiException&);
-  TS_ASSERT_THROWS(
-      d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}),
-      CVC4ApiException&);
-}
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
new file mode 100644
index 000000000..538899a0f
--- /dev/null
+++ b/test/unit/api/solver_black.h
@@ -0,0 +1,230 @@
+/*********************                                                        */
+/*! \file api_guards_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 guards of the C++ API functions.
+ **
+ ** Black box testing of the guards of the C++ API functions.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+
+class SolverBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() override;
+  void tearDown() override;
+
+  void testMkBitVectorSort();
+  void testMkFloatingPointSort();
+  void testMkDatatypeSort();
+  void testMkFunctionSort();
+  void testMkPredicateSort();
+  void testMkTupleSort();
+  void testDeclareFun();
+  void testDefineFun();
+  void testDefineFunRec();
+  void testDefineFunsRec();
+
+ private:
+  Solver d_solver;
+};
+
+void SolverBlack::setUp() {}
+
+void SolverBlack::tearDown() {}
+
+void SolverBlack::testMkBitVectorSort()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVectorSort(32));
+  TS_ASSERT_THROWS(d_solver.mkBitVectorSort(0), CVC4ApiException&);
+}
+
+void SolverBlack::testMkFloatingPointSort()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkFloatingPointSort(4, 8));
+  TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(0, 8), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(4, 0), CVC4ApiException&);
+}
+
+void SolverBlack::testMkDatatypeSort()
+{
+  DatatypeDecl dtypeSpec("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
+  cons.addSelector(head);
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  dtypeSpec.addConstructor(nil);
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkDatatypeSort(dtypeSpec));
+  DatatypeDecl throwsDtypeSpec("list");
+  TS_ASSERT_THROWS(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException&);
+}
+
+void SolverBlack::testMkFunctionSort()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort(
+      d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()));
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  TS_ASSERT_THROWS(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort(
+      {d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()},
+      d_solver.getIntegerSort()));
+  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                          d_solver.getIntegerSort());
+  TS_ASSERT_THROWS(
+      d_solver.mkFunctionSort({funSort2, d_solver.mkUninterpretedSort("u")},
+                              d_solver.getIntegerSort()),
+      CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.mkFunctionSort({d_solver.getIntegerSort(),
+                                            d_solver.mkUninterpretedSort("u")},
+                                           funSort2),
+                   CVC4ApiException&);
+}
+
+void SolverBlack::testMkPredicateSort()
+{
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver.mkPredicateSort({d_solver.getIntegerSort()}));
+  TS_ASSERT_THROWS(d_solver.mkPredicateSort({}), CVC4ApiException&);
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  TS_ASSERT_THROWS(
+      d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort}),
+      CVC4ApiException&);
+}
+
+void SolverBlack::testMkTupleSort()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver.mkTupleSort({d_solver.getIntegerSort()}));
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  TS_ASSERT_THROWS(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}),
+                   CVC4ApiException&);
+}
+
+void SolverBlack::testDeclareFun()
+{
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f1", bvSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f2", funSort));
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort));
+  TS_ASSERT_THROWS(d_solver.declareFun("f4", {bvSort, funSort}, bvSort),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.declareFun("f5", {bvSort, bvSort}, funSort),
+                   CVC4ApiException&);
+}
+
+void SolverBlack::testDefineFun()
+{
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
+  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                          d_solver.getIntegerSort());
+  Term b1 = d_solver.mkBoundVar("b1", bvSort);
+  Term b11 = d_solver.mkBoundVar("b1", bvSort);
+  Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort());
+  Term b3 = d_solver.mkBoundVar("b3", funSort2);
+  Term v1 = d_solver.mkBoundVar("v1", bvSort);
+  Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort());
+  Term v3 = d_solver.mkVar("v3", funSort2);
+  Term f1 = d_solver.declareFun("f1", funSort1);
+  Term f2 = d_solver.declareFun("f2", funSort2);
+  Term f3 = d_solver.declareFun("f3", bvSort);
+  TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("f", {}, bvSort, v1));
+  TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("ff", {b1, b2}, bvSort, v1));
+  TS_ASSERT_THROWS_NOTHING(d_solver.defineFun(f1, {b1, b11}, v1));
+  TS_ASSERT_THROWS(d_solver.defineFun("fff", {b1}, bvSort, v3),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFun("ffff", {b1}, funSort2, v3),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1}, v1), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v2), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v3), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFun(f2, {b1}, v2), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFun(f3, {b1}, v1), CVC4ApiException&);
+}
+
+void SolverBlack::testDefineFunRec()
+{
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
+  Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                          d_solver.getIntegerSort());
+  Term b1 = d_solver.mkBoundVar("b1", bvSort);
+  Term b11 = d_solver.mkBoundVar("b1", bvSort);
+  Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort());
+  Term b3 = d_solver.mkBoundVar("b3", funSort2);
+  Term v1 = d_solver.mkBoundVar("v1", bvSort);
+  Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort());
+  Term v3 = d_solver.mkVar("v3", funSort2);
+  Term f1 = d_solver.declareFun("f1", funSort1);
+  Term f2 = d_solver.declareFun("f2", funSort2);
+  Term f3 = d_solver.declareFun("f3", bvSort);
+  TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("f", {}, bvSort, v1));
+  TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("ff", {b1, b2}, bvSort, v1));
+  TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec(f1, {b1, b11}, v1));
+  TS_ASSERT_THROWS(d_solver.defineFunRec("fff", {b1}, bvSort, v3),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunRec("ffff", {b1}, funSort2, v3),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1}, v1), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunRec(f2, {b1}, v2), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunRec(f3, {b1}, v1), CVC4ApiException&);
+}
+
+void SolverBlack::testDefineFunsRec()
+{
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
+  Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
+  Term b1 = d_solver.mkBoundVar("b1", bvSort);
+  Term b11 = d_solver.mkBoundVar("b1", bvSort);
+  Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort());
+  Term b3 = d_solver.mkBoundVar("b3", funSort2);
+  Term b4 = d_solver.mkBoundVar("b4", uSort);
+  Term v1 = d_solver.mkBoundVar("v1", bvSort);
+  Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort());
+  Term v3 = d_solver.mkVar("v3", funSort2);
+  Term v4 = d_solver.mkVar("v4", uSort);
+  Term f1 = d_solver.declareFun("f1", funSort1);
+  Term f2 = d_solver.declareFun("f2", funSort2);
+  Term f3 = d_solver.declareFun("f3", bvSort);
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2}));
+  TS_ASSERT_THROWS(
+      d_solver.defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}),
+      CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}),
+      CVC4ApiException&);
+}
diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h
new file mode 100644
index 000000000..d9337e627
--- /dev/null
+++ b/test/unit/api/sort_black.h
@@ -0,0 +1,279 @@
+/*********************                                                        */
+/*! \file api_guards_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 guards of the C++ API functions.
+ **
+ ** Black box testing of the guards of the C++ API functions.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+
+class SortBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() override;
+  void tearDown() override;
+
+  void testGetDatatype();
+  void testInstantiate();
+  void testGetFunctionArity();
+  void testGetFunctionDomainSorts();
+  void testGetFunctionCodomainSort();
+  void testGetArrayIndexSort();
+  void testGetArrayElementSort();
+  void testGetSetElementSort();
+  void testGetUninterpretedSortName();
+  void testIsUninterpretedSortParameterized();
+  void testGetUninterpretedSortParamSorts();
+  void testGetUninterpretedSortConstructorName();
+  void testGetUninterpretedSortConstructorArity();
+  void testGetBVSize();
+  void testGetFPExponentSize();
+  void testGetFPSignificandSize();
+  void testGetDatatypeParamSorts();
+  void testGetDatatypeArity();
+  void testGetTupleLength();
+  void testGetTupleSorts();
+
+ private:
+  Solver d_solver;
+};
+
+void SortBlack::setUp() {}
+
+void SortBlack::tearDown() {}
+
+void SortBlack::testGetDatatype()
+{
+  // create datatype sort, check should not fail
+  DatatypeDecl dtypeSpec("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
+  cons.addSelector(head);
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  dtypeSpec.addConstructor(nil);
+  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
+  TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatype());
+  // create bv sort, check should fail
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getDatatype(), CVC4ApiException&);
+}
+
+void SortBlack::testInstantiate()
+{
+  // instantiate parametric datatype, check should not fail
+  Sort sort = d_solver.mkParamSort("T");
+  DatatypeDecl paramDtypeSpec("paramlist", sort);
+  DatatypeConstructorDecl paramCons("cons");
+  DatatypeConstructorDecl paramNil("nil");
+  DatatypeSelectorDecl paramHead("head", sort);
+  paramCons.addSelector(paramHead);
+  paramDtypeSpec.addConstructor(paramCons);
+  paramDtypeSpec.addConstructor(paramNil);
+  Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec);
+  TS_ASSERT_THROWS_NOTHING(
+      paramDtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}));
+  // instantiate non-parametric datatype sort, check should fail
+  DatatypeDecl dtypeSpec("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
+  cons.addSelector(head);
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  dtypeSpec.addConstructor(nil);
+  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
+  TS_ASSERT_THROWS(
+      dtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}),
+      CVC4ApiException&);
+}
+
+void SortBlack::testGetFunctionArity()
+{
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  TS_ASSERT_THROWS_NOTHING(funSort.getFunctionArity());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getFunctionArity(), CVC4ApiException&);
+}
+
+void SortBlack::testGetFunctionDomainSorts()
+{
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  TS_ASSERT_THROWS_NOTHING(funSort.getFunctionDomainSorts());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getFunctionDomainSorts(), CVC4ApiException&);
+}
+
+void SortBlack::testGetFunctionCodomainSort()
+{
+  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+                                         d_solver.getIntegerSort());
+  TS_ASSERT_THROWS_NOTHING(funSort.getFunctionCodomainSort());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getFunctionCodomainSort(), CVC4ApiException&);
+}
+
+void SortBlack::testGetArrayIndexSort()
+{
+  Sort elementSort = d_solver.mkBitVectorSort(32);
+  Sort indexSort = d_solver.mkBitVectorSort(32);
+  Sort arraySort = d_solver.mkArraySort(indexSort, elementSort);
+  TS_ASSERT_THROWS_NOTHING(arraySort.getArrayIndexSort());
+  TS_ASSERT_THROWS(indexSort.getArrayIndexSort(), CVC4ApiException&);
+}
+
+void SortBlack::testGetArrayElementSort()
+{
+  Sort elementSort = d_solver.mkBitVectorSort(32);
+  Sort indexSort = d_solver.mkBitVectorSort(32);
+  Sort arraySort = d_solver.mkArraySort(indexSort, elementSort);
+  TS_ASSERT_THROWS_NOTHING(arraySort.getArrayElementSort());
+  TS_ASSERT_THROWS(indexSort.getArrayElementSort(), CVC4ApiException&);
+}
+
+void SortBlack::testGetSetElementSort()
+{
+  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+  TS_ASSERT_THROWS_NOTHING(setSort.getSetElementSort());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getSetElementSort(), CVC4ApiException&);
+}
+
+void SortBlack::testGetUninterpretedSortName()
+{
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortName());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getUninterpretedSortName(), CVC4ApiException&);
+}
+
+void SortBlack::testIsUninterpretedSortParameterized()
+{
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  TS_ASSERT_THROWS_NOTHING(uSort.isUninterpretedSortParameterized());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.isUninterpretedSortParameterized(),
+                   CVC4ApiException&);
+}
+
+void SortBlack::testGetUninterpretedSortParamSorts()
+{
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortParamSorts());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException&);
+}
+
+void SortBlack::testGetUninterpretedSortConstructorName()
+{
+  Sort sSort = d_solver.mkSortConstructorSort("s", 2);
+  TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorName());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getSortConstructorName(), CVC4ApiException&);
+}
+
+void SortBlack::testGetUninterpretedSortConstructorArity()
+{
+  Sort sSort = d_solver.mkSortConstructorSort("s", 2);
+  TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorArity());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getSortConstructorArity(), CVC4ApiException&);
+}
+
+void SortBlack::testGetBVSize()
+{
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS_NOTHING(bvSort.getBVSize());
+  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+  TS_ASSERT_THROWS(setSort.getBVSize(), CVC4ApiException&);
+}
+
+void SortBlack::testGetFPExponentSize()
+{
+  Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
+  TS_ASSERT_THROWS_NOTHING(fpSort.getFPExponentSize());
+  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+  TS_ASSERT_THROWS(setSort.getFPExponentSize(), CVC4ApiException&);
+}
+
+void SortBlack::testGetFPSignificandSize()
+{
+  Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
+  TS_ASSERT_THROWS_NOTHING(fpSort.getFPSignificandSize());
+  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+  TS_ASSERT_THROWS(setSort.getFPSignificandSize(), CVC4ApiException&);
+}
+
+void SortBlack::testGetDatatypeParamSorts()
+{
+  // create parametric datatype, check should not fail
+  Sort sort = d_solver.mkParamSort("T");
+  DatatypeDecl paramDtypeSpec("paramlist", sort);
+  DatatypeConstructorDecl paramCons("cons");
+  DatatypeConstructorDecl paramNil("nil");
+  DatatypeSelectorDecl paramHead("head", sort);
+  paramCons.addSelector(paramHead);
+  paramDtypeSpec.addConstructor(paramCons);
+  paramDtypeSpec.addConstructor(paramNil);
+  Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec);
+  TS_ASSERT_THROWS_NOTHING(paramDtypeSort.getDatatypeParamSorts());
+  // create non-parametric datatype sort, check should fail
+  DatatypeDecl dtypeSpec("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
+  cons.addSelector(head);
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  dtypeSpec.addConstructor(nil);
+  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
+  TS_ASSERT_THROWS(dtypeSort.getDatatypeParamSorts(), CVC4ApiException&);
+}
+
+void SortBlack::testGetDatatypeArity()
+{
+  // create datatype sort, check should not fail
+  DatatypeDecl dtypeSpec("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", d_solver.getIntegerSort());
+  cons.addSelector(head);
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  dtypeSpec.addConstructor(nil);
+  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
+  TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatypeArity());
+  // create bv sort, check should fail
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getDatatypeArity(), CVC4ApiException&);
+}
+
+void SortBlack::testGetTupleLength()
+{
+  Sort tupleSort = d_solver.mkTupleSort(
+      {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
+  TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleLength());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getTupleLength(), CVC4ApiException&);
+}
+
+void SortBlack::testGetTupleSorts()
+{
+  Sort tupleSort = d_solver.mkTupleSort(
+      {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
+  TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleSorts());
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  TS_ASSERT_THROWS(bvSort.getTupleSorts(), CVC4ApiException&);
+}