diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-10-07 18:37:48 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-10-07 18:37:48 -0700 |
| commit | 217710627bd440cb28524d014afb5f10058302fd (patch) | |
| tree | 7f6ee4d6ed7b17dff5d0619e2f5dcf17af319bfd /test/unit | |
| parent | 97c7e81a68b31328e5bf40dd6939826e3cc1cf93 (diff) | |
New C++ API: Add Term::getId(). (#3360)
+ use explicit types in NodeValue
+ add unit test for Term::isParameterized()
Co-Authored-By: makaimann <makaim@stanford.edu>
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/api/term_black.h | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index e8128ef7e..945944467 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -25,9 +25,11 @@ class TermBlack : public CxxTest::TestSuite void tearDown() override {} void testEq(); + void testGetId(); void testGetKind(); void testGetSort(); void testIsNull(); + void testIsParameterized(); void testNotTerm(); void testAndTerm(); void testOrTerm(); @@ -57,6 +59,19 @@ void TermBlack::testEq() TS_ASSERT(x != z); } +void TermBlack::testGetId() +{ + Term n; + TS_ASSERT_THROWS(n.getId(), CVC4ApiException&); + Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x"); + TS_ASSERT_THROWS_NOTHING(x.getId()); + Term y = x; + TS_ASSERT_EQUALS(x.getId(), y.getId()); + + Term z = d_solver.mkVar(d_solver.getIntegerSort(), "z"); + TS_ASSERT_DIFFERS(x.getId(), z.getId()); +} + void TermBlack::testGetKind() { Sort uSort = d_solver.mkUninterpretedSort("u"); @@ -173,6 +188,14 @@ 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); |