Add missing functions to new C++ API (#3769)

3 files changed, 297 insertions, 2 deletions

diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h
index b9c671a30..2d7a9c12b 100644
--- a/test/unit/api/datatype_api_black.h
+++ b/test/unit/api/datatype_api_black.h
@@ -28,6 +28,9 @@ class DatatypeBlack : public CxxTest::TestSuite
 
   void testMkDatatypeSort();
 
+  void testDatatypeStructs();
+  void testDatatypeNames();
+
  private:
   Solver d_solver;
 };
@@ -50,8 +53,117 @@ void DatatypeBlack::testMkDatatypeSort()
   DatatypeConstructor consConstr = d[0];
   DatatypeConstructor nilConstr = d[1];
   TS_ASSERT_THROWS(d[2], CVC4ApiException&);
-  TS_ASSERT(consConstr.isResolved());
-  TS_ASSERT(nilConstr.isResolved());
   TS_ASSERT_THROWS_NOTHING(consConstr.getConstructorTerm());
   TS_ASSERT_THROWS_NOTHING(nilConstr.getConstructorTerm());
 }
+
+void DatatypeBlack::testDatatypeStructs()
+{
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+
+  // create datatype sort to test
+  DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", intSort);
+  cons.addSelector(head);
+  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
+  cons.addSelector(tail);
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  dtypeSpec.addConstructor(nil);
+  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
+  Datatype dt = dtypeSort.getDatatype();
+  TS_ASSERT(!dt.isCodatatype());
+  TS_ASSERT(!dt.isTuple());
+  TS_ASSERT(!dt.isRecord());
+  TS_ASSERT(!dt.isFinite());
+  TS_ASSERT(dt.isWellFounded());
+  // get constructor
+  DatatypeConstructor dcons = dt[0];
+  Term consTerm = dcons.getConstructorTerm();
+  TS_ASSERT(dcons.getNumSelectors() == 2);
+  // get tester name: notice this is only to support the Z3-style datatypes
+  // prior to SMT-LIB 2.6 where testers where changed to indexed symbols.
+  TS_ASSERT_THROWS_NOTHING(dcons.getTesterName());
+
+  // create datatype sort to test
+  DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum");
+  DatatypeConstructorDecl ca("A");
+  dtypeSpecEnum.addConstructor(ca);
+  DatatypeConstructorDecl cb("B");
+  dtypeSpecEnum.addConstructor(cb);
+  DatatypeConstructorDecl cc("C");
+  dtypeSpecEnum.addConstructor(cc);
+  Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum);
+  Datatype dtEnum = dtypeSortEnum.getDatatype();
+  TS_ASSERT(!dtEnum.isTuple());
+  TS_ASSERT(dtEnum.isFinite());
+
+  // create codatatype
+  DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true);
+  DatatypeConstructorDecl consStream("cons");
+  DatatypeSelectorDecl headStream("head", intSort);
+  consStream.addSelector(headStream);
+  DatatypeSelectorDecl tailStream("tail", DatatypeDeclSelfSort());
+  consStream.addSelector(tailStream);
+  dtypeSpecStream.addConstructor(consStream);
+  Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream);
+  Datatype dtStream = dtypeSortStream.getDatatype();
+  TS_ASSERT(dtStream.isCodatatype());
+  TS_ASSERT(!dtStream.isFinite());
+  // codatatypes may be well-founded
+  TS_ASSERT(dtStream.isWellFounded());
+
+  // create tuple
+  Sort tupSort = d_solver.mkTupleSort({boolSort});
+  Datatype dtTuple = tupSort.getDatatype();
+  TS_ASSERT(dtTuple.isTuple());
+  TS_ASSERT(!dtTuple.isRecord());
+  TS_ASSERT(dtTuple.isFinite());
+  TS_ASSERT(dtTuple.isWellFounded());
+
+  // create record
+  std::vector<std::pair<std::string, Sort>> fields = {
+      std::make_pair("b", boolSort), std::make_pair("i", intSort)};
+  Sort recSort = d_solver.mkRecordSort(fields);
+  TS_ASSERT(recSort.isDatatype());
+  Datatype dtRecord = recSort.getDatatype();
+  TS_ASSERT(!dtRecord.isTuple());
+  TS_ASSERT(dtRecord.isRecord());
+  TS_ASSERT(!dtRecord.isFinite());
+  TS_ASSERT(dtRecord.isWellFounded());
+}
+
+void DatatypeBlack::testDatatypeNames()
+{
+  Sort intSort = d_solver.getIntegerSort();
+
+  // create datatype sort to test
+  DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", intSort);
+  cons.addSelector(head);
+  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
+  cons.addSelector(tail);
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  dtypeSpec.addConstructor(nil);
+  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
+  Datatype dt = dtypeSort.getDatatype();
+  TS_ASSERT(dt.getName() == std::string("list"));
+  TS_ASSERT_THROWS_NOTHING(dt.getConstructor("nil"));
+  TS_ASSERT_THROWS_NOTHING(dt["cons"]);
+  TS_ASSERT_THROWS(dt.getConstructor("head"), CVC4ApiException&);
+  TS_ASSERT_THROWS(dt.getConstructor(""), CVC4ApiException&);
+
+  DatatypeConstructor dcons = dt[0];
+  TS_ASSERT(dcons.getName() == std::string("cons"));
+  TS_ASSERT_THROWS_NOTHING(dcons.getSelector("head"));
+  TS_ASSERT_THROWS_NOTHING(dcons["tail"]);
+  TS_ASSERT_THROWS(dcons.getSelector("cons"), CVC4ApiException&);
+
+  // get selector
+  DatatypeSelector dselTail = dcons[1];
+  TS_ASSERT(dselTail.getName() == std::string("tail"));
+}
diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h
index 4ea29b8d7..1bac8a283 100644
--- a/test/unit/api/sort_black.h
+++ b/test/unit/api/sort_black.h
@@ -27,6 +27,7 @@ class SortBlack : public CxxTest::TestSuite
   void tearDown() override;
 
   void testGetDatatype();
