Updates to the unit tests, api, and examples for datatypes (#3459)

* Updates to the unit tests, api, and examples for datatypes

* Format

examples/api/datatypes-new.cpp

@@ -27,7 +27,7 @@ void test(Solver& slv, Sort& consListSort)
   // the complete spec for the datatype from the DatatypeSort, and
   // this Datatype object has constructor symbols (and others) filled in.
 
-  Datatype consList = consListSort.getDatatype();
+  const Datatype& consList = consListSort.getDatatype();
 
   // t = cons 0 nil
   //
@@ -103,7 +103,7 @@ void test(Solver& slv, Sort& consListSort)
   Sort paramConsIntListSort =
       paramConsListSort.instantiate(std::vector<Sort>{slv.getIntegerSort()});
 
-  Datatype paramConsList = paramConsListSort.getDatatype();
+  const Datatype& paramConsList = paramConsListSort.getDatatype();
 
   std::cout << "parameterized datatype sort is " << std::endl;
   for (const DatatypeConstructor& ctor : paramConsList)
@@ -169,7 +169,13 @@ int main()
             << ">>> Alternatively, use declareDatatype" << std::endl;
   std::cout << std::endl;
 
-  std::vector<DatatypeConstructorDecl> ctors = {cons, nil};
+  DatatypeConstructorDecl cons2("cons");
+  DatatypeSelectorDecl head2("head", slv.getIntegerSort());
+  DatatypeSelectorDecl tail2("tail", DatatypeDeclSelfSort());
+  cons2.addSelector(head2);
+  cons2.addSelector(tail2);
+  DatatypeConstructorDecl nil2("nil");
+  std::vector<DatatypeConstructorDecl> ctors = {cons2, nil2};
   Sort consListSort2 = slv.declareDatatype("list2", ctors);
   test(slv, consListSort2);
 

examples/api/datatypes.cpp

@@ -114,7 +114,7 @@ int main() {
   DatatypeType paramConsListType = em.mkDatatypeType(paramConsListSpec);
   Type paramConsIntListType = paramConsListType.instantiate(std::vector<Type>{em.integerType()});
 
-  Datatype paramConsList = paramConsListType.getDatatype();
+  const Datatype& paramConsList = paramConsListType.getDatatype();
 
   std::cout << "parameterized datatype sort is " << std::endl;
   for (const DatatypeConstructor& ctor : paramConsList)

src/api/cvc4cpp.cpp

@@ -1542,8 +1542,8 @@ std::string DatatypeConstructorDecl::toString() const
 
 // !!! This is only temporarily available until the parser is fully migrated
 // to the new API. !!!
-CVC4::DatatypeConstructor DatatypeConstructorDecl::getDatatypeConstructor(
-    void) const
+const CVC4::DatatypeConstructor&
+DatatypeConstructorDecl::getDatatypeConstructor(void) const
 {
   return *d_ctor;
 }
@@ -1613,7 +1613,7 @@ std::string DatatypeDecl::toString() const
 
 // !!! This is only temporarily available until the parser is fully migrated
 // to the new API. !!!
-CVC4::Datatype DatatypeDecl::getDatatype(void) const { return *d_dtype; }
+const CVC4::Datatype& DatatypeDecl::getDatatype(void) const { return *d_dtype; }
 
 std::ostream& operator<<(std::ostream& out,
                          const DatatypeSelectorDecl& stordecl)
@@ -1782,7 +1782,7 @@ std::string DatatypeConstructor::toString() const
 
 // !!! This is only temporarily available until the parser is fully migrated
 // to the new API. !!!
-CVC4::DatatypeConstructor DatatypeConstructor::getDatatypeConstructor(
+const CVC4::DatatypeConstructor& DatatypeConstructor::getDatatypeConstructor(
     void) const
 {
   return *d_ctor;
@@ -1850,7 +1850,7 @@ Datatype::const_iterator Datatype::end() const
 
 // !!! This is only temporarily available until the parser is fully migrated
 // to the new API. !!!
-CVC4::Datatype Datatype::getDatatype(void) const { return *d_dtype; }
+const CVC4::Datatype& Datatype::getDatatype(void) const { return *d_dtype; }
 
 Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype,
                                          bool begin)

src/api/cvc4cpp.h

@@ -1022,7 +1022,7 @@ class CVC4_PUBLIC DatatypeConstructorDecl
 
   // !!! This is only temporarily available until the parser is fully migrated
   // to the new API. !!!
-  CVC4::DatatypeConstructor getDatatypeConstructor(void) const;
+  const CVC4::DatatypeConstructor& getDatatypeConstructor(void) const;
 
  private:
   /**
@@ -1095,7 +1095,7 @@ class CVC4_PUBLIC DatatypeDecl
 
   // !!! This is only temporarily available until the parser is fully migrated
   // to the new API. !!!
-  CVC4::Datatype getDatatype(void) const;
+  const CVC4::Datatype& getDatatype(void) const;
 
  private:
   /* The internal (intermediate) datatype wrapped by this datatype
@@ -1309,7 +1309,7 @@ class CVC4_PUBLIC DatatypeConstructor
 
   // !!! This is only temporarily available until the parser is fully migrated
   // to the new API. !!!
-  CVC4::DatatypeConstructor getDatatypeConstructor(void) const;
+  const CVC4::DatatypeConstructor& getDatatypeConstructor(void) const;
 
  private:
   /**
@@ -1461,7 +1461,7 @@ class CVC4_PUBLIC Datatype
 
   // !!! This is only temporarily available until the parser is fully migrated
   // to the new API. !!!
-  CVC4::Datatype getDatatype(void) const;
+  const CVC4::Datatype& getDatatype(void) const;
 
  private:
   /**

test/unit/api/solver_black.h

@@ -624,6 +624,7 @@ void SolverBlack::testMkTermFromOpTerm()
   OpTerm opterm2 = d_solver->mkOpTerm(DIVISIBLE_OP, 1);
   OpTerm opterm3 = d_solver->mkOpTerm(CHAIN_OP, EQUAL);
   // list datatype
+
   Sort sort = d_solver->mkParamSort("T");
   DatatypeDecl listDecl("paramlist", sort);
   DatatypeConstructorDecl cons("cons");
@@ -776,17 +777,21 @@ void SolverBlack::testMkConstArray()
 
 void SolverBlack::testDeclareDatatype()
 {
-  DatatypeConstructorDecl cons("cons");
   DatatypeConstructorDecl nil("nil");
   std::vector<DatatypeConstructorDecl> ctors1 = {nil};
-  std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil};
-  std::vector<DatatypeConstructorDecl> ctors3;
   TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("a"), ctors1));
+  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl nil2("nil");
+  std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil2};
   TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("b"), ctors2));
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors2));
-  TS_ASSERT_THROWS(d_solver->declareDatatype(std::string("c"), ctors3),
+  DatatypeConstructorDecl cons2("cons");
+  DatatypeConstructorDecl nil3("nil");
+  std::vector<DatatypeConstructorDecl> ctors3 = {cons2, nil3};
+  TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors3));
+  std::vector<DatatypeConstructorDecl> ctors4;
+  TS_ASSERT_THROWS(d_solver->declareDatatype(std::string("c"), ctors4),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors3),
+  TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors4),
                    CVC4ApiException&);
 }
 
@@ -983,7 +988,6 @@ void SolverBlack::testSimplify()
   Sort uSort = d_solver->mkUninterpretedSort("u");
   Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
   Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort());
-
   DatatypeDecl consListSpec("list");
   DatatypeConstructorDecl cons("cons");
   DatatypeSelectorDecl head("head", d_solver->getIntegerSort());

test/unit/util/datatype_black.h

@@ -277,21 +277,39 @@ class DatatypeBlack : public CxxTest::TestSuite {
     Debug("groundterms") << "ground term of " << dtts[1].getDatatype().getName() << endl
                          << "  is " << dtts[1].mkGroundTerm() << endl;
     TS_ASSERT(dtts[1].mkGroundTerm().getType() == dtts[1]);
+  }
+  void testMutualListTrees2()
+  {
+    Datatype tree("tree");
+    DatatypeConstructor node("node", "is_node");
+    node.addArg("left", DatatypeSelfType());
+    node.addArg("right", DatatypeSelfType());
+    tree.addConstructor(node);
+
+    DatatypeConstructor leaf("leaf", "is_leaf");
+    leaf.addArg("leaf", DatatypeUnresolvedType("list"));
+    tree.addConstructor(leaf);
+
+    Datatype list("list");
+    DatatypeConstructor cons("cons", "is_cons");
+    cons.addArg("car", DatatypeUnresolvedType("tree"));
+    cons.addArg("cdr", DatatypeSelfType());
+    list.addConstructor(cons);
+
+    DatatypeConstructor nil("nil", "is_nil");
+    list.addConstructor(nil);
 
     // add another constructor to list datatype resulting in an
     // "otherNil-list"
     DatatypeConstructor otherNil("otherNil", "is_otherNil");
-    dts[1].addConstructor(otherNil);
+    list.addConstructor(otherNil);
 
+    vector<Datatype> dts;
+    dts.push_back(tree);
+    dts.push_back(list);
     // remake the types
     vector<DatatypeType> dtts2 = d_em->mkMutualDatatypeTypes(dts);
 
-    TS_ASSERT_DIFFERS(dtts, dtts2);
-    TS_ASSERT_DIFFERS(dtts[1], dtts2[1]);
-
-    // tree is also different because it's a tree of otherNil-lists
-    TS_ASSERT_DIFFERS(dtts[0], dtts2[0]);
-
     TS_ASSERT(! dtts2[0].getDatatype().isFinite());
     TS_ASSERT(dtts2[0].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL);
     TS_ASSERT(dtts2[0].getDatatype().isWellFounded());