summaryrefslogtreecommitdiff
path: root/test/unit
diff options
context:
space:
mode:
authoryoni206 <yoni206@users.noreply.github.com>2021-08-27 03:34:12 +0300
committerGitHub <noreply@github.com>2021-08-27 00:34:12 +0000
commit1639655ca7b8f0f18145fdbb515253810b119d08 (patch)
treedfd7b7be07b803453864902893988156cfdc21b6 /test/unit
parent8915e3234871e56eb9fa1c188f89a8d825dc10e8 (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.cpp34
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback