Change datatype selector/constructor/tester to terms (#3773)

5 files changed, 211 insertions, 114 deletions

diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index 43f97796e..c5773fa72 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -36,9 +36,11 @@ void test(Solver& slv, Sort& consListSort)
   // which is equivalent to consList["cons"].getConstructor().  Note that
   // "nil" is a constructor too, so it needs to be applied with
   // APPLY_CONSTRUCTOR, even though it has no arguments.
-  Term t = slv.mkTerm(consList.getConstructorTerm("cons"),
-                      slv.mkReal(0),
-                      slv.mkTerm(consList.getConstructorTerm("nil")));
+  Term t = slv.mkTerm(
+      APPLY_CONSTRUCTOR,
+      consList.getConstructorTerm("cons"),
+      slv.mkReal(0),
+      slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
 
   std::cout << "t is " << t << std::endl
             << "sort of cons is "
@@ -51,7 +53,8 @@ void test(Solver& slv, Sort& consListSort)
   // Here we first get the DatatypeConstructor for cons (with
   // consList["cons"]) in order to get the "head" selector symbol
   // to apply.
-  Term t2 = slv.mkTerm(consList["cons"].getSelectorTerm("head"), t);
+  Term t2 =
+      slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t);
 
   std::cout << "t2 is " << t2 << std::endl
             << "simplify(t2) is " << slv.simplify(t2) << std::endl
@@ -116,7 +119,8 @@ void test(Solver& slv, Sort& consListSort)
   Term a = slv.mkConst(paramConsIntListSort, "a");
   std::cout << "term " << a << " is of sort " << a.getSort() << std::endl;
 
-  Term head_a = slv.mkTerm(paramConsList["cons"].getSelectorTerm("head"), a);
+  Term head_a = slv.mkTerm(
+      APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a);
   std::cout << "head_a is " << head_a << " of sort " << head_a.getSort()
             << std::endl
             << "sort of cons is "
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index ef7296089..f4ca1147f 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -593,6 +593,18 @@ namespace {
 
 bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; }
 
+/** Returns true if the internal kind is one where the API term structure
+ *  differs from internal structure. This happens for APPLY_* kinds.
+ *  The API takes a "higher-order" perspective and treats functions as well
+ *  as datatype constructors/selectors/testers as terms
+ *  but interally they are not
+ */
+bool isApplyKind(CVC4::Kind k)
+{
+  return (k == CVC4::Kind::APPLY_UF || k == CVC4::Kind::APPLY_CONSTRUCTOR
+          || k == CVC4::Kind::APPLY_SELECTOR || k == CVC4::Kind::APPLY_TESTER);
+}
+
 #ifdef CVC4_ASSERTIONS
 bool isDefinedIntKind(CVC4::Kind k)
 {
@@ -611,8 +623,20 @@ uint32_t maxArity(Kind k)
 {
   Assert(isDefinedKind(k));
   Assert(isDefinedIntKind(extToIntKind(k)));
-  return CVC4::ExprManager::maxArity(extToIntKind(k));
+  uint32_t max = CVC4::ExprManager::maxArity(extToIntKind(k));
+
+  // special cases for API level
+  // higher-order logic perspective at API
+  // functions/constructors/selectors/testers are terms
+  if (isApplyKind(extToIntKind(k))
+      && max != std::numeric_limits<uint32_t>::max())  // be careful not to
+                                                       // overflow
+  {
+    max++;
+  }
+  return max;
 }
+
 }  // namespace
 
 std::string kindToString(Kind k)
@@ -1327,36 +1351,31 @@ Op Term::getOp() const
   CVC4_API_CHECK_NOT_NULL;
   CVC4_API_CHECK(d_expr->hasOperator())
       << "Expecting Term to have an Op when calling getOp()";
-  CVC4::Expr op = d_expr->getOperator();
-  CVC4::Type t = op.getType();
 
-  // special cases for Datatype operators
-  if (t.isSelector())
+  // special cases for parameterized operators that are not indexed operators
+  // the API level differs from the internal structure
+  // indexed operators are stored in Ops
+  // whereas functions and datatype operators are terms, and the Op
+  // is one of the APPLY_* kinds
+  if (isApplyKind(d_expr->getKind()))
   {
-    return Op(APPLY_SELECTOR, op);
+    return Op(intToExtKind(d_expr->getKind()));
   }
-  else if (t.isConstructor())
+  else if (d_expr->isParameterized())
   {
-    return Op(APPLY_CONSTRUCTOR, op);
-  }
-  else if (t.isTester())
-  {
-    return Op(APPLY_TESTER, op);
+    // it's an indexed operator
+    // so we should return the indexed op
+    CVC4::Expr op = d_expr->getOperator();
+    return Op(intToExtKind(d_expr->getKind()), op);
   }
   else
   {
-    return Op(intToExtKind(op.getKind()), op);
+    return Op(intToExtKind(d_expr->getKind()));
   }
 }
 
 bool Term::isNull() const { return isNullHelper(); }
 