+  void testDatatypeSorts();
   void testInstantiate();
   void testGetFunctionArity();
   void testGetFunctionDomainSorts();
@@ -47,6 +48,9 @@ class SortBlack : public CxxTest::TestSuite
   void testGetTupleLength();
   void testGetTupleSorts();
 
+  void testSortCompare();
+  void testSortSubtyping();
+
  private:
   Solver d_solver;
 };
@@ -72,6 +76,49 @@ void SortBlack::testGetDatatype()
   TS_ASSERT_THROWS(bvSort.getDatatype(), CVC4ApiException&);
 }
 
+void SortBlack::testDatatypeSorts()
+{
+  Sort intSort = d_solver.getIntegerSort();
+  // create datatype sort to test
+  DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
+  DatatypeConstructorDecl cons("cons");
+  DatatypeSelectorDecl head("head", intSort);
+  cons.addSelector(head);
+  DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort());
+  cons.addSelector(tail);
+  dtypeSpec.addConstructor(cons);
+  DatatypeConstructorDecl nil("nil");
+  dtypeSpec.addConstructor(nil);
+  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
+  Datatype dt = dtypeSort.getDatatype();
+  TS_ASSERT(!dtypeSort.isConstructor());
+  TS_ASSERT_THROWS(dtypeSort.getConstructorCodomainSort(), CVC4ApiException&);
+  TS_ASSERT_THROWS(dtypeSort.getConstructorDomainSorts(), CVC4ApiException&);
+  TS_ASSERT_THROWS(dtypeSort.getConstructorArity(), CVC4ApiException&);
+
+  // get constructor
+  DatatypeConstructor dcons = dt[0];
+  Term consTerm = dcons.getConstructorTerm();
+  Sort consSort = consTerm.getSort();
+  TS_ASSERT(consSort.isConstructor());
+  TS_ASSERT(!consSort.isTester());
+  TS_ASSERT(!consSort.isSelector());
+  TS_ASSERT(consSort.getConstructorArity() == 2);
+  std::vector<Sort> consDomSorts = consSort.getConstructorDomainSorts();
+  TS_ASSERT(consDomSorts[0] == intSort);
+  TS_ASSERT(consDomSorts[1] == dtypeSort);
+  TS_ASSERT(consSort.getConstructorCodomainSort() == dtypeSort);
+
+  // get tester
+  Term isConsTerm = dcons.getTesterTerm();
+  TS_ASSERT(isConsTerm.getSort().isTester());
+
+  // get selector
+  DatatypeSelector dselTail = dcons[1];
+  Term tailTerm = dselTail.getSelectorTerm();
+  TS_ASSERT(tailTerm.getSort().isSelector());
+}
+
 void SortBlack::testInstantiate()
 {
   // instantiate parametric datatype, check should not fail
@@ -277,3 +324,37 @@ void SortBlack::testGetTupleSorts()
   Sort bvSort = d_solver.mkBitVectorSort(32);
   TS_ASSERT_THROWS(bvSort.getTupleSorts(), CVC4ApiException&);
 }
