diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-12-12 23:19:30 +0000 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-12-12 23:19:30 +0000 |
commit | 12f88ad664c24ee522643073dcddf144854ca1ef (patch) | |
tree | fa9e7df652e760db8f780bebda5eadecbc035c57 /test | |
parent | fb6bab97d8a9103a0d9c94ea9ba54cb04ed2a2a8 (diff) |
API: Add simple empty/sigma regexp unit tests (#2746)
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/api/solver_black.h | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 538899a0f..7527a5c55 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -36,6 +36,8 @@ class SolverBlack : public CxxTest::TestSuite void testDefineFun(); void testDefineFunRec(); void testDefineFunsRec(); + void testMkRegexpEmpty(); + void testMkRegexpSigma(); private: Solver d_solver; @@ -228,3 +230,19 @@ void SolverBlack::testDefineFunsRec() d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}), CVC4ApiException&); } + +void SolverBlack::testMkRegexpEmpty() +{ + Sort strSort = d_solver.getStringSort(); + Term s = d_solver.mkVar("s", strSort); + TS_ASSERT_THROWS_NOTHING( + d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty())); +} + +void SolverBlack::testMkRegexpSigma() +{ + Sort strSort = d_solver.getStringSort(); + Term s = d_solver.mkVar("s", strSort); + TS_ASSERT_THROWS_NOTHING( + d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma())); +} |