139 lines
4.5 KiB
C++
139 lines
4.5 KiB
C++
// Copyright 2010-2021 Google LLC
|
|
// Licensed under the Apache License, Version 2.0 (the "License");
|
|
// you may not use this file except in compliance with the License.
|
|
// You may obtain a copy of the License at
|
|
//
|
|
// http://www.apache.org/licenses/LICENSE-2.0
|
|
//
|
|
// Unless required by applicable law or agreed to in writing, software
|
|
// distributed under the License is distributed on an "AS IS" BASIS,
|
|
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
|
|
// See the License for the specific language governing permissions and
|
|
// limitations under the License.
|
|
|
|
#ifndef OR_TOOLS_SAT_OPB_READER_H_
|
|
#define OR_TOOLS_SAT_OPB_READER_H_
|
|
|
|
#include <algorithm>
|
|
#include <memory>
|
|
#include <string>
|
|
#include <vector>
|
|
|
|
#include "absl/strings/numbers.h"
|
|
#include "absl/strings/str_split.h"
|
|
#include "ortools/base/filelineiter.h"
|
|
#include "ortools/base/logging.h"
|
|
#include "ortools/base/macros.h"
|
|
#include "ortools/sat/boolean_problem.pb.h"
|
|
|
|
namespace operations_research {
|
|
namespace sat {
|
|
|
|
// This class loads a file in pbo file format into a LinearBooleanProblem.
|
|
// The format is described here:
|
|
// http://www.cril.univ-artois.fr/PB12/format.pdf
|
|
class OpbReader {
|
|
public:
|
|
OpbReader() {}
|
|
|
|
// Loads the given opb filename into the given problem.
|
|
bool Load(const std::string& filename, LinearBooleanProblem* problem) {
|
|
problem->Clear();
|
|
problem->set_name(ExtractProblemName(filename));
|
|
|
|
num_variables_ = 0;
|
|
int num_lines = 0;
|
|
for (const std::string& line : FileLines(filename)) {
|
|
++num_lines;
|
|
ProcessNewLine(problem, line);
|
|
}
|
|
if (num_lines == 0) {
|
|
LOG(FATAL) << "File '" << filename << "' is empty or can't be read.";
|
|
}
|
|
problem->set_num_variables(num_variables_);
|
|
return true;
|
|
}
|
|
|
|
private:
|
|
// Since the problem name is not stored in the cnf format, we infer it from
|
|
// the file name.
|
|
static std::string ExtractProblemName(const std::string& filename) {
|
|
const int found = filename.find_last_of('/');
|
|
const std::string problem_name =
|
|
found != std::string::npos ? filename.substr(found + 1) : filename;
|
|
return problem_name;
|
|
}
|
|
|
|
void ProcessNewLine(LinearBooleanProblem* problem, const std::string& line) {
|
|
const std::vector<std::string> words =
|
|
absl::StrSplit(line, absl::ByAnyChar(" ;"), absl::SkipEmpty());
|
|
if (words.empty() || words[0].empty() || words[0][0] == '*') {
|
|
return;
|
|
}
|
|
|
|
if (words[0] == "min:") {
|
|
LinearObjective* objective = problem->mutable_objective();
|
|
for (int i = 1; i < words.size(); ++i) {
|
|
const std::string& word = words[i];
|
|
if (word.empty() || word[0] == ';') continue;
|
|
if (word[0] == 'x') {
|
|
int literal;
|
|
CHECK(absl::SimpleAtoi(word.substr(1), &literal));
|
|
num_variables_ = std::max(num_variables_, literal);
|
|
objective->add_literals(literal);
|
|
} else {
|
|
int64_t value;
|
|
CHECK(absl::SimpleAtoi(word, &value));
|
|
objective->add_coefficients(value);
|
|
}
|
|
}
|
|
if (objective->literals_size() != objective->coefficients_size()) {
|
|
LOG(INFO) << "words.size() = " << words.size();
|
|
LOG(FATAL) << "Failed to parse objective:\n " << line;
|
|
}
|
|
return;
|
|
}
|
|
LinearBooleanConstraint* constraint = problem->add_constraints();
|
|
for (int i = 0; i < words.size(); ++i) {
|
|
const std::string& word = words[i];
|
|
CHECK(!word.empty());
|
|
if (word == ">=") {
|
|
CHECK_LT(i + 1, words.size());
|
|
int64_t value;
|
|
CHECK(absl::SimpleAtoi(words[i + 1], &value));
|
|
constraint->set_lower_bound(value);
|
|
break;
|
|
} else if (word == "=") {
|
|
CHECK_LT(i + 1, words.size());
|
|
int64_t value;
|
|
CHECK(absl::SimpleAtoi(words[i + 1], &value));
|
|
constraint->set_upper_bound(value);
|
|
constraint->set_lower_bound(value);
|
|
break;
|
|
} else {
|
|
if (word[0] == 'x') {
|
|
int literal;
|
|
CHECK(absl::SimpleAtoi(word.substr(1), &literal));
|
|
num_variables_ = std::max(num_variables_, literal);
|
|
constraint->add_literals(literal);
|
|
} else {
|
|
int64_t value;
|
|
CHECK(absl::SimpleAtoi(words[i], &value));
|
|
constraint->add_coefficients(value);
|
|
}
|
|
}
|
|
}
|
|
if (constraint->literals_size() != constraint->coefficients_size()) {
|
|
LOG(FATAL) << "Failed to parse constraint:\n " << line;
|
|
}
|
|
}
|
|
|
|
int num_variables_;
|
|
DISALLOW_COPY_AND_ASSIGN(OpbReader);
|
|
};
|
|
|
|
} // namespace sat
|
|
} // namespace operations_research
|
|
|
|
#endif // OR_TOOLS_SAT_OPB_READER_H_
|