diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2021-08-27 03:34:12 +0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-08-27 00:34:12 +0000 |
commit | 1639655ca7b8f0f18145fdbb515253810b119d08 (patch) | |
tree | dfd7b7be07b803453864902893988156cfdc21b6 /test/unit | |
parent | 8915e3234871e56eb9fa1c188f89a8d825dc10e8 (diff) |
Add `isNull` to cpp api tests, python api, and python api tests (#7059)
While working on API documentation for python, I noticed that isNull is not wrapped
by the python API. It is also not tested in the cpp API tests. This PR fixes both issues,
and also updates the python api tests accordingly.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/api/datatype_api_black.cpp | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp index f82e722d3..745abc17c 100644 --- a/test/unit/api/datatype_api_black.cpp +++ b/test/unit/api/datatype_api_black.cpp @@ -42,6 +42,40 @@ TEST_F(TestApiBlackDatatype, mkDatatypeSort) ASSERT_NO_THROW(nilConstr.getConstructorTerm()); } +TEST_F(TestApiBlackDatatype, isNull) +{ + // creating empty (null) objects. + DatatypeDecl dtypeSpec; + DatatypeConstructorDecl cons; + Datatype d; + DatatypeConstructor consConstr; + DatatypeSelector sel; + + // verifying that the objects are considered null. + ASSERT_TRUE(dtypeSpec.isNull()); + ASSERT_TRUE(cons.isNull()); + ASSERT_TRUE(d.isNull()); + ASSERT_TRUE(consConstr.isNull()); + ASSERT_TRUE(sel.isNull()); + + // changing the objects to be non-null + dtypeSpec = d_solver.mkDatatypeDecl("list"); + cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("head", d_solver.getIntegerSort()); + dtypeSpec.addConstructor(cons); + Sort listSort = d_solver.mkDatatypeSort(dtypeSpec); + d = listSort.getDatatype(); + consConstr = d[0]; + sel = consConstr[0]; + + // verifying that the new objects are non-null + ASSERT_FALSE(dtypeSpec.isNull()); + ASSERT_FALSE(cons.isNull()); + ASSERT_FALSE(d.isNull()); + ASSERT_FALSE(consConstr.isNull()); + ASSERT_FALSE(sel.isNull()); +} + TEST_F(TestApiBlackDatatype, mkDatatypeSorts) { /* Create two mutual datatypes corresponding to this definition |