diff --git a/src/math/lp/mps_reader.h b/src/math/lp/mps_reader.h deleted file mode 100644 index 8093954b11e..00000000000 --- a/src/math/lp/mps_reader.h +++ /dev/null @@ -1,891 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - - -Abstract: - - - -Author: - - Lev Nachmanson (levnach) - -Revision History: - - ---*/ - -#pragma once - -// reads an MPS file representing a Mixed Integer Program -#include -#include -#include -#include "util/vector.h" -#include -#include -#include -#include -#include "math/lp/lp_primal_simplex.h" -#include "math/lp/lp_dual_simplex.h" -#include "math/lp/lar_solver.h" -#include "math/lp/lp_utils.h" -#include "math/lp/lp_solver.h" -namespace lp { -inline bool my_white_space(const char & a) { - return a == ' ' || a == '\t'; -} -inline size_t number_of_whites(const std::string & s) { - size_t i = 0; - for(;i < s.size(); i++) - if (!my_white_space(s[i])) return i; - return i; -} -inline size_t number_of_whites_from_end(const std::string & s) { - size_t ret = 0; - for(int i = static_cast(s.size()) - 1;i >= 0; i--) - if (my_white_space(s[i])) ret++;else break; - - return ret; -} - - - // trim from start -inline std::string <rim(std::string &s) { - s.erase(0, number_of_whites(s)); - return s; -} - - - - - // trim from end -inline std::string &rtrim(std::string &s) { - // s.erase(std::find_if(s.rbegin(), s.rend(), std::not1(std::ptr_fun(std::isspace))).base(), s.end()); - s.erase(s.end() - number_of_whites_from_end(s), s.end()); - return s; -} - // trim from both ends -inline std::string &trim(std::string &s) { - return ltrim(rtrim(s)); -} - -inline std::string trim(std::string const &r) { - std::string s = r; - return ltrim(rtrim(s)); -} - - -inline vector string_split(const std::string &source, const char *delimiter, bool keep_empty) { - vector results; - size_t prev = 0; - size_t next = 0; - while ((next = source.find_first_of(delimiter, prev)) != std::string::npos) { - if (keep_empty || (next - prev != 0)) { - results.push_back(source.substr(prev, next - prev)); - } - prev = next + 1; - } - if (prev < source.size()) { - results.push_back(source.substr(prev)); - } - return results; -} - -inline vector split_and_trim(const std::string &line) { - auto split = string_split(line, " \t", false); - vector ret; - for (auto s : split) { - ret.push_back(trim(s)); - } - return ret; -} - -template -class mps_reader { - enum row_type { Cost, Less_or_equal, Greater_or_equal, Equal }; - struct bound { - T m_low; - T m_upper; - bool m_low_is_set; - bool m_upper_is_set; - bool m_value_is_fixed; - T m_fixed_value; - bool m_free; - // constructor - bound() : m_low(numeric_traits::zero()), - m_low_is_set(true), - m_upper_is_set(false), - m_value_is_fixed(false), - m_free(false) {} // it seems all mps files I have seen have the default low value 0 on a variable - }; - - struct column { - std::string m_name; - bound * m_bound; - unsigned m_index; - column(const std::string &name, unsigned index): m_name(name), - m_bound(nullptr), - m_index(index) { - } - }; - - struct row { - row_type m_type; - std::string m_name; - std::unordered_map m_row_columns; - unsigned m_index; - T m_right_side; - T m_range; - row(row_type type, const std::string &name, unsigned index) : - m_type(type), - m_name(name), - m_index(index), - m_right_side(zero_of_type()), - m_range(zero_of_type()) - { - } - }; - - bool m_is_OK; - std::string m_file_name; - std::unordered_map m_rows; - std::unordered_map m_columns; - std::unordered_map m_names_to_var_index; - std::string m_line; - std::string m_name; - std::string m_cost_row_name; - std::ifstream m_file_stream; - // needed to adjust the index row - unsigned m_cost_line_count; - unsigned m_line_number; - std::ostream * m_message_stream; - - void set_m_ok_to_false() { - *m_message_stream << "setting m_is_OK to false" << std::endl; - m_is_OK = false; - } - - std::string get_string_from_position(unsigned offset) { - unsigned i = offset; - for (; i < m_line.size(); i++){ - if (m_line[i] == ' ') - break; - } - lp_assert(m_line.size() >= offset); - lp_assert(m_line.size() >> i); - lp_assert(i >= offset); - return m_line.substr(offset, i - offset); - } - - void set_boundary_for_column(unsigned col, bound * b, lp_solver * solver){ - if (b == nullptr) { - solver->set_lower_bound(col, numeric_traits::zero()); - return; - } - - if (b->m_free) { - return; - } - if (b->m_low_is_set) { - solver->set_lower_bound(col, b->m_low); - } - if (b->m_upper_is_set) { - solver->set_upper_bound(col, b->m_upper); - } - - if (b->m_value_is_fixed) { - solver->set_fixed_value(col, b->m_fixed_value); - } - } - - bool all_white_space() { - for (unsigned i = 0; i < m_line.size(); i++) { - char c = m_line[i]; - if (c != ' ' && c != '\t') { - return false; - } - } - return true; - } - - void read_line() { - while (m_is_OK) { - if (!getline(m_file_stream, m_line)) { - m_line_number++; - set_m_ok_to_false(); - *m_message_stream << "cannot read from file" << std::endl; - } - m_line_number++; - if (!m_line.empty() && m_line[0] != '*' && !all_white_space()) - break; - } - } - - void read_name() { - do { - read_line(); - if (m_line.find("NAME") != 0) { - continue; - } - m_line = m_line.substr(4); - m_name = trim(m_line); - break; - } while (m_is_OK); - } - - void read_rows() { - // look for start of the rows - read_line(); - do { - if (static_cast(m_line.find("ROWS")) >= 0) { - break; - } - } while (m_is_OK); - do { - read_line(); - if (m_line.find("COLUMNS") == 0) { - break; - } - add_row(); - } while (m_is_OK); - } - - void read_column_by_columns(const std::string & column_name, std::string column_data) { - // uph, let us try to work with columns - if (column_data.size() >= 22) { - std::string ss = column_data.substr(0, 8); - std::string row_name = trim(ss); - auto t = m_rows.find(row_name); - - if (t == m_rows.end()) { - *m_message_stream << "cannot find " << row_name << std::endl; - goto fail; - } else { - row * row = t->second; - row->m_row_columns[column_name] = numeric_traits::from_string(column_data.substr(8)); - if (column_data.size() > 24) { - column_data = column_data.substr(25); - if (column_data.size() >= 22) { - read_column_by_columns(column_name, column_data); - } - } - } - } else { - fail: - set_m_ok_to_false(); - *m_message_stream << "cannot understand this line\n" - "line = " << m_line << ", line number is " << m_line_number << std::endl; - return; - } - } - - void read_column(const std::string & column_name, const std::string & column_data){ - auto tokens = split_and_trim(column_data); - for (unsigned i = 0; i < tokens.size() - 1; i+= 2) { - auto row_name = tokens[i]; - if (row_name == "'MARKER'") return; // it is the integrality marker, no real data here - auto t = m_rows.find(row_name); - if (t == m_rows.end()) { - read_column_by_columns(column_name, column_data); - return; - } - row *r = t->second; - r->m_row_columns[column_name] = numeric_traits::from_string(tokens[i + 1]); - } - } - - void read_columns(){ - std::string column_name; - do { - read_line(); - if (m_line.find("RHS") == 0) { - break; - } - if (m_line.size() < 22) { - (*m_message_stream) << "line is too short for a column" << std::endl; - (*m_message_stream) << m_line << std::endl; - (*m_message_stream) << "line number is " << m_line_number << std::endl; - set_m_ok_to_false(); - return; - } - std::string column_name_tmp = trim(m_line.substr(4, 8)); - if (!column_name_tmp.empty()) { - column_name = column_name_tmp; - } - auto col_it = m_columns.find(column_name); - mps_reader::column * col; - if (col_it == m_columns.end()) { - col = new mps_reader::column(column_name, static_cast(m_columns.size())); - m_columns[column_name] = col; - // (*m_message_stream) << column_name << '[' << col->m_index << ']'<< std::endl; - } else { - col = col_it->second; - } - read_column(column_name, m_line.substr(14)); - } while (m_is_OK); - } - - void read_rhs() { - do { - read_line(); - if (m_line.find("BOUNDS") == 0 || m_line.find("ENDATA") == 0 || m_line.find("RANGES") == 0) { - break; - } - fill_rhs(); - } while (m_is_OK); - } - - - void fill_rhs_by_columns(std::string rhsides) { - // uph, let us try to work with columns - if (rhsides.size() >= 22) { - std::string ss = rhsides.substr(0, 8); - std::string row_name = trim(ss); - auto t = m_rows.find(row_name); - - if (t == m_rows.end()) { - (*m_message_stream) << "cannot find " << row_name << std::endl; - goto fail; - } else { - row * row = t->second; - row->m_right_side = numeric_traits::from_string(rhsides.substr(8)); - if (rhsides.size() > 24) { - rhsides = rhsides.substr(25); - if (rhsides.size() >= 22) { - fill_rhs_by_columns(rhsides); - } - } - } - } else { - fail: - set_m_ok_to_false(); - (*m_message_stream) << "cannot understand this line" << std::endl; - (*m_message_stream) << "line = " << m_line << ", line number is " << m_line_number << std::endl; - return; - } - } - - void fill_rhs() { - if (m_line.size() < 14) { - (*m_message_stream) << "line is too short" << std::endl; - (*m_message_stream) << m_line << std::endl; - (*m_message_stream) << "line number is " << m_line_number << std::endl; - set_m_ok_to_false(); - return; - } - std::string rhsides = m_line.substr(14); - vector splitted_line = split_and_trim(rhsides); - - for (unsigned i = 0; i < splitted_line.size() - 1; i += 2) { - auto t = m_rows.find(splitted_line[i]); - if (t == m_rows.end()) { - fill_rhs_by_columns(rhsides); - return; - } - row * row = t->second; - row->m_right_side = numeric_traits::from_string(splitted_line[i + 1]); - } - } - - void read_bounds() { - if (m_line.find("BOUNDS") != 0) { - return; - } - - do { - read_line(); - if (m_line[0] != ' ') { - break; - } - create_or_update_bound(); - } while (m_is_OK); - } - - void read_ranges() { - if (m_line.find("RANGES") != 0) { - return; - } - do { - read_line(); - auto sl = split_and_trim(m_line); - if (sl.size() < 2) { - break; - } - read_range(sl); - } while (m_is_OK); - } - - - void read_bound_by_columns(const std::string & colstr) { - if (colstr.size() < 14) { - (*m_message_stream) << "line is too short" << std::endl; - (*m_message_stream) << m_line << std::endl; - (*m_message_stream) << "line number is " << m_line_number << std::endl; - set_m_ok_to_false(); - return; - } - // uph, let us try to work with columns - if (colstr.size() >= 22) { - std::string ss = colstr.substr(0, 8); - std::string column_name = trim(ss); - auto t = m_columns.find(column_name); - - if (t == m_columns.end()) { - (*m_message_stream) << "cannot find " << column_name << std::endl; - goto fail; - } else { - vector bound_string; - bound_string.push_back(column_name); - if (colstr.size() > 14) { - bound_string.push_back(colstr.substr(14)); - } - mps_reader::column * col = t->second; - bound * b = col->m_bound; - if (b == nullptr) { - col->m_bound = b = new bound(); - } - update_bound(b, bound_string); - } - } else { - fail: - set_m_ok_to_false(); - (*m_message_stream) << "cannot understand this line" << std::endl; - (*m_message_stream) << "line = " << m_line << ", line number is " << m_line_number << std::endl; - return; - } - } - - void update_bound(bound * b, vector bound_string) { - /* - UP means an upper bound is applied to the variable. A bound of type LO means a lower bound is applied. A bound type of FX ("fixed") means that the variable has upper and lower bounds equal to a single value. A bound type of FR ("free") means the variable has neither lower nor upper bounds and so can take on negative values. A variation on that is MI for free negative, giving an upper bound of 0 but no lower bound. Bound type PL is for a free positive for zero to plus infinity, but as this is the normal default, it is seldom used. There are also bound types for use in MIP models - BV for binary, being 0 or 1. UI for upper integer and LI for lower integer. SC stands for semi-continuous and indicates that the variable may be zero, but if not must be equal to at least the value given. - */ - - std::string bound_type = get_string_from_position(1); - if (bound_type == "BV") { - b->m_upper_is_set = true; - b->m_upper = 1; - return; - } - - if (bound_type == "UP" || bound_type == "UI" || bound_type == "LIMITMAX") { - if (bound_string.size() <= 1){ - set_m_ok_to_false(); - return; - } - b->m_upper_is_set = true; - b->m_upper= numeric_traits::from_string(bound_string[1]); - } else if (bound_type == "LO" || bound_type == "LI") { - if (bound_string.size() <= 1){ - set_m_ok_to_false(); - return; - } - - b->m_low_is_set = true; - b->m_low = numeric_traits::from_string(bound_string[1]); - } else if (bound_type == "FR") { - b->m_free = true; - } else if (bound_type == "FX") { - if (bound_string.size() <= 1){ - set_m_ok_to_false(); - return; - } - - b->m_value_is_fixed = true; - b->m_fixed_value = numeric_traits::from_string(bound_string[1]); - } else if (bound_type == "PL") { - b->m_low_is_set = true; - b->m_low = 0; - } else if (bound_type == "MI") { - b->m_upper_is_set = true; - b->m_upper = 0; - } else { - (*m_message_stream) << "unexpected bound type " << bound_type << " at line " << m_line_number << std::endl; - set_m_ok_to_false(); - throw; - } - } - - void create_or_update_bound() { - const unsigned name_offset = 14; - lp_assert(m_line.size() >= 14); - vector bound_string = split_and_trim(m_line.substr(name_offset, m_line.size())); - - if (bound_string.empty()) { - set_m_ok_to_false(); - (*m_message_stream) << "error at line " << m_line_number << std::endl; - throw m_line; - } - - std::string name = bound_string[0]; - auto it = m_columns.find(name); - if (it == m_columns.end()){ - read_bound_by_columns(m_line.substr(14)); - return; - } - mps_reader::column * col = it->second; - bound * b = col->m_bound; - if (b == nullptr) { - col->m_bound = b = new bound(); - } - update_bound(b, bound_string); - } - - - - void read_range_by_columns(std::string rhsides) { - if (m_line.size() < 14) { - (*m_message_stream) << "line is too short" << std::endl; - (*m_message_stream) << m_line << std::endl; - (*m_message_stream) << "line number is " << m_line_number << std::endl; - set_m_ok_to_false(); - return; - } - // uph, let us try to work with columns - if (rhsides.size() >= 22) { - std::string ss = rhsides.substr(0, 8); - std::string row_name = trim(ss); - auto t = m_rows.find(row_name); - - if (t == m_rows.end()) { - (*m_message_stream) << "cannot find " << row_name << std::endl; - goto fail; - } else { - row * row = t->second; - row->m_range = numeric_traits::from_string(rhsides.substr(8)); - maybe_modify_current_row_and_add_row_for_range(row); - if (rhsides.size() > 24) { - rhsides = rhsides.substr(25); - if (rhsides.size() >= 22) { - read_range_by_columns(rhsides); - } - } - } - } else { - fail: - set_m_ok_to_false(); - (*m_message_stream) << "cannot understand this line" << std::endl; - (*m_message_stream) << "line = " << m_line << ", line number is " << m_line_number << std::endl; - return; - } - } - - - void read_range(vector & splitted_line){ - for (unsigned i = 1; i < splitted_line.size() - 1; i += 2) { - auto it = m_rows.find(splitted_line[i]); - if (it == m_rows.end()) { - read_range_by_columns(m_line.substr(14)); - return; - } - row * row = it->second; - row->m_range = numeric_traits::from_string(splitted_line[i + 1]); - maybe_modify_current_row_and_add_row_for_range(row); - } - } - - void maybe_modify_current_row_and_add_row_for_range(row * row_with_range) { - unsigned index= static_cast(m_rows.size() - m_cost_line_count); - std::string row_name = row_with_range->m_name + "_range"; - row * other_bound_range_row; - switch (row_with_range->m_type) { - case row_type::Greater_or_equal: - m_rows[row_name] = other_bound_range_row = new row(row_type::Less_or_equal, row_name, index); - other_bound_range_row->m_right_side = row_with_range->m_right_side + abs(row_with_range->m_range); - break; - case row_type::Less_or_equal: - m_rows[row_name] = other_bound_range_row = new row(row_type::Greater_or_equal, row_name, index); - other_bound_range_row->m_right_side = row_with_range->m_right_side - abs(row_with_range->m_range); - break; - case row_type::Equal: - if (row_with_range->m_range > 0) { - row_with_range->m_type = row_type::Greater_or_equal; // the existing row type change - m_rows[row_name] = other_bound_range_row = new row(row_type::Less_or_equal, row_name, index); - } else { // row->m_range < 0; - row_with_range->m_type = row_type::Less_or_equal; // the existing row type change - m_rows[row_name] = other_bound_range_row = new row(row_type::Greater_or_equal, row_name, index); - } - other_bound_range_row->m_right_side = row_with_range->m_right_side + row_with_range->m_range; - break; - default: - (*m_message_stream) << "unexpected bound type " << row_with_range->m_type << " at line " << m_line_number << std::endl; - set_m_ok_to_false(); - throw; - } - - for (auto s : row_with_range->m_row_columns) { - lp_assert(m_columns.find(s.first) != m_columns.end()); - other_bound_range_row->m_row_columns[s.first] = s.second; - } - } - - void add_row() { - if (m_line.length() < 2) { - return; - } - - m_line = trim(m_line); - char c = m_line[0]; - m_line = m_line.substr(1); - m_line = trim(m_line); - add_row(c); - } - - void add_row(char c) { - unsigned index= static_cast(m_rows.size() - m_cost_line_count); - switch (c) { - case 'E': - m_rows[m_line] = new row(row_type::Equal, m_line, index); - break; - case 'L': - m_rows[m_line] = new row(row_type::Less_or_equal, m_line, index); - break; - case 'G': - m_rows[m_line] = new row(row_type::Greater_or_equal, m_line, index); - break; - case 'N': - m_rows[m_line] = new row(row_type::Cost, m_line, index); - m_cost_row_name = m_line; - m_cost_line_count++; - break; - } - } - unsigned range_count() { - unsigned ret = 0; - for (auto s : m_rows) { - if (s.second->m_range != 0) { - ret++; - } - } - return ret; - } - - /* - If rhs is a constraint's right-hand-side value and range is the constraint's range value, then the range interval is defined according to the following table: - sense interval - G [rhs, rhs + |range|] - L [rhs - |range|, rhs] - E [rhs, rhs + |range|] if range > 0, - [rhs - |range|, rhs] if range < 0 - where |range| is range's absolute value. - */ - - lp_relation get_relation_from_row(row_type rt) { - switch (rt) { - case mps_reader::Less_or_equal: return lp_relation::Less_or_equal; - case mps_reader::Greater_or_equal: return lp_relation::Greater_or_equal; - case mps_reader::Equal: return lp_relation::Equal; - default: - (*m_message_stream) << "Unexpected rt " << rt << std::endl; - set_m_ok_to_false(); - throw; - } - } - - unsigned solver_row_count() { - return m_rows.size() - m_cost_line_count + range_count(); - } - - void fill_solver_on_row(row * row, lp_solver *solver) { - if (row->m_name != m_cost_row_name) { - solver->add_constraint(get_relation_from_row(row->m_type), row->m_right_side, row->m_index); - for (auto s : row->m_row_columns) { - lp_assert(m_columns.find(s.first) != m_columns.end()); - solver->set_row_column_coefficient(row->m_index, m_columns[s.first]->m_index, s.second); - } - } else { - set_solver_cost(row, solver); - } - } - - T abs(T & t) { return t < numeric_traits::zero() ? -t: t; } - - void fill_solver_on_rows(lp_solver * solver) { - for (auto row_it : m_rows) { - fill_solver_on_row(row_it.second, solver); - } - } - - - void fill_solver_on_columns(lp_solver * solver){ - for (auto s : m_columns) { - mps_reader::column * col = s.second; - unsigned index = col->m_index; - set_boundary_for_column(index, col->m_bound, solver); - // optional call - solver->give_symbolic_name_to_column(col->m_name, col->m_index); - } - } - - void fill_solver(lp_solver *solver) { - fill_solver_on_rows(solver); - fill_solver_on_columns(solver); - } - - void set_solver_cost(row * row, lp_solver *solver) { - for (auto s : row->m_row_columns) { - std::string name = s.first; - lp_assert(m_columns.find(name) != m_columns.end()); - mps_reader::column * col = m_columns[name]; - solver->set_cost_for_column(col->m_index, s.second); - } - } - -public: - - void set_message_stream(std::ostream * o) { - lp_assert(o != nullptr); - m_message_stream = o; - } - vector column_names() { - vector v; - for (auto s : m_columns) { - v.push_back(s.first); - } - return v; - } - - ~mps_reader() { - for (auto s : m_rows) { - delete s.second; - } - for (auto s : m_columns) { - auto col = s.second; - delete col->m_bound; - delete col; - } - } - - mps_reader(const std::string & file_name): - m_is_OK(true), - m_file_name(file_name), - m_file_stream(file_name), - m_cost_line_count(0), - m_line_number(0), - m_message_stream(& std::cout) {} - void read() { - if (!m_file_stream.is_open()){ - set_m_ok_to_false(); - return; - } - - read_name(); - read_rows(); - read_columns(); - read_rhs(); - if (m_line.find("BOUNDS") == 0) { - read_bounds(); - read_ranges(); - } else if (m_line.find("RANGES") == 0) { - read_ranges(); - read_bounds(); - } - } - - bool is_ok() { - return m_is_OK; - } - - lp_solver * create_solver(bool dual) { - lp_solver * solver = dual? (lp_solver*)new lp_dual_simplex() : new lp_primal_simplex(); - fill_solver(solver); - return solver; - } - - lconstraint_kind get_lar_relation_from_row(row_type rt) { - switch (rt) { - case Less_or_equal: return LE; - case Greater_or_equal: return GE; - case Equal: return EQ; - default: - (*m_message_stream) << "Unexpected rt " << rt << std::endl; - set_m_ok_to_false(); - throw; - } - } - - unsigned get_var_index(std::string s) { - auto it = m_names_to_var_index.find(s); - if (it != m_names_to_var_index.end()) - return it->second; - unsigned ret = static_cast(m_names_to_var_index.size()); - m_names_to_var_index[s] = ret; - return ret; - } - - void fill_lar_solver_on_row(row * row, lar_solver *solver, int row_index) { - if (row->m_name != m_cost_row_name) { - auto kind = get_lar_relation_from_row(row->m_type); - vector> ls; - for (auto s : row->m_row_columns) { - var_index i = solver->add_var(get_var_index(s.first), false); - ls.push_back(std::make_pair(s.second, i)); - } - unsigned j = solver->add_term(ls, row_index); - solver->add_var_bound(j, kind, row->m_right_side); - } else { - // ignore the cost row - } - } - - - void fill_lar_solver_on_rows(lar_solver * solver) { - int row_index = 0; - for (auto row_it : m_rows) { - fill_lar_solver_on_row(row_it.second, solver, row_index++); - } - } - - void create_low_constraint_for_var(column* col, bound * b, lar_solver *solver) { - var_index i = solver->add_var(col->m_index, false); - solver->add_var_bound(i, GE, b->m_low); - } - - void create_upper_constraint_for_var(column* col, bound * b, lar_solver *solver) { - var_index i = solver->add_var(col->m_index, false); - solver->add_var_bound(i, LE, b->m_upper); - } - - void create_equality_contraint_for_var(column* col, bound * b, lar_solver *solver) { - var_index i = solver->add_var(col->m_index, false); - solver->add_var_bound(i, LE, b->m_fixed_value); - solver->add_var_bound(i, GE, b->m_fixed_value); - } - - void fill_lar_solver_on_columns(lar_solver * solver) { - for (auto s : m_columns) { - mps_reader::column * col = s.second; - solver->add_var(col->m_index, false); - auto b = col->m_bound; - if (b == nullptr) return; - - if (b->m_free) continue; - - if (b->m_low_is_set) { - create_low_constraint_for_var(col, b, solver); - } - if (b->m_upper_is_set) { - create_upper_constraint_for_var(col, b, solver); - } - if (b->m_value_is_fixed) { - create_equality_contraint_for_var(col, b, solver); - } - } - } - - - void fill_lar_solver(lar_solver * solver) { - fill_lar_solver_on_columns(solver); - fill_lar_solver_on_rows(solver); - } - - lar_solver * create_lar_solver() { - lar_solver * solver = new lar_solver(); - fill_lar_solver(solver); - return solver; - } -}; -} diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index d9b74f162f9..c0e9c85050f 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -28,7 +28,6 @@ add_executable(shell opt_frontend.cpp smtlib_frontend.cpp z3_log_frontend.cpp - lp_frontend.cpp # FIXME: shell should really link against libz3 but it can't due to requiring # use of some hidden symbols. Also libz3 has the ``api_dll`` component which # we don't want (I think). diff --git a/src/shell/lp_frontend.cpp b/src/shell/lp_frontend.cpp deleted file mode 100644 index 8d6425533c8..00000000000 --- a/src/shell/lp_frontend.cpp +++ /dev/null @@ -1,109 +0,0 @@ -/*++ -Copyright (c) 2016 Microsoft Corporation - -Author: - - Lev Nachmanson 2016-10-27 - ---*/ - -#include "math/lp/lp_settings.h" -#include "math/lp/mps_reader.h" -#include "util/timeout.h" -#include "util/cancel_eh.h" -#include "util/scoped_timer.h" -#include "util/rlimit.h" -#include "util/gparams.h" -#include "util/mutex.h" -#include -#include -#include "smt/params/smt_params_helper.hpp" - -namespace { -static mutex *display_stats_mux = new mutex; - -static lp::lp_solver* g_solver = nullptr; - -static void display_statistics() { - lock_guard lock(*display_stats_mux); - if (g_solver && g_solver->settings().print_statistics) { - // TBD display relevant information about statistics - } -} - -static void STD_CALL on_ctrl_c(int) { - signal (SIGINT, SIG_DFL); - display_statistics(); - raise(SIGINT); -} - -static void on_timeout() { - display_statistics(); - _Exit(0); -} - -struct front_end_resource_limit : public lp::lp_resource_limit { - reslimit& m_reslim; - - front_end_resource_limit(reslimit& lim): - m_reslim(lim) - {} - - bool get_cancel_flag() override { return !m_reslim.inc(); } -}; - -void run_solver(smt_params_helper & params, char const * mps_file_name) { - - reslimit rlim; - unsigned timeout = gparams::get_ref().get_uint("timeout", 0); - unsigned rlimit = gparams::get_ref().get_uint("rlimit", 0); - front_end_resource_limit lp_limit(rlim); - - scoped_rlimit _rlimit(rlim, rlimit); - cancel_eh eh(rlim); - scoped_timer timer(timeout, &eh); - - std::string fn(mps_file_name); - lp::mps_reader reader(fn); - reader.set_message_stream(&std::cout); // can be redirected - reader.read(); - if (!reader.is_ok()) { - std::cerr << "cannot process " << mps_file_name << std::endl; - return; - } - lp::lp_solver * solver = reader.create_solver(false); // false - to create the primal solver - solver->settings().set_resource_limit(lp_limit); - g_solver = solver; - if (params.arith_min()) { - solver->flip_costs(); - } - solver->settings().set_message_ostream(&std::cout); - solver->settings().report_frequency = params.arith_rep_freq(); - solver->settings().print_statistics = params.arith_print_stats(); - solver->settings().set_simplex_strategy(lp:: simplex_strategy_enum::lu); - - solver->find_maximal_solution(); - - *(solver->settings().get_message_ostream()) << "status is " << lp_status_to_string(solver->get_status()) << std::endl; - if (solver->get_status() == lp::lp_status::OPTIMAL) { - if (params.arith_min()) { - solver->flip_costs(); - } - solver->print_model(std::cout); - } - - display_statistics(); - g_solver = nullptr; - delete solver; -} -} - -unsigned read_mps_file(char const * mps_file_name) { - signal(SIGINT, on_ctrl_c); - register_on_timeout_proc(on_timeout); - smt_params_helper p; - param_descrs r; - p.collect_param_descrs(r); - run_solver(p, mps_file_name); - return 0; -} diff --git a/src/shell/lp_frontend.h b/src/shell/lp_frontend.h deleted file mode 100644 index b24be811f18..00000000000 --- a/src/shell/lp_frontend.h +++ /dev/null @@ -1,7 +0,0 @@ -/* - Copyright (c) 2013 Microsoft Corporation. All rights reserved. - - Author: Lev Nachmanson -*/ -#pragma once -unsigned read_mps_file(char const * mps_file_name); diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 4c26d91d968..26325d3d0a2 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -37,14 +37,13 @@ Revision History: #include "util/gparams.h" #include "util/env_params.h" #include "util/file_path.h" -#include "shell/lp_frontend.h" #include "shell/drat_frontend.h" #if defined( _WINDOWS ) && defined( __MINGW32__ ) && ( defined( __GNUG__ ) || defined( __clang__ ) ) #include #endif -typedef enum { IN_UNSPECIFIED, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_LP, IN_Z3_LOG, IN_MPS, IN_DRAT } input_kind; +typedef enum { IN_UNSPECIFIED, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_LP, IN_Z3_LOG, IN_DRAT } input_kind; static char const * g_input_file = nullptr; static char const * g_drat_input_file = nullptr; @@ -377,10 +376,6 @@ int STD_CALL main(int argc, char ** argv) { else if (strcmp(ext, "smt2") == 0) { g_input_kind = IN_SMTLIB_2; } - else if (strcmp(ext, "mps") == 0 || strcmp(ext, "sif") == 0 || - strcmp(ext, "MPS") == 0 || strcmp(ext, "SIF") == 0) { - g_input_kind = IN_MPS; - } } } switch (g_input_kind) { @@ -406,9 +401,6 @@ int STD_CALL main(int argc, char ** argv) { case IN_Z3_LOG: replay_z3_log(g_input_file); break; - case IN_MPS: - return_value = read_mps_file(g_input_file); - break; case IN_DRAT: return_value = read_drat(g_drat_input_file); break; diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index c82cdd0a4b4..984c7b4bb0c 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -34,7 +34,6 @@ #include #include "math/lp/lp_utils.h" #include "math/lp/lp_primal_simplex.h" -#include "math/lp/mps_reader.h" #include "test/lp/smt_reader.h" #include "math/lp/binary_heap_priority_queue.h" #include "test/lp/argument_parser.h" @@ -59,6 +58,71 @@ #include "math/lp/cross_nested.h" #include "math/lp/int_cube.h" #include "math/lp/emonics.h" + +bool my_white_space(const char & a) { + return a == ' ' || a == '\t'; +} +size_t number_of_whites(const std::string & s) { + size_t i = 0; + for(;i < s.size(); i++) + if (!my_white_space(s[i])) return i; + return i; +} +size_t number_of_whites_from_end(const std::string & s) { + size_t ret = 0; + for(int i = static_cast(s.size()) - 1;i >= 0; i--) + if (my_white_space(s[i])) ret++;else break; + + return ret; +} + + +std::string <rim(std::string &s) { + s.erase(0, number_of_whites(s)); + return s; +} + + + + + // trim from end +inline std::string &rtrim(std::string &s) { + // s.erase(std::find_if(s.rbegin(), s.rend(), std::not1(std::ptr_fun(std::isspace))).base(), s.end()); + s.erase(s.end() - number_of_whites_from_end(s), s.end()); + return s; +} + // trim from both ends +inline std::string &trim(std::string &s) { + return ltrim(rtrim(s)); +} + + +vector string_split(const std::string &source, const char *delimiter, bool keep_empty) { + vector results; + size_t prev = 0; + size_t next = 0; + while ((next = source.find_first_of(delimiter, prev)) != std::string::npos) { + if (keep_empty || (next - prev != 0)) { + results.push_back(source.substr(prev, next - prev)); + } + prev = next + 1; + } + if (prev < source.size()) { + results.push_back(source.substr(prev)); + } + return results; +} + +vector split_and_trim(const std::string &line) { + auto split = string_split(line, " \t", false); + vector ret; + for (auto s : split) { + ret.push_back(trim(s)); + } + return ret; +} + + namespace nla { void test_horner(); void test_monics(); @@ -1408,156 +1472,12 @@ void setup_solver(unsigned time_limit, bool look_for_min, argument_parser & args bool values_are_one_percent_close(double a, double b); -void print_x(mps_reader & reader, lp_solver * solver) { - for (const auto & name : reader.column_names()) { - std::cout << name << "=" << solver->get_column_value_by_name(name) << ' '; - } - std::cout << std::endl; -} -void compare_solutions(mps_reader & reader, lp_solver * solver, lp_solver * solver0) { - for (const auto & name : reader.column_names()) { - double a = solver->get_column_value_by_name(name); - double b = solver0->get_column_value_by_name(name); - if (!values_are_one_percent_close(a, b)) { - std::cout << "different values for " << name << ":" << a << " and " << b << std::endl; - } - } -} -void solve_mps_double(std::string file_name, bool look_for_min, unsigned time_limit, bool dual, bool compare_with_primal, argument_parser & args_parser) { - mps_reader reader(file_name); - reader.read(); - if (!reader.is_ok()) { - std::cout << "cannot process " << file_name << std::endl; - return; - } - - lp_solver * solver = reader.create_solver(dual); - setup_solver(time_limit, look_for_min, args_parser, solver); - stopwatch sw; - sw.start(); - if (dual) { - std::cout << "solving for dual" << std::endl; - } - solver->find_maximal_solution(); - sw.stop(); - double span = sw.get_seconds(); - std::cout << "Status: " << lp_status_to_string(solver->get_status()) << std::endl; - if (solver->get_status() == lp_status::OPTIMAL) { - if (reader.column_names().size() < 20) { - print_x(reader, solver); - } - double cost = solver->get_current_cost(); - if (look_for_min) { - cost = -cost; - } - std::cout << "cost = " << cost << std::endl; - } - std::cout << "processed in " << span / 1000.0 << " seconds, running for " << solver->m_total_iterations << " iterations" << " one iter for " << (double)span/solver->m_total_iterations << " ms" << std::endl; - if (compare_with_primal) { - auto * primal_solver = reader.create_solver(false); - setup_solver(time_limit, look_for_min, args_parser, primal_solver); - primal_solver->find_maximal_solution(); - if (solver->get_status() != primal_solver->get_status()) { - std::cout << "statuses are different: dual " << lp_status_to_string(solver->get_status()) << " primal = " << lp_status_to_string(primal_solver->get_status()) << std::endl; - } else { - if (solver->get_status() == lp_status::OPTIMAL) { - double cost = solver->get_current_cost(); - if (look_for_min) { - cost = -cost; - } - double primal_cost = primal_solver->get_current_cost(); - if (look_for_min) { - primal_cost = -primal_cost; - } - std::cout << "primal cost = " << primal_cost << std::endl; - if (!values_are_one_percent_close(cost, primal_cost)) { - compare_solutions(reader, primal_solver, solver); - print_x(reader, primal_solver); - std::cout << "dual cost is " << cost << ", but primal cost is " << primal_cost << std::endl; - lp_assert(false); - } - } - } - delete primal_solver; - } - delete solver; -} - -void solve_mps_rational(std::string file_name, bool look_for_min, unsigned time_limit, bool dual, argument_parser & args_parser) { - mps_reader reader(file_name); - reader.read(); - if (reader.is_ok()) { - auto * solver = reader.create_solver(dual); - setup_solver(time_limit, look_for_min, args_parser, solver); - stopwatch sw; - sw.start(); - solver->find_maximal_solution(); - std::cout << "Status: " << lp_status_to_string(solver->get_status()) << std::endl; - - if (solver->get_status() == lp_status::OPTIMAL) { - // for (auto name: reader.column_names()) { - // std::cout << name << "=" << solver->get_column_value_by_name(name) << ' '; - // } - lp::mpq cost = solver->get_current_cost(); - if (look_for_min) { - cost = -cost; - } - std::cout << "cost = " << cost.get_double() << std::endl; - } - std::cout << "processed in " << sw.get_current_seconds() / 1000.0 << " seconds, running for " << solver->m_total_iterations << " iterations" << std::endl; - delete solver; - } else { - std::cout << "cannot process " << file_name << std::endl; - } -} void get_time_limit_and_max_iters_from_parser(argument_parser & args_parser, unsigned & time_limit); // forward definition -void solve_mps(std::string file_name, bool look_for_min, unsigned time_limit, bool solve_for_rational, bool dual, bool compare_with_primal, argument_parser & args_parser) { - if (!solve_for_rational) { - std::cout << "solving " << file_name << std::endl; - solve_mps_double(file_name, look_for_min, time_limit, dual, compare_with_primal, args_parser); - } - else { - std::cout << "solving " << file_name << " in rationals " << std::endl; - solve_mps_rational(file_name, look_for_min, time_limit, dual, args_parser); - } -} -void solve_mps(std::string file_name, argument_parser & args_parser) { - bool look_for_min = args_parser.option_is_used("--min"); - unsigned time_limit; - bool solve_for_rational = args_parser.option_is_used("--mpq"); - bool dual = args_parser.option_is_used("--dual"); - bool compare_with_primal = args_parser.option_is_used("--compare_with_primal"); - get_time_limit_and_max_iters_from_parser(args_parser, time_limit); - solve_mps(file_name, look_for_min, time_limit, solve_for_rational, dual, compare_with_primal, args_parser); -} - -void solve_mps_in_rational(std::string file_name, bool dual, argument_parser & /*args_parser*/) { - std::cout << "solving " << file_name << std::endl; - - mps_reader reader(file_name); - reader.read(); - if (reader.is_ok()) { - auto * solver = reader.create_solver(dual); - solver->find_maximal_solution(); - std::cout << "status is " << lp_status_to_string(solver->get_status()) << std::endl; - if (solver->get_status() == lp_status::OPTIMAL) { - if (reader.column_names().size() < 20) { - for (const auto & name : reader.column_names()) { - std::cout << name << "=" << solver->get_column_value_by_name(name).get_double() << ' '; - } - } - std::cout << std::endl << "cost = " << numeric_traits::get_double(solver->get_current_cost()) << std::endl; - } - delete solver; - } else { - std::cout << "cannot process " << file_name << std::endl; - } -} void test_upair_queue() { int n = 10; @@ -1626,53 +1546,6 @@ void test_binary_priority_queue() { std::cout << " done" << std::endl; } -bool solution_is_feasible(std::string file_name, const std::unordered_map & solution) { - mps_reader reader(file_name); - reader.read(); - if (reader.is_ok()) { - lp_primal_simplex * solver = static_cast *>(reader.create_solver(false)); - return solver->solution_is_feasible(solution); - } - return false; -} - - -void solve_mps_with_known_solution(std::string file_name, std::unordered_map * solution, lp_status status, bool dual) { - std::cout << "solving " << file_name << std::endl; - mps_reader reader(file_name); - reader.read(); - if (reader.is_ok()) { - auto * solver = reader.create_solver(dual); - solver->find_maximal_solution(); - std::cout << "status is " << lp_status_to_string(solver->get_status()) << std::endl; - if (status != solver->get_status()){ - std::cout << "status should be " << lp_status_to_string(status) << std::endl; - lp_assert(status == solver->get_status()); - throw "status is wrong"; - } - if (solver->get_status() == lp_status::OPTIMAL) { - std::cout << "cost = " << solver->get_current_cost() << std::endl; - if (solution != nullptr) { - for (auto it : *solution) { - if (fabs(it.second - solver->get_column_value_by_name(it.first)) >= 0.000001) { - std::cout << "expected:" << it.first << "=" << - it.second <<", got " << solver->get_column_value_by_name(it.first) << std::endl; - } - lp_assert(fabs(it.second - solver->get_column_value_by_name(it.first)) < 0.000001); - } - } - if (reader.column_names().size() < 20) { - for (const auto & name : reader.column_names()) { - std::cout << name << "=" << solver->get_column_value_by_name(name) << ' '; - } - std::cout << std::endl; - } - } - delete solver; - } else { - std::cout << "cannot process " << file_name << std::endl; - } -} int get_random_rows() { return 5 + my_random() % 2; @@ -1896,140 +1769,9 @@ void find_dir_and_file_name(std::string a, std::string & dir, std::string& fn) { // std::cout << "fn = " << fn << std::endl; } -void process_test_file(std::string test_dir, std::string test_file_name, argument_parser & args_parser, std::string out_dir, unsigned max_iters, unsigned time_limit, unsigned & successes, unsigned & failures, unsigned & inconclusives); - -void solve_some_mps(argument_parser & args_parser) { - unsigned max_iters = UINT_MAX, time_limit = UINT_MAX; - get_time_limit_and_max_iters_from_parser(args_parser, time_limit); - unsigned successes = 0; - unsigned failures = 0; - unsigned inconclusives = 0; - std::set minimums; - vector file_names; - fill_file_names(file_names, minimums); - bool solve_for_rational = args_parser.option_is_used("--mpq"); - bool dual = args_parser.option_is_used("--dual"); - bool compare_with_primal = args_parser.option_is_used("--compare_with_primal"); - bool compare_with_glpk = args_parser.option_is_used("--compare_with_glpk"); - if (compare_with_glpk) { - std::string out_dir = args_parser.get_option_value("--out_dir"); - if (out_dir.size() == 0) { - out_dir = "/tmp/test"; - } - test_out_dir(out_dir); - for (auto& a : file_names) { - try { - std::string file_dir; - std::string file_name; - find_dir_and_file_name(a, file_dir, file_name); - process_test_file(file_dir, file_name, args_parser, out_dir, max_iters, time_limit, successes, failures, inconclusives); - } - catch(const char *s){ - std::cout<< "exception: "<< s << std::endl; - } - } - std::cout << "comparing with glpk: successes " << successes << ", failures " << failures << ", inconclusives " << inconclusives << std::endl; - return; - } - if (!solve_for_rational) { - solve_mps(file_names[6], false, time_limit, false, dual, compare_with_primal, args_parser); - solve_mps_with_known_solution(file_names[3], nullptr, lp_status::INFEASIBLE, dual); // chvatal: 135(d) - std::unordered_map sol; - sol["X1"] = 0; - sol["X2"] = 6; - sol["X3"] = 0; - sol["X4"] = 15; - sol["X5"] = 2; - sol["X6"] = 1; - sol["X7"] = 1; - sol["X8"] = 0; - solve_mps_with_known_solution(file_names[9], &sol, lp_status::OPTIMAL, dual); - solve_mps_with_known_solution(file_names[0], &sol, lp_status::OPTIMAL, dual); - sol.clear(); - sol["X1"] = 25.0/14.0; - // sol["X2"] = 0; - // sol["X3"] = 0; - // sol["X4"] = 0; - // sol["X5"] = 0; - // sol["X6"] = 0; - // sol["X7"] = 9.0/14.0; - solve_mps_with_known_solution(file_names[5], &sol, lp_status::OPTIMAL, dual); // chvatal: 135(e) - solve_mps_with_known_solution(file_names[4], &sol, lp_status::OPTIMAL, dual); // chvatal: 135(e) - solve_mps_with_known_solution(file_names[2], nullptr, lp_status::UNBOUNDED, dual); // chvatal: 135(c) - solve_mps_with_known_solution(file_names[1], nullptr, lp_status::UNBOUNDED, dual); // chvatal: 135(b) - solve_mps(file_names[8], false, time_limit, false, dual, compare_with_primal, args_parser); - // return; - for (auto& s : file_names) { - try { - solve_mps(s, minimums.find(s) != minimums.end(), time_limit, false, dual, compare_with_primal, args_parser); - } - catch(const char *s){ - std::cout<< "exception: "<< s << std::endl; - } - } - } else { - // unsigned i = 0; - for (auto& s : file_names) { - // if (i++ > 9) return; - try { - solve_mps_in_rational(s, dual, args_parser); - } - catch(const char *s){ - std::cout<< "exception: "<< s << std::endl; - } - } - } -} -#endif - -void solve_rational() { - lp_primal_simplex solver; - solver.add_constraint(lp_relation::Equal, lp::mpq(7), 0); - solver.add_constraint(lp_relation::Equal, lp::mpq(-3), 1); - - // setting the cost - int cost[] = {-3, -1, -1, 2, -1, 1, 1, -4}; - std::string var_names[8] = {"x1", "x2", "x3", "x4", "x5", "x6", "x7", "x8"}; - for (unsigned i = 0; i < 8; i++) { - solver.set_cost_for_column(i, lp::mpq(cost[i])); - solver.give_symbolic_name_to_column(var_names[i], i); - } - - int row0[] = {1, 0, 3, 1, -5, -2 , 4, -6}; - for (unsigned i = 0; i < 8; i++) { - solver.set_row_column_coefficient(0, i, lp::mpq(row0[i])); - } - - int row1[] = {0, 1, -2, -1, 4, 1, -3, 5}; - for (unsigned i = 0; i < 8; i++) { - solver.set_row_column_coefficient(1, i, lp::mpq(row1[i])); - } - - int bounds[] = {8, 6, 4, 15, 2, 10, 10, 3}; - for (unsigned i = 0; i < 8; i++) { - solver.set_lower_bound(i, lp::mpq(0)); - solver.set_upper_bound(i, lp::mpq(bounds[i])); - } - - std::unordered_map expected_sol; - expected_sol["x1"] = lp::mpq(0); - expected_sol["x2"] = lp::mpq(6); - expected_sol["x3"] = lp::mpq(0); - expected_sol["x4"] = lp::mpq(15); - expected_sol["x5"] = lp::mpq(2); - expected_sol["x6"] = lp::mpq(1); - expected_sol["x7"] = lp::mpq(1); - expected_sol["x8"] = lp::mpq(0); - solver.find_maximal_solution(); - lp_assert(solver.get_status() == lp_status::OPTIMAL); -#ifdef Z3DEBUG - for (const auto & it : expected_sol) { - (void)it; - lp_assert(it.second == solver.get_column_value_by_name(it.first)); - } #endif -} + std::string read_line(bool & end, std::ifstream & file) { @@ -2047,49 +1789,6 @@ bool contains(std::string const & s, char const * pattern) { } -std::unordered_map * get_solution_from_glpsol_output(std::string & file_name) { - std::ifstream file(file_name); - if (!file.is_open()){ - std::cerr << "cannot open " << file_name << std::endl; - return nullptr; - } - std::string s; - bool end; - do { - s = read_line(end, file); - if (end) { - std::cerr << "unexpected file end " << file_name << std::endl; - return nullptr; - } - if (contains(s, "Column name")){ - break; - } - } while (true); - - read_line(end, file); - if (end) { - std::cerr << "unexpected file end " << file_name << std::endl; - return nullptr; - } - - auto ret = new std::unordered_map(); - - do { - s = read_line(end, file); - if (end) { - std::cerr << "unexpected file end " << file_name << std::endl; - return nullptr; - } - auto split = string_split(s, " \t", false); - if (split.empty()) { - return ret; - } - - lp_assert(split.size() > 3); - (*ret)[split[1]] = atof(split[3].c_str()); - } while (true); -} - void test_init_U() { @@ -2189,7 +1888,6 @@ void setup_args_parser(argument_parser & parser) { parser.add_option_with_help_string("--test_lp_0", "solve a small lp"); parser.add_option_with_help_string("--solve_some_mps", "solves a list of mps problems"); parser.add_option_with_after_string_with_help("--test_file_directory", "loads files from the directory for testing"); - parser.add_option_with_help_string("--compare_with_glpk", "compares the results by running glpsol"); parser.add_option_with_after_string_with_help("--out_dir", "setting the output directory for tests, if not set /tmp is used"); parser.add_option_with_help_string("--dual", "using the dual simplex solver"); parser.add_option_with_help_string("--compare_with_primal", "using the primal simplex solver for comparison"); @@ -2360,237 +2058,9 @@ std::string get_status(std::string file_name) { throw 0; } -// returns true if the costs should be compared too -bool compare_statuses(std::string glpk_out_file_name, std::string lp_out_file_name, unsigned & successes, unsigned & failures) { - std::string glpk_status = get_status(glpk_out_file_name); - std::string lp_tst_status = get_status(lp_out_file_name); - if (glpk_status != lp_tst_status) { - if (glpk_status == "UNDEFINED" && (lp_tst_status == "UNBOUNDED" || lp_tst_status == "INFEASIBLE")) { - successes++; - return false; - } else { - std::cout << "glpsol and lp_tst disagree: glpsol status is " << glpk_status; - std::cout << " but lp_tst status is " << lp_tst_status << std::endl; - failures++; - return false; - } - } - return lp_tst_status == "OPTIMAL"; -} -double get_glpk_cost(std::string file_name) { - std::ifstream f(file_name); - if (!f.is_open()) { - std::cout << "cannot open " << file_name << std::endl; - throw 0; - } - std::string str; - while (getline(f, str)) { - if (str.find("Objective") != std::string::npos) { - vector tokens = split_and_trim(str); - if (tokens.size() != 5) { - std::cout << "unexpected Objective std::string " << str << std::endl; - throw 0; - } - return atof(tokens[3].c_str()); - } - } - std::cout << "cannot find the Objective line in " << file_name << std::endl; - throw 0; -} -double get_lp_tst_cost(std::string file_name) { - std::ifstream f(file_name); - if (!f.is_open()) { - std::cout << "cannot open " << file_name << std::endl; - throw 0; - } - std::string str; - std::string cost_string; - while (getline(f, str)) { - if (str.find("cost") != std::string::npos) { - cost_string = str; - } - } - if (cost_string.empty()) { - std::cout << "cannot find the cost line in " << file_name << std::endl; - throw 0; - } - - vector tokens = split_and_trim(cost_string); - if (tokens.size() != 3) { - std::cout << "unexpected cost string " << cost_string << std::endl; - throw 0; - } - return atof(tokens[2].c_str()); -} - -bool values_are_one_percent_close(double a, double b) { - double maxval = std::max(fabs(a), fabs(b)); - if (maxval < 0.000001) { - return true; - } - - double one_percent = maxval / 100; - return fabs(a - b) <= one_percent; -} - -// returns true if both are optimal -void compare_costs(std::string glpk_out_file_name, - std::string lp_out_file_name, - unsigned & successes, - unsigned & failures) { - double a = get_glpk_cost(glpk_out_file_name); - double b = get_lp_tst_cost(lp_out_file_name); - - if (values_are_one_percent_close(a, b)) { - successes++; - } else { - failures++; - std::cout << "glpsol cost is " << a << " lp_tst cost is " << b << std::endl; - } -} - - - -void compare_with_glpk(std::string glpk_out_file_name, std::string lp_out_file_name, unsigned & successes, unsigned & failures, std::string /*lp_file_name*/) { -#ifdef CHECK_GLPK_SOLUTION - std::unordered_map * solution_table = get_solution_from_glpsol_output(glpk_out_file_name); - if (solution_is_feasible(lp_file_name, *solution_table)) { - std::cout << "glpk solution is feasible" << std::endl; - } else { - std::cout << "glpk solution is infeasible" << std::endl; - } - delete solution_table; -#endif - if (compare_statuses(glpk_out_file_name, lp_out_file_name, successes, failures)) { - compare_costs(glpk_out_file_name, lp_out_file_name, successes, failures); - } -} -void test_lar_on_file(std::string file_name, argument_parser & args_parser); - -void process_test_file(std::string test_dir, std::string test_file_name, argument_parser & args_parser, std::string out_dir, unsigned max_iters, unsigned time_limit, unsigned & successes, unsigned & failures, unsigned & inconclusives) { - bool use_mpq = args_parser.option_is_used("--mpq"); - bool minimize = args_parser.option_is_used("--min"); - std::string full_lp_tst_out_name = out_dir + "/" + create_output_file_name(minimize, test_file_name, use_mpq); - - std::string input_file_name = test_dir + "/" + test_file_name; - if (input_file_name[input_file_name.size() - 1] == '~') { - // std::cout << "ignoring " << input_file_name << std::endl; - return; - } - std::cout <<"processing " << input_file_name << std::endl; - - std::ofstream out(full_lp_tst_out_name); - if (!out.is_open()) { - std::cout << "cannot open file " << full_lp_tst_out_name << std::endl; - throw 0; - } - std::streambuf *coutbuf = std::cout.rdbuf(); // save old buffer - std::cout.rdbuf(out.rdbuf()); // redirect std::cout to dir_entry->d_name! - bool dual = args_parser.option_is_used("--dual"); - try { - if (args_parser.option_is_used("--lar")) - test_lar_on_file(input_file_name, args_parser); - else - solve_mps(input_file_name, minimize, time_limit, use_mpq, dual, false, args_parser); - } - catch(...) { - std::cout << "catching the failure" << std::endl; - failures++; - std::cout.rdbuf(coutbuf); // reset to standard output again - return; - } - std::cout.rdbuf(coutbuf); // reset to standard output again - - if (args_parser.option_is_used("--compare_with_glpk")) { - std::string glpk_out_file_name = out_dir + "/" + create_output_file_name_for_glpsol(minimize, std::string(test_file_name)); - int glpk_exit_code = run_glpk(input_file_name, glpk_out_file_name, minimize, time_limit); - if (glpk_exit_code != 0) { - std::cout << "glpk failed" << std::endl; - inconclusives++; - } else { - compare_with_glpk(glpk_out_file_name, full_lp_tst_out_name, successes, failures, input_file_name); - } - } -} -/* - int my_readdir(DIR *dirp, struct dirent * - #ifndef LEAN_WINDOWS - entry - #endif - , struct dirent **result) { - #ifdef LEAN_WINDOWS - *result = readdir(dirp); // NOLINT - return *result != nullptr? 0 : 1; - #else - return readdir_r(dirp, entry, result); - #endif - } -*/ -/* - vector> get_file_list_of_dir(std::string test_file_dir) { - DIR *dir; - if ((dir = opendir(test_file_dir.c_str())) == nullptr) { - std::cout << "Cannot open directory " << test_file_dir << std::endl; - throw 0; - } - vector> ret; - struct dirent entry; - struct dirent* result; - int return_code; - for (return_code = my_readdir(dir, &entry, &result); - #ifndef LEAN_WINDOWS - result != nullptr && - #endif - return_code == 0; - return_code = my_readdir(dir, &entry, &result)) { - DIR *tmp_dp = opendir(result->d_name); - struct stat file_record; - if (tmp_dp == nullptr) { - std::string s = test_file_dir+ "/" + result->d_name; - int stat_ret = stat(s.c_str(), & file_record); - if (stat_ret!= -1) { - ret.push_back(make_pair(result->d_name, file_record.st_size)); - } else { - perror("stat"); - exit(1); - } - } else { - closedir(tmp_dp); - } - } - closedir(dir); - return ret; - } -*/ -/* - struct file_size_comp { - unordered_map& m_file_sizes; - file_size_comp(unordered_map& fs) :m_file_sizes(fs) {} - int operator()(std::string a, std::string b) { - std::cout << m_file_sizes.size() << std::endl; - std::cout << a << std::endl; - std::cout << b << std::endl; - - auto ls = m_file_sizes.find(a); - std::cout << "fa" << std::endl; - auto rs = m_file_sizes.find(b); - std::cout << "fb" << std::endl; - if (ls != m_file_sizes.end() && rs != m_file_sizes.end()) { - std::cout << "fc " << std::endl; - int r = (*ls < *rs? -1: (*ls > *rs)? 1 : 0); - std::cout << "calc r " << std::endl; - return r; - } else { - std::cout << "sc " << std::endl; - return 0; - } - } - }; - -*/ struct sort_pred { bool operator()(const std::pair &left, const std::pair &right) { return left.second < right.second; @@ -2598,121 +2068,11 @@ struct sort_pred { }; -void test_files_from_directory(std::string test_file_dir, argument_parser & args_parser) { - /* - std::cout << "loading files from directory \"" << test_file_dir << "\"" << std::endl; - std::string out_dir = args_parser.get_option_value("--out_dir"); - if (out_dir.size() == 0) { - out_dir = "/tmp/test"; - } - DIR *out_dir_p = opendir(out_dir.c_str()); - if (out_dir_p == nullptr) { - std::cout << "Cannot open output directory \"" << out_dir << "\"" << std::endl; - return; - } - closedir(out_dir_p); - vector> files = get_file_list_of_dir(test_file_dir); - std::sort(files.begin(), files.end(), sort_pred()); - unsigned max_iters, time_limit; - get_time_limit_and_max_iters_from_parser(args_parser, time_limit); - unsigned successes = 0, failures = 0, inconclusives = 0; - for (auto & t : files) { - process_test_file(test_file_dir, t.first, args_parser, out_dir, max_iters, time_limit, successes, failures, inconclusives); - } - std::cout << "comparing with glpk: successes " << successes << ", failures " << failures << ", inconclusives " << inconclusives << std::endl; - */ -} -std::unordered_map get_solution_map(lp_solver * lps, mps_reader & reader) { - std::unordered_map ret; - for (const auto & it : reader.column_names()) { - ret[it] = lps->get_column_value_by_name(it); - } - return ret; -} -void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_reader * reader) { - std::string maxng = args_parser.get_option_value("--maxng"); - if (!maxng.empty()) { - solver->settings().max_number_of_iterations_with_no_improvements = atoi(maxng.c_str()); - } - if (args_parser.option_is_used("-pd")){ - solver->settings().presolve_with_double_solver_for_lar = true; - } - - if (args_parser.option_is_used("--compare_with_primal")){ - if (reader == nullptr) { - std::cout << "cannot compare with primal, the reader is null " << std::endl; - return; - } - auto * lps = reader->create_solver(false); - lps->find_maximal_solution(); - std::unordered_map sol = get_solution_map(lps, *reader); - std::cout << "status = " << lp_status_to_string(solver->get_status()) << std::endl; - return; - } - stopwatch sw; - sw.start(); - lp_status status = solver->solve(); - std::cout << "status is " << lp_status_to_string(status) << ", processed for " << sw.get_current_seconds() <<" seconds, and " << solver->get_total_iterations() << " iterations" << std::endl; - if (solver->get_status() == lp_status::INFEASIBLE) { - explanation evidence; - solver->get_infeasibility_explanation(evidence); - } - if (args_parser.option_is_used("--randomize_lar")) { - if (solver->get_status() != lp_status::OPTIMAL) { - std::cout << "cannot check randomize on an infeazible problem" << std::endl; - return; - } - std::cout << "checking randomize" << std::endl; - vector all_vars; - for (unsigned j = 0; j < solver->number_of_vars(); j++) - all_vars.push_back(j); - - unsigned m = all_vars.size(); - if (m > 100) - m = 100; - - var_index *vars = new var_index[m]; - for (unsigned i = 0; i < m; i++) - vars[i]=all_vars[i]; - - solver->random_update(m, vars); - delete []vars; - } -} -lar_solver * create_lar_solver_from_file(std::string file_name, argument_parser & args_parser) { - if (args_parser.option_is_used("--smt")) { - smt_reader reader(file_name); - reader.read(); - if (!reader.is_ok()){ - std::cout << "cannot process " << file_name << std::endl; - return nullptr; - } - return reader.create_lar_solver(); - } - mps_reader reader(file_name); - reader.read(); - if (!reader.is_ok()) { - std::cout << "cannot process " << file_name << std::endl; - return nullptr; - } - return reader.create_lar_solver(); -} -void test_lar_on_file(std::string file_name, argument_parser & args_parser) { - lar_solver * solver = create_lar_solver_from_file(file_name, args_parser); - mps_reader reader(file_name); - mps_reader * mps_reader = nullptr; - reader.read(); - if (reader.is_ok()) { - mps_reader = & reader; - run_lar_solver(args_parser, solver, mps_reader); - } - delete solver; -} vector get_file_names_from_file_list(std::string filelist) { std::ifstream file(filelist); @@ -2733,23 +2093,6 @@ vector get_file_names_from_file_list(std::string filelist) { return ret; } -void test_lar_solver(argument_parser & args_parser) { - - std::string file_name = args_parser.get_option_value("--file"); - if (!file_name.empty()) { - test_lar_on_file(file_name, args_parser); - return; - } - - std::string file_list = args_parser.get_option_value("--filelist"); - if (!file_list.empty()) { - for (const std::string & fn : get_file_names_from_file_list(file_list)) - test_lar_on_file(fn, args_parser); - return; - } - - std::cout << "give option --file or --filelist to test_lar_solver\n"; -} void test_numeric_pair() { numeric_pair a; @@ -3934,22 +3277,6 @@ void test_lp_local(int argn, char**argv) { return finalize(0); } - if (args_parser.option_is_used("--test_mpq")) { - test_rationals(); - return finalize(0); - } - - if (args_parser.option_is_used("--test_mpq_np")) { - test_rationals_no_numeric_pairs(); - return finalize(0); - } - - if (args_parser.option_is_used("--test_mpq_np_plus")) { - test_rationals_no_numeric_pairs_plus(); - return finalize(0); - } - - if (args_parser.option_is_used("--test_int_set")) { test_int_set(); @@ -3967,29 +3294,8 @@ void test_lp_local(int argn, char**argv) { return finalize(0); } -#ifdef Z3DEBUG - if (args_parser.option_is_used("--test_swaps")) { - square_sparse_matrix m(10, 0); - fill_matrix(m); - test_swap_rows_with_permutation(m); - test_swap_cols_with_permutation(m); - return finalize(0); - } -#endif - if (args_parser.option_is_used("--test_perm")) { - test_permutations(); - return finalize(0); - } - if (args_parser.option_is_used("--test_file_directory")) { - test_files_from_directory(args_parser.get_option_value("--test_file_directory"), args_parser); - return finalize(0); - } - std::string file_list = args_parser.get_option_value("--filelist"); - if (!file_list.empty()) { - for (const std::string & fn : get_file_names_from_file_list(file_list)) - solve_mps(fn, args_parser); - return finalize(0); - } + + if (args_parser.option_is_used("-tbq")) { test_binary_priority_queue(); @@ -3997,100 +3303,6 @@ void test_lp_local(int argn, char**argv) { return finalize(ret); } -#ifdef Z3DEBUG - lp_settings settings; - update_settings(args_parser, settings); - if (args_parser.option_is_used("--test_lu")) { - test_lu(settings); - ret = 0; - return finalize(ret); - } - - if (args_parser.option_is_used("--test_small_lu")) { - test_small_lu(settings); - ret = 0; - return finalize(ret); - } - - if (args_parser.option_is_used("--lar")){ - std::cout <<"calling test_lar_solver" << std::endl; - test_lar_solver(args_parser); - return finalize(0); - } - - - - if (args_parser.option_is_used("--test_larger_lu")) { - test_larger_lu(settings); - ret = 0; - return finalize(ret); - } - - if (args_parser.option_is_used("--test_larger_lu_with_holes")) { - test_larger_lu_with_holes(settings); - ret = 0; - return finalize(ret); - } -#endif - if (args_parser.option_is_used("--eti")) { - test_evidence_for_total_inf_simple(args_parser); - ret = 0; - return finalize(ret); - } - - if (args_parser.option_is_used("--maximize_term")) { - test_maximize_term(); - ret = 0; - return finalize(ret); - } - - if (args_parser.option_is_used("--test_lp_0")) { - test_lp_0(); - ret = 0; - return finalize(ret); - } - - if (args_parser.option_is_used("--smap")) { - test_stacked(); - ret = 0; - return finalize(ret); - } - if (args_parser.option_is_used("--term")) { - test_term(); - ret = 0; - return finalize(ret); - } - unsigned time_limit; - get_time_limit_and_max_iters_from_parser(args_parser, time_limit); - bool dual = args_parser.option_is_used("--dual"); - bool solve_for_rational = args_parser.option_is_used("--mpq"); - std::string file_name = args_parser.get_option_value("--file"); - if (!file_name.empty()) { - solve_mps(file_name, args_parser.option_is_used("--min"), time_limit, solve_for_rational, dual, args_parser.option_is_used("--compare_with_primal"), args_parser); - ret = 0; - return finalize(ret); - } - - if (args_parser.option_is_used("--solve_some_mps")) { -#ifndef _WINDOWS - solve_some_mps(args_parser); -#endif - ret = 0; - return finalize(ret); - } - // lp::ccc = 0; - return finalize(0); - test_init_U(); - test_replace_column(); -#ifdef Z3DEBUG - square_sparse_matrix_with_permutations_test(); - test_dense_matrix(); - test_swap_operations(); - test_permutations(); - test_pivot_like_swaps_and_pivot(); -#endif - tst1(); - std::cout << "done with LP tests\n"; return finalize(0); // has_violations() ? 1 : 0); } } diff --git a/src/test/lp/smt_reader.h b/src/test/lp/smt_reader.h index 2ab0c1ea69a..ee41a418aef 100644 --- a/src/test/lp/smt_reader.h +++ b/src/test/lp/smt_reader.h @@ -20,7 +20,6 @@ Revision History: #pragma once -// reads an MPS file representing a Mixed Integer Program #include #include #include @@ -31,7 +30,6 @@ Revision History: #include #include #include -#include "math/lp/mps_reader.h" #include "math/lp/ul_pair.h" #include "math/lp/lar_constraints.h" #include