Remove regex header from cvc4cpp.cpp (#5826)

This PR replaces the heavy hammer std::regex_match for checking numbers with string operations

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index abec4d8ddc07061a2e045aa811e748cf4866ea8d..541c5f5a57a97197a9cc7cf4169a4edb588e85b8 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -34,7 +34,6 @@
 #include "api/cvc4cpp.h"
 
 #include <cstring>
-#include <regex>
 #include <sstream>
 
 #include "base/check.h"
@@ -3924,11 +3923,48 @@ Term Solver::mkPi() const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+bool Solver::isValidInteger(const std::string& s) const
+{
+  if (s.length() == 0)
+  {
+    // string should not be empty
+    return false;
+  }
+
+  size_t index = 0;
+  if (s[index] == '-')
+  {
+    if (s.length() == 1)
+    {
+      // negative integers should contain at least one digit
+      return false;
+    }
+    index = 1;
+  }
+
+  if (s[index] == '0' && s.length() > (index + 1))
+  {
+    // From SMT-Lib 2.6: A〈numeral〉is the digit 0 or a non-empty sequence of
+    // digits not starting with 0. So integers like 001, 000 are not allowed
+    return false;
+  }
+
+  // all remaining characters should be decimal digits
+  for (; index < s.length(); ++index)
+  {
+    if (!std::isdigit(s[index]))
+    {
+      return false;
+    }
+  }
+
+  return true;
+}
+
 Term Solver::mkInteger(const std::string& s) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_ARG_CHECK_EXPECTED(std::regex_match(s, std::regex("-?\\d+")), s)
-      << " an integer ";
+  CVC4_API_ARG_CHECK_EXPECTED(isValidInteger(s), s) << " an integer ";
   Term integer = mkRealFromStrHelper(s);
   CVC4_API_ARG_CHECK_EXPECTED(integer.getSort() == getIntegerSort(), s)
       << " an integer";

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 66ba4f23b322edb4c2359af0c2296122e1e4c82f..60127d18bc56e28398129ad702959fbc80588852 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -3595,6 +3595,9 @@ class CVC4_PUBLIC Solver
                       bool isInv = false,
                       Grammar* g = nullptr) const;
 
+  /** check whether string s is a valid decimal integer */
+  bool isValidInteger(const std::string& s) const;
+
   /* The expression manager of this solver. */
   std::unique_ptr<ExprManager> d_exprMgr;
   /* The SMT engine of this solver. */

diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index 50d67688da1a384e76303d15a4a4a0554ccdf533..b6f8fc4ed7f779ec846fe50396911b118bfbc991 100644 (file)
--- 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 d63f6b0293b0459041cdc3bbbaccd9ee2a601bf7..507ccb791fbaec3e1a3adc0e17b32907bd5865e1 100644 (file)
--- 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() {