Method parseDIMACS

examples/sat.cpp:141–233

Post constraints according to DIMACS file \a f

  /// Post constraints according to DIMACS file \a f
  void parseDIMACS(const char* f) {
    int variables = 0;
    int clauses = 0;
    std::ifstream dimacs(f);
    if (!dimacs) {
      std::cerr << "error: file '" << f << "' not found" << std::endl;
      exit(1);
    }
    std::cout << "Solving problem from DIMACS file '" << f << "'"
              << std::endl;
    std::string line;
    int c = 0;
    while (dimacs.good()) {
      std::getline(dimacs,line);
      // Comments (ignore them)
      if (line[0] == 'c' || line == "") {
      }
      // Line has format "p cnf <variables> <clauses>"
      else if (variables == 0 && clauses == 0 &&
               line[0] == 'p' && line[1] == ' ' &&
               line[2] == 'c' && line[3] == 'n' &&
               line[4] == 'f' && line[5] == ' ') {
        int i = 6;
        while (line[i] >= '0' && line[i] <= '9') {
          variables = 10*variables + line[i] - '0';
          i++;
        }
        i++;
        while (line[i] >= '0' && line[i] <= '9') {
          clauses = 10*clauses + line[i] - '0';
          i++;
        }
        std::cout << "(" << variables << " variables, "
                  << clauses << " clauses)" << std::endl << std::endl;
        // Add variables to array
        x = BoolVarArray(*this, variables, 0, 1);
      }
      // Parse regular clause
      else if (variables > 0 &&
      ((line[0] >= '0' && line[0] <= '9') || line[0] == '-' || line[0] == ' ')) {
        c++;
        std::vector<int> pos;
        std::vector<int> neg;
        int i = 0;
        while (line[i] != 0) {
          if (line[i] == ' ') {
            i++;
            continue;
          }
          bool positive = true;
          if (line[i] == '-') {
            positive = false;
            i++;
          }
          int value = 0;
          while (line[i] >= '0' && line[i] <= '9') {
            value = 10 * value + line[i] - '0';
            i++;