mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 12:28:44 +00:00
Cleaned up LP test code.
This commit is contained in:
Christoph M. Wintersteiger
parent
d61b722b68
commit
6d51265d9d
|
|
@ -1,9 +1,22 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Author: Lev Nachmanson
|
||||
*/
|
||||
Module Name:
|
||||
|
||||
<name>
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Lev Nachmanson (levnach)
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#include <unordered_map>
|
||||
#include <vector>
|
||||
|
|
@ -11,7 +24,7 @@ Author: Lev Nachmanson
|
|||
#include <set>
|
||||
#include <iostream>
|
||||
|
||||
namespace lean {
|
||||
namespace lp {
|
||||
class argument_parser {
|
||||
std::unordered_map<std::string, std::string> m_options;
|
||||
std::unordered_map<std::string, std::string> m_options_with_after_string;
|
||||
|
|
|
|||
297
src/test/lp.cpp
297
src/test/lp.cpp
|
|
@ -1,7 +1,23 @@
|
|||
/*
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Author: Lev Nachmanson
|
||||
*/
|
||||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
<name>
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Lev Nachmanson (levnach)
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#include <limits>
|
||||
#if _LINUX_
|
||||
#include <dirent.h>
|
||||
|
|
@ -31,8 +47,9 @@ Author: Lev Nachmanson
|
|||
#include "util/lp/stacked_unordered_set.h"
|
||||
#include "util/lp/int_set.h"
|
||||
#include "util/stopwatch.h"
|
||||
namespace lean {
|
||||
unsigned seed = 1;
|
||||
|
||||
namespace lp {
|
||||
unsigned seed = 1;
|
||||
|
||||
random_gen g_rand;
|
||||
static unsigned my_random() {
|
||||
|
|
@ -78,7 +95,7 @@ void test_matrix(sparse_matrix<T, X> & a) {
|
|||
|
||||
a.set(i, j, t);
|
||||
|
||||
lean_assert(a.get(i, j) == t);
|
||||
SASSERT(a.get(i, j) == t);
|
||||
|
||||
unsigned j1;
|
||||
if (j < m - 1) {
|
||||
|
|
@ -155,7 +172,7 @@ void tst1() {
|
|||
|
||||
test_matrix(m10by9);
|
||||
std::cout <<"zeroing m10by9\n";
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
for (unsigned int i = 0; i < m10by9.dimension(); i++)
|
||||
for (unsigned int j = 0; j < m10by9.column_count(); j++)
|
||||
m10by9.set(i, j, 0);
|
||||
|
|
@ -170,7 +187,7 @@ vector<int> allocate_basis_heading(unsigned count) { // the rest of initilizatio
|
|||
|
||||
|
||||
void init_basic_part_of_basis_heading(vector<unsigned> & basis, vector<int> & basis_heading) {
|
||||
lean_assert(basis_heading.size() >= basis.size());
|
||||
SASSERT(basis_heading.size() >= basis.size());
|
||||
unsigned m = basis.size();
|
||||
for (unsigned i = 0; i < m; i++) {
|
||||
unsigned column = basis[i];
|
||||
|
|
@ -205,7 +222,7 @@ void change_basis(unsigned entering, unsigned leaving, vector<unsigned>& basis,
|
|||
}
|
||||
|
||||
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
void test_small_lu(lp_settings & settings) {
|
||||
std::cout << " test_small_lu" << std::endl;
|
||||
static_matrix<double, double> m(3, 6);
|
||||
|
|
@ -218,61 +235,61 @@ void test_small_lu(lp_settings & settings) {
|
|||
m(1, 1) = 4; m(1, 4) = 7;
|
||||
m(2, 0) = 1.8; m(2, 2) = 5; m(2, 4) = 2; m(2, 5) = 8;
|
||||
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
print_matrix(m, std::cout);
|
||||
#endif
|
||||
vector<int> heading = allocate_basis_heading(m.column_count());
|
||||
vector<unsigned> non_basic_columns;
|
||||
init_basis_heading_and_non_basic_columns_vector(basis, heading, non_basic_columns);
|
||||
lu<double, double> l(m, basis, settings);
|
||||
lean_assert(l.is_correct(basis));
|
||||
SASSERT(l.is_correct(basis));
|
||||
indexed_vector<double> w(m.row_count());
|
||||
std::cout << "entering 2, leaving 0" << std::endl;
|
||||
l.prepare_entering(2, w); // to init vector w
|
||||
l.replace_column(0, w, heading[0]);
|
||||
change_basis(2, 0, basis, non_basic_columns, heading);
|
||||
// #ifdef LEAN_DEBUG
|
||||
// #ifdef Z3DEBUG
|
||||
// std::cout << "we were factoring " << std::endl;
|
||||
// print_matrix(get_B(l));
|
||||
// #endif
|
||||
lean_assert(l.is_correct(basis));
|
||||
SASSERT(l.is_correct(basis));
|
||||
std::cout << "entering 4, leaving 3" << std::endl;
|
||||
l.prepare_entering(4, w); // to init vector w
|
||||
l.replace_column(0, w, heading[3]);
|
||||
change_basis(4, 3, basis, non_basic_columns, heading);
|
||||
std::cout << "we were factoring " << std::endl;
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
{
|
||||
auto bl = get_B(l, basis);
|
||||
print_matrix(&bl, std::cout);
|
||||
}
|
||||
#endif
|
||||
lean_assert(l.is_correct(basis));
|
||||
SASSERT(l.is_correct(basis));
|
||||
|
||||
std::cout << "entering 5, leaving 1" << std::endl;
|
||||
l.prepare_entering(5, w); // to init vector w
|
||||
l.replace_column(0, w, heading[1]);
|
||||
change_basis(5, 1, basis, non_basic_columns, heading);
|
||||
std::cout << "we were factoring " << std::endl;
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
{
|
||||
auto bl = get_B(l, basis);
|
||||
print_matrix(&bl, std::cout);
|
||||
}
|
||||
#endif
|
||||
lean_assert(l.is_correct(basis));
|
||||
SASSERT(l.is_correct(basis));
|
||||
std::cout << "entering 3, leaving 2" << std::endl;
|
||||
l.prepare_entering(3, w); // to init vector w
|
||||
l.replace_column(0, w, heading[2]);
|
||||
change_basis(3, 2, basis, non_basic_columns, heading);
|
||||
std::cout << "we were factoring " << std::endl;
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
{
|
||||
auto bl = get_B(l, basis);
|
||||
print_matrix(&bl, std::cout);
|
||||
}
|
||||
#endif
|
||||
lean_assert(l.is_correct(basis));
|
||||
SASSERT(l.is_correct(basis));
|
||||
|
||||
m.add_row();
|
||||
m.add_column();
|
||||
|
|
@ -291,7 +308,7 @@ void test_small_lu(lp_settings & settings) {
|
|||
auto columns_to_replace = l.get_set_of_columns_to_replace_for_add_last_rows(heading);
|
||||
l.add_last_rows_to_B(heading, columns_to_replace);
|
||||
std::cout << "here" << std::endl;
|
||||
lean_assert(l.is_correct(basis));
|
||||
SASSERT(l.is_correct(basis));
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -351,7 +368,7 @@ void fill_larger_sparse_matrix(static_matrix<double, double> & m){
|
|||
|
||||
int perm_id = 0;
|
||||
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
void test_larger_lu_exp(lp_settings & settings) {
|
||||
std::cout << " test_larger_lu_exp" << std::endl;
|
||||
static_matrix<double, double> m(6, 12);
|
||||
|
|
@ -373,7 +390,7 @@ void test_larger_lu_exp(lp_settings & settings) {
|
|||
|
||||
dense_matrix<double, double> left_side = l.get_left_side(basis);
|
||||
dense_matrix<double, double> right_side = l.get_right_side();
|
||||
lean_assert(left_side == right_side);
|
||||
SASSERT(left_side == right_side);
|
||||
int leaving = 3;
|
||||
int entering = 8;
|
||||
for (unsigned i = 0; i < m.row_count(); i++) {
|
||||
|
|
@ -385,12 +402,12 @@ void test_larger_lu_exp(lp_settings & settings) {
|
|||
l.prepare_entering(entering, w);
|
||||
l.replace_column(0, w, heading[leaving]);
|
||||
change_basis(entering, leaving, basis, non_basic_columns, heading);
|
||||
lean_assert(l.is_correct(basis));
|
||||
SASSERT(l.is_correct(basis));
|
||||
|
||||
l.prepare_entering(11, w); // to init vector w
|
||||
l.replace_column(0, w, heading[0]);
|
||||
change_basis(11, 0, basis, non_basic_columns, heading);
|
||||
lean_assert(l.is_correct(basis));
|
||||
SASSERT(l.is_correct(basis));
|
||||
}
|
||||
|
||||
void test_larger_lu_with_holes(lp_settings & settings) {
|
||||
|
|
@ -432,7 +449,7 @@ void test_larger_lu_with_holes(lp_settings & settings) {
|
|||
l.prepare_entering(8, w); // to init vector w
|
||||
l.replace_column(0, w, heading[0]);
|
||||
change_basis(8, 0, basis, non_basic_columns, heading);
|
||||
lean_assert(l.is_correct(basis));
|
||||
SASSERT(l.is_correct(basis));
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -479,7 +496,7 @@ void test_larger_lu(lp_settings& settings) {
|
|||
l.prepare_entering(9, w); // to init vector w
|
||||
l.replace_column(0, w, heading[0]);
|
||||
change_basis(9, 0, basis, non_basic_columns, heading);
|
||||
lean_assert(l.is_correct(basis));
|
||||
SASSERT(l.is_correct(basis));
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -550,7 +567,7 @@ void test_lp_1() {
|
|||
m(1, 0) = -1; m(1, 2) = 3; m(1, 4) = 1;
|
||||
m(2, 0) = 2; m(2, 1) = -1; m(2, 2) = 2; m(2, 5) = 1;
|
||||
m(3, 0) = 2; m(3, 1) = 3; m(3, 2) = -1; m(3, 6) = 1;
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
print_matrix(m, std::cout);
|
||||
#endif
|
||||
vector<double> x_star(7);
|
||||
|
|
@ -604,7 +621,7 @@ void test_lp_primal_core_solver() {
|
|||
}
|
||||
|
||||
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
template <typename T, typename X>
|
||||
void test_swap_rows_with_permutation(sparse_matrix<T, X>& m){
|
||||
std::cout << "testing swaps" << std::endl;
|
||||
|
|
@ -612,7 +629,7 @@ void test_swap_rows_with_permutation(sparse_matrix<T, X>& m){
|
|||
dense_matrix<double, double> original(&m);
|
||||
permutation_matrix<double, double> q(dim);
|
||||
print_matrix(m, std::cout);
|
||||
lean_assert(original == q * m);
|
||||
SASSERT(original == q * m);
|
||||
for (int i = 0; i < 100; i++) {
|
||||
unsigned row1 = my_random() % dim;
|
||||
unsigned row2 = my_random() % dim;
|
||||
|
|
@ -620,7 +637,7 @@ void test_swap_rows_with_permutation(sparse_matrix<T, X>& m){
|
|||
std::cout << "swap " << row1 << " " << row2 << std::endl;
|
||||
m.swap_rows(row1, row2);
|
||||
q.transpose_from_left(row1, row2);
|
||||
lean_assert(original == q * m);
|
||||
SASSERT(original == q * m);
|
||||
print_matrix(m, std::cout);
|
||||
std::cout << std::endl;
|
||||
}
|
||||
|
|
@ -628,7 +645,7 @@ void test_swap_rows_with_permutation(sparse_matrix<T, X>& m){
|
|||
#endif
|
||||
template <typename T, typename X>
|
||||
void fill_matrix(sparse_matrix<T, X>& m); // forward definition
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
template <typename T, typename X>
|
||||
void test_swap_cols_with_permutation(sparse_matrix<T, X>& m){
|
||||
std::cout << "testing swaps" << std::endl;
|
||||
|
|
@ -636,7 +653,7 @@ void test_swap_cols_with_permutation(sparse_matrix<T, X>& m){
|
|||
dense_matrix<double, double> original(&m);
|
||||
permutation_matrix<double, double> q(dim);
|
||||
print_matrix(m, std::cout);
|
||||
lean_assert(original == q * m);
|
||||
SASSERT(original == q * m);
|
||||
for (int i = 0; i < 100; i++) {
|
||||
unsigned row1 = my_random() % dim;
|
||||
unsigned row2 = my_random() % dim;
|
||||
|
|
@ -644,7 +661,7 @@ void test_swap_cols_with_permutation(sparse_matrix<T, X>& m){
|
|||
std::cout << "swap " << row1 << " " << row2 << std::endl;
|
||||
m.swap_rows(row1, row2);
|
||||
q.transpose_from_right(row1, row2);
|
||||
lean_assert(original == q * m);
|
||||
SASSERT(original == q * m);
|
||||
print_matrix(m, std::cout);
|
||||
std::cout << std::endl;
|
||||
}
|
||||
|
|
@ -663,8 +680,8 @@ void test_swap_rows(sparse_matrix<T, X>& m, unsigned i0, unsigned i1){
|
|||
m.swap_rows(i0, i1);
|
||||
|
||||
for (unsigned j = 0; j < m.dimension(); j++) {
|
||||
lean_assert(mcopy(i0, j) == m(i1, j));
|
||||
lean_assert(mcopy(i1, j) == m(i0, j));
|
||||
SASSERT(mcopy(i0, j) == m(i1, j));
|
||||
SASSERT(mcopy(i1, j) == m(i0, j));
|
||||
}
|
||||
}
|
||||
template <typename T, typename X>
|
||||
|
|
@ -678,15 +695,15 @@ void test_swap_columns(sparse_matrix<T, X>& m, unsigned i0, unsigned i1){
|
|||
m.swap_columns(i0, i1);
|
||||
|
||||
for (unsigned j = 0; j < m.dimension(); j++) {
|
||||
lean_assert(mcopy(j, i0) == m(j, i1));
|
||||
lean_assert(mcopy(j, i1) == m(j, i0));
|
||||
SASSERT(mcopy(j, i0) == m(j, i1));
|
||||
SASSERT(mcopy(j, i1) == m(j, i0));
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < m.dimension(); i++) {
|
||||
if (i == i0 || i == i1)
|
||||
continue;
|
||||
for (unsigned j = 0; j < m.dimension(); j++) {
|
||||
lean_assert(mcopy(j, i)== m(j, i));
|
||||
SASSERT(mcopy(j, i)== m(j, i));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -731,7 +748,7 @@ void test_pivot_like_swaps_and_pivot(){
|
|||
m(target_row, 3) = 0;
|
||||
m(target_row, 5) = 0;
|
||||
m(pivot_row, 6) = 0;
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
print_matrix(m, std::cout);
|
||||
#endif
|
||||
|
||||
|
|
@ -748,11 +765,11 @@ void test_pivot_like_swaps_and_pivot(){
|
|||
m.pivot_row_to_row(pivot_row_0, beta, target_row, settings);
|
||||
// print_matrix(m);
|
||||
for (unsigned j = 0; j < m.dimension(); j++) {
|
||||
lean_assert(abs(row[j] - m(target_row, j)) < 0.00000001);
|
||||
SASSERT(abs(row[j] - m(target_row, j)) < 0.00000001);
|
||||
}
|
||||
}
|
||||
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
void test_swap_rows() {
|
||||
sparse_matrix<double, double> m(10);
|
||||
fill_matrix(m);
|
||||
|
|
@ -853,57 +870,57 @@ void sparse_matrix_with_permutaions_test() {
|
|||
m.multiply_from_left(q0);
|
||||
for (unsigned i = 0; i < dim; i++) {
|
||||
for (unsigned j = 0; j < dim; j++) {
|
||||
lean_assert(m(i, j) == dm0.get_elem(q0[i], j));
|
||||
SASSERT(m(i, j) == dm0.get_elem(q0[i], j));
|
||||
}
|
||||
}
|
||||
|
||||
auto q0_dm = q0 * dm;
|
||||
lean_assert(m == q0_dm);
|
||||
SASSERT(m == q0_dm);
|
||||
|
||||
m.multiply_from_left(q1);
|
||||
for (unsigned i = 0; i < dim; i++) {
|
||||
for (unsigned j = 0; j < dim; j++) {
|
||||
lean_assert(m(i, j) == dm0.get_elem(q0[q1[i]], j));
|
||||
SASSERT(m(i, j) == dm0.get_elem(q0[q1[i]], j));
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
auto q1_q0_dm = q1 * q0_dm;
|
||||
|
||||
lean_assert(m == q1_q0_dm);
|
||||
SASSERT(m == q1_q0_dm);
|
||||
|
||||
m.multiply_from_right(p0);
|
||||
|
||||
for (unsigned i = 0; i < dim; i++) {
|
||||
for (unsigned j = 0; j < dim; j++) {
|
||||
lean_assert(m(i, j) == dm0.get_elem(q0[q1[i]], p0[j]));
|
||||
SASSERT(m(i, j) == dm0.get_elem(q0[q1[i]], p0[j]));
|
||||
}
|
||||
}
|
||||
|
||||
auto q1_q0_dm_p0 = q1_q0_dm * p0;
|
||||
|
||||
lean_assert(m == q1_q0_dm_p0);
|
||||
SASSERT(m == q1_q0_dm_p0);
|
||||
|
||||
m.multiply_from_right(p1);
|
||||
|
||||
for (unsigned i = 0; i < dim; i++) {
|
||||
for (unsigned j = 0; j < dim; j++) {
|
||||
lean_assert(m(i, j) == dm0.get_elem(q0[q1[i]], p1[p0[j]]));
|
||||
SASSERT(m(i, j) == dm0.get_elem(q0[q1[i]], p1[p0[j]]));
|
||||
}
|
||||
}
|
||||
|
||||
auto q1_q0_dm_p0_p1 = q1_q0_dm_p0 * p1;
|
||||
lean_assert(m == q1_q0_dm_p0_p1);
|
||||
SASSERT(m == q1_q0_dm_p0_p1);
|
||||
|
||||
m.multiply_from_right(p1);
|
||||
for (unsigned i = 0; i < dim; i++) {
|
||||
for (unsigned j = 0; j < dim; j++) {
|
||||
lean_assert(m(i, j) == dm0.get_elem(q0[q1[i]], p1[p1[p0[j]]]));
|
||||
SASSERT(m(i, j) == dm0.get_elem(q0[q1[i]], p1[p1[p0[j]]]));
|
||||
}
|
||||
}
|
||||
auto q1_q0_dm_p0_p1_p1 = q1_q0_dm_p0_p1 * p1;
|
||||
|
||||
lean_assert(m == q1_q0_dm_p0_p1_p1);
|
||||
SASSERT(m == q1_q0_dm_p0_p1_p1);
|
||||
}
|
||||
|
||||
void test_swap_columns() {
|
||||
|
|
@ -1021,10 +1038,10 @@ void test_apply_reverse_from_right_to_perm(permutation_matrix<double, double> &
|
|||
pclone[4] = 1;
|
||||
|
||||
p.multiply_by_reverse_from_right(l);
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
auto rev = l.get_inverse();
|
||||
auto rs = pclone * rev;
|
||||
lean_assert(p == rs)
|
||||
SASSERT(p == rs);
|
||||
#endif
|
||||
}
|
||||
|
||||
|
|
@ -1051,8 +1068,8 @@ void test_permutations() {
|
|||
|
||||
p.apply_reverse_from_right_to_T(v);
|
||||
p.apply_reverse_from_right_to_T(vi);
|
||||
lean_assert(vectors_are_equal(v, vi.m_data));
|
||||
lean_assert(vi.is_OK());
|
||||
SASSERT(vectors_are_equal(v, vi.m_data));
|
||||
SASSERT(vi.is_OK());
|
||||
}
|
||||
|
||||
void lp_solver_test() {
|
||||
|
|
@ -1200,7 +1217,7 @@ void solve_mps_double(std::string file_name, bool look_for_min, unsigned max_ite
|
|||
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;
|
||||
lean_assert(false);
|
||||
SASSERT(false);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1210,7 +1227,7 @@ void solve_mps_double(std::string file_name, bool look_for_min, unsigned max_ite
|
|||
}
|
||||
|
||||
void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_iterations, unsigned time_limit, bool dual, argument_parser & args_parser) {
|
||||
mps_reader<lean::mpq, lean::mpq> reader(file_name);
|
||||
mps_reader<lp::mpq, lp::mpq> reader(file_name);
|
||||
reader.read();
|
||||
if (reader.is_ok()) {
|
||||
auto * solver = reader.create_solver(dual);
|
||||
|
|
@ -1224,7 +1241,7 @@ void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_i
|
|||
// for (auto name: reader.column_names()) {
|
||||
// std::cout << name << "=" << solver->get_column_value_by_name(name) << ' ';
|
||||
// }
|
||||
lean::mpq cost = solver->get_current_cost();
|
||||
lp::mpq cost = solver->get_current_cost();
|
||||
if (look_for_min) {
|
||||
cost = -cost;
|
||||
}
|
||||
|
|
@ -1262,7 +1279,7 @@ void solve_mps(std::string file_name, argument_parser & 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<lean::mpq, lean::mpq> reader(file_name);
|
||||
mps_reader<lp::mpq, lp::mpq> reader(file_name);
|
||||
reader.read();
|
||||
if (reader.is_ok()) {
|
||||
auto * solver = reader.create_solver(dual);
|
||||
|
|
@ -1274,7 +1291,7 @@ void solve_mps_in_rational(std::string file_name, bool dual, argument_parser & /
|
|||
std::cout << name << "=" << solver->get_column_value_by_name(name).get_double() << ' ';
|
||||
}
|
||||
}
|
||||
std::cout << std::endl << "cost = " << numeric_traits<lean::mpq>::get_double(solver->get_current_cost()) << std::endl;
|
||||
std::cout << std::endl << "cost = " << numeric_traits<lp::mpq>::get_double(solver->get_current_cost()) << std::endl;
|
||||
}
|
||||
delete solver;
|
||||
} else {
|
||||
|
|
@ -1318,7 +1335,7 @@ void test_binary_priority_queue() {
|
|||
|
||||
for (unsigned i = 0; i < 10; i++) {
|
||||
unsigned de = q.dequeue();
|
||||
lean_assert(i == de);
|
||||
SASSERT(i == de);
|
||||
std::cout << de << std::endl;
|
||||
}
|
||||
q.enqueue(2, 2);
|
||||
|
|
@ -1337,11 +1354,11 @@ void test_binary_priority_queue() {
|
|||
q.dequeue();
|
||||
q.remove(33);
|
||||
q.enqueue(0, 0);
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
unsigned t = 0;
|
||||
while (q.size() > 0) {
|
||||
unsigned d =q.dequeue();
|
||||
lean_assert(t++ == d);
|
||||
SASSERT(t++ == d);
|
||||
std::cout << d << std::endl;
|
||||
}
|
||||
#endif
|
||||
|
|
@ -1370,7 +1387,7 @@ void solve_mps_with_known_solution(std::string file_name, std::unordered_map<std
|
|||
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;
|
||||
lean_assert(status == solver->get_status());
|
||||
SASSERT(status == solver->get_status());
|
||||
throw "status is wrong";
|
||||
}
|
||||
if (solver->get_status() == lp_status::OPTIMAL) {
|
||||
|
|
@ -1381,7 +1398,7 @@ void solve_mps_with_known_solution(std::string file_name, std::unordered_map<std
|
|||
std::cout << "expected:" << it.first << "=" <<
|
||||
it.second <<", got " << solver->get_column_value_by_name(it.first) << std::endl;
|
||||
}
|
||||
lean_assert(fabs(it.second - solver->get_column_value_by_name(it.first)) < 0.000001);
|
||||
SASSERT(fabs(it.second - solver->get_column_value_by_name(it.first)) < 0.000001);
|
||||
}
|
||||
}
|
||||
if (reader.column_names().size() < 20) {
|
||||
|
|
@ -1706,48 +1723,48 @@ void solve_some_mps(argument_parser & args_parser) {
|
|||
#endif
|
||||
|
||||
void solve_rational() {
|
||||
lp_primal_simplex<lean::mpq, lean::mpq> solver;
|
||||
solver.add_constraint(lp_relation::Equal, lean::mpq(7), 0);
|
||||
solver.add_constraint(lp_relation::Equal, lean::mpq(-3), 1);
|
||||
lp_primal_simplex<lp::mpq, lp::mpq> 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, lean::mpq(cost[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, lean::mpq(row0[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, lean::mpq(row1[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_low_bound(i, lean::mpq(0));
|
||||
solver.set_upper_bound(i, lean::mpq(bounds[i]));
|
||||
solver.set_low_bound(i, lp::mpq(0));
|
||||
solver.set_upper_bound(i, lp::mpq(bounds[i]));
|
||||
}
|
||||
|
||||
std::unordered_map<std::string, lean::mpq> expected_sol;
|
||||
expected_sol["x1"] = lean::mpq(0);
|
||||
expected_sol["x2"] = lean::mpq(6);
|
||||
expected_sol["x3"] = lean::mpq(0);
|
||||
expected_sol["x4"] = lean::mpq(15);
|
||||
expected_sol["x5"] = lean::mpq(2);
|
||||
expected_sol["x6"] = lean::mpq(1);
|
||||
expected_sol["x7"] = lean::mpq(1);
|
||||
expected_sol["x8"] = lean::mpq(0);
|
||||
std::unordered_map<std::string, lp::mpq> 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();
|
||||
lean_assert(solver.get_status() == OPTIMAL);
|
||||
SASSERT(solver.get_status() == OPTIMAL);
|
||||
for (auto it : expected_sol) {
|
||||
lean_assert(it.second == solver.get_column_value_by_name(it.first));
|
||||
SASSERT(it.second == solver.get_column_value_by_name(it.first));
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1805,7 +1822,7 @@ std::unordered_map<std::string, double> * get_solution_from_glpsol_output(std::s
|
|||
return ret;
|
||||
}
|
||||
|
||||
lean_assert(split.size() > 3);
|
||||
SASSERT(split.size() > 3);
|
||||
(*ret)[split[1]] = atof(split[3].c_str());
|
||||
} while (true);
|
||||
}
|
||||
|
|
@ -1817,7 +1834,7 @@ void test_init_U() {
|
|||
m(0, 0) = 10; m(0, 1) = 11; m(0, 2) = 12; m(0, 3) = 13; m(0, 4) = 14;
|
||||
m(1, 0) = 20; m(1, 1) = 21; m(1, 2) = 22; m(1, 3) = 23; m(1, 5) = 24;
|
||||
m(2, 0) = 30; m(2, 1) = 31; m(2, 2) = 32; m(2, 3) = 33; m(2, 6) = 34;
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
print_matrix(m, std::cout);
|
||||
#endif
|
||||
vector<unsigned> basis(3);
|
||||
|
|
@ -1829,7 +1846,7 @@ void test_init_U() {
|
|||
|
||||
for (unsigned i = 0; i < 3; i++) {
|
||||
for (unsigned j = 0; j < 3; j ++) {
|
||||
lean_assert(m(i, basis[j]) == u(i, j));
|
||||
SASSERT(m(i, basis[j]) == u(i, j));
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1857,7 +1874,7 @@ void test_replace_column() {
|
|||
for (unsigned column_to_replace = 0; column_to_replace < m.dimension(); column_to_replace ++) {
|
||||
m.replace_column(column_to_replace, w, settings);
|
||||
for (unsigned i = 0; i < m.dimension(); i++) {
|
||||
lean_assert(abs(w[i] - m(i, column_to_replace)) < 0.00000001);
|
||||
SASSERT(abs(w[i] - m(i, column_to_replace)) < 0.00000001);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1961,7 +1978,7 @@ void test_stacked_unsigned() {
|
|||
v = 3;
|
||||
v = 4;
|
||||
v.pop();
|
||||
lean_assert(v == 2);
|
||||
SASSERT(v == 2);
|
||||
v ++;
|
||||
v++;
|
||||
std::cout << "before push v=" << v << std::endl;
|
||||
|
|
@ -1971,7 +1988,7 @@ void test_stacked_unsigned() {
|
|||
v+=1;
|
||||
std::cout << "v = " << v << std::endl;
|
||||
v.pop(2);
|
||||
lean_assert(v == 4);
|
||||
SASSERT(v == 4);
|
||||
const unsigned & rr = v;
|
||||
std::cout << rr << std:: endl;
|
||||
|
||||
|
|
@ -2010,7 +2027,7 @@ void test_stacked_vector() {
|
|||
}
|
||||
|
||||
void test_stacked_set() {
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
std::cout << "test_stacked_set" << std::endl;
|
||||
stacked_unordered_set<int> s;
|
||||
s.insert(1);
|
||||
|
|
@ -2020,7 +2037,7 @@ void test_stacked_set() {
|
|||
s.push();
|
||||
s.insert(4);
|
||||
s.pop();
|
||||
lean_assert(s() == scopy);
|
||||
SASSERT(s() == scopy);
|
||||
s.push();
|
||||
s.push();
|
||||
s.insert(4);
|
||||
|
|
@ -2028,7 +2045,7 @@ void test_stacked_set() {
|
|||
s.push();
|
||||
s.insert(4);
|
||||
s.pop(3);
|
||||
lean_assert(s() == scopy);
|
||||
SASSERT(s() == scopy);
|
||||
#endif
|
||||
}
|
||||
|
||||
|
|
@ -2397,15 +2414,15 @@ void test_files_from_directory(std::string test_file_dir, argument_parser & args
|
|||
}
|
||||
|
||||
|
||||
std::unordered_map<std::string, lean::mpq> get_solution_map(lp_solver<lean::mpq, lean::mpq> * lps, mps_reader<lean::mpq, lean::mpq> & reader) {
|
||||
std::unordered_map<std::string, lean::mpq> ret;
|
||||
std::unordered_map<std::string, lp::mpq> get_solution_map(lp_solver<lp::mpq, lp::mpq> * lps, mps_reader<lp::mpq, lp::mpq> & reader) {
|
||||
std::unordered_map<std::string, lp::mpq> ret;
|
||||
for (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<lean::mpq, lean::mpq> * reader) {
|
||||
void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_reader<lp::mpq, lp::mpq> * reader) {
|
||||
std::string maxng = args_parser.get_option_value("--maxng");
|
||||
if (maxng.size() > 0) {
|
||||
solver->settings().max_number_of_iterations_with_no_improvements = atoi(maxng.c_str());
|
||||
|
|
@ -2425,7 +2442,7 @@ void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_read
|
|||
}
|
||||
auto * lps = reader->create_solver(false);
|
||||
lps->find_maximal_solution();
|
||||
std::unordered_map<std::string, lean::mpq> sol = get_solution_map(lps, *reader);
|
||||
std::unordered_map<std::string, lp::mpq> sol = get_solution_map(lps, *reader);
|
||||
std::cout << "status = " << lp_status_to_string(solver->get_status()) << std::endl;
|
||||
return;
|
||||
}
|
||||
|
|
@ -2434,7 +2451,7 @@ void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_read
|
|||
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() == INFEASIBLE) {
|
||||
vector<std::pair<lean::mpq, constraint_index>> evidence;
|
||||
vector<std::pair<lp::mpq, constraint_index>> evidence;
|
||||
solver->get_infeasibility_explanation(evidence);
|
||||
}
|
||||
if (args_parser.option_is_used("--randomize_lar")) {
|
||||
|
|
@ -2467,7 +2484,7 @@ lar_solver * create_lar_solver_from_file(std::string file_name, argument_parser
|
|||
}
|
||||
return reader.create_lar_solver();
|
||||
}
|
||||
mps_reader<lean::mpq, lean::mpq> reader(file_name);
|
||||
mps_reader<lp::mpq, lp::mpq> reader(file_name);
|
||||
reader.read();
|
||||
if (!reader.is_ok()) {
|
||||
std::cout << "cannot process " << file_name << std::endl;
|
||||
|
|
@ -2478,8 +2495,8 @@ lar_solver * create_lar_solver_from_file(std::string file_name, argument_parser
|
|||
|
||||
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<lean::mpq, lean::mpq> reader(file_name);
|
||||
mps_reader<lean::mpq, lean::mpq> * mps_reader = nullptr;
|
||||
mps_reader<lp::mpq, lp::mpq> reader(file_name);
|
||||
mps_reader<lp::mpq, lp::mpq> * mps_reader = nullptr;
|
||||
reader.read();
|
||||
if (reader.is_ok()) {
|
||||
mps_reader = & reader;
|
||||
|
|
@ -2524,28 +2541,28 @@ void test_lar_solver(argument_parser & args_parser) {
|
|||
}
|
||||
|
||||
void test_numeric_pair() {
|
||||
numeric_pair<lean::mpq> a;
|
||||
numeric_pair<lean::mpq> b(2, lean::mpq(6, 2));
|
||||
numeric_pair<lp::mpq> a;
|
||||
numeric_pair<lp::mpq> b(2, lp::mpq(6, 2));
|
||||
a = b;
|
||||
numeric_pair<lean::mpq> c(0.1, 0.5);
|
||||
numeric_pair<lp::mpq> c(0.1, 0.5);
|
||||
a += 2*c;
|
||||
a -= c;
|
||||
lean_assert (a == b + c);
|
||||
numeric_pair<lean::mpq> d = a * 2;
|
||||
SASSERT (a == b + c);
|
||||
numeric_pair<lp::mpq> d = a * 2;
|
||||
std::cout << a << std::endl;
|
||||
lean_assert(b == b);
|
||||
lean_assert(b < a);
|
||||
lean_assert(b <= a);
|
||||
lean_assert(a > b);
|
||||
lean_assert(a != b);
|
||||
lean_assert(a >= b);
|
||||
lean_assert(-a < b);
|
||||
lean_assert(a < 2 * b);
|
||||
lean_assert(b + b > a);
|
||||
lean_assert(lean::mpq(2.1) * b + b > a);
|
||||
lean_assert(-b * lean::mpq(2.1) - b < lean::mpq(0.99) * a);
|
||||
std::cout << - b * lean::mpq(2.1) - b << std::endl;
|
||||
lean_assert(-b *(lean::mpq(2.1) + 1) == - b * lean::mpq(2.1) - b);
|
||||
SASSERT(b == b);
|
||||
SASSERT(b < a);
|
||||
SASSERT(b <= a);
|
||||
SASSERT(a > b);
|
||||
SASSERT(a != b);
|
||||
SASSERT(a >= b);
|
||||
SASSERT(-a < b);
|
||||
SASSERT(a < 2 * b);
|
||||
SASSERT(b + b > a);
|
||||
SASSERT(lp::mpq(2.1) * b + b > a);
|
||||
SASSERT(-b * lp::mpq(2.1) - b < lp::mpq(0.99) * a);
|
||||
std::cout << - b * lp::mpq(2.1) - b << std::endl;
|
||||
SASSERT(-b *(lp::mpq(2.1) + 1) == - b * lp::mpq(2.1) - b);
|
||||
}
|
||||
|
||||
void get_matrix_dimensions(std::ifstream & f, unsigned & m, unsigned & n) {
|
||||
|
|
@ -2566,7 +2583,7 @@ void read_row_cols(unsigned i, static_matrix<double, double>& A, std::ifstream &
|
|||
if (line== "row_end")
|
||||
break;
|
||||
auto r = split_and_trim(line);
|
||||
lean_assert(r.size() == 4);
|
||||
SASSERT(r.size() == 4);
|
||||
unsigned j = atoi(r[1].c_str());
|
||||
double v = atof(r[3].c_str());
|
||||
A.set(i, j, v);
|
||||
|
|
@ -2594,7 +2611,7 @@ void read_basis(vector<unsigned> & basis, std::ifstream & f) {
|
|||
std::cout << "reading basis" << std::endl;
|
||||
std::string line;
|
||||
getline(f, line);
|
||||
lean_assert(line == "basis_start");
|
||||
SASSERT(line == "basis_start");
|
||||
do {
|
||||
getline(f, line);
|
||||
if (line == "basis_end")
|
||||
|
|
@ -2607,7 +2624,7 @@ void read_basis(vector<unsigned> & basis, std::ifstream & f) {
|
|||
void read_indexed_vector(indexed_vector<double> & v, std::ifstream & f) {
|
||||
std::string line;
|
||||
getline(f, line);
|
||||
lean_assert(line == "vector_start");
|
||||
SASSERT(line == "vector_start");
|
||||
do {
|
||||
getline(f, line);
|
||||
if (line == "vector_end") break;
|
||||
|
|
@ -2641,13 +2658,13 @@ void check_lu_from_file(std::string lufile_name) {
|
|||
indexed_vector<double> d(A.row_count());
|
||||
unsigned entering = 26;
|
||||
lsuhl.solve_Bd(entering, d, v);
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
auto B = get_B(lsuhl, basis);
|
||||
vector<double> a(m);
|
||||
A.copy_column_to_vector(entering, a);
|
||||
indexed_vector<double> cd(d);
|
||||
B.apply_from_left(cd.m_data, settings);
|
||||
lean_assert(vectors_are_equal(cd.m_data , a));
|
||||
SASSERT(vectors_are_equal(cd.m_data , a));
|
||||
#endif
|
||||
}
|
||||
|
||||
|
|
@ -2662,7 +2679,7 @@ void test_square_dense_submatrix() {
|
|||
for (unsigned i = index_start; i < parent_dim; i++)
|
||||
for (unsigned j = index_start; j < parent_dim; j++)
|
||||
d[i][j] = i*3+j*2;
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
unsigned dim = parent_dim - index_start;
|
||||
dense_matrix<double, double> m(dim, dim);
|
||||
for (unsigned i = index_start; i < parent_dim; i++)
|
||||
|
|
@ -2673,7 +2690,7 @@ void test_square_dense_submatrix() {
|
|||
for (unsigned i = index_start; i < parent_dim; i++)
|
||||
for (unsigned j = index_start; j < parent_dim; j++)
|
||||
d[i][j] = d[j][i];
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
for (unsigned i = index_start; i < parent_dim; i++)
|
||||
for (unsigned j = index_start; j < parent_dim; j++)
|
||||
m[i-index_start][j-index_start] = d[i][j];
|
||||
|
|
@ -2738,7 +2755,7 @@ void test_evidence_for_total_inf_simple(argument_parser & args_parser) {
|
|||
auto status = solver.solve();
|
||||
std::cout << lp_status_to_string(status) << std::endl;
|
||||
std::unordered_map<var_index, mpq> model;
|
||||
lean_assert(solver.get_status() == INFEASIBLE);
|
||||
SASSERT(solver.get_status() == INFEASIBLE);
|
||||
}
|
||||
void test_bound_propagation_one_small_sample1() {
|
||||
/*
|
||||
|
|
@ -2934,8 +2951,8 @@ void test_total_case_l(){
|
|||
ls.solve();
|
||||
lp_bound_propagator bp(ls);
|
||||
ls.propagate_bounds_for_touched_rows(bp);
|
||||
lean_assert(ev.size() == 4);
|
||||
lean_assert(contains_j_kind(x, GE, - one_of_type<mpq>(), ev));
|
||||
SASSERT(ev.size() == 4);
|
||||
SASSERT(contains_j_kind(x, GE, - one_of_type<mpq>(), ev));
|
||||
}
|
||||
void test_bound_propagation() {
|
||||
test_total_case_u();
|
||||
|
|
@ -2955,17 +2972,17 @@ void test_int_set() {
|
|||
s.insert(1);
|
||||
s.insert(2);
|
||||
s.print(std::cout);
|
||||
lean_assert(s.contains(2));
|
||||
lean_assert(s.size() == 2);
|
||||
SASSERT(s.contains(2));
|
||||
SASSERT(s.size() == 2);
|
||||
s.erase(2);
|
||||
lean_assert(s.size() == 1);
|
||||
SASSERT(s.size() == 1);
|
||||
s.erase(2);
|
||||
lean_assert(s.size() == 1);
|
||||
SASSERT(s.size() == 1);
|
||||
s.print(std::cout);
|
||||
s.insert(3);
|
||||
s.insert(2);
|
||||
s.clear();
|
||||
lean_assert(s.size() == 0);
|
||||
SASSERT(s.size() == 0);
|
||||
|
||||
|
||||
}
|
||||
|
|
@ -3112,7 +3129,7 @@ void test_lp_local(int argn, char**argv) {
|
|||
return finalize(0);
|
||||
}
|
||||
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
if (args_parser.option_is_used("--test_swaps")) {
|
||||
sparse_matrix<double, double> m(10);
|
||||
fill_matrix(m);
|
||||
|
|
@ -3142,7 +3159,7 @@ void test_lp_local(int argn, char**argv) {
|
|||
return finalize(ret);
|
||||
}
|
||||
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
lp_settings settings;
|
||||
update_settings(args_parser, settings);
|
||||
if (args_parser.option_is_used("--test_lu")) {
|
||||
|
|
@ -3219,11 +3236,11 @@ void test_lp_local(int argn, char**argv) {
|
|||
ret = 0;
|
||||
return finalize(ret);
|
||||
}
|
||||
// lean::ccc = 0;
|
||||
// lp::ccc = 0;
|
||||
return finalize(0);
|
||||
test_init_U();
|
||||
test_replace_column();
|
||||
#ifdef LEAN_DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
sparse_matrix_with_permutaions_test();
|
||||
test_dense_matrix();
|
||||
test_swap_operations();
|
||||
|
|
@ -3236,5 +3253,5 @@ void test_lp_local(int argn, char**argv) {
|
|||
}
|
||||
}
|
||||
void tst_lp(char ** argv, int argc, int& i) {
|
||||
lean::test_lp_local(argc - 2, argv + 2);
|
||||
lp::test_lp_local(argc - 2, argv + 2);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,9 +1,22 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Author: Lev Nachmanson
|
||||
*/
|
||||
Module Name:
|
||||
|
||||
<name>
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Lev Nachmanson (levnach)
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#pragma once
|
||||
|
||||
|
|
@ -23,7 +36,7 @@
|
|||
#include "util/lp/lar_constraints.h"
|
||||
#include <sstream>
|
||||
#include <cstdlib>
|
||||
namespace lean {
|
||||
namespace lp {
|
||||
|
||||
template<typename T>
|
||||
T from_string(const std::string& str) {
|
||||
|
|
@ -108,13 +121,13 @@ namespace lean {
|
|||
|
||||
void fill_simple_elem(lisp_elem & lm) {
|
||||
int separator = first_separator();
|
||||
lean_assert(-1 != separator && separator != 0);
|
||||
SASSERT(-1 != separator && separator != 0);
|
||||
lm.m_head = m_line.substr(0, separator);
|
||||
m_line = m_line.substr(separator);
|
||||
}
|
||||
|
||||
void fill_nested_elem(lisp_elem & lm) {
|
||||
lean_assert(m_line[0] == '(');
|
||||
SASSERT(m_line[0] == '(');
|
||||
m_line = m_line.substr(1);
|
||||
int separator = first_separator();
|
||||
lm.m_head = m_line.substr(0, separator);
|
||||
|
|
@ -181,11 +194,11 @@ namespace lean {
|
|||
}
|
||||
|
||||
void adjust_rigth_side(formula_constraint & /* c*/, lisp_elem & /*el*/) {
|
||||
// lean_assert(el.m_head == "0"); // do nothing for the time being
|
||||
// SASSERT(el.m_head == "0"); // do nothing for the time being
|
||||
}
|
||||
|
||||
void set_constraint_coeffs(formula_constraint & c, lisp_elem & el) {
|
||||
lean_assert(el.m_elems.size() == 2);
|
||||
SASSERT(el.m_elems.size() == 2);
|
||||
set_constraint_coeffs_on_coeff_element(c, el.m_elems[0]);
|
||||
adjust_rigth_side(c, el.m_elems[1]);
|
||||
}
|
||||
|
|
@ -201,7 +214,7 @@ namespace lean {
|
|||
add_mult_elem(c, el.m_elems);
|
||||
} else if (el.m_head == "~") {
|
||||
lisp_elem & minel = el.m_elems[0];
|
||||
lean_assert(minel.is_simple());
|
||||
SASSERT(minel.is_simple());
|
||||
c.m_right_side += mpq(str_to_int(minel.m_head));
|
||||
} else {
|
||||
std::cout << "unexpected input " << el.m_head << std::endl;
|
||||
|
|
@ -211,14 +224,14 @@ namespace lean {
|
|||
}
|
||||
|
||||
std::string get_name(lisp_elem & name) {
|
||||
lean_assert(name.is_simple());
|
||||
lean_assert(!is_integer(name.m_head));
|
||||
SASSERT(name.is_simple());
|
||||
SASSERT(!is_integer(name.m_head));
|
||||
return name.m_head;
|
||||
}
|
||||
|
||||
|
||||
void add_mult_elem(formula_constraint & c, std::vector<lisp_elem> & els) {
|
||||
lean_assert(els.size() == 2);
|
||||
SASSERT(els.size() == 2);
|
||||
mpq coeff = get_coeff(els[0]);
|
||||
std::string col_name = get_name(els[1]);
|
||||
c.add_pair(coeff, col_name);
|
||||
|
|
@ -228,16 +241,16 @@ namespace lean {
|
|||
if (le.is_simple()) {
|
||||
return mpq(str_to_int(le.m_head));
|
||||
} else {
|
||||
lean_assert(le.m_head == "~");
|
||||
lean_assert(le.size() == 1);
|
||||
SASSERT(le.m_head == "~");
|
||||
SASSERT(le.size() == 1);
|
||||
lisp_elem & el = le.m_elems[0];
|
||||
lean_assert(el.is_simple());
|
||||
SASSERT(el.is_simple());
|
||||
return -mpq(str_to_int(el.m_head));
|
||||
}
|
||||
}
|
||||
|
||||
int str_to_int(std::string & s) {
|
||||
lean_assert(is_integer(s));
|
||||
SASSERT(is_integer(s));
|
||||
return atoi(s.c_str());
|
||||
}
|
||||
|
||||
|
|
@ -245,7 +258,7 @@ namespace lean {
|
|||
if (el.size()) {
|
||||
add_complex_sum_elem(c, el);
|
||||
} else {
|
||||
lean_assert(is_integer(el.m_head));
|
||||
SASSERT(is_integer(el.m_head));
|
||||
int v = atoi(el.m_head.c_str());
|
||||
mpq vr(v);
|
||||
c.m_right_side -= vr;
|
||||
|
|
@ -263,7 +276,7 @@ namespace lean {
|
|||
} else if (el.m_head == "+") {
|
||||
add_sum(c, el.m_elems);
|
||||
} else {
|
||||
lean_assert(false); // unexpected input
|
||||
SASSERT(false); // unexpected input
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,9 +1,23 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
<name>
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Lev Nachmanson (levnach)
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
Author: Lev Nachmanson
|
||||
*/
|
||||
#pragma once
|
||||
|
||||
// reads a text file
|
||||
|
|
@ -15,7 +29,7 @@ Author: Lev Nachmanson
|
|||
#include "util/lp/lp_utils.h"
|
||||
#include "util/lp/lp_solver.h"
|
||||
|
||||
namespace lean {
|
||||
namespace lp {
|
||||
|
||||
template <typename T>
|
||||
struct test_result {
|
||||
|
|
|
|||
Loading…
Reference in a new issue