diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2021-01-28 14:51:28 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-28 14:51:28 -0600 |
| commit | 2f4bae4b4ffe6e913925f3d8f2c857a01aeea3bd (patch) | |
| tree | 09aa68a87615a64766aa4ce5240771cf9444b974 /test/unit | |
| parent | e234ff58f561ac97642df15c698962faa9d1e5e4 (diff) | |
Remove regex header from cvc4cpp.cpp (#5826)
This PR replaces the heavy hammer std::regex_match for checking numbers with string operations
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/api/term_black.cpp | 11 | ||||
| -rw-r--r-- | test/unit/parser/parser_black.h | 2 |
2 files changed, 12 insertions, 1 deletions
diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp index 50d67688d..b6f8fc4ed 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/term_black.cpp @@ -684,6 +684,17 @@ TEST_F(TestApiTermBlack, getInteger) Term int9 = d_solver.mkInteger("4294967296"); Term int10 = d_solver.mkInteger("18446744073709551615"); Term int11 = d_solver.mkInteger("18446744073709551616"); + Term int12 = d_solver.mkInteger("-0"); + + ASSERT_THROW(d_solver.mkInteger(""), CVC4ApiException); + ASSERT_THROW(d_solver.mkInteger("-"), CVC4ApiException); + ASSERT_THROW(d_solver.mkInteger("-1-"), CVC4ApiException); + ASSERT_THROW(d_solver.mkInteger("0.0"), CVC4ApiException); + ASSERT_THROW(d_solver.mkInteger("-0.1"), CVC4ApiException); + ASSERT_THROW(d_solver.mkInteger("012"), CVC4ApiException); + ASSERT_THROW(d_solver.mkInteger("0000"), CVC4ApiException); + ASSERT_THROW(d_solver.mkInteger("-01"), CVC4ApiException); + ASSERT_THROW(d_solver.mkInteger("-00"), CVC4ApiException); ASSERT_TRUE(!int1.isInt32() && !int1.isUInt32() && !int1.isInt64() && !int1.isUInt64() && int1.isInteger()); diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index d63f6b029..507ccb791 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -379,7 +379,7 @@ public: tryGoodExpr("1.5"); tryGoodExpr("#xfab09c7"); tryGoodExpr("#b0001011"); - tryGoodExpr("(* 5 01)"); // '01' is OK in non-strict mode + tryGoodExpr("(* 5 1)"); } void testBadSmt2Exprs() { |