+
+void SortBlack::testSortCompare()
+{
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort intSort = d_solver.getIntegerSort();
+  Sort bvSort = d_solver.mkBitVectorSort(32);
+  Sort bvSort2 = d_solver.mkBitVectorSort(32);
+  TS_ASSERT(bvSort >= bvSort2);
+  TS_ASSERT(bvSort <= bvSort2);
+  TS_ASSERT((intSort > boolSort) != (intSort < boolSort));
+  TS_ASSERT((intSort > bvSort || intSort == bvSort) == (intSort >= bvSort));
+}
+
+void SortBlack::testSortSubtyping()
+{
+  Sort intSort = d_solver.getIntegerSort();
+  Sort realSort = d_solver.getRealSort();
+  TS_ASSERT(intSort.isSubsortOf(realSort));
+  TS_ASSERT(!realSort.isSubsortOf(intSort));
+  TS_ASSERT(intSort.isComparableTo(realSort));
+  TS_ASSERT(realSort.isComparableTo(intSort));
+
+  Sort arraySortII = d_solver.mkArraySort(intSort, intSort);
+  Sort arraySortIR = d_solver.mkArraySort(intSort, realSort);
+  TS_ASSERT(!arraySortII.isComparableTo(intSort));
+  // we do not support subtyping for arrays
+  TS_ASSERT(!arraySortII.isComparableTo(arraySortIR));
+
+  Sort setSortI = d_solver.mkSetSort(intSort);
+  Sort setSortR = d_solver.mkSetSort(realSort);
+  // we support subtyping for sets
+  TS_ASSERT(setSortI.isSubsortOf(setSortR));
+  TS_ASSERT(setSortR.isComparableTo(setSortI));
+}
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index ea619db7c..8f63c55ec 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -39,6 +39,10 @@ class TermBlack : public CxxTest::TestSuite
   void testIteTerm();
 
   void testTermAssignment();
+  void testTermCompare();
+  void testTermChildren();
+  void testSubstitute();
+  void testIsConst();
 
  private:
   Solver d_solver;
@@ -652,3 +656,101 @@ void TermBlack::testTermAssignment()
   t2 = d_solver.mkReal(2);
   TS_ASSERT_EQUALS(t1, d_solver.mkReal(1));
 }
