[optimizer] Allow calling optimizer with USE_RATIONAL=false using ECC set generated with USE_RATIONAL=true

.github/workflows/pre-commit.yml

@@ -10,5 +10,8 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
-      - uses: actions/setup-python@v3
+      - name: Set up Python 3.11  # <-- add this name for clarity
+        uses: actions/setup-python@v3
+        with:
+          python-version: '3.11'   # <-- explicitly pin Python version
       - uses: pre-commit/action@v3.0.0

.pre-commit-config.yaml

@@ -21,6 +21,7 @@ repos:
             [
                 "--skip-string-normalization",
             ]
+        language_version: python3.11
 
 -   repo: https://github.com/pre-commit/pre-commit-hooks
     rev: v2.3.0

src/quartz/utils/string_utils.cpp

@@ -9,4 +9,73 @@ std::string quartz::to_string_with_precision(const Rational &val,
                                              int precision) {
   return "\"" + val.to_string() + "\"";
 }
+
+bool read_json_style_vector(std::istream &ss, std::vector<double> &vec) {
+  char c;
+  while (ss >> c) {
+    if (c == '[') {
+      // start of a vector
+      break;
+    } else if (!std::isspace(c)) {
+      // not a vector, input corrupted
+      return false;
+    }
+  }
+  if (ss.eof()) {
+    return false;
+  }
+  int vec_size;
+  if (!(ss >> vec_size)) {
+    return false;
+  }
+  vec.reserve(vec_size);
+  vec.clear();
+  while (ss >> c) {
+    if (c == ',') {
+      // start of the first item
+      break;
+    }
+  }
+  if (ss.eof()) {
+    return false;
+  }
+  for (int i = 0; i < vec_size; i++) {
+    std::string current;
+    bool is_rational = false;
+    while (ss >> c) {
+      if (i == vec_size - 1 ? c == ']' : c == ',') {
+        // separation of two items or end of vector
+        break;
+      } else if (!std::isspace(c)) {
+        current += c;
+        if (c == '/') {
+          is_rational = true;
+        }
+      }
+    }
+    if (ss.eof()) {
+      return false;
+    }
+    double item;
+    if (is_rational) {
+      Rational value(current);
+      item = value.to_double();
+    } else {
+      try {
+        item = std::stod(current);
+      } catch (const std::invalid_argument &e) {
+        std::cerr << "Invalid argument: " << e.what() << std::endl;
+        return false;
+      } catch (const std::out_of_range &e) {
+        std::cerr << "Out of range: " << e.what() << std::endl;
+        return false;
+      }
+    }
+    vec.push_back(std::move(item));
+  }
+  if (ss.eof()) {
+    return false;
+  }
+  return true;
+}
 }  // namespace quartz

src/quartz/utils/string_utils.h

@@ -105,4 +105,15 @@ bool read_json_style_vector(S &ss, std::vector<T> &vec) {
   return true;
 }
 
+/**
+ * Specialization: also handle the case "a/b" when reading a floating-point
+ * value from std::istream.
+ * @param ss The istream with a json array at the beginning,
+ * created by to_json_style_string(vec) above but potentially in Rational
+ * instead of double.
+ * @param vec The returned vector. The original content is deleted.
+ * @return True iff the read is successful.
+ */
+bool read_json_style_vector(std::istream &ss, std::vector<double> &vec);
+
 }  // namespace quartz