-bool Term::isParameterized() const
-{
-  CVC4_API_CHECK_NOT_NULL;
-  return d_expr->isParameterized();
-}
-
 Term Term::notTerm() const
 {
   CVC4_API_CHECK_NOT_NULL;
@@ -1528,14 +1547,18 @@ Term::const_iterator Term::const_iterator::operator++(int)
 Term Term::const_iterator::operator*() const
 {
   Assert(d_orig_expr != nullptr);
-  if (!d_pos && (d_orig_expr->getKind() == CVC4::Kind::APPLY_UF))
+  // this term has an extra child (mismatch between API and internal structure)
+  // the extra child will be the first child
+  bool extra_child = isApplyKind(d_orig_expr->getKind());
+
+  if (!d_pos && extra_child)
   {
     return Term(d_orig_expr->getOperator());
   }
   else
   {
     uint32_t idx = d_pos;
-    if (d_orig_expr->getKind() == CVC4::Kind::APPLY_UF)
+    if (extra_child)
     {
       Assert(idx > 0);
       --idx;
@@ -1553,7 +1576,13 @@ Term::const_iterator Term::begin() const
 Term::const_iterator Term::end() const
 {
   int endpos = d_expr->getNumChildren();
-  if (d_expr->getKind() == CVC4::Kind::APPLY_UF)
+  // special cases for APPLY_*
+  // the API differs from the internal structure
+  // the API takes a "higher-order" perspective and the applied
+  //   function or datatype constructor/selector/tester is a Term
+  // which means it needs to be one of the children, even though
+  //   internally it is not
+  if (isApplyKind(d_expr->getKind()))
   {
     // one more child if this is a UF application (count the UF as a child)
     ++endpos;
@@ -1771,11 +1800,11 @@ DatatypeSelector::~DatatypeSelector() {}
 
 bool DatatypeSelector::isResolved() const { return d_stor->isResolved(); }
 
-Op DatatypeSelector::getSelectorTerm() const
+Term DatatypeSelector::getSelectorTerm() const
 {
   CVC4_API_CHECK(isResolved()) << "Expected resolved datatype selector.";
-  CVC4::Expr sel = d_stor->getSelector();
-  return Op(APPLY_SELECTOR, sel);
+  Term sel = d_stor->getSelector();
+  return sel;
 }
 
 std::string DatatypeSelector::toString() const
@@ -1812,11 +1841,11 @@ DatatypeConstructor::~DatatypeConstructor() {}
 
 bool DatatypeConstructor::isResolved() const { return d_ctor->isResolved(); }
 
-Op DatatypeConstructor::getConstructorTerm() const
+Term DatatypeConstructor::getConstructorTerm() const
 {
   CVC4_API_CHECK(isResolved()) << "Expected resolved datatype constructor.";
-  CVC4::Expr ctor = d_ctor->getConstructor();
-  return Op(APPLY_CONSTRUCTOR, ctor);
+  Term ctor = d_ctor->getConstructor();
+  return ctor;
 }
 
 DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
@@ -1833,12 +1862,12 @@ DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const
   return (*d_ctor)[name];
 }
 
-Op DatatypeConstructor::getSelectorTerm(const std::string& name) const
+Term DatatypeConstructor::getSelectorTerm(const std::string& name) const
 {
   // CHECK: cons with name exists?
   // CHECK: is resolved?
-  CVC4::Expr sel = d_ctor->getSelector(name);
-  return Op(APPLY_SELECTOR, sel);
+  Term sel = d_ctor->getSelector(name);
+  return sel;
 }
 
 DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
@@ -1963,12 +1992,12 @@ DatatypeConstructor Datatype::getConstructor(const std::string& name) const
   return (*d_dtype)[name];
 }
 
-Op Datatype::getConstructorTerm(const std::string& name) const
+Term Datatype::getConstructorTerm(const std::string& name) const
 {
   // CHECK: cons with name exists?
   // CHECK: is resolved?
-  CVC4::Expr ctor = d_dtype->getConstructor(name);
-  return Op(APPLY_CONSTRUCTOR, ctor);
+  Term ctor = d_dtype->getConstructor(name);
+  return ctor;
 }
 
 size_t Datatype::getNumConstructors() const
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 84615afc0..f7f16832a 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -753,23 +753,6 @@ class CVC4_PUBLIC Term
   bool isNull() const;
 
   /**
-   * @return true if this expression is parameterized.
-   *
-   * !!! The below documentation is not accurate until we have a way of getting
-   * operators from terms.
-   *
-   * In detail, a term that is parameterized is one that has an operator that
-   * must be provided in addition to its kind to construct it. For example,
-   * say we want to re-construct a Term t where its children a1, ..., an are
-   * replaced by b1 ... bn. Then there are two cases:
-   * (1) If t is parametric, call:
-   *   mkTerm(t.getKind(), t.getOperator(), b1, ..., bn )
-   * (2) If t is not parametric, call:
-   *   mkTerm(t.getKind(), b1, ..., bn )
-   */
-  bool isParameterized() const;
-
-  /**
    * Boolean negation.
    * @return the Boolean negation of this term
    */
@@ -1218,9 +1201,9 @@ class CVC4_PUBLIC DatatypeSelector
 
   /**
    * Get the selector operator of this datatype selector.
-   * @return the selector operator
+   * @return the selector term
    */
-  Op getSelectorTerm() const;
+  Term getSelectorTerm() const;
 
   /**
    * @return a string representation of this datatype selector
@@ -1275,9 +1258,9 @@ class CVC4_PUBLIC DatatypeConstructor
 
   /**
    * Get the constructor operator of this datatype constructor.
-   * @return the constructor operator
+   * @return the constructor term
    */
-  Op getConstructorTerm() const;
+  Term getConstructorTerm() const;
 
   /**
    * Get the datatype selector with the given name.
@@ -1296,7 +1279,7 @@ class CVC4_PUBLIC DatatypeConstructor
    * @param name the name of the datatype selector
    * @return a term representing the datatype selector with the given name
    */
-  Op getSelectorTerm(const std::string& name) const;
+  Term getSelectorTerm(const std::string& name) const;
 
   /**
    * @return a string representation of this datatype constructor
@@ -1443,7 +1426,7 @@ class CVC4_PUBLIC Datatype
    * similarly-named constructors, the
    * first is returned.
    */
-  Op getConstructorTerm(const std::string& name) const;
+  Term getConstructorTerm(const std::string& name) const;
 
   /** Get the number of constructors for this Datatype. */
   size_t getNumConstructors() const;
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 2831b840d..e53b989f0 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -642,47 +642,55 @@ void SolverBlack::testMkTermFromOp()
   Term c = d_solver->mkConst(intListSort, "c");
   Datatype list = listSort.getDatatype();
   // list datatype constructor and selector operator terms
-  Op consTerm1 = list.getConstructorTerm("cons");
-  Op consTerm2 = list.getConstructor("cons").getConstructorTerm();
-  Op nilTerm1 = list.getConstructorTerm("nil");
-  Op nilTerm2 = list.getConstructor("nil").getConstructorTerm();
-  Op headTerm1 = list["cons"].getSelectorTerm("head");
-  Op headTerm2 = list["cons"].getSelector("head").getSelectorTerm();
-  Op tailTerm1 = list["cons"].getSelectorTerm("tail");
-  Op tailTerm2 = list["cons"]["tail"].getSelectorTerm();
-
-  // mkTerm(Kind kind, Op op) const
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(nilTerm1));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(nilTerm2));
-  TS_ASSERT_THROWS(d_solver->mkTerm(consTerm1), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(consTerm2), CVC4ApiException&);
+  Term consTerm1 = list.getConstructorTerm("cons");
+  Term consTerm2 = list.getConstructor("cons").getConstructorTerm();
+  Term nilTerm1 = list.getConstructorTerm("nil");
+  Term nilTerm2 = list.getConstructor("nil").getConstructorTerm();
+  Term headTerm1 = list["cons"].getSelectorTerm("head");
+  Term headTerm2 = list["cons"].getSelector("head").getSelectorTerm();
+  Term tailTerm1 = list["cons"].getSelectorTerm("tail");
+  Term tailTerm2 = list["cons"]["tail"].getSelectorTerm();
+
+  // mkTerm(Op op, Term term) const
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm2));
+  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, nilTerm1),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, consTerm1),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm2),
+                   CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(headTerm1), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(tailTerm2), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, headTerm1),
+                   CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&);
 