+
+void TermBlack::testTermCompare()
+{
+  Term t1 = d_solver.mkReal(1);
+  Term t2 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2));
+  Term t3 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2));
+  TS_ASSERT(t2 >= t3);
+  TS_ASSERT(t2 <= t3);
+  TS_ASSERT((t1 > t2) != (t1 < t2));
+  TS_ASSERT((t1 > t2 || t1 == t2) == (t1 >= t2));
+}
+
+void TermBlack::testTermChildren()
+{
+  // simple term 2+3
+  Term two = d_solver.mkReal(2);
+  Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkReal(3));
+  TS_ASSERT(t1[0] == two);
+  TS_ASSERT(t1.getNumChildren() == 2);
+  Term tnull;
+  TS_ASSERT_THROWS(tnull.getNumChildren(), CVC4ApiException&);
+
+  // apply term f(2)
+  Sort intSort = d_solver.getIntegerSort();
+  Sort fsort = d_solver.mkFunctionSort(intSort, intSort);
+  Term f = d_solver.mkConst(fsort, "f");
+  Term t2 = d_solver.mkTerm(APPLY_UF, f, two);
+  // due to our higher-order view of terms, we treat f as a child of APPLY_UF
+  TS_ASSERT(t2.getNumChildren() == 2);
+  TS_ASSERT_EQUALS(t2[0], f);
+  TS_ASSERT_EQUALS(t2[1], two);
+  TS_ASSERT_THROWS(tnull[0], CVC4ApiException&);
+}
+
+void TermBlack::testSubstitute()
+{
+  Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
+  Term one = d_solver.mkReal(1);
+  Term ttrue = d_solver.mkTrue();
+  Term xpx = d_solver.mkTerm(PLUS, x, x);
+  Term onepone = d_solver.mkTerm(PLUS, one, one);
+
+  TS_ASSERT_EQUALS(xpx.substitute(x, one), onepone);
+  TS_ASSERT_EQUALS(onepone.substitute(one, x), xpx);
+  // incorrect due to type
+  TS_ASSERT_THROWS(xpx.substitute(one, ttrue), CVC4ApiException&);
+
+  // simultaneous substitution
+  Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y");
+  Term xpy = d_solver.mkTerm(PLUS, x, y);
+  Term xpone = d_solver.mkTerm(PLUS, y, one);
+  std::vector<Term> es;
+  std::vector<Term> rs;
+  es.push_back(x);
+  rs.push_back(y);
+  es.push_back(y);
+  rs.push_back(one);
+  TS_ASSERT_EQUALS(xpy.substitute(es, rs), xpone);
+
+  // incorrect substitution due to arity
+  rs.pop_back();
+  TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&);
+
+  // incorrect substitution due to types
+  rs.push_back(ttrue);
+  TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&);
+
+  // null cannot substitute
+  Term tnull;
+  TS_ASSERT_THROWS(tnull.substitute(one, x), CVC4ApiException&);
+  TS_ASSERT_THROWS(xpx.substitute(tnull, x), CVC4ApiException&);
+  TS_ASSERT_THROWS(xpx.substitute(x, tnull), CVC4ApiException&);
+  rs.pop_back();
+  rs.push_back(tnull);
+  TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&);
+  es.clear();
+  rs.clear();
+  es.push_back(x);
+  rs.push_back(y);
+  TS_ASSERT_THROWS(tnull.substitute(es, rs), CVC4ApiException&);
+  es.push_back(tnull);
+  rs.push_back(one);
+  TS_ASSERT_THROWS(xpx.substitute(es, rs), CVC4ApiException&);
+}
+
+void TermBlack::testIsConst()
+{
+  Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
+  Term one = d_solver.mkReal(1);
+  Term xpone = d_solver.mkTerm(PLUS, x, one);
+  Term onepone = d_solver.mkTerm(PLUS, one, one);
+  TS_ASSERT(!x.isConst());
+  TS_ASSERT(one.isConst());
+  TS_ASSERT(!xpone.isConst());
+  TS_ASSERT(!onepone.isConst());
+  Term tnull;
+  TS_ASSERT_THROWS(tnull.isConst(), CVC4ApiException&);
+}