-  // mkTerm(Kind kind, Op op, Term child) const
+  // mkTerm(Op op, Term child) const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, d_solver->mkReal(1)));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(headTerm1, c));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(tailTerm2, c));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, headTerm1, c));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2, c));
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, a), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkTerm(consTerm1, d_solver->mkReal(0)),
-                   CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)),
+      CVC4ApiException&);
 
-  // mkTerm(Kind kind, Op op, Term child1, Term child2) const
+  // mkTerm(Op op, Term child1, Term child2) const
   TS_ASSERT_THROWS_NOTHING(
       d_solver->mkTerm(opterm3, d_solver->mkReal(1), d_solver->mkReal(2)));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(
-      consTerm1, d_solver->mkReal(0), d_solver->mkTerm(nilTerm1)));
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver->mkTerm(APPLY_CONSTRUCTOR,
+                       consTerm1,
+                       d_solver->mkReal(0),
+                       d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, d_solver->mkReal(1), Term()),
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, Term(), d_solver->mkReal(1)),
                    CVC4ApiException&);
 
-  // mkTerm(Kind kind, Op op, Term child1, Term child2, Term child3)
+  // mkTerm(Op op, Term child1, Term child2, Term child3)
   // const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(
       opterm3, d_solver->mkReal(1), d_solver->mkReal(1), d_solver->mkReal(2)));
@@ -942,26 +950,23 @@ void SolverBlack::testGetOp()
   Sort consListSort = d_solver->mkDatatypeSort(consListSpec);
   Datatype consList = consListSort.getDatatype();
 
-  Op consTerm = consList.getConstructorTerm("cons");
-  Op nilTerm = consList.getConstructorTerm("nil");
-  Op headTerm = consList["cons"].getSelectorTerm("head");
-
-  TS_ASSERT(consTerm.getKind() == APPLY_CONSTRUCTOR);
-  TS_ASSERT(nilTerm.getKind() == APPLY_CONSTRUCTOR);
-  TS_ASSERT(headTerm.getKind() == APPLY_SELECTOR);
+  Term consTerm = consList.getConstructorTerm("cons");
+  Term nilTerm = consList.getConstructorTerm("nil");
+  Term headTerm = consList["cons"].getSelectorTerm("head");
 
-  Term listnil = d_solver->mkTerm(nilTerm);
-  Term listcons1 = d_solver->mkTerm(consTerm, d_solver->mkReal(1), listnil);
-  Term listhead = d_solver->mkTerm(headTerm, listcons1);
+  Term listnil = d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm);
+  Term listcons1 = d_solver->mkTerm(
+      APPLY_CONSTRUCTOR, consTerm, d_solver->mkReal(1), listnil);
+  Term listhead = d_solver->mkTerm(APPLY_SELECTOR, headTerm, listcons1);
 
   TS_ASSERT(listnil.hasOp());
-  TS_ASSERT_EQUALS(listnil.getOp(), nilTerm);
+  TS_ASSERT_EQUALS(listnil.getOp(), APPLY_CONSTRUCTOR);
 
   TS_ASSERT(listcons1.hasOp());
-  TS_ASSERT_EQUALS(listcons1.getOp(), consTerm);
+  TS_ASSERT_EQUALS(listcons1.getOp(), APPLY_CONSTRUCTOR);
 
   TS_ASSERT(listhead.hasOp());
-  TS_ASSERT_EQUALS(listhead.getOp(), headTerm);
+  TS_ASSERT_EQUALS(listhead.getOp(), APPLY_SELECTOR);
 }
 
 void SolverBlack::testPush1()
@@ -1074,12 +1079,14 @@ void SolverBlack::testSimplify()
   TS_ASSERT(i1 == d_solver->simplify(i3));
 
   Datatype consList = consListSort.getDatatype();
-  Term dt1 =
-      d_solver->mkTerm(consList.getConstructorTerm("cons"),
-                       d_solver->mkReal(0),
-                       d_solver->mkTerm(consList.getConstructorTerm("nil")));
+  Term dt1 = d_solver->mkTerm(
+      APPLY_CONSTRUCTOR,
+      consList.getConstructorTerm("cons"),
+      d_solver->mkReal(0),
+      d_solver->mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt1));
-  Term dt2 = d_solver->mkTerm(consList["cons"].getSelectorTerm("head"), dt1);
+  Term dt2 = d_solver->mkTerm(
+      APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1);
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt2));
 
   Term b1 = d_solver->mkVar(bvSort, "b1");
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index 0d5400f5f..ea619db7c 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -28,8 +28,8 @@ class TermBlack : public CxxTest::TestSuite
   void testGetId();
   void testGetKind();
   void testGetSort();
+  void testGetOp();
   void testIsNull();
-  void testIsParameterized();
   void testNotTerm();
   void testAndTerm();
   void testOrTerm();
@@ -152,6 +152,88 @@ void TermBlack::testGetSort()
   TS_ASSERT(p_f_y.getSort() == boolSort);
 }
 
+void TermBlack::testGetOp()
+{
+  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");
+
+  TS_ASSERT(!x.hasOp());
+  TS_ASSERT_THROWS(x.getOp(), CVC4ApiException&);
+
+  Term ab = d_solver.mkTerm(SELECT, a, b);
+  Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
+  Term extb = d_solver.mkTerm(ext, b);
+
+  TS_ASSERT(ab.hasOp());
+  TS_ASSERT_EQUALS(ab.getOp(), Op(SELECT));
+  TS_ASSERT(!ab.getOp().isIndexed());
+  // can compare directly to a Kind (will invoke Op constructor)
+  TS_ASSERT_EQUALS(ab.getOp(), SELECT);
+  TS_ASSERT(extb.hasOp());
+  TS_ASSERT(extb.getOp().isIndexed());
+  TS_ASSERT_EQUALS(extb.getOp(), ext);
+
+  Term f = d_solver.mkConst(funsort, "f");
+  Term fx = d_solver.mkTerm(APPLY_UF, f, x);
+
+  TS_ASSERT(!f.hasOp());
+  TS_ASSERT_THROWS(f.getOp(), CVC4ApiException&);
+  TS_ASSERT(fx.hasOp());
+  TS_ASSERT_EQUALS(fx.getOp(), APPLY_UF);
+  std::vector<Term> children(fx.begin(), fx.end());
+  // testing rebuild from op and children
+  TS_ASSERT_EQUALS(fx, d_solver.mkTerm(fx.getOp(), children));
+
+  // Test Datatypes Ops
+  Sort sort = d_solver.mkParamSort("T");
+  DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
+  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl nil("nil");
+  DatatypeSelectorDecl head("head", sort);
+  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
+  cons.addSelector(head);
+  cons.addSelector(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.mkReal(0), nilTerm);
+  Term headTerm = d_solver.mkTerm(APPLY_SELECTOR, headOpTerm, consTerm);
+  Term tailTerm = d_solver.mkTerm(APPLY_SELECTOR, tailOpTerm, consTerm);
+
+  TS_ASSERT(nilTerm.hasOp());
+  TS_ASSERT(consTerm.hasOp());
+  TS_ASSERT(headTerm.hasOp());
+  TS_ASSERT(tailTerm.hasOp());
+
+  TS_ASSERT_EQUALS(nilTerm.getOp(), APPLY_CONSTRUCTOR);
+  TS_ASSERT_EQUALS(consTerm.getOp(), APPLY_CONSTRUCTOR);
+  TS_ASSERT_EQUALS(headTerm.getOp(), APPLY_SELECTOR);
+  TS_ASSERT_EQUALS(tailTerm.getOp(), APPLY_SELECTOR);
+
+  // Test rebuilding
+  children.clear();
+  children.insert(children.begin(), headTerm.begin(), headTerm.end());
+  TS_ASSERT_EQUALS(headTerm, d_solver.mkTerm(headTerm.getOp(), children));
+}
+
 void TermBlack::testIsNull()
 {
   Term x;
@@ -189,14 +271,6 @@ void TermBlack::testNotTerm()
   TS_ASSERT_THROWS_NOTHING(p_f_x.notTerm());
 }
 
-void TermBlack::testIsParameterized()
-{
-  Term n;
-  TS_ASSERT_THROWS(n.isParameterized(), CVC4ApiException&);
-  Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x");
-  TS_ASSERT_THROWS_NOTHING(x.isParameterized());
-}
-
 void TermBlack::testAndTerm()
 {
   Sort bvSort = d_solver.mkBitVectorSort